5 documents found, page 1 of 1
Formally verifying Kyber. Episode IV: implementation correctness
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Grégoire, Benjamin; Laporte, Vincent; Léchenet, Jean-Christophe; Oliveira, Tiago; Pacheco, HugoIn this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present hi...
Certified compilation for cryptography: Extended x86 instructions and constant-...
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Laporte, Vincent; Oliveira, TiagoWe present a new tool for the generation and verification of high-assurance high-speed machine-level cryptography implementations: a certified C compiler supporting instruction extensions to the x86. We demonstrate the practical applicability of our tool by incorporating it into supercop: a toolkit for measuring the performance of cryptographic software, which includes over 2000 different implementations. We sh...
The last mile: High-Assurance and High-Speed cryptographic implementations
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Gregoire, Benjamin; Koutsos, Adrien; Laporte, Vincent; Oliveira, Tiago; Strub, Pierre-YvesWe develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illustrate our approach using ChaCha20Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outpe...
Machine-checked proofs for cryptographic standards indifferentiability of SPONG...
Almeida, José Bacelar; Baritel-Ruet, Cecile; Barbosa, Manuel; Barthe, Gilles; Dupressoir, Francois; Gregoire, Benjamin; Laporte, VincentWe 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 secur...
A fast and verified software stack for secure function evaluation
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles Jacques Denis; Dupressoir, François; Grégoire, Benjamin; Laporte, Vincent; Pereira, VitorWe present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao’s SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for sec...