我给自己立了一个flag是年底之前完成一篇科普小作文，今天是12月31日，所以不管写成什么样，一定要贴出来 :)

什么是形式化验证？

形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。

Formal Verification可以拆成2个关键字，即 formal 和 verification。

Formal指的是formal method，形式化方法，指用形式化的语言（如逻辑、代数等）描述系统的行为，然后进行数学推理。形式化方法除了用于做验证，还有其它用途，比如求解、程序合成。在CCF，这个方向的专委名字叫‘形式化方法专业委员会’。有一个CCF-A类会议，名字就叫Formal Methods，今年我们团队有一篇论文’UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking’ 在FM’24发表。

Verification这个词的意思就比较含混了，有时候它约等于proof，即严格的证明，有时候它约等于test, check or monitor。有个学术会议就叫Runtime Verification，是一个CCF-C类会议，它讨论的内容可以不那么formal，更宽松一些，实用性强一些。在芯片行业，有个岗位叫verification engineer，它跟test engineer非常接近，区别在于，验证工程师是在流片前做验证和测试工作，而测试工程师指流片之后对芯片做测试工作。

很多熟悉我的老同学老朋友，会觉得奇怪，我怎么又跳到‘形式化验证’这个领域里了？其实我的工作中有一条很长的线索，串联了“通信”、“网络安全”和“形式化验证”。我最早做通信协议的研究，然后接触了软件无线电，从而进入无线安全领域。从无线安全领域，扩展到IoT安全和移动端安全。做了几年网络安全以后，感觉到漏洞是无穷无尽的，永远也挖不完。所以就很想尝试一下，最极致的‘形式化验证’能不能把安全水位推进到极限（虽然我们永远也无法得到绝对安全）。我现在所在的研究小组，就致力于用形式化方法证明一个系统的安全性，而我自己主要关注于协议的形式化验证。

形式化验证的经典案例

在讲形式化验证的具体技术之前，先聊一聊这个领域的经典应用案例，给各位看官一点感性认识。

Joseph Sifakis与空客飞机软件的形式化验证

Joseph Sifakis 在1993年创立了VERIMAG实验室。该实验室发明了一种基于model checking的工具SCADE，用于开发空客飞机的关键的系统软件（safety critical systems），保障飞机的安全性（主要指safety）。SCADE对空客A320的成功做出了巨大贡献，SCADE后来成为航空业的事实上的标准。2007年，Joseph Sifakis与Edmund Clarke and E. Allen Emerson一起，因在model checking上取得的贡献，获得图灵奖。所以2007年之后的几年，是形式化验证专业备受关注的时期。

Intel奔腾处理器浮点运算器错误

2024年是Intel宣布发现奔腾处理器浮点运算器错误（FDIV bug）30周年 :P 30年前，这个错误导致Intel付出了5亿美元的代价。Intel聘请了剑桥大学的专家John Harrison，对浮点运算器的正确性（correctness）进行了形式化验证[1]。

现在很多大型芯片公司都聘用了形式化验证专业的工程师，对一些EDA软件无法验证的模块单独做形式化验证。其余的绝大部分的芯片验证工作，都可以通过EDA软件完成。EDA软件中主要使用model checking类的技术，进行验证，因此EDA公司也有一些形式化验证人才。

SEL4和华为鸿蒙微内核的形式化验证

以上两个例子稍微有点年代久远，再举两个新一点的例子。
2009年，SEL4[2]微内核出现，它是世界上第一个被完全的形式化验证的操作系统，是一个高可靠性、高性能的微内核。SEL4是个开源项目，至今仍保持活跃的更新，它已经拥有一个丰富的生态系统，在汽车、航空、基础设施、医疗与国防等各个领域得到应用。

2019年，华为HarmonyOS 可信执行环境（TEE）实践了形式化方法，通过形式化方法显著提升了可
信执行环境内核及关键模块的安全等级，获得了CC EAL5+证书，2023年了获得CC EAL6+证书[3][4]。这一系列的验证工作，证明的主要是鸿蒙TEE的安全性质（security）。

阿里云DNS域名解析服务的形式化验证

DNS服务是互联网最重要的基础服务之一，它的正确性和稳定性是非常重要的。因此阿里云和北京大学合作，使用形式化验证，对阿里云基础设施网络的DNS权威解析服务进行严格检查，保证其无代码bug、正确稳定运行，这是世界上第一个针对工业界产品级DNS权威解析进行代码级形式化验证的工作[5]。

以上是形式化验证的一些历史案例。它们都使用了形式化方法，证明的性质各不相同：safety, correctness, security, reliability。

这个领域工业界在做什么，大玩家有哪些？

如果把工业界形式化验证相关的公司，分为形式化方法的提供方（乙方）和用形式化方法做验证的用户方（甲方），可以按甲乙方分别介绍，然后再按行业领域分类讨论。

