6 citations · 8 across the 8 of their papers we have counts for
8 papers
Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
Stella Lau, Andres Erbsen, Adam Chlipala
Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of…
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…
CryptOpt: Automatic Optimization of Straightline Code
Joel Kuepper, Andres Erbsen, Jason Gross +9
Manual engineering of high-performance implementations typically consumes many resources and requires in-depth knowledge of the hardware. Compilers try to address these problems; h…
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Jason Gross, Andres Erbsen, Jade Philipoom +2
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof…
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)
Joel Kuepper, Andres Erbsen, Jason Gross +9
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have th…
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…
Flexible Instruction-Set Semantics via Type Classes
Thomas Bourgeat, Ian Clester, Andres Erbsen +4
Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely o…