Opendata, web and dolomites


Efficient Formally Secure Compilers to a Tagged Architecture

Total Cost €


EC-Contrib. €






 SECOMP project word cloud

Explore the words cloud of the SECOMP project. It provides you a very rough idea of what is the project "SECOMP" about.

protection    scarce    inherently    confidence    software    securely    violated    mechanisms    compiler    word    gain    components    programming    severe    security    coarse    semantics    sacrificing    safer    remotely    ensures    efficiency    untrusted    efficient    attackers    attacker    grained    tags    correctness    construct    code    compiled    formally    compilation    cyber    happens    checked    abstractions    abstraction    interacting    insecure    scenarios    complements    variant    establishing    guarantee    secure    architecture    standard    leveraging    formal    machine    tag    harm    respect    rules    vulnerabilities    abound    hardware    languages    mainstream    attacks    era    language    too    designed    inefficient    workloads    big    carefully    benchmark    checks    first    propagates    source    full    architectures    dependently    typed    off    optimize    tagged    realistic    property    metadata    fine    practical    experimentally    associates    trade    ml    suites    programs    absence    compilers    verification    proofs    computer   

Project "SECOMP" data sheet

The following table provides information about the project.


Organization address
postcode: 78153

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country France [FR]
 Project website
 Total cost 1˙498˙444 €
 EC max contribution 1˙498˙444 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2016-STG
 Funding Scheme ERC-STG
 Starting year 2017
 Duration (year-month-day) from 2017-01-01   to  2021-12-31


Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 


 Project objective

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 programming languages, both low-level (the C language) and high-level (ML and a dependently-typed variant). 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 will target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. We will experimentally evaluate and carefully optimize the efficiency of our secure compilers on realistic workloads and standard benchmark suites. We will use property-based testing and formal verification to provide high confidence that our compilers are indeed secure. Formally, we will construct machine-checked proofs of full abstraction with respect to a secure high-level semantics. This strong property complements compiler correctness and ensures that no machine-code attacker can do more harm to securely compiled components than a component in the secure source language already could.


year authors and title journal last update
List of publications.
2019 Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, Éric Tanter
Dijkstra monads for all
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3341708
Proceedings of the ACM on Programming Languages 3/ICFP 2019-08-29
2019 Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
A reasonably exceptional type theory
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3341712
Proceedings of the ACM on Programming Languages 3/ICFP 2019-08-29
2019 Abate, Carmine; Blanco, Roberto; Garg, Deepak; Hritcu, Catalin; Patrignani, Marco; Thibault, Jérémy
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
published pages: , ISSN: , DOI: 10.1109/csf.2019.00025
32nd IEEE Computer Security Foundations Symposium (CSF) 2019-08-29
2019 Joseph Eremondi, Éric Tanter, Ronald Garcia
Approximate normalization for gradual dependent types
published pages: 1-30, ISSN: 2475-1421, DOI: 10.1145/3341692
Proceedings of the ACM on Programming Languages 3/ICFP 2019-08-29
2017 Jonathan Protzenko, Cédric Fournet, Nikhil Swamy, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan
Verified low-level programming embedded in F*
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3110261
Proceedings of the ACM on Programming Languages 1/ICFP 2019-06-13
2018 Abate, Carmine; de Amorim, Arthur Azevedo; Blanco, Roberto; Evans, Ana Nora; Fachini, Guglielmo; Hritcu, Catalin; Laurent, Théo; Pierce, Benjamin C.; Stronati, Marco; Tolmach, Andrew
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
published pages: , ISSN: , DOI:
To appear in 25th ACM Conference on Computer and Communications Security (CCS 2018) 1 2019-06-13
2018 Martínez, Guido; Ahman, Danel; Dumitrescu, Victor; Giannarakis, Nick; Hawblitzel, Chris; Hritcu, Catalin; Narasimhamurthy, Monal; Paraskevopoulou, Zoe; Pit-Claudel, Clément; Protzenko, Jonathan; Ramananandro, Tahina; Rastogi, Aseem; Swamy, Nikhil
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
published pages: , ISSN: , DOI:
1 2019-06-13
2018 Max S. New, Amal Ahmed
Graduality from Embedding-projection Pairs
published pages: , ISSN: 2475-1421, DOI:
To appear in International Conference on Functional Programming - ICFP 2018 2/ICFP 2019-06-13
2017 Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Recalling a witness: foundations and applications of monotonic state
published pages: 1-30, ISSN: 2475-1421, DOI: 10.1145/3158153
Proceedings of the ACM on Programming Languages 2/POPL 2019-06-13
2018 Weiss, Aaron; Patterson, Daniel; Ahmed, Amal
Rust Distilled: An Expressive Tower of Languages
published pages: , ISSN: , DOI:
1 2019-06-13
2017 William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed
Type-preserving CPS translation of Σ and Π types is not not possible
published pages: 1-33, ISSN: 2475-1421, DOI: 10.1145/3158110
Proceedings of the ACM on Programming Languages 2/POPL 2019-06-13
2017 Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
Correctness of speculative optimizations with dynamic deoptimization
published pages: 1-28, ISSN: 2475-1421, DOI: 10.1145/3158137
Proceedings of the ACM on Programming Languages 2/POPL 2019-06-13
2017 Danel Ahman
Handling fibred algebraic effects
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3158095
Proceedings of the ACM on Programming Languages 2/POPL 2019-06-13
2019 Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
Trace-Relating Compiler Correctness and Secure Compilation
published pages: , ISSN: , DOI:
2018 Niki Vazou, Éric Tanter, David Van Horn
Gradual liquid type inference
published pages: 1-25, ISSN: 2475-1421, DOI: 10.1145/3276502
Proceedings of the ACM on Programming Languages 2/OOPSLA 2019-08-29
2019 Raimil Cruz, Éric Tanter
Polymorphic Relaxed Noninterference
published pages: , ISSN: , DOI:
Proceedings of the IEEE Secure Development Conference (SecDev 2019) 2019-08-29
2018 Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Equivalences for free: univalent parametricity for effective transport
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3236787
Proceedings of the ACM on Programming Languages 2/ICFP 2019-08-29
2018 Matías Toro, Ronald Garcia, Éric Tanter
Type-Driven Gradual Security with References
published pages: 1-55, ISSN: 0164-0925, DOI: 10.1145/3229061
ACM Transactions on Programming Languages and Systems 40/4 2019-08-29
2019 Matías Toro, Elizabeth Labrada, Éric Tanter
Gradual parametricity, revisited
published pages: 1-30, ISSN: 2475-1421, DOI: 10.1145/3290330
Proceedings of the ACM on Programming Languages 3/POPL 2019-08-29
2019 Catalin Hritcu
The Quest for Formally Secure Compartmentalizing Compilation
published pages: , ISSN: , DOI:

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "SECOMP" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email ( and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "SECOMP" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

NanoPD_P (2020)

High throughput multiplexed trace-analyte screening for diagnostics applications

Read More  


Streamlined carbon dioxide conversion in ionic liquids – a platform strategy for modern carbonylation chemistry

Read More  

NeuroMag (2019)

The Neurological Basis of the Magnetic Sense

Read More