2 papers
cs.PL2025
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Jérémy Thibault, Joseph Lenormand, Catalin Hritcu
Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversar…
cs.PL2025
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Jérémy Thibault, Roberto Blanco, Dongjae Lee +5
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs int…