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

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5

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 ag…