Language-theoretic Security

Research programme treating input-handling bugs as recognition-theoretic failures: minimise input-language power and build validating recognisers.

In this vault

The Halting Problems of Network Stack Insecurity
Seven Turrets Of Babel
PKI Layer Cake - Kaminsky Patterson Sassaman
Parser Differential
Distributed Security
Security Applications Of Formal Language Theory
Exploit Programming - From Buffer Overflows To Weird Machines
CBCL - Safe Self-Extending Agent Communication — first ACL designed from LangSec principles
Deterministic Context-Free Language
Parser Differential Attack

Backlinks

Linked Pages

Parser Differential Attack

Exploitation strategy in which two implementations of the same input grammar produce different parse trees for the same input — typically because the grammar is ambiguous or the spec underdetermines edge cases — letting an attacker bypass one validator while triggering execution in another. Demonstrated dramatically against X.509 PKI by Kaminsky, Patterson and Sassaman (PKI Layer Cake - Kaminsky Patterson Sassaman), where parser-differential certificates allowed name-spoofing attacks. The class-level fix recommended by LangSec is to design protocol input languages within the Deterministic Context-Free Language class, whose grammars are class-level unambiguous: every conformant parser must produce the same parse tree for every input, eliminating differentials at the grammar layer. CBCL - Safe Self-Extending Agent Communication applies this principle to agent communication; remaining implementation-level divergences (e.g. Unicode handling) are mitigated by canonical serialization.

In this vault

Deterministic Context-Free Language

The class of languages recognised by deterministic pushdown automata — equivalently, those generated by LR(k) grammars. DCFL is the minimal class above regular that supports nested structure (parentheses, envelopes, scoped sub-grammars) while guaranteeing parser equivalence: every conformant implementation produces exactly one parse tree for every input. General context-free grammars admit ambiguity and therefore parser-differential attacks; DCFLs do not. DCFL is the LangSec-recommended target class for protocol input languages: validity is decidable in linear time, recognisers are total, and the class is rich enough for nested message envelopes. DCFLs are not closed under union in general — a property that has to be sidestepped (e.g. by prefix-free dispatch tags) when designing self-extending protocols like CBCL - Safe Self-Extending Agent Communication.

In this vault

CBCL - Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Reference: O’Connor, H. (2026). LangSec Workshop, IEEE Security and Privacy Workshops (SPW 2026). arXiv:2604.14512v1 [cs.CR], 16 Apr 2026. Source file: oconnor-cbcl-langsec26.pdf. URL. Reference implementation: https://codeberg.org/anuna/cbcl-rs.

Summary

Building on McCarthy’s 1975/1982 Common Business Communication Language vision and the language-theoretic security programme of Sassaman, Patterson, Bratus and Locasto (Security Applications Of Formal Language Theory), this paper presents a contemporary CBCL: an agent communication language designed so that all messages — including runtime language extensions — remain within the deterministic context-free (DCFL) complexity class. The motivating diagnosis is that contemporary agent communication has slid up the Chomsky hierarchy without acknowledging the security cost: KQML and FIPA-ACL are CFL with informal extensibility, but MCP and LLM-based agent frameworks operate over inputs whose effective complexity is recursively-enumerable, where the validity of an arbitrary message is undecidable and “weird machines” (Exploit Programming - From Buffer Overflows To Weird Machines) become unavoidable. CBCL takes the opposite tack: minimal core (8 performatives — tell, ask, reply, hello, bye, ok, error, cancel) plus a homoiconic dialect mechanism that lets agents define, transmit, and adopt domain-specific vocabularies as first-class CBCL messages, with three machine-checked safety invariants — R1 (no recursion in dialect templates), R2 (declared resource bounds on depth, expansion size, verification time), R3 (core-vocabulary preservation) — that together guarantee DCFL preservation under arbitrary finite sequences of dialect installations.

