2 papers
cs.PL2021
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Akram El-Korashy, Roberto Blanco, Jérémy Thibault +3
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-tra…
cs.PL2020
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
Akram El-Korashy, Stelios Tsampas, Marco Patrignani +3
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to…