Efficient Formally Secure Compilation to a Tagged Architecture

SECOMP is a research project aimed at building the first efficient formally secure compilation chains for realistic programming languages (see project description below). The project encompasses a core team at MPI-SP and several external collaborators. Cătălin Hriţcu and the core team at MPI-SP were generously funded for 5 years (until the end of 2021) by an ERC Starting Grant.

Team

The core SECOMP team is located at MPI-SP in Bochum, Germany, and currently includes Cătălin Hriţcu, several students, and one postdoc. The project also includes excellent external collaborators and we are looking forward to work with additional world-class researchers with an interest in secure compilation (see the PriSC workshop @ POPL and a series of Dagstuhl Seminars on secure compilation (2018, 2021)).

Core team at MPI-SP as of end of 2021

External collaborators

Past members

SECOMP Project

Description

Severe low-level vulnerabilities abound in today’s computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilation chains, and hardware architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. Mainstream programming languages like C are currently insecure, since any undefined behavior (e.g., a buffer overflow) can compromise the security of the whole application. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient and inconvenient for most practical scenarios.

This line of research is aimed at leveraging emerging hardware capabilities for fine-grained compartmentalization and memory safety to build the first efficient secure compilation chains for realistic programming languages, in particular for C. Such compilation chains enforce that compartmentalized applications are compiled securely, so every component in C is protected from other C components compromised by undefined behavior. To achieve such security without sacrificing efficiency, we compile to a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules.

At the conclusion of the project, we have achieved and in some ways exceeded our most important objective. We have built a secure compilation chain for C components based on the CompCert formally verified C compiler, as well as several smaller prototype compilation chains targeting a tagged architecture and software-fault isolation. We used a combination of machine-checked proofs and property-based testing in the Coq proof assistant to provide high confidence that our compilation chains achieve an unprecedented level of security.

Github Repos

Chatting

Most Relevant Publications

Talks on SECOMP

Course on Secure Compilation