The paper accompanies the design with a Lean 4 formalization (≈5,400 lines, 16 modules, 176 machine-checked theorems, zero sorry gaps, no custom axioms) covering parser correctness (soundness + completeness), R1–R3 verification, pipeline totality, and the central dcfl_preserved closure theorem; a verified parser binary cbcl-parse is extracted from the proofs. A separately-developed Rust reference implementation (cbcl-rs, ≈11,000 lines, no_std-compatible core) ships a hand-rolled O(n) parser, dialect verification engine, gossip-based dialect propagation (O(log n) convergence per Demers et al.), C FFI/WASM bindings, property-based and differential tests, and cargo-fuzz targets; differential tests cross-validate the Rust parser against the Lean-extracted binary, eliminating spec-implementation parser differentials. Five example dialects (precision agriculture, AI planning, cross-chain asset transfer, artifact management, email) are R1–R3-verified end-to-end. A draft IETF Internet-Draft specifying application/cbcl and a Nostr transport binding (cbcl-nostr) accompany the paper. The Discussion explicitly aligns the design with Singh’s social-agency programme: dialect installation is treated as a public commitment to the dialect’s declared semantics — semantic divergence becomes a breach of commitment, observable and accountable, rather than a hidden failure of shared mental state — sidestepping the unverifiable mentalistic semantics critique of Verifiable Semantics for ACLs.

Implementation status (post-paper, cbcl-rs). The reference implementation has shipped two further safety invariants the paper sketches as future work, plus a richer Lean formalisation: R4 (Integrity) — Ed25519-style signatures over canonical encodings via an algorithm-agnostic Signer trait, with three-valued install verdicts (Valid / Unsigned / Invalid) — and R5 (Contract Well-formedness) — optional (protocol …) and (shape …) clauses on a dialect, expressing causal Merkle DAG protocols and per-performative shape contracts; R5 enforces acyclicity, reachability from begin, performative definedness with ancestor closure for extends, step uniqueness, and depth-bound respect, all decidable in linear fuel at install time. The §VII-D structural-contracts vision is therefore live (SPEC-002, SPEC-003): verify_monotone, verify_all_is_meet, and verify_eventually_consistent are proved theorems showing causal-protocol verification is a lattice homomorphism that joins coordination-free under G-Set store merge — explicit CALM Theorem alignment. The Lean codebase has grown to 380+ declarations across 19 files (still zero sorry, only the standard axioms propext / Classical.choice / Quot.sound); the workspace ships 837 tests including 584 cbcl-core unit tests, 37 proptest cases, 21 differential integration tests against the Lean-extracted binary, libFuzzer harnesses, and cargo-mutants mutation testing at a 90% kill threshold. The crate layout has grown from the paper’s five to seven: the original cbcl-core / cbcl-parser / cbcl-cli / cbcl-wasm / cbcl-ffi plus cbcl-erl (Erlang/LFE binding, SPEC-009 — with SPEC-010 binding-conformance suite) and cbcl-arena (Agent Arena platform, SPEC-012 — composable referee on cbcl-lfe-router with capability-keyed message routing and signed receipt logs). A worked sealed-bid auction dialect (SPEC-004) demonstrates structural defence against false-claim manipulation — concrete evidence that the R5 contract layer is rich enough to encode mechanism-design integrity properties decidably. The earlier Scheme prototype (anuna-research/cbcl) is superseded; architecture decisions live as ADRs under .hence/ (purity boundary, parser library choice, error handling, WASM API surface, R4 adversarial review).

Key Ideas

