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 are generously funded for 5 years (until the end of 2021) by an ERC Starting Grant. Over the project’s duration we are looking to hire several excellent young researchers and students to work on the project.

Current 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, 2020)).

Core team at MPI-SP

External collaborators

Past members at Inria Paris

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 architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. The semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, establishing security with respect to a high-level semantics does not guarantee the absence of low-level attacks. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient for most practical scenarios.

This project is aimed at leveraging emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilation chains for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilation chains will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing efficiency, our secure compilation chains target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. We are using property-based testing and formal verification to provide high confidence that our compilation chains are indeed secure. Formally, we are constructing machine-checked proofs in Coq of various new security criteria, which are defined as the preservation of property classes even against an adversarial context. These strong criteria complement compiler correctness and ensure that no machine-code attacker can do more harm to securely compiled components than a component already could with respect to a secure source-level semantics.

Github Repo

Chatting

Most Relevant Publications

Talks on SECOMP

Course on Secure Compilation