SECOMP SIGNED
Efficient Formally Secure Compilers to a Tagged Architecture
Total Cost €
0EC-Contrib. €
0Partnership
0Views
0SECOMP 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.
Project "SECOMP" data sheet
The following table provides information about the project.
| Coordinator |
INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE
Organization address contact info |
| Coordinator Country | France [FR] |
| Project website | https://secure-compilation.github.io |
| 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 |
Partnership
Take a look of project's partnership.
| # | ||||
|---|---|---|---|---|
| 1 | INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE | FR (LE CHESNAY CEDEX) | coordinator | 1˙498˙444.00 |
Map
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.
Publications
| year | authors and title | journal | last update |
|---|---|---|---|
| 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: |
2019-08-29 | |
| 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: |
2019-08-29 |
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 (fabio@fabiodisconzi.com) 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.)
evolSingleCellGRN (2019)
Constraint, Adaptation, and Heterogeneity: Genomic and single-cell approaches to understanding the evolution of developmental gene regulatory networks
Read MoreHEIST (2020)
High-temperature Electrochemical Impedance Spectroscopy Transmission electron microscopy on energy materials
Read MoreIMMUNOTHROMBOSIS (2019)
Cross-talk between platelets and immunity - implications for host homeostasis and defense
Read More