本博客是我发表在就技术来说，鸿蒙OS到底是个什么层面的东西？上的科普形式化验证的文章。现略微修改后在我的个人网页上发表。
我目前做的工作是基于微内核OS来做无人机整体系统的安全性方面的研究，需对微内核进行形式化验证。因为形式化验证方法很多，验证工具也有很多。在此我只能就我所研究的内容谈一谈。
什么是形式化验证:
所谓形式化验证是指采用形式化方法对计算机软件或硬件进行验证的过程。而形式化方法是基于严格的数学基础，对计算机硬件和软件系统进行描述，开发和验证的技术。其数学基础是建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上。正是由于形式化方法的数学严格性使得经过形式化验证的程序安全性得以保证。
理论上形式化验证的开发过程
原本的程序开发过程应该是从抽象到具体，先提出Requirements，再不断加入开发过程中的细节知识，称为Specifications，最后不断求精（具体化）得到最终的程序:
$ \text{Requirements} \rightarrow \text{spec}_1 \rightarrow \cdots \rightarrow \text{spec}_n \rightarrow \text{Program}. $
这里的每一个箭头都表示一次精化（Refinement），其中每一个Spec（Specification）的抽象角度和层次是不同的。简单的来说我们只需要证明最后的程序满足最初提出的Requirements就完成了证明，这就要求我们最先提出的requirements是完全正确的。再验证每一步的Refinement(或者称作Transformation Step)是保持正确性的(Preserve Correctness)就可以验证最后得到的程序是满足Requirements的。 所以可以看出提Requirement和写Specification是非常重要也是形式化验证中最为困难的。
实际中形式化验证怎么做
实际应用中，我们往往是已经有了程序，而不是一步一步从Requirement逐步精化得到的，那对于这样的程序，我们怎么对它进行形式化验证?
这里，我们采用的是耶鲁大学的FLINT实验室提出的基于Deep Spec的形式化验证方法。
- 将我们已有的OS进行分层，
- 在Coq中写出每一层中所有函数的Specification
- 使用可信编译器CompCert提供的ClightGen将每个c代码函数转换为Clight语言对应的函数(也就是在Coq中将C语言代码进行描述)，因为Clight语言是C语言的子集去除了side-effect 所以我们可能需要对C代码进行调整以便验证的顺利进行。
- 与Clight相同抽象级别写出C代码的函数LowSpec，因为它们处在同一抽象层，所以我们可以验证该Clignt函数(也就是C函数，因为它们等价)和LowSpec之间的关系是identity的。
- 为LowSpec和HighSpec定义抽象关系包括数据和内存状态两个方面的关系
- 验证它们之间确实满足这样的抽象关系。
- 这样就完成了一个层基本的证明。
最后需要使用Layer Calculate将所有验证的层Link到一起得到从bottom到top的经过链接的完整OS，最后利用Coq的Extraction提取出可执行程序就得到了经过验证的OS。
实际操作起来可不止这么简单，还需要考虑OS的部分代码是汇编写的，需要处理汇编层和普通层之间的关系等等复杂的事情。
为什么形式化验证能做到Bug-free
首先Bug是由于我们的C代码函数没有完成我们想让它完成的工作，而做了不该做的事情从而被黑客利用。形式化验证中为函数写Specification就是使用数学语言描述函数应该做的事情，因为数学语言是严格的，不像自然语言那样存在歧义所以一旦验证了C代码程序确实和我们的Specification拥有某种数学关系，那就说明我们的程序满足Specification。
总结
这里只是简单的对形式化验证的实际应用过程做了描述。失去了很多的严谨性，所以有什么错误或遗漏的滴地方还请各位谅解与补充，不慎感激。有想深入探讨的可以继续交流。