#	Pagina
attuale pagina	/open-h2020/projects/207394/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - SECOMP (Efficient Formally Secure Compilers to a Tagged Architecture)

Teaser

Summary

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, compilation chains, 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 compilation chains for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilation chains 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 compilation chains target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. We are using property-based testing and formal verification to provide high confidence that our compilation chains are indeed secure. Formally, we are constructing machine-checked proofs in Coq of various new security criteria, which are defined as the preservation of property classes even against an adversarial context. These strong criteria 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.

Work performed

- We introduced many novel formal criteria characterizing the end-to-end guarantees of secure compilation chains like the ones we are building in SECOMP. These secure compilation criteria are defined as the preservation of property classes even against an adversarial context and allow for finer-grained trade-offs between security and efficiency compared to the previous state-of-the-art (a criterion called full abstraction). Moreover, we showed how to adapt our criteria to capture the security of mutually distrustful components written in unsafe languages like C.

- We built a first prototype secure compilation chain for mutually distrustful components written in a simple unsafe language. This compilation chain can target not only our micro-policy machine, but also software fault isolation, which allows us to compare the two approaches. We achieve high assurance for this secure compilation chain by combing Coq proofs and property-based testing with QuickChick.

- We proposed a novel formal characterization for the end-to-end security guarantees provided by memory safety.

- We extended the F* verification system with Dijkstra monads, monadic reification, monotonic state, support for tactics, and relational reasoning (ongoing).

- We built a direct extraction mechanism from a subset of F* called Low* to C. This allows us to focus our energy on building a secure compilation from Low* to C, avoiding the previously envisioned detour via ML.

- We introduced Luck, a new domain-specific language for property-based generators, and integrated the main innovations of Luck into QuickChick.

- We devised an initial design for a C variant extended with micro-policies.

Final results

The final goal of SECOMP is to build formally a secure compiler chain from Low* to C and from C to RISC-V assembly. This compiler chain will provide security for programs written in a combination of Low*, C, and assembly, by providing more secure semantics to C programs and by protecting the abstractions of each language against attacks from the lower-level ones. To achieve this level of security without sacrificing efficiency, our compiler chain targets our micro-policies tagged architecture. We aim to apply this compilation chains to realistic source programs, with EverCrypt and miTLS as the main end-to-end case studies. In order to ensure high confidence in the security of our compiler chains, we are using a combination of property-based testing and formal verification using Coq and F*.

Particular conceptual challenges we aim to solve by the end of this project include:

- Further improving our secure compilation criteria, and in particular dealing with different trace models between the source and target languages, with dynamic component creation, and with dynamic privileges (capabilities, dynamic interfaces).

- Scaling our prototype compilation chain to more of the C language, starting with support for pointer passing (capabilities).

- Extending our prototype compilation chain to robustly preserving hypersafety properties such as confidentiality, which is particularly challenging in the presence of side-channels.

- Verifying compartmentalized applications, using novel verification tools that exploit the source reasoning principles provided by our secure compilation criteria.

- Extending F* with scalable relational reasoning about probabilistic programs such as EverCrypt and miTLS.

- Devising a secure compilation chain from Low* to C that protects higher-level abstractions using components, contracts, and dynamic sealing.

- Enforcing memory safety for C and its interactions with untrusted RISC-V assembly.

- Devising a variant of C extended with micro-policies and a compiler that maps C-level micro-policies to ASM-level ones.