DCFL as the Goldilocks complexity class: Regular is too weak for nested envelopes/dialects; general CFL admits ambiguous grammars and parser-differential attacks; context-sensitive is PSPACE-complete; Type-0 is undecidable. DCFL is the minimal class that supports nested structure with class-level unambiguity (parser equivalence under language evolution).
Homoiconic self-extension: Dialect definitions are themselves valid CBCL messages, parsed by the same recogniser used for ordinary communication — a single attack surface, no separate meta-language. Inspired by Racket’s #lang mechanism.
Three safety invariants R1–R3: declarative pattern-template substitution only (no recursion, no iteration, no reflection); declared resource bounds (depth ≤ 64, expansion ≤ 8192 chars, verification ≤ 1000 ms); the eight core performatives cannot be redefined.
DCFL preservation theorem: dialect invocations must appear inside a (lang name …) wrapper; the lang tag plus a unique dialect name forms a prefix-free partition that lets a deterministic pushdown automaton dispatch to the appropriate subgrammar without extra lookahead — circumventing the fact that DCFLs are not closed under union in general. Mechanised in Lean 4 as dcfl_preserved.
Lean 4 formalization with extraction: 176 theorems, 0 sorry gaps, no custom axioms; the verified parser binary cbcl-parse is extracted from the proofs and runs the same fuel-bounded recursive-descent parser as the model.
Rust reference implementation: cbcl-core (no_std, no unsafe), cbcl-parser, cbcl-cli, cbcl-ffi, cbcl-wasm. Differential tests against the Lean-extracted binary; cargo-fuzz over five entry points.
Eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) plus four message categories (simple, meta, lang-scoped, wrapped); keyword parameters in Common-Lisp style (:thread, :in-reply-to).
Single-pass template expansion: terminates in time linear in the template plus argument size; not Turing-complete; output is not fed back into the expander, ruling out unbounded re-expansion.
Epidemic dialect propagation: gossip-based with Demers et al.’s O(log n) convergence bound; agents independently verify R1–R3 and signatures before installing.
Canonical serialization per RFC 9804 for cryptographic operations — deterministic byte representation as a precondition for signature verification.
Dialect identity by content hash: name collisions resolved by canonical-form hash; downgrade attacks rejected at installation.
Self-expression vs self-adaptation (Zambonelli et al.): traditional ACLs support only parameter tuning within fixed structure; CBCL is a self-expressive protocol whose vocabulary structurally evolves under safety constraints.
Singh-aligned reading of dialect installation: a public commitment to declared semantics, with :examples clauses providing machine-checkable behavioural anchors — semantic divergence as observable breach rather than hidden mental-state mismatch.
Stated limitations: DCFL ceiling means no recursive transformations, no cross-field references (e.g. checksums over fields), no aggregation over variable-length collections, no context-sensitive validation. Standish-taxonomy paraphrastic only — no Orthophrase, no Metaphrase. Trust infrastructure (key distribution, revocation) and dialect-curation policy left to deployment.
Structural-contracts extension (sketched in §VII-D, shipped post-paper as R4 + R5): Ed25519-style dialect signatures plus protocol constraints as causal Merkle DAGs over performative-typed messages, with Visibly Pushdown Languages for shape constraints and coordination-free monotonic verification over an append-only store. Lean-mechanised lattice-homomorphism theorems (verify_monotone, verify_all_is_meet, verify_eventually_consistent) establish that replica verdicts join under G-Set merge.

Connections

