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 Inria Paris and several external collaborators. Cătălin Hriţcu and the core team at Inria Paris are generously funded for 5 years (between 2017 and 2021) by an ERC Starting Grant. Over the project’s duration we are looking to hire several excellent young researchers and students to work at Inria Paris (see open positions below).

Current Team

The core SECOMP team is located at Inria Paris, and currently includes Cătălin Hriţcu, several students, and one postdoc. We expect to hire a few more people in the coming years. 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 the recent Dagstuhl Seminar on secure compilation).

Core team at Inria Paris

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 hope to experimentally evaluate and carefully optimize the efficiency of our secure compilation chains on realistic workloads and standard benchmark suites. We are also 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 of a new security criterion we call robustly safe compilation, which is defined as the preservation of safety properties even against an adversarial context. This strong criterion complements compiler correctness and ensures 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.

Talks on SECOMP

Course on Secure Compilation

Github Repos

Most Relevant Publications

Open Positions

We are looking for excellent young researchers and students for PostDoc, Starting Researcher, PhD Student, Research Internship, and Research Engineer positions at Inria Paris, under the supervision of Cătălin Hriţcu. We can additionally support exceptional candidates for permanent Researcher positions funded and awarded competitively by Inria. More details about each of these positions are followed by some general information about all the positions.

Postdoctoral Researcher Positions

We are seeking exceptional candidates with a strong, internationally competitive research track record in programming languages, formal verification, or security. Particularly interesting for us is research expertise in:

Candidates are expected to work collaboratively on SECOMP topics and help advise students, but can also dedicate a fraction of their time to their own projects.

Inria PostDocs are hired on 2 year contracts (extensible up 6 years) and have a net monthly salary of €2122-2574.

Starting Researcher Positions

Starting Researchers can propose and follow their own research agenda in secure compilation and be fairly independent.

We are seeking exceptional candidates with a strong, internationally competitive research track record in programming languages, formal verification, or security.

Inria Starting Researchers are hired on 3 year contracts (extensible up to 6 years) and earn €2348-3344 net each month, based on experience.

Research Internships

Our research internships are for highly motivated students at the MSc level interested in getting an initial contact with research. Successful internships normally result in a research publication at a good international conference, and most often the MSc students we advise continue with a PhD. Research internships at Inria are very flexible: they usually take between 3 and 6 months and can happen any time of the year, not just in the summer.

We are especially interested in interns with previous exposure or strong desire to learn:

For some potential topics, please have a look here.

PhD Student Positions

We are seeking exceptional PhD candidates with a strong theoretical background and eager to strike a balance between solving deep foundational problems and achieving a practical impact by building innovative security and verification tools. We are particularly looking for candidates with some prior exposure to state-of-the-art research in

In France, an MSc degree or equivalent is required for pursuing a PhD. A PhD typically takes 3 years, and involves very little to no course-work, so a strong theoretical background and previous exposure to research are pre-requisites for a successful PhD. We thus strongly encourage prospective PhD students without a strong research background to follow at least the 2nd year of the MPRI programme, an intensive, research-oriented MSc programme in computer science taught by some of the best researchers in Paris. The 2nd year in the MPRI ends with a 4.5 month research internship, and, as mentioned above, SECOMP is also looking for good interns.

Inria PhD students have a gross salary of €1958 per month for their first two years (€1586 net) and €2059 per month for their third year (€1668 net). For more information about doing a PhD at Inria please consult Xavier Leroy’s post on the topic or the official Inria FAQ.

Research Engineer Positions

Are you an amazing hacker with an interest in state-of-the-art security and verification tools? Are you experienced at programming in C and/or ML and/or Haskell? Have you worked on a compiler before? Can you envision hacking in Coq or F*? If you answered yes to some of these questions a Research Engineer position on SECOMP could be well-suited for you.

Research Engineer positions are full time and moving to Paris is a prerequisite. The net monthly salary is €2049-4265 based on experience. These are temporary positions that can be prolonged up to 5-6 years, but we can also support excellent candidates for permanent research engineering positions awarded competitively by Inria.

Support for Permanent Researcher Positions at Inria

Researcher positions at Inria are permanent and are awarded via an extremely competitive contest. Each Inria team can realistically support at most one candidate in each yearly competition. If you are an exceptional candidate interested in working in the Prosecco team, the right time to get in touch with us is before the end of December. Working in Prosecco as a PostDoc or Starting Researcher is not a prerequisite but can also help in obtaining our support for a permanent position.

These are permanent French civil servant positions that provide a lot of scientific freedom and opportunities to grow. They are, however, poorly payed, especially so compared to the cost of living in Paris. The precise amounts vary based on experience and slowly increase with time, but you can expect to have €2000-2200 as your starting net salary. This can be topped up by bonuses (quite substantial if obtaining an ERC grant for instance), consulting for industry, etc.

Flexible Starting Dates, but Long Hiring Process

The non-permanent positions above can be filled over several years, so the starting dates are very flexible. Please be advised though that the hiring process for Inria Prosecco normally takes 3+ months, irrespective of the level at which you apply (including internships!). Getting in touch with us early enough is thus crucial.

(The “normal” hiring process takes 2+ months at Inria, but Prosecco gets special treatment in the form of an extra security clearance check, that makes the whole process even longer!)

Pardon My French

The language of communication in the SECOMP project is English and normally one can get along just fine in Paris with only a minimal level of French. Inria Paris provides free French courses to interested students and researchers.

How to Apply

If you are interested in applying for a position on the SECOMP project please send an email to including an up-to-date curriculum vitae. For any questions please use the same email address.