形式化验证的成本，目前仍然很高，所以它作为商业产品的市场并不大。这个领域的乙方公司并不多，规模也不大。实际上很多甲方的需求，只能找高校等科研单位去解决。以下列举了一些乙方公司，排名先后没有特别含义，随意的，有些是非常小型的初创公司：

  • Galois（美国）：把形式化方法应用到很多领域，有很多美国政府大客户的单子。
  • AdaCore（法国）：AdaCore是支持Ada和SPARK编程语言的公司，该公司在航空电子、航天和国防工业领域有超过二十年的经验。
  • CertiK（美国）：主要做区块链安全审计，部分环节使用形式化验证。创始人之一是哥伦比亚大学计算机系教授顾荣辉。
  • 望安科技（中国）：主要做航天及汽车系统形式化验证，“核心技术已应用于C919国产大飞机、载人航天工程、中航工业集团、航天科技集团、中国移动、小米科技等产品和机构”，还提供CC认证服务。创始人是浙江大学教授赵永望。
  • 成都链安（中国）：主要做区块链安全审计。该公司孵化于电子科技大学。
  • TrustInSoft（法国）：产品是C代码形式化验证工具，主要基于抽象解释技术。
  • Runtime Verification（美国）：基于一个称为K-framework的形式化语义框架，使其可以支持很多种编程语言，在同一个框架内解释执行，便于使用同一种规约语言做验证。主要服务于区块链客户。创始人是UIUC的教授Grigore Rosu。
  • Cryspen（法国）：这个公司主要做密码学软件的形式化验证。创始人之一是法国Inria的教授Karthikeyan Bhargavan。
  • AWS 可证安全产品Provable Security（美国）：这是唯一一家把形式化验证包装成产品的‘大厂’，包括代码扫描、网络配置验证、访问控制配置验证等很多应用场景。
    可以看到乙方公司中有很多是高校老师创办的企业。

再来看看甲方都是什么单位。甲方里最大头的是这些对安全有极高要求的行业，国防、航空航天、铁路、汽车。比如说美国NASA。NASA甚至有一个学术会议NASA Formal Methods Symposium（NFM）已经办了好多年了，论文质量还是可以的。咱们国内这几个领域也大量的应用了形式化验证，支持这些甲方需求的人，主要来自国防科大、西电、北航这些大学。

除了这些传统上被人们熟知的高安全系统，其次的，最热衷于使用形式化验证的就是区块链！为什么区块链会对形式化验证有强需求？因为它关系到‘钱’！安比实验室有篇科普文章[6]写得还不错，“由于区块链自身不可篡改的特点，智能合约在部署之前要确保没有bug，这与传统软件开发允许试错，快速迭代的特点十分不同；又由于区块链在金融领域的应用使得相关智能合约直接与数字资产绑定，而智能合约一旦被攻破，所有者的资产将化为乌有。基于数学证明的形式化方法为开发高可信的软件系统提供了有效的手段。”因此现在很多的链，都需要找乙方安全公司做审计。

我把AWS和华为这类IT领域的甲方，放在第三位。类似云计算XX配置的安全性，手机的TEE OS的安全性，可以说不是非常的安全攸关（跟飞机掉下来相比），但是用上形式化验证则可以把安全水位推到极致。

还有一类就是芯片和EDA软件公司，这些公司基本上也都是‘大厂’了。

总的来说，我眼中这个领域工业界的大玩家有，NASA、AWS和华为。

最近比较火的是哪些子方向？

FM for 区块链已经火了有几年了，这个方向就不提了。我个人觉得现在形式化方法比较火的子方向有，大模型与数学证明的结合，基于Rust语言的形式化验证。

大模型与数学证明

2024年，是大模型年，连南方周末的新年献词都以AI为主题，大模型 + 一切，形式化方法也绕不过去。陶哲轩在过去两年中非常积极的，使用大模型辅助数学定理证明。形式化方法出身的人，希望大模型能像机器人一样帮忙做一些推理过程中的脏活累活；AI出身的人，希望Lean这类形式化语言能成为大模型‘慢思考’的工具，完成一些更严谨的不会出错的推理任务。
如果LLM + Lean能出活，那么LLM + Isabelle/Coq/Verus/Kani/Tamarin … 应该也能出活吧。到那时候，世界会变成怎样？

基于Rust语言的形式化验证

形式化验证的概念，在Rust开发者中的普及度很高，因为Rust本身在设计和开发过程中就融入了多种形式化方法。2024年2月，美国白宫发布技术报告呼吁开发者使用内存安全的编程语言；3月，谷歌发表了一篇非常好的综述文章“Secure by Design: Google’s Perspective on Memory Safety”；美国DARPA发起了一个TRACTOR项目，目标是研发自动化工具把C代码自动转成Rust；10月，美国网络安全和基础设施安全局（国土安全部的下属单位）发布了一个‘Product Security Bad Practices’的文章，建议关键基础设施软件在2026年以前使用内存安全的编程语言；11 月，Rust 基金会联合AWS发起 Rust 标准库的形式化验证项目。可以看到各方力量正在通力合作，推动着 C 语言等传统语言向内存安全的 Rust 的迁移。这一趋势不仅将显著提升软件的安全性与可靠性，也将催生出全新的软件开发范式。

讲到这里，似乎还在讨论很浅层的，形式化验证有什么用途，尚未触及到它的本质。下一篇，将从几个具体的例子，show the code，讲一讲形式化验证到底在做什么。

参考文献

  1. Formal Proofs of Floating-Point Algorithms，https://www.cl.cam.ac.uk/~jrh13/slides/scan-28sep10/slides.pdf
  2. SEL4，https://sel4.systems/
  3. Certification Report, HongMeng Kernel, https://www.commoncriteriaportal.org/nfs/ccpfiles/files/epfiles/nscib-cc-0618835-cr.pdf
  4. Huawei HongMeng Kernel Common Criteria Evaluation, ST: Security Target for Specified Hardware, https://www.commoncriteriaportal.org/nfs/ccpfiles/files/epfiles/huawei_h_st-v2.0.pdf
  5. Automated Verification of an In-Production DNS Authoritative Engine, https://dl.acm.org/doi/10.1145/3600006.3613153
  6. Don’t Test, Verify —— 哪个故事真正符合你对形式化验证的想象？https://secbit.io/blog/2018/10/24/formal-verification-background/