Showing 2026Show all
2 papers · 1 filter
cs.CR2026
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…
cs.CR2026
Securing Filesystems for Confidential Computing
Dimitra Giantsidi, Antoine Delignat-Lavaud, Cédric Fournet +5
Confidential computing protects applications inside Trusted Execution Environments (TEEs), but it leaves storage vulnerable. Even with disk encryption, a malicious cloud provider c…