From the 1 of 8 linked papers with an AI index.
8 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…
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…
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…
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…
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…