- Trust in computing systems is ultimately based on what
computations they (provably) can and cannot perform.
- Exploits are actually proofs by construction that a
system trusted to not be capable of particular computations under
any inputs or conditions can in fact perform it under given inputs
They are constructed as programs that
produce the unexpected computation on the target.
They are written as
sequences of crafted inputs that trigger and compose the effects
of the target's computational artifacts such as memory
corruptions; the overall effect is that of assembly-level
programming in "weird instructions", such as a
carefully set up memory corruption implementing a desired
mov with some undesirable side effects to be corrected with
The totality of these "instructions"
makes up a "weird machine" that shares the target's memory and inputs.
- A well-constructed, well-described exploit (more precisely,
exploit-program) is, simultaneously, a description and proof
of existence of a "weird machine" inside the target that
performs the unexpected computation -- in mathematical terms,
precisely a "proof by construction".
- "Weird machines" that manifest their existence within the
target in response to crafted input exploit-programs can be
discovered by considering their containing platform as a
recognizer machine for the language (in the formal languages
theory sense) of all inputs expected or accepted by the target.
See the "Exploiting
the Forest with Trees" and
a Formal Theory of Computer Insecurity: a
Language-theoretic Approach" by Len Sassaman and
Meredith L. Patterson.
- Conversely, every software component that handles input includes
a de facto recognizer for the de facto language of
valid or expected inputs. If this language and this recognizer are
not clearly understood as such, are only vaguely described, and
the recognizer code is scattered throughout other code, ample
unforeseen computations and "weird machines" are likely to exist.
- Eliminating unexpected computation and computational structures
("weird machines") from components that must recognize complex input
languages starting at certain levels of complexity is hard, and
may in fact be impossible.
- When recognizing an input language is a solvable (decidable)
problem, different classes of input language complexity
require matching computational power to recognize them (see
Chomsky Hierarchy of Languages). Whenever recognition is attempted
with a weaker, inadequate de facto recognizer, some inputs will
cause unexpected state and state transitions in the recognizer, most
likely resulting in a "weird machine".
- Protocol designers should stay with
regular or context-free languages, as these require only
finite state machines and pushdown automata respectively to recognize
them, and these automata are the easiest to auto-generate and get
- Protocol designers must understand that input complexity can make
recognition of valid or expected structures (and rejection of invalid
or unexpected ones, such as crafted exploit-programs) an
undecidable problem, i.e., not solvable in any reasonably
functional approximation by any amount of programming or testing effort.
"There is no 80/20 engineering solution to the Halting Problem."
There are (at least) two "natural" ways a design can run into the
- "Type I": Input Recognition in an input-handling component.
If the input language of valid or expected inputs
is Turing-complete, its recognition is an undecidable problem.
No "partial" solution to telling safe inputs from unsafe one will
likely be good enough.
- "Type II": Endpoint Computational Equivalence between the
components implementing a protocol. When exactly the same
interpretation of messages is a security requirement,
programming, testing, or verification effort must be taken to
ensure the endpoint implementations must be computationally
Yet the problem of verifying that two recognizer automata are
computationally equivalent is undecidable beyond finite state
machines and deterministic pushdown automata (i.e., beyond
regular and unambiguous context-free languages). Thus, no amount
of effort and testing will likely help to verify the "functional"
equivalence of two recognizer implementations for ambiguous
context-free grammars or stronger.