biblio.bib

@INPROCEEDINGS{9152665,  author={Almeida, José Bacelar and Barbosa, Manuel and
Barthe, Gilles and Grégoire, Benjamin and Koutsos, Adrien and Laporte, Vincent
and Oliveira, Tiago and Strub, Pierre-Yves},  booktitle={2020 IEEE Symposium on
Security and Privacy (SP)},   title={The Last Mile: High-Assurance and
High-Speed Cryptographic Implementations},   year={2020},  volume={},
number={},  pages={965-982},  doi={10.1109/SP40000.2020.00028}}

@inproceedings{10.1145/3319535.3363211,
author = {Almeida, Jos\'{e} Bacelar and Baritel-Ruet, C\'{e}cile and Barbosa,
Manuel and Barthe, Gilles and Dupressoir, Fran\c{c}ois and Gr\'{e}goire,
Benjamin and Laporte, Vincent and Oliveira, Tiago and Stoughton, Alley and
Strub, Pierre-Yves},
title = {Machine-Checked Proofs for Cryptographic Standards: Indifferentiability
of Sponge and Secure High-Assurance Implementations of SHA-3},
year = {2019},
isbn = {9781450367479},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3319535.3363211},
doi = {10.1145/3319535.3363211},
abstract = {We present a high-assurance and high-speed implementation of the
SHA-3 hash function. Our implementation is written in the Jasmin programming
language, and is formally verified for functional correctness, provable security
and timing attack resistance in the EasyCrypt proof assistant. Our
implementation is the first to achieve simultaneously the four desirable
properties (efficiency, correctness, provable security, and side-channel
protection) for a non-trivial cryptographic primitive. Concretely, our
mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from
a random oracle, and thus is resistant against collision, first and second
preimage attacks; 2) the SHA-3 hash function is correctly implemented by a
vectorized x86 implementation. Furthermore, the implementation is provably
protected against timing attacks in an idealized model of timing leaks. The
proofs include new EasyCrypt libraries of independent interest for programmable
random oracles and modular indifferentiability proofs.},
booktitle = {Proceedings of the 2019 ACM SIGSAC Conference on Computer and
Communications Security},
pages = {1607–1622},
numpages = {16},
keywords = {high-assurance cryptography, Jasmin, SHA-3, EasyCrypt,
indifferentiability},
location = {London, United Kingdom},
series = {CCS '19}
}

@inproceedings{10.1145/3133956.3134078,
author = {Almeida, Jos\'{e} Bacelar and Barbosa, Manuel and Barthe, Gilles and
Blot, Arthur and Gr\'{e}goire, Benjamin and Laporte, Vincent and Oliveira, Tiago
and Pacheco, Hugo and Schmidt, Benedikt and Strub, Pierre-Yves},
title = {Jasmin: High-Assurance and High-Speed Cryptography},
year = {2017},
isbn = {9781450349468},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3133956.3134078},
doi = {10.1145/3133956.3134078},
abstract = {Jasmin is a framework for developing high-speed and high-assurance
cryptographic software. The framework is structured around the Jasmin
programming language and its compiler. The language is designed for enhancing
portability of programs and for simplifying verification tasks. The compiler is
designed to achieve predictability and efficiency of the output code (currently
limited to x64 platforms), and is formally verified in the Coq proof assistant.
Using the supercop framework, we evaluate the Jasmin compiler on representative
cryptographic routines and conclude that the code generated by the compiler is
as efficient as fast, hand-crafted, implementations. Moreover, the framework
includes highly automated tools for proving memory safety and constant-time
security (for protecting against cache-based timing attacks). We also
demonstrate the effectiveness of the verification tools on a large set of
cryptographic routines.},
booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and
Communications Security},
pages = {1807–1823},
numpages = {17},
keywords = {cryptographic implementations, safety, verified compiler,
constant-time security},
location = {Dallas, Texas, USA},
series = {CCS '17}
}