Crux：一个针对Rust和其他语言的精确验证器

Crux是一个跨语言验证工具，适用于Rust和C/LLVM，尤其针对人类难以确保正确性的复杂代码段，例如加密模块和序列化/反序列化程序对。Crux建立在成熟的SAW-Cryptol工具链的框架之上，但它提供了一个接口，其中的证明被表述为符号单元测试。Crux设计用于生产环境，并且已经在工业中得到应用。本文重点介绍了Crux-MIR，这是一个针对Rust的验证工具，它提供了一个精确的Rust安全和非安全代码模型，可以用于检查Rust代码的内联属性，以及与Cryptol或hacspec方言编写的可执行规范的扩展等价性。Crux-MIR支持组合推理，这对于扩展到中等复杂度的证明是必要的。该工具通过验证Ring库中SHA1和SHA2的实现与现有功能规范的符合性进行了演示。