SoK: Computer-aided cryptography
Computer-aided cryptography is an active area of research that develops and applies
formal, machine-checkable approaches to the design, analysis, and implementation of …
formal, machine-checkable approaches to the design, analysis, and implementation of …
Evercrypt: A fast, verified, cross-platform cryptographic provider
J Protzenko, B Parno, A Fromherz… - … IEEE Symposium on …, 2020 - ieeexplore.ieee.org
We present EverCrypt: a comprehensive collection of verified, high-performance
cryptographic functionalities available via a carefully designed API. The API provably …
cryptographic functionalities available via a carefully designed API. The API provably …
“They're not that hard to mitigate”: What cryptographic library developers think about timing attacks
Timing attacks are among the most devastating side-channel attacks, allowing remote
attackers to retrieve secret material, including cryptographic keys, with relative ease. In …
attackers to retrieve secret material, including cryptographic keys, with relative ease. In …
Simple high-level code for cryptographic arithmetic: With proofs, without compromises
We introduce an unusual approach for implementing cryptographic arithmetic in short high-
level code with machinechecked proofs of functional correctness. We further demonstrate …
level code with machinechecked proofs of functional correctness. We further demonstrate …
Formal verification of a constant-time preserving C compiler
Timing side-channels are arguably one of the main sources of vulnerabilities in
cryptographic implementations. One effective mitigation against timing side-channels is to …
cryptographic implementations. One effective mitigation against timing side-channels is to …
Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
G Barthe, B Grégoire, V Laporte - 2018 IEEE 31st Computer …, 2018 - ieeexplore.ieee.org
Software-based countermeasures provide effective mitigation against side-channel attacks,
often with minimal efficiency and deployment overheads. Their effectiveness is often …
often with minimal efficiency and deployment overheads. Their effectiveness is often …
Automatically eliminating speculative leaks from cryptographic code with blade
We introduce Blade, a new approach to automatically and efficiently eliminate speculative
leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative …
leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative …
HyCC: Compilation of hybrid protocols for practical secure computation
While secure multi-party computation (MPC) is a vibrant research topic and a multitude of
practical MPC applications have been presented recently, their development is still a tedious …
practical MPC applications have been presented recently, their development is still a tedious …
Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level
The constant-time programming discipline (CT) is an efficient countermeasure against timing
side-channel attacks, requiring the control flow and the memory accesses to be independent …
side-channel attacks, requiring the control flow and the memory accesses to be independent …
Ct-wasm: type-driven secure cryptography for the web ecosystem
A significant amount of both client and server-side cryptography is implemented in
JavaScript. Despite widespread concerns about its security, no other language has been …
JavaScript. Despite widespread concerns about its security, no other language has been …