形式化验证方法概述

Formal verification: the only way to guarantee that a system is free of programming errors.

按照陈海波老师 Lecture 中所讲，形式化验证是确保系统无编程错误的唯一方法。

形式化验证为构建正确、可靠的系统提供了系统化手段。基于这种方式构建起来的系统，具备高可信度，由于目前经验证的只是系统局部，由于环境因素必须无条件信任一些未经证明数学完备的构件，所以可以理解为，形式化验证可以达到 99%正确。

根据现在的发展，形式化验证方法主要分为三大类^[1]：

• 交互式证明（interactive verification）
• 半自动化证明（auto-active verification）
• 一键证明（push-button verification）

交互式证明

交互式证明（interactive verification），借助 Coq、Isabelle 等交互式证明工具，耗费相当多时间构建证明，一步一进。

半自动化证明

半自动化证明（auto-active verification），借助如 Dafny、Verifast 等半自动化证明器这样的工具。这需要开发人员提供证明注释，包括前置条件和后置条件、循环变量和框架注释来指导验证器。虽然与交互验证器相比，自动激活验证器可以减少证明负担，但它们仍然需要大量的工作^[2]。

一键证明

基于 symbolic evaluation 等技术的一键验证，是 UNSAT 一系列工作的研究成果。文献^[2]是该实验室 2020 年一篇硕士论文，总结了近几年的成果。简言之，最小化验证系统软件所需的手动证明负担。

思路构想，就验证的复杂性、技术或工具而言，并不是所有的系统设计都能平等地验证其正确性。与交互式或自动验证相比，按钮方法将手工校对和注释的负担转移到设计阶段，而设计阶段必须满足三个关键需求^[2]。

下面两个核心要点保证了可用符号执行的方式自动化验证实现是否符合抽象规范。

• first-order logic
• finite interface

使用的核心工具 SMT Z3。

1. SOSP 2019——SJTU-IPADS 的集体见闻（Day-2） ↩
2. Helgi Sigurbjarnarson. Push-Button Verification of Systems Software. PhD thesis, University of Washington, Apr 2020. ↩