4 papers
Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
Stella Lau, Andres Erbsen, Adam Chlipala
Granite provides a modular framework for formally verifying both functional correctness and the absence of timing side‑channel leaks in RTL processor designs against ISA‑level leak…
Securing Cryptographic Software via Typed Assembly Language (Extended Version)
Shixin Song, Tingzhen Dong, Kosi Nwabueze +4
Authors of cryptographic software are well aware that their code should not leak secrets through its timing behavior, and, until 2018, they believed that following industry-standar…
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
Owen Conoly, Andres Erbsen, Adam Chlipala
Formal verification of software and compilers has been used to rule out large classes of security-critical issues, but risk of unintentional information leakage has received much l…
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Jason Gross, Andres Erbsen, Jade Philipoom +2
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to im…