zetl

The Halting Problems of Network Stack Insecurity

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

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

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.

Tags

#langsec #security #formal-languages #protocols

Backlinks