Weird Machines as Insecure Compilation

TL;DR

This paper introduces a new framework for understanding weird machines as insecure compilation, using programming language semantics to analyze exploits and security violations in compiled programs.

Contribution

It presents a novel approach to characterize weird machines through programming language semantics, linking exploits to insecure compilation rather than formal computational models.

Findings

Framework for analyzing exploits as insecure compilation

Characterization of security property violations by exploits

Examples of exploits and potential mitigations

Abstract

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.