# 形式化验证学习

1. 如何学习形式化验证？知乎：<https://www.zhihu.com/question/329390814>
2. 评估形式化验证工具

- serval工具
<https://github.com/uw-unsat/jitterbug>
关于这个的论文阅读与复现流程：<https://platinum-khaan-271.notion.site/Specification-and-verification-in-the-field-Applying-formal-methods-to-BPF-just-in-time-compilers-i-a021dd1ab42c40f9a1edfc062f121c50>
- coq 形式化验证
简单的 demo 到处都是：
   1. <https://www.cnblogs.com/chesium/p/coq-tutorial.html> Mike Nahas's Coq Tutorial
  基于定理证明器，需要人来手写证明代码，更类似于数学证明（估计算法用的比较多，一般来说不适用于工程化？
- Sel4工具
  - 参考：操作系统形式化验证实践教程(1) - 证明第一个定理：<https://www.jianshu.com/p/93ff2242a5eb>
  - 操作系统形式化验证实践教程(5) - 搭建seL4环境：https://www.jianshu.com/p/b3d40b2226d6

几篇综述
<https://dl.acm.org/doi/abs/10.1145/3230627>
<https://www.trustworthy.systems/publications/full_text/Klein_AKMHF_18.pdf> （上面的 PDF）

一篇 Blog <https://www.computer.org/csdl/magazine/sp/2022/03/09733177/1BENJJewLKw>

在过去的五年里，伽罗华已经正式验证了几个在苛刻的工业环境中使用的加密系统。本文讨论了我们对这些验证项目的方法，重点是在行业中构建和部署证明时存在的实际工程挑战。在过去的五年里，Galois一直在正式验证在苛刻的行业环境中使用的加密软件。利用二十多年来开发的工具，我们已经正式验证了s2n传输层安全（TLS）堆栈1、AWS LibCrypto库2和blst库3的关键属性。这些证明是工业界有史以来最复杂的部署，它们所验证的软件为数亿用户的数据保密性和完整性提供保护。

像其他保证工具一样，形式验证提供了保证证据。验证过程的结果是一个可以自动检查的数学证明，它提供了非常高的信心，即代码在每个指定的情况下都满足所需的属性。C、LLVM或x86机器代码通常可以进行实际的形式验证，特别是对于商业系统中感兴趣的两个软件属性。

- 首先是安全性，即没有崩溃、内存安全错误、竞赛条件等。在我们的项目中，我们最常证明的是C和LLVM意义上的未定义行为不会发生。
- 第二种是功能正确性，意味着代码和一些参考规范之间的等价性。在我们的项目中，规范最常描述的是实现的加密算法。
-

最近几年，有几个高安全性的系统被明确开发出来，进行形式上的验证。例如，一个C语言编译器（CompCert6），一个操作系统（SeL47），以及一个HTTP协议栈（Project Everest8）。这些项目为未经验证的代码提供了高质量和高可靠性的替代方案，我们在许多使用案例中推荐它们。但是在实践中，大多数系统并没有使用内置的验证代码。为了使我们的方法具有广泛的适用性，我们以没有（或只有表面的）修改的已有系统为目标。这样做的结果是使证明更具挑战性：我们的经验是，预先存在的系统比为验证而建立的系统更难验证。
