Innovating Works

SECOMP

Financiado
Efficient Formally Secure Compilers to a Tagged Architecture
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... 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. ver más
31/12/2021
MPG
1M€
Duración del proyecto: 61 meses Fecha Inicio: 2016-11-07
Fecha Fin: 2021-12-31

Línea de financiación: concedida

El organismo H2020 notifico la concesión del proyecto el día 2021-12-31
Línea de financiación objetivo El proyecto se financió a través de la siguiente ayuda:
ERC-2016-STG: ERC Starting Grant
Cerrada hace 8 años
Presupuesto El presupuesto total del proyecto asciende a 1M€
Líder del proyecto
MAXPLANCKGESELLSCHAFT ZUR FORDERUNG DER WISSE... No se ha especificado una descripción o un objeto social para esta compañía.
Perfil tecnológico TRL 4-5