比 C 擅长就行。
2 个赞
os的代码验证是需要将c代码转换成证明助手使用的语言,这里使用的中间语言是通过可信编译器compcert提供的clightgen生成的clight语言,clight语言又是c语言的子集(去除了side-effect),所以是可以验证的.一个bug-free的OS也不是简单的添加前置和后置条件,其中最难的部分就是写specification.
1 个赞
我说这种是因为我们是这么做的 我们用的证明助手是Coq
你是华为公司的吗？
能给大家普及一下形式化验证吗？
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 总结
这里只是简单的对形式化验证的实际应用过程做了描述.失去了很多的严谨性,所以有什么错误或遗漏的滴地方还请各位谅解与补充,不慎感激.有想深入探讨的可以继续交流.
14 个赞
感觉有点像TDD(Type-Driven-Development)
既然OS内核一般很小（特别是RTOS），为什么要使用已有的程序，而不是直接使用一门支持依赖类型的语言开发呢？（比如：写个后端直接生成代码）
很好奇clightgen是怎么去掉C语言里的side-effect的，难道会自动生成monad之类的东西？很想看一下：把一段含side-effect的代码转成pure的clight代码长什么样子。
-
依赖类型语言没有能胜任内核开发性能，底层操作要求，实时性要求，又同时满足能找几个到会的人的。比如 Idris 一开始就吹能搞 OS，然后实际 codegen 出来就把宣传变成 Application 了。
-
对性能之类要求不高的话，其实 Coq 本来就主打程序生成。你可以把 Coq 看成一个 dependent types PL。
-
形式化验证和依赖类型是两码。现在硬件和 OS 验证仍然比较流行的 HOL 就是在用 classical logic。选用 Coq 也只是因为生态工具的原因加上那么一点 constructive logic 能生成程序的原因。原则上，即使用 classical logic/Hoare Logic 也能生成程序，dependent type 说不上是什么必须的东西。
说白了你还没理解 dependent type 是什么，为什么要它，只是听说它很先进，PL 都在搞它。
你想多了，就是简单粗暴禁止全局变量赋值，只能函数传参。这种其实你看看 ACL2 用的 pure lisp 就懂怎么回事了。当然为了方便其实有 single thread object 这种在引用透明前提下允许一定程度上副作用的东西。
1 个赞
ok, 对于你提到的TDD,我去查了下Something interesting. 也许有空的话可以去学习一下.
直接使用支持依赖类型的语言开发os应该也有,但我们不是这么做的,至于为什么不直接使用支持依赖类型的语言进行开发我不清楚.也许是可以的.
我不知道RTOS的代码量可以小到多少? 我们的微内核有一万来行代码.
我使用clightgen转换了一个简单的程序:
int main()
{
int i, j;
i = 3;
j = (i++) + (i++) + (++i);
return 0;
}
结果如下:
Definition f_main := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_i, tint) :: (_j, tint) :: (_t'3, tint) :: (_t'2, tint) ::
(_t'1, tint) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Sset _i (Econst_int (Int.repr 3) tint))
(Ssequence
(Ssequence
(Ssequence
(Ssequence
(Ssequence
(Ssequence
(Ssequence
(Sset _t'1 (Etempvar _i tint))
(Sset _i
(Ebinop Oadd (Etempvar _t'1 tint)
(Econst_int (Int.repr 1) tint) tint)))
(Sset _t'2 (Etempvar _i tint)))
(Sset _i
(Ebinop Oadd (Etempvar _t'2 tint)
(Econst_int (Int.repr 1) tint) tint)))
(Sset _t'3
(Ecast
(Ebinop Oadd (Etempvar _i tint)
(Econst_int (Int.repr 1) tint) tint) tint)))
(Sset _i (Etempvar _t'3 tint)))
(Sset _j
(Ebinop Oadd
(Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint)
(Etempvar _t'3 tint) tint)))
(Sreturn (Some (Econst_int (Int.repr 0) tint)))))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.
我只贴出了函数体部分,里面用到的以下划线开头的标识符都是clight自己定义的一些表示中间变量的ident 用正数表示的. 转换之后的文件有近400行,我们用的时候主要就是用函数体部分 ident部分自己写的.
具体来讲它到底是怎么去除了side effect我就不懂了, compcert宣称在转换为clight这一步就去除了side-effect,Figure 1.1: General structure of the CompCert C compiler.
还望赐教.
1 个赞
对,我觉得也是考虑到开发者的原因,我们的系统也是历经好几届师兄共同开发完成的,用c还是通用一些.而且涉及到内联汇编的时候我不知道idris等类似语言如何处理,我在coq中还没见到.
其实 program refinement 这个方法最早可以追溯到 Dijkstra 的 Structured Programming 一书 (1972)。在这本书他非常超前地提出了即使程序员不能提供完整的证明，写程序时就要考虑如何给证明提供方便。
1 个赞
厉害啊, 受教了. 谢谢
感觉只是把代码转成了没有被压扁前的线性IR
仍然有副作用，比如：
(Sset _t'1 (Etempvar _i tint))
很像s表达式。。。
怎么帖子越走越偏了
越走越专业了 
他们果然都没了解过现在的OS。USB驱动以及很多其他驱动本来就是功能驱动共用一个大类驱动。 另外内存错误只占错误当中很小的一部分，有的是其他方法当掉程序，如果是在核心模式里结果都会导致系统当掉。
说点能看懂的，给我们小白参与个机会