The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

We develop a new approach for building cryptographic implementations. Our\napproach goes the last mile and delivers assembly code that is provably\nfunctionally correct, protected against side-channels, and as efficient as\nhand-written assembly. We illustrate ur approach using ChaCha20-Poly1305, one\nof the mandatory ciphersuites in TLS 1.3, and deliver formally verified\nvectorized implementations which outperform the fastest non-verified code.\n We realize our approach by combining the Jasmin framework, which offers in a\nsingle language features of high-level and low-level programming, and the\nEasyCrypt proof assistant, which offers a versatile verification infrastructure\nthat supports proofs of functional correctness and equivalence checking.\nNeither of these tools had been used for functional correctness before. Taken\ntogether, these infrastructures empower programmers to develop efficient and\nverified implementations by "game hopping", starting from reference\nimplementations that are proved functionally correct against a specification,\nand gradually introducing program optimizations that are proved correct by\nequivalence checking.\n We also make several contributions of independent interest, including a new\nand extensible verified compiler for Jasmin, with a richer memory model and\nsupport for vectorized instructions, and a new embedding of Jasmin in\nEasyCrypt.\n