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