[PriSC'23] Blame-Preserving Secure Compilation

Описание: [PriSC'23] Blame-Preserving Secure Compilation

Marco Patrignani, Matthis Kruse

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.