Efficient Formally Secure Compilers to a Tagged Architecture

SECOMP is a research project aimed at building the first efficient formally secure compilers for realistic programming languages (see project description below). The project encompasses a core team at Inria Paris and external collaborators at University of Pennsylvania, Portland State University, MIT, Northeastern University, Microsoft Research, and Draper Labs (see current team below). Cătălin Hriţcu and the core team at Inria Paris are generously funded for 5 years (between 2017 and 2021) by a recently awarded ERC Starting Grant.

Over the duration of the project we are looking to hire several excellent students and young researchers to work at Inria Paris (see open positions below). We also have funding for sabbaticals and short-term visits to Paris for researchers with an interest in secure compilation.

Current Team

The SECOMP core team is located at Inria Paris, and currently includes Cătălin Hriţcu, a couple of students, and a postdoc. We expect this core team to grow significantly in the coming years by hiring students and young researchers. The SECOMP project also includes many external collaborators and we are looking forward to work with additional world-class researchers with an interest in secure compilation.

Core team at Inria Paris

Past members at Inria Paris

External collaborators

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, compilers, 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 compilers for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilers 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 compilers 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 compilers on realistic workloads and standard benchmark suites. We are also using property-based testing and formal verification to provide high confidence that our compilers are indeed secure. Formally, we are constructing machine-checked proofs of fully abstract compilation and of a new property we call robust compilation, which implies the preservation of trace properties even against an adversarial context. These strong properties 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.

Talks on SECOMP

Relevant Publications

Github Repos

Open Positions

We are looking for excellent students and young researchers for Research Internship, PhD Student, PostDoc, Starting Researcher, 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 of them.

Research Internships

The research internships are for highly motivated students at the BSc and MSc levels interested in getting an initial contact with research and for PhD students at other institutions who are interested in getting hands on experience with research on the SECOMP project. Successful internships normally result in a research publication at a good international conference, and most often the BSc and 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 strictly 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 and second year (€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.

PostDoc and Starting Researcher Positions

For the PostDoc (2+ year contract) and Starting Researcher (3+ year contract) positions we are seeking exceptional candidates with a strong, internationally competitive track record of research in programming languages, formal verification, or security. Particularly interesting research areas are:

PostDocs and Starting Researchers can propose and follow their own research agenda in secure compilation and be fairly independent. They are expected to work collaboratively and co-advise interns and PhD students.

Inria PostDocs have a net monthly salary of €2122-2574, while Starting Researchers earn €2348-3344 each month, based on experience.

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, and each Inria team can realistically support at most one candidate each year in this 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 can 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.

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 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 updated curriculum vitae. For any questions please use the same email address.