  Weird machines---the computational models accessible by exploiting security
vulnerabilities---arise from the difference between the model a programmer has
in her head of how her program should run and the implementation that actually
executes. Previous attempts to reason about or identify weird machines have
viewed these models through the lens of formal computational structures such as
state machines and Turing machines. But because programmers rarely think about
programs in this way, it is difficult to effectively apply insights about weird
machines to improve security.
  We present a new view of weird machines based on techniques from programming
languages theory and secure compilation. Instead of an underspecified model
drawn from a programmers' head, we start with a program written in a high-level
source language that enforces security properties by design. Instead of state
machines to describe computation, we use the well-defined semantics of this
source language and a target language, into which the source program will be
compiled. Weird machines are the sets of behaviors that can be achieved by a
compiled source program in the target language that cannot be achieved in the
source language directly. That is, exploits are witnesses to insecure
compilation.
  This paper develops a framework for characterizing weird machines as insecure
compilation, and illustrates the framework with examples of common exploits. We
study the classes of security properties that exploits violate, the
compositionality of exploits in a compiler stack, and the weird machines and
mitigations that arise.
