TY - GEN
T1 - The last mile
T2 - 41st IEEE Symposium on Security and Privacy, SP 2020
AU - Almeida, Jose Bacelar
AU - Barbosa, Manuel
AU - Barthe, Gilles
AU - Gregoire, Benjamin
AU - Koutsos, Adrien
AU - Laporte, Vincent
AU - Oliveira, Tiago
AU - Strub, Pierre Yves
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/5/1
Y1 - 2020/5/1
N2 - We 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 hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.
AB - We 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 hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.
UR - https://www.scopus.com/pages/publications/85091558511
U2 - 10.1109/SP40000.2020.00028
DO - 10.1109/SP40000.2020.00028
M3 - Conference contribution
AN - SCOPUS:85091558511
T3 - Proceedings - IEEE Symposium on Security and Privacy
SP - 965
EP - 982
BT - Proceedings - 2020 IEEE Symposium on Security and Privacy, SP 2020
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 18 May 2020 through 21 May 2020
ER -