26 citations · 70 across the 17 of their papers we have counts for
4 papers · 1 filter
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…