A compiler is secure for property 𝑃, if for any source component C, if C robustly preserves property 𝑃, then C also robustly preserves 𝑃. Sometimes, we may be interested in determining whether a compiler is secure but the problem lies in the chosen source language. Let us now consider C as the source language, Rust as the target language, and a compiler between the two that aims at preserving temporal memory safety (TMS). Unfortunately, in C, the proposition ‘any source component C robustly preserves TMS’ is trivially false. This is because to uphold a property robustly, one must prove that a component C has that property when interoperating with any larger program context K (which is still a C program in this case). Alas, this proposition is false, because in C several of those larger program simply do pointer arithmetic and violate TMS of any C. Thus, any compiler from C to Rust can be proven to be secure according to the definition of secure compilation above: the premise of the implication is false! In this paper we investigate a novel secure compilation criterion to be used in case one wants to prove that the compiled code has some property 𝑃 robustly, but the source language does not uphold 𝑃 robustly. We call this criterion Blame-Preserving Compilation (BPC), since it builds on the existing notion of blame.
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 25mTalk | Blame-Preserving Secure Compilation PriSC Marco Patrignani University of Trento, Matthis Kruse CISPA Helmholtz Center for Information Security Pre-print | ||
14:25 25mTalk | Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed InterfacesRecorded PriSC Pre-print File Attached | ||
14:50 25mTalk | SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine PriSC Jérémy Thibault MPI-SP, Arthur Azevedo de Amorim Boston University, Roberto Blanco MPI-SP, Aina Linn Georges Aarhus University, Cătălin Hriţcu MPI-SP, Andrew Tolmach Portland State University Pre-print Media Attached File Attached |