最后一英里：高保障与高速密码实现
密码学与安全
2019-04-10 v1
摘要
我们开发了一种构建密码实现的新方法。我们的方法走完最后一英里，交付可证明功能正确、抗侧信道且效率与手写汇编相当的汇编代码。我们使用 TLS 1.3 中强制要求的密码套件之一 ChaCha20-Poly1305 来阐释我们的方法，并交付形式化验证的向量化实现，其性能优于最快的非验证代码。我们通过结合 Jasmin 框架与 EasyCrypt 证明辅助工具来实现该方法：Jasmin 在单一语言中提供高级与低级编程特性，EasyCrypt 提供通用的验证基础设施，支持功能正确性证明与等价性检查。这些工具此前均未被用于功能正确性验证。总体而言，这些基础设施使程序员能够通过“游戏跳跃”开发高效且已验证的实现，从针对规范被证明功能正确的参考实现出发，逐步引入通过等价性检查证明正确的程序优化。我们还做出了若干具有独立意义的贡献，包括一个新的可扩展的 Jasmin 验证编译器，具有更丰富的内存模型并支持向量化指令，以及 Jasmin 在 EasyCrypt 中的新嵌入。
引用
@article{arxiv.1904.04606,
title = {The Last Mile: High-Assurance and High-Speed Cryptographic Implementations},
author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Benjamin Grégoire and Adrien Koutsos and Vincent Laporte and Tiago Oliveira and Pierre-Yves Strub},
journal= {arXiv preprint arXiv:1904.04606},
year = {2019}
}