Opendata, web and dolomites

SECOMP SIGNED

Efficient Formally Secure Compilers to a Tagged Architecture

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

 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.

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

Project "SECOMP" data sheet

The following table provides information about the project.

Coordinator
INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE 

Organization address
address: DOMAINE DE VOLUCEAU ROCQUENCOURT
city: LE CHESNAY CEDEX
postcode: 78153
website: www.inria.fr

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 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.

# participants  country  role  EC contrib. [€] 
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
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:
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 More  

HEIST (2020)

High-temperature Electrochemical Impedance Spectroscopy Transmission electron microscopy on energy materials

Read More  

IMMUNOTHROMBOSIS (2019)

Cross-talk between platelets and immunity - implications for host homeostasis and defense

Read More