Hi, 你好啊. 很抱歉我不是华为公司的,我是做形式化验证研究的学生, 我们是基于微内核os来做飞控系统的安全性方面的研究,所以我们也是需要对微内核进行形式化验证,我只能讲讲我们用的形式化验证方法. 但是因为形式化验证方法有很多种,验证工具也有很多种,我只能就我所研究的内容谈一谈.
1 什么是形式化验证:
我们所谓的形式化验证,是基于严格的数学基础,对计算机硬件和软件系统进行描述, 开发和验证的技术.因为它的数学基础是建立在形式语言,语义和推理证明的形式逻辑系统之上,所以才有上面各位讨论的证明语言需要有依赖类型.
2 理论上形式化验证的开发过程
原本的程序开发过程本来应该是从抽象都具体,先提出requirements,再不断加入开发过程中的细节知识,称为specifications,最后不断具体化之后得到最后的程序:
Requirements —> spec_1 —> … —> spec_n ----> Program.
这里的每一个箭头都表示一次refinement,其中每一个spec的抽象角度和层次是不同的,简单的来说我们只需要证明最后的程序满足最初提出的requirements就完成了证明,这就要求我们最先提出的requirements是完全正确的,然后验证每一步的refinement(或者称作transformation step)是保持正确性的(preserve correctness)就可以验证最后得到的程序是满足requirements的. 所以可以看出提requirement和写specification是非常重要也是形式化验证中最为困难的.
3 实际中形式化验证怎么做
实际中我们很容易是已经有了程序,而不是一步一步从requirement逐步精化得到的,那对于这样的程序,我们怎么对它进行形式化验证?
这里,我们采用的是耶鲁大学的flint实验室提出的基于deep-spec的形式化验证方法.
- 将我们已有的os进行分层,
- 在coq中写出每一层中每个函数的specification
- 使用可信编译器compcert提供的clightgen将每个c代码函数转换为clight语言对应的函数(也就是在coq中将c语言代码进行描述),因为clight语言是c代码的子集去除了side-effect 所以我们可能需要对c代码进行调整以便验证的顺利进行.
- 与clight相同抽象级别写出c代码的函数low spec,因为它们处在同一抽象层,所以我们可以验证该clignt函数(也就是c函数,因为它们等价)和low spec之间的关系是identity的.
- 为low spec和high spec定义抽象关系包括数据和内存状态两个方面的关系
- 验证它们之间确实满足这样的抽象关系.
- 这样就完成了一个层基本的证明. 最后需要使用layer calculate将所有验证的层link到一起得到从bottom到top的经过链接的完整os,最后利用coq的extraction提取出可执行程序就得到了经过验证的os. 实际操作起来可不止这么简单,还需要考虑os的部分代码是汇编写的,需要处理汇编层和普通层之间的关系等等复杂的事情.
4 为什么形式化验证能做到bug-free
首先bug是由于我们的c代码函数没有完成我们想让它完成的工作,而做了不该做的事情从而被黑客利用.形式化验证中为函数写specification就是使用数学语言描述函数应该做的事情,因为数学语言是严格的,不像自然语言那样存在歧义所以一旦验证了c代码程序确实和我们的specification拥有某种数学关系,那就说明我们的程序满足specification.
5 总结
这里只是简单的对形式化验证的实际应用过程做了描述.失去了很多的严谨性,所以有什么错误或遗漏的滴地方还请各位谅解与补充,不慎感激.有想深入探讨的可以继续交流.