Everrs

Everrs为形式化验证的HACL*/EverCrypt加密库提供安全绑定：EverCrypt形式化验证实现与规范的一致性以及实现是恒定时间的。

尽管有这些保证，EverCrypt的性能仍然具有很强的竞争力。

警告： Everrs仍处于早期开发阶段，API可能还会发生变化。

原语

最终将提供所有EverCrypt原语的绑定。目前支持以下原语

• X25519
• ChaCha20Poly1305

对于X25519，API是（几乎是）对x25519-dalek库的直接替代。

以下是一个使用Everrs加密和验证缓冲区的简单示例

use everrs::chacha20poly1305::{seal, open};

...

let mut ct : Vec<u8> = vec![0; pt.len()];
let mut tag : [u8; 16] = [0; 16];
seal(&key, &nonce, &ad[..], &pt, &mut ct, &mut tag);
open(&key, &nonce, &ad[..], &mut ptt, &ct, &tag).expect("authentication failure");

API哲学

恐慌与结果

大多数（所有？）加密函数是纯函数，因此本质上存在两类错误/失败

1. 开发者提供了无效的参数（本质上类型系统不足以阻止他），例如结果缓冲区的大小不足以存储解密后的密文，或者密钥对于方案来说太短。
2. 来自认证失败的失败。

Everrs采用哲学，认为错误应该是运行时的有意义的信号，而不是编程错误的指示。因此，我们相信第一种类型的错误最好通过引起“恐慌”来处理，而不是返回“Result”，这可能会被处理，但库在使用正确时永远不会发生。这与例如在切片中访问越界元素时的行为一致。