Common Business Communication Language — McCarthy’s 1975/1982 origin; CBCL is the formally-verified realisation of that vision.
Security Applications Of Formal Language Theory — Sassaman et al.’s LangSec foundations.
Proof-Carrying Code - Necula — Necula 1997, the architectural ancestor of CBCL’s R4 split (host runs a small certified verifier; producer ships the proof).
Enforceable Security Policies - Schneider — Schneider 2000, the formal warrant for R5 monotone-verdict trace monitoring.
An Axiomatic Basis for Computer Programming - Hoare — Hoare 1969, root of the contract-based verification line CBCL inherits.
Authentication in Distributed Systems - Lampson Abadi Burrows Wobber — Lampson et al. 1992, the Speaks-For Calculus for delegated commitments.
Articulating Reasons - Brandom — Brandom 2000, the philosophical underwriting of Public Semantics (entry point).
Making It Explicit - Brandom — Brandom 1994, the full inferentialist treatise.
Empiricism and the Philosophy of Mind - Sellars — Sellars 1956, the Myth of the Given that makes Semantics-Without-Minds possible.
Philosophical Investigations - Wittgenstein — Wittgenstein 1953, Meaning As Use / language-games / rule-following.
Two Dogmas of Empiricism - Quine — Quine 1951, Semantic Holism.
Assertion - Stalnaker — Stalnaker 1978, Common Ground update semantics — operational analogue of CBCL’s verdict ledger.
Languages and Language - Lewis — Lewis 1975, Convention of Truthfulness picture of how an abstract language gets in force in a population.
Communicative Actions for Artificial Agents - Cohen Levesque — Cohen & Levesque 1995, the Mentalistic Semantics high-water mark CBCL deliberately is not.
FIPA-ACL Specifications — the engineering of FIPA-ACL (envelope, conversation-id, ontology slot) CBCL inherits; the semantics it replaces.
An Ontology for Commitments in Multiagent Systems - Singh — Singh 1999, the formal commitment ontology CBCL’s dialect contracts instantiate.
Jones-Sergot Normative Systems — Jones & Sergot 1993, the Counts-As Relation that gives wire events institutional meaning under a dialect contract.
Exploit Programming - From Buffer Overflows To Weird Machines — weird-machine analysis CBCL is designed to preclude at the parser layer.
PKI Layer Cake - Kaminsky Patterson Sassaman — concrete parser-differential attacks; CBCL’s class-level unambiguity rules these out at the grammar level.
The Halting Problems of Network Stack Insecurity
A Language-Based Approach To Prevent DDoS
LangSec
KQML as an Agent Communication Language
KQML - A Language And Protocol For Knowledge And Information Exchange
FIPA-ACL
ACL Rethinking Principles — Singh’s social-agency critique that CBCL’s “dialect installation as public commitment” inherits.
Agent Communication Languages - Rethinking the Principles
Verifiable Semantics for ACLs
A Common Ontology Of ACLs
Commitment-based Semantics
The State of the Art in Agent Communication Languages
Trends in Agent Communication Language
Toward Principles for the Design of Ontologies Used for Knowledge Sharing — Gruber’s ontological-commitment principle CBCL inherits.
Some Philosophical Problems from the Standpoint of Artificial Intelligence — McCarthy & Hayes’s representation/computation separation.
Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy’s intra-program speech-act counterpart to CBCL’s inter-organisational vision.
Adjectival Modifiers
S-expression
Homoiconicity
Code as Data
Creating Languages in Racket — Flatt’s #lang mechanism that inspired CBCL’s homoiconic self-extension.
Extensibility in Programming Language Design - Standish
Language Extensibility Taxonomy
Paraphrase
Orthophrase
Metaphrase
Self-Expression
Self-Adaptation Self-Expression Self-Awareness ASCENS
Dialects and Idiolects
Keeping CALM - When Distributed Consistency is Easy — CALM theorem underwriting the forthcoming coordination-free contracts extension.
Visibly Pushdown Languages
MCP Landscape Security Threats And Future Research Directions
Survey Of AI Agent Protocols
Survey Of Agent Interoperability Protocols
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — concrete LLM-agent worm whose root-cause analysis CBCL’s lang-scoped provenance addresses.
Why AI Agents Communicate In Human Language
Why Do Multi-Agent LLM Systems Fail
Gossiping in Distributed Systems
Gossip-based Aggregation in Large Dynamic Networks

Conceptual Contribution

