研究人员 国立信息学与自动化研究所（INRIA), 微软研究院和卡内基梅隆大学发表 的第一个试用版 EverCrypt密码库 在Everest项目中开发并使用数学方法进行形式的可靠性验证。
对于其功能和性能， EverCrypt与现有的加密库非常接近 （OpenSSL），但与它们不同，它提供了可靠性和安全性的其他保证。
例如： 验证过程归结为定义详细规范 描述程序的所有行为 以及书面代码的数学证明 符合准备的规格。
与基于证据的质量控制方法不同， 验证提供可靠的保证 该程序将仅按照开发人员的预期运行，并且没有特定类型的错误。
例如，符合规范 确保内存安全工作，并且没有导致缓冲区溢出的错误，取消引用指针，访问已释放的存储区或两次释放存储块。
什么是EverCrypt？
永远的密码 提供强大的类型和值检查-一个组件将永远不会将参数传递给其他不兼容的组件，也不会访问其他组件的内部状态。
输入/输出行为 完全符合简单的数学函数操作，在加密标准中定义。
防范攻击 在第三方渠道中， 计算过程中的行为 （例如，执行的持续时间或存在对某些内存的访问） 它不依赖于处理的机密数据。
项目代码 用功能语言F *编写 （F星） , 提供依赖类型和细化的系统，它允许为程序建立精确的规格（数学模型），并通过SMT公式和辅助测试工具来保证实现的正确性和正确性。
F *中的代码在Apache 2.0许可下分发，而最终模块在C和MIT许可下的汇编器下分发。
根据参考代码F *， 汇编器，C，OCaml，JavaScript生成 以及网络汇编代码。
代码的某些部分 准备好的 通过项目已经在Firefox，Windows内核中使用 ， Tezos和VPN Wireguard。
EverCrypt组件
在本质上， EverCrypt结合了HACL *和Vale的两个先前截然不同的项目，提供基于它们的统一API，并使它们适合在实际项目中使用。
HACL *用低写*，其目标是提供可在C程序中使用的加密原语 他们使用libsodium和NaCL样式的API。
萨尔瓦多PROYECTO 淡水河谷开发了一种特定的语言 域以在汇编器中创建验证。
大约110万行HACL *低*语言代码和25行Vale代码 并用通用语言F *用大约70万行代码重写，它们也正在开发中 作为Everest项目的一部分。
EverCrypt库的第一个版本 具有经过验证的功能 以下密码算法 建议使用C或汇编程序版本（使用时。
其中，以下在项目页面上脱颖而出：
- 哈希算法：SHA2，SHA3，SHA1和MD5的所有变体
- 身份验证代码：用于数据源身份验证的SHA1，SHA2-256，SHA2-384和SHA2-512上的HMAC
- HKDF密钥生成算法（基于HMAC的提取和扩展密钥推导函数）
- ChaCha20流加密（提供非优化的C版本）
- Poly1305消息认证算法（MAC）（C和汇编程序版本）
- 椭圆曲线Curve25519上的Diffie-Hellman协议（C和汇编版本，基于BMI2和ADX指令进行了优化）
- 块加密模式AEAD（经过身份验证的加密）ChachaPoly（版本C未优化）
- AEAD AES-GCM块加密模式（具有AES-NI优化的汇编程序版本）。
在第一 alpha版本，代码验证已完成 在很大程度上，但是仍然存在一些未发现的区域。
另外， API尚未稳定，它将被扩展 在以下Alpha版本中 （计划统一所有API的结构。
在这些缺陷中，还强调了与x86_64架构的兼容性（在第一阶段，主要目标是可靠性，而在第二阶段将实现优化和平台）。
数据来源： https://jonathan.protzenko.fr