6 papers
Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
Jonathan Baumann, Yonghyun Kim, Yan Farba +2
This paper introduces Triosecuris, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inse…
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman +3
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded program…
FSLH: Flexible Mechanized Speculative Load Hardening
Jonathan Baumann, Roberto Blanco, Léon Ducruet +2
The Spectre speculative side-channel attacks pose formidable threats for security. Research has shown that code following the cryptographic constant-time discipline can be efficien…
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…
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu +4
We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style…
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…