26 citations · 70 across the 17 of their papers we have counts for
17 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…
Causality and Semantic Separation
Anna Zhang, Qinglan Luo, London Bielicke +2
The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confoundi…
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…
Pyrosome: Verified Compilation for Modular Metatheory
Dustin Jamner, Gabriel Kammer, Ritam Nag +1
We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniqu…
PLanet: Formalizing and Analyzing Assignment Procedures in the Design of Experiments
London Bielicke, Anna Zhang, Shruti Tyagi +3
Experimental designs reflect assumptions about variable relationships that determine what causal queries researchers can answer through the experiment. Accounting for and communica…
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…
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Jason Gross, Théo Zimmermann, Rajashree Agrawal +1
As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof assistant evolution…
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…
Computable decision making on the reals and other spaces via partiality and nondeterminism
Benjamin Sherman, Luke Sciarappa, Adam Chlipala +1
Though many safety-critical software systems use floating point to represent real-world input and output, programmers usually have idealized versions in mind that compute with real…
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit--Claudel +2
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more wor…
Experience Implementing a Performant Category-Theory Library in Coq
Jason Gross, Adam Chlipala, David I. Spivak
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we h…
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant +2
We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and…
Formal Verification of Hardware Synthesis
Thomas Braibant, Adam Chlipala
We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version o…