Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
We formalize a programming framework that advocates programming systems like TEEs as a collection of compartments that access separate memory locations and conform to a public interface. We propose an approach that leverages compartmentalization to bring security-relevant properties verified at the source level down to the binary via certified compilers. Compartmentalization at the source level allows us to establish the desired properties over every concurrent execution of a program by verifying each compartment in isolation. To preserve compartmentalization at the target level and benefit from its compositional behavior, we define interface-preserving compilers, which preserve the structure and properties of compartments when compiling them in isolation. We show that CASCompCert, in particular, is interface-preserving.
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30
|Semantic Intermediate Representations for Sound Language Interoperability|
Amal Ahmed Northeastern University, USAPre-print
|Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers|
Farzaneh Derakhshan Carnegie Mellon University, Zichao Zhang Carnegie Mellon University, Amit Vasudevan Carnegie Mellon University, Limin Jia Carnegie Mellon UniversityFile Attached