Claim: Agent communication languages can be simultaneously expressive, runtime-extensible, and tractably verifiable iff every message — including those that extend the language — is constrained to the deterministic context-free language class; this constraint is compatible with first-class self-extension, can be machine-checked end-to-end, and converts the unverifiable-mental-state problem of mentalistic ACLs into a public-commitment problem at the protocol layer.
Mechanism: Eight-performative core grammar (LL(1), DCFL); homoiconic dialect mechanism — dialect definitions are valid CBCL messages with extend clauses describing pattern-template substitutions; three safety invariants R1–R3 enforced at installation (no recursion via DFS cycle detection, declared resource bounds, core-vocabulary preservation); (lang name …) wrapper providing prefix-free deterministic dispatch into per-dialect sub-grammars so the union remains DCFL. Lean 4 formalization (LeanCbcl, ~5,400 LoC, 176 theorems) covering parser soundness/completeness, R1–R3, pipeline totality, and dcfl_preserved; verified parser extracted to a runnable binary (cbcl-parse). Rust reference implementation (cbcl-rs, ~11,000 LoC) with a ResourceContext-tracked single-pass expander, gossip-based dialect propagation (O(log n) per Demers et al.), canonical RFC-9804 serialization for signing, algorithm-agnostic Signer trait, C FFI / WASM bindings, property-based + differential tests, fuzz targets. Draft IETF application/cbcl Internet-Draft and Nostr transport binding.
Concepts introduced/used: Deterministic Context-Free Language, LangSec, Homoiconicity, S-expression, Dialects and Idiolects, Performatives, Self-Expression, Paraphrase, Orthophrase, Metaphrase, Visibly Pushdown Languages, CALM Theorem, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Adjectival Modifiers, Ontological Commitment, Lean 4, Property-Based Testing, Parser Differential Attack, Weird Machine, Gossip Protocols, Canonical Serialization, Nostr, hence
Stance: engineering / formal-methods, with explicit position-taking on the agent-communication design space
Relates to: Realises McCarthy’s Common Business Communication Language vision (1975/1982) by giving formal safety guarantees McCarthy could only gesture at. Sits squarely in the LangSec programme of Security Applications Of Formal Language Theory and Exploit Programming - From Buffer Overflows To Weird Machines, extending it from input-validation analysis to protocol design — claiming, plausibly, to be the first ACL designed from LangSec principles and the first to demonstrate that LangSec is compatible with runtime self-extension. Inherits the DCFL-vs-ambiguous-CFG argument from PKI Layer Cake - Kaminsky Patterson Sassaman and applies it at the message layer rather than the certificate layer. Builds explicitly on Singh’s social-agency critique (ACL Rethinking Principles) and Wooldridge’s verifiability programme (Verifiable Semantics for ACLs) by treating dialect installation as a public commitment whose semantics are anchored by the :examples clause — a machine-checkable analogue of the commitment-trace conformance that Flexible Protocol Specification and Execution (Yolum & Singh) and Commitment Machines - Yolum and Singh establish for protocol actions. Where Pact - A Choreographic Language for Agentic Ecosystems takes the individual-rationality fork to answer “why follow a protocol?”, CBCL takes the publicness/verifiability fork: the meaning of a message is fully determined by the formal grammar plus declared semantics, with no mental-state inference required. Inherits Gruber’s ontological-commitment architecture but replaces “out-of-band agreement” with in-protocol propose/query/teach. The extensibility design draws on Creating Languages in Racket (Flatt’s #lang) and respects the boundary set by Extensibility in Programming Language Design - Standish: paraphrastic only, deliberately excluding orthophrase/metaphrase to keep the attack surface bounded. The forthcoming structural-contracts extension uses Visibly Pushdown Languages for shape constraints and the CALM Theorem for coordination-free verification — a natural bridge to commitment-machine semantics. The LLM-agent threat-model framing (ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems, MCP Landscape Security Threats And Future Research Directions) positions CBCL as the structural alternative to MCP/JSON-RPC-with-natural-language: same extensibility, vastly tighter security envelope.

Exploit Programming - From Buffer Overflows To Weird Machines

Exploit Programming: From Buffer Overflows to “Weird Machines” and Theory of Computation

Reference: Bratus, Locasto, Patterson, Sassaman, Shubina (2011). ;login: The USENIX Magazine, Vol. 36, No. 6 (December 2011). Source file: Bratus.pdf. URL

Summary

This influential ;login: article reframes exploitation research as a discipline of computation theory. The authors trace the evolution from simple stack-smashing (Aleph One) through return-to-libc, return-oriented programming, heap feng shui, and format string exploits, and argue that every such technique amounts to identifying and programming a “weird machine” latent inside a target: an unintended computational model realized by crafted inputs that drive the target’s own code into performing computations its designers never intended.

The essay is dedicated to Len Sassaman and is both a memorial and a manifesto. It argues that “attack papers,” often dismissed as intellectually marginal, are in fact constructive proofs that a target contains a stronger automaton than its designers believed, and thereby exposes incorrect assumptions about the computational nature of the system. Exploitation, in this view, comes full circle to the foundational questions of Church and Turing (“what can a given machine compute?”) and deserves treatment as a rigorous subdiscipline unifying hacker practice with language-theoretic and computation-theoretic analysis.

Key Ideas

Exploits are programs for weird machines instantiated inside a target.
Evolution: stack smashing -> return-to-libc -> ROP -> heap feng shui -> format strings.
“Weird instructions” as attacker-programmable primitives borrowed from target code (strcpy+RET, malloc bookkeeping, printf %n).
Attack papers as constructive proofs of unintended computational power.
Exploitation research as empirical computability theory: “what can this machine actually compute?”
Language- and computation-theoretic methods can redefine weaknesses previously overlooked.
Call to unify hacker craft with academic theory of computation.

Connections

Weird Machine
LangSec
Security Applications Of Formal Language Theory
Shotgun Parsing
Distributed Security
CBCL - Safe Self-Extending Agent Communication — agent-communication ACL designed to preclude weird machines at the parser/expander layer by constraining input to DCFL.

Conceptual Contribution

Claim: Exploitation is the empirical study of unintended computational models (“weird machines”) inside real systems, and brings security research back to the Church-Turing questions of what a given machine can compute.
Mechanism: Reconstructs the history of memory-corruption exploitation as a progression of increasingly general ways to program target-internal weird machines using crafted input data as instructions borrowed from the target’s own code and data-interpretation loops; reinterprets attack papers as constructive proofs presenting a computationally stronger automaton than expected.
Concepts introduced/used: Weird Machine, Exploit Programming, Return-Oriented Programming, Computability, LangSec, Attack Papers
Stance: foundational
Relates to: Companion essay to Security Applications Of Formal Language Theory by the same authors; provides the conceptual vocabulary (Weird Machine) invoked throughout LangSec and pertinent to Agent Security and LLM Agents where crafted prompts or tool inputs similarly instantiate unintended computation (Prompt Injection, Tool Use).

Security Applications of Formal Language Theory

Reference: Sassaman, Patterson, Bratus, Locasto, Shubina (2011). Dartmouth College Computer Science Technical Report TR2011-709. Source file: Security Applications of Formal Language Theory.pdf. URL

Summary

This is the foundational LangSec technical report: a sustained argument that the hardest unsolved problems of secure composition (unsafe input handling, mutually intelligible but divergent message interpretations between components) are consequences of ignoring formal language theory in protocol and software design. The authors connect everyday security failures to decidability results: if a protocol’s input language requires recognizers more powerful than necessary (or worse, undecidable), then safely accepting inputs and ensuring identical interpretation across endpoints become theoretically unachievable, producing an endless stream of 0-days that no amount of patching can stop.

Part I develops the formalism, situates exploitation as a constructive proof of unintended computation (“weird machines”), introduces the parse tree differential attack as a systematic technique for finding interpretation mismatches, and applies the framework to SQL validation, PKCS#1 (proven context-sensitive), X.509, ASN.1, and IDS/IPS composition failures. Part II distills the analysis into accessible design principles for protocol designers, developers, and auditors.

The core prescription: keep input languages at the lowest Chomsky level that suffices, build recognizers that fully validate input before any processing, never mix recognition with action (“shotgun parsing”), and ensure identical parsers across endpoints to prevent parser differentials.

Key Ideas

Composition is the primary engineering means and the primary security challenge.
Safely accepting inputs and identically interpreting messages across endpoints are both fundamentally language-theoretic problems.
Undecidable/overpowered input languages yield unfixable vulnerability classes.
Parse tree differential attack: exploiting divergence between implementations of the “same” language.
Weird machines as constructive proofs of unintended computation.
PKCS#1 proven context-sensitive (not regular, not context-free).
Design principles: minimize language power, full recognition before processing, identical parsers at all endpoints, no shotgun parsing.
Critique of “good enough” (80/20) solutions to undecidable problems.

Connections

LangSec
Shotgun Parsing
Weird Machine
Parser Differential
Chomsky Hierarchy
Distributed Security
CBCL - Safe Self-Extending Agent Communication — first ACL designed from these LangSec principles; constrains all messages (including runtime extensions) to DCFL.

Conceptual Contribution

Claim: Insecurity at protocol and component boundaries is a language-theoretic phenomenon: when input languages exceed what recognizers can safely decide, secure composition is impossible, and the resulting vulnerabilities are not bugs but inevitable consequences of design choices.
Mechanism: Analyzes inputs as formal languages; classifies protocols by Chomsky level; shows that context-sensitive or undecidable languages force ad-hoc parsers whose implementation differences enable parse tree differential attacks; demonstrates weird machines as constructive proofs; prescribes minimal-power input languages, full recognition before processing, and identical recognizers at endpoints.
Concepts introduced/used: LangSec, Chomsky Hierarchy, Parser Differential, Shotgun Parsing, Weird Machine, Input Validation, Protocol Design, Distributed Security
Stance: foundational
Relates to: The canonical reference underlying LangSec and Shotgun Parsing in this vault; the theoretical substrate for A Language-Based Approach To Prevent DDoS and for applying parser-theoretic discipline to ACL design (ACL Design Principles, ACL Verifiability) and to Agent Security concerns around message interpretation in LLM Agents and Tool Use settings.

Distributed Security

Security of distributed/agent systems: mobile code, secure messaging, language-based defences.

Parser Differential

Attack exploiting the fact that two parsers accept or interpret the same input differently.

In this vault

PKI Layer Cake - Kaminsky Patterson Sassaman

PKI Layer Cake: New Collision Attacks Against the Global X.509 Infrastructure

Reference: Dan Kaminsky, Meredith L. Patterson, and Len Sassaman (2009). Black Hat USA / IOActive technical report. Source file: 1299769.pdf. URL

Summary

Presents several new classes of attacks against the X.509 certificate infrastructure: MD2 preimage exploitation of VeriSign’s still-trusted root, PKCS#10 Subject Name confusion attacks exploiting inconsistent ASN.1 BER parsing between CAs and browsers (multiple CNs, OID leading-zero padding, integer overflow, early null terminators), SQL injection through PKCS#10 subject names, generic SSL client-authentication bypasses, and EV-certificate hijacking via mixed script content.

The paper is largely a case study in how ambiguity at the interface between components — in parsers, in semantics of fields like Common Name, in trust-store EKU handling — turns into exploitable security pathologies. It is of interest to agent-communication research as a cautionary tale about shared-format ambiguity between senders and receivers.

Key Ideas

ASN.1 BER is context-sensitive and handwritten parsers disagree subtly
Subject Name parsing varies across OpenSSL, NSS, CryptoAPI — attacker exploits the gap
MD2 preimage attack enables signature transfer to forged intermediate CA
“Sender-receiver parsing disagreement” as a general attack pattern
Postel’s robustness principle considered harmful for security-critical parsing

Connections

Making Smart Contracts Smarter
Agent Communication Languages
Parser Differential Attack
CBCL - Safe Self-Extending Agent Communication — applies the parser-differential lesson at the message-layer of agent communication; DCFL grammars are class-level unambiguous.

Conceptual Contribution

Claim: The global X.509 PKI is vulnerable not only because of weak hashes (MD2/MD5) but because layered, ambiguously-specified parsers (ASN.1 BER, PKCS#10, Subject Name handling) disagree about what a certificate says — an inter-layer semantic gap exploitable by attackers.
Mechanism: Demonstrate concrete attacks: MD2RSA signature transfer from Verisign’s root, Subject Name Confusion via implementation-dependent CN-selection policies, PKCS#10-tunneled SQL/ASN.1 injection, OID leading-zero/integer-overflow tricks, null-terminator CN spoofing, SSL Client Authentication EKU bypass, and EV hijacking via mixed-trust scripting.
Concepts introduced/used: Parser Differential, Parser Differentials, X.509 PKI, ASN.1 BER Ambiguity, Certificate Authorities, Protocol Layering Attacks, Distributed Security, LangSec, Language-theoretic Security, Postel’s Robustness Principle
Stance: empirical / security-critique
Relates to: Canonical case study for Distributed Security and a prime example of why A Language-Based Approach To Prevent DDoS-style disciplined parsing matters. The ambiguity of ASN.1 BER mirrors the semantic-drift concerns in agent communication languages (A Common Ontology Of ACLs, ACL Rethinking Principles) — when two parties disagree about message meaning, security or coordination fails.

The Seven Turrets of Babel: A Taxonomy of LangSec Errors and How to Expunge Them

Reference: Momot, Bratus, Hallberg, Patterson (2016). IEEE Cybersecurity Development (SecDev). Source file: 7turretsaspublished.pdf. URL

Summary

The authors catalogue seven recurring classes of input-handling bugs under the LangSec (language-theoretic security) lens: shotgun parsing, non-minimalist input-handling code, differing interpretations of the input language, incomplete protocol specification, overloaded fields in input format, permissive processing of invalid input, and inability to express input languages in the Chomsky hierarchy. Each class is grounded in concrete CVEs (Heartbleed, Android Master Key, Rosetta Flash, OpenSSL CVE-2016-0752).

LangSec’s remedy is to treat input acceptance as a formal language-recognition problem: specify a grammar no more complex than deterministic context-free, build a recognizer that fully validates before any processing, and cleanly separate parsing from application logic. The paper proposes new CWE entries naming each weakness so auditors can precisely describe vulnerable input-handling code.

Key Ideas

LangSec: input should be a well-defined language with a fully-validating recognizer.
Seven anti-patterns: shotgun parsing, non-minimalist code, interpretation drift, incomplete spec, field overloading, permissive invalid input, undecidable grammars.
Chomsky hierarchy as a safety ceiling for input languages.
Hand-rolled parsers vs parser-combinator / generator tooling (e.g., Hammer).
Proposed new CWEs to label LangSec anti-patterns.

Connections

Conceptual Contribution

Claim: Most serious input-handling vulnerabilities reduce to seven recurring anti-patterns, all addressable by treating input acceptance as a formal language-recognition problem bounded by the Chomsky hierarchy.
Mechanism: Catalogues each anti-pattern (shotgun parsing, non-minimalist code, interpretation drift, incomplete spec, field overloading, permissive invalid input, undecidable grammars) against real CVEs (Heartbleed, Android Master Key, Rosetta Flash); prescribes grammar-first validating recognizers and proposes new CWE entries.
Concepts introduced/used: LangSec, Shotgun Parsing, Chomsky Hierarchy, Parser Combinators, Distributed Security, Common Weakness Enumeration
Stance: engineering / critique
Relates to: Shares a language-theoretic security stance with A Language-Based Approach To Prevent DDoS and Security Kernel Lambda Calculus; its grammar-discipline arguments apply directly to the schema/protocol surfaces catalogued in Survey Of Agent Interoperability Protocols and exploited in MalTool Malicious Tool Attacks.

Summary

The paper founds language-theoretic security (LangSec) on a startling thesis: accepted/valid inputs to a program form an input language, and a program’s input-handling code is effectively a recognizer for that language. Insecurity arises when this recognizer problem is computationally too powerful — recognizing context-sensitive or Turing-complete input languages makes validity checking undecidable, so exploitable mismatches between the intended and actual recognizer are inevitable.

Through examples (X.509 ASN.1 parsing, SQL injection, network-stack fingerprinting, 802.15.4 SFD attacks, qmail), the authors show how handwritten ad-hoc recognizers introduce “weird machines” on which crafted inputs execute exploit programs. They propose two principles: (1) Starve the Turing beast — give parsers only the minimum computational power needed; (2) Secure composition requires parser computational equivalence. They argue HTML5’s Turing-completeness regresses safety, and JSON/S-expressions exemplify the right design.

Key Ideas

Inputs form a formal language; parsers are recognizers.
Undecidability of input validity => unexploitable security impossible.
Exploits run on “weird machines” built from crafted inputs.
Minimal computational power principle (a LangSec Least Privilege).
Postel’s robustness principle harmful for security.

Connections

Language Workbenches
LangSec
Parser Differential
Protocol Documents
Agent Communication Languages
Multi-Agent Systems
An Unsolvable Problem of Elementary Number Theory — Church 1936, the undecidability result the title invokes.
Recursively Enumerable Sets of Positive Integers and Their Decision Problems — Post 1944, decision-problem framing behind the recognizer view.
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I — Gödel 1931, the incompleteness ancestor of the LangSec impossibility argument.
CBCL - Safe Self-Extending Agent Communication — applies the “starve the Turing beast” principle to agent-communication languages: DCFL-bounded inputs, including runtime extensions.

Conceptual Contribution

Claim: Much network-stack insecurity is a consequence of treating input validation as an ad-hoc engineering task rather than as a formal recognition problem; if the input language is too powerful, safe validation is undecidable and exploitable “weird machines” are inevitable.
Mechanism: Sassaman et al. recast every parser as a recognizer for a formal language and map concrete vulnerability classes (ASN.1 in X.509, SQL injection, TCP/IP fingerprint ambiguity, 802.15.4 SFD spoofing, qmail overflows) onto the Chomsky hierarchy. They derive two design principles — starve the Turing beast (keep parsers minimal: regular/context-free where possible) and require computational equivalence of parsers for secure composition — and argue Postel’s robustness principle exacerbates the problem.
Concepts introduced/used: LangSec, Weird Machine, Input Language, Recognizer, Chomsky Hierarchy, Parser Equivalence, Postel’s Law Critique, Halting Problem
Stance: foundational
Relates to: Frames the security motivation behind language-workbench approaches like The Spoofax Language Workbench and the language-based DDoS defence in A Language-Based Approach To Prevent DDoS; its recognizer view complements the calculus-level security of Secure Communications Processing for Distributed Languages.