就技术来说,鸿蒙OS到底是个什么层面的东西?

比 C 擅长就行。

2 个赞

haskell的dt可以试试这个库 singletons

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的形式化验证方法.

  1. 将我们已有的os进行分层,
  2. 在coq中写出每一层中每个函数的specification
  3. 使用可信编译器compcert提供的clightgen将每个c代码函数转换为clight语言对应的函数(也就是在coq中将c语言代码进行描述),因为clight语言是c代码的子集去除了side-effect 所以我们可能需要对c代码进行调整以便验证的顺利进行.
  4. 与clight相同抽象级别写出c代码的函数low spec,因为它们处在同一抽象层,所以我们可以验证该clignt函数(也就是c函数,因为它们等价)和low spec之间的关系是identity的.
  5. 为low spec和high spec定义抽象关系包括数据和内存状态两个方面的关系
  6. 验证它们之间确实满足这样的抽象关系.
  7. 这样就完成了一个层基本的证明. 最后需要使用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代码长什么样子。

  1. 依赖类型语言没有能胜任内核开发性能,底层操作要求,实时性要求,又同时满足能找几个到会的人的。比如 Idris 一开始就吹能搞 OS,然后实际 codegen 出来就把宣传变成 Application 了。

  2. 对性能之类要求不高的话,其实 Coq 本来就主打程序生成。你可以把 Coq 看成一个 dependent types PL。

  3. 形式化验证和依赖类型是两码。现在硬件和 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表达式。。。

就是 S exp。不知道为啥连 SMT-LIB 都是用 S exp。

你可以把它当成 lisp 的 let⋯⋯

怎么帖子越走越偏了

越走越专业了 :rofl:

附上王垠关于微内核的对话: 关于微内核的对话

他们果然都没了解过现在的OS。USB驱动以及很多其他驱动本来就是功能驱动共用一个大类驱动。 另外内存错误只占错误当中很小的一部分,有的是其他方法当掉程序,如果是在核心模式里结果都会导致系统当掉。

说点能看懂的,给我们小白参与个机会