Enforcing C-level security policies using machine-level tags

Andrew Tolmach

One promising way to improve the security of legacy software is to provide hardware support for programmable runtime reference monitoring at the level of individual hardware instructions, based on metadata tags attached to register and memory contents. This technique has been demonstrated to enforce policies such as memory safety and taint tracking with reasonable efficiency, while making minimal assumptions about the correctness of the system software.

However, some useful policies are awkward or impossible to specify at the level of machine code. A more effective approach may be to specify policies in the semantic framework of a higher-level language such as C, provided we are willing to include the C compiler in our trusted computing base. In this talk, I will describe an approach to specifying C-level tag-based policies and compiling them automatically into machine-level policies. I will illustrate the approach on two families of high-level policies: dynamic information flow control for structured code, and function-level compartmentalization. Finally, I will sketch the correctness requirements placed on the compiler and outline our plans for verifying these using a variant of CompCert.

This is joint work with Sean Anderson and Chris Chak (PSU), Catalin Hritcu (INRIA), and Benjamin Pierce (UPenn).

---

Previous: | ECOOP paper
Next: Léon Gondelman | Semi-Automated Reasoning About Non-Determinism in C Expressions