  We propose a new formal criterion for evaluating secure compilation schemes
for unsafe languages, expressing end-to-end security guarantees for software
components that may become compromised after encountering undefined
behavior---for example, by accessing an array out of bounds.
  Our criterion is the first to model dynamic compromise in a system of
mutually distrustful components with clearly specified privileges. It
articulates how each component should be protected from all the others---in
particular, from components that have encountered undefined behavior and become
compromised. Each component receives secure compilation guarantees---in
particular, its internal invariants are protected from compromised
components---up to the point when this component itself becomes compromised,
after which we assume an attacker can take complete control and use this
component's privileges to attack other components. More precisely, a secure
compilation chain must ensure that a dynamically compromised component cannot
break the safety properties of the system at the target level any more than an
arbitrary attacker-controlled component (with the same interface and
privileges, but without undefined behaviors) already could at the source level.
  To illustrate the model, we construct a secure compilation chain for a small
unsafe language with buffers, procedures, and components, targeting a simple
abstract machine with built-in compartmentalization. We give a machine-checked
proof in Coq that this compiler satisfies our secure compilation criterion.
Finally, we show that the protection guarantees offered by the
compartmentalized abstract machine can be achieved at the machine-code level
using either software fault isolation or a tag-based reference monitor.
