耶鲁大学邵中：操作系统发展拐点已到，我们需要的是“反黑客入侵”的CertiKOS | CCF-GAI

耶鲁大学邵中：操作系统发展拐点已到，我们需要的是“反黑客入侵”的CertiKOS | CCF-GAIR 2017

*耶鲁大学邵中教授在CCF-GAIR 2017大会现场

雷锋网按：2017年7月9日，中国计算机学会（CCF）主办、雷锋网与香港中文大学（深圳）承办的第二届全球人工智能与机器人峰会（CCF-GAIR 2017）进入到最后一天的议程。自动驾驶作为人工智能大潮中一个最重要的分支，在这天得到广泛而深入的探讨。

事实上，自动驾驶的各个环节，都不得不面对网络安全问题。来自耶鲁大学的邵中教授，作为计算机程序语言设计的权威专家受邀进行了大会主题演讲，为我们阐述了其正在研发的“反黑客攻击”操作系统CertiKOS背后的理念。

1.

大家都知道，无论是区块链、机器人还是自动驾驶，其核心软件都有一个操作系统，操作系统一旦被黑客攻击，上层安全便得不到保证。所以自动驾驶汽车的信息安全问题是一个特别大的挑战。

最近几年，业内发生了很多黑客攻击汽车的案例，他们根本不需要靠近车辆，便可轻松获取十英里外车辆的控制权。这些攻击还不能很快修复，且每年都有发生。此外，勒索病毒、物联网病毒等，一直困扰着那些联网的设备，哪怕只是其中某一部件被攻击，后果也不堪设想。

近来，纽约时报的一篇文章中提到，自动驾驶系统比你见到的手机、电脑的系统更加复杂，其上的联网接口数不胜数，一旦被攻击，不是修复（reboot）一下就了事的，这辆车很可能变成黑客的武器，危及公众安全。

2.

为了从底层来解决这些问题，邵中带领耶鲁大学的团队开启了研发项目，重新设计操作系统——黑客无法进行攻击。

目前，一般的软件出了错，都是用Test的方式来找到Bug的位置，了解其在特定的执行状态和攻击下会有什么状况。如果要解决Bug就不能用Test，唯一能做的就是形式化验证。那么，如何能够用Formal Methods（形式化方法）来验证新的不带Bug的操作系统？

所谓Formal Methods，就跟中学里的数学证明一样，一个简单的数学定理要花一页纸，要验证它有什么样的可能性，会不会成功。但是不管它能不能做到，形式化验证要证明这个程序满足它的规范，而且是在任何执行条件下，面对某一类攻击时都不会有错，这是形式化验证要达到的效果。

形式化验证为什么到现在还没有成功应用到商业的各个部门呢？原因主要有这么几类。

第一，写证明要有形式化支持，比如下图是在2009年操作系统大会上，第一个被验证的操作系统内核。有7500行代码，但是光7500行的C语言代码就花了11个人年为其工作，其中还有500行的汇编代码1000多行的C语言代码没有被验证，可以看出工作量非常大。

另外一个问题是，用户平时写C语言代码的时候，究竟对它有多清晰的概念？C语言也不是特别好的语言，一旦要用它来写操作系统最底端的东西，可能就会出现C语言代码、汇编代码以及C语言代码和汇编代码杂交体并存的情况，依赖性很强，一旦这些代码连在一起组成一个复杂的系统，要保证其不出错简直是不可能完成的任务。

除了这个问题以外，所有的操作系统，尤其是现在新的多核的CPU平台上，还有用Concurrency（并发）的，往往有好几个版本，要验证它也非常难。

所以，现在的系统能做到的程度与理想状态还有一个很大的Gap，像IoT、自动驾驶平台这类系统会变得越来越复杂，所以Gap会越拉越大。

3.

我们要做的这个系统就是要解决以上所有这些挑战，我们所采用的技术是Certified Abstraction Layers。

Certified Abstraction Layers这个技术不只是用于现有的系统，而且还作为一种新的技术来开发新的系统，目的就是要让Gap变得越来越小。

怎么做到呢？我们会有一个个模块，每一个小的模块想象成一个代码，每个软件模块写的时候总会实现一些新的功能，所以有了M1，每一个被验证的模块就叫Certified Abstraction Layers，这中间会有一个模拟的关系，如果都是在一个抽象层上建立的话，就可以把它们并成一块。

如果这些代码是运用C语言写的，已经被验证满足这些规范的话，可以把它用编译器编译以后生成汇编代码，这些汇编代码也是完全被验证的，因为这个编译器能保证生成的代码和原代码之间是完全一致的。这样就能组成一个大的系统，用模块化的方式将其组成一个大的系统。

我们这个课题在2、3年前做的，加了支持中断，用在车上可以保证车里面的部件互相不受影响。最近我们做的是并发的内核，可以在多核上运行，每个核上都可以跑一个Linux系统。所以我们能证明的不只是功能性，还可以证明它不会“死”，所有普通意义上黑客能攻击的模块都会被去掉。

整个证明都是通过Coq Proof Assistant来进行，该工具在2014年还获得了（ACM Software System Award）奖项。

在具体应用上，CertiKOS可以用在机器人及智能系统上，也可以运用在无人机上，好处就是能保证操作系统内核里没有任何可被黑客攻击的模块。

4.

接下来会介绍如果要建立这样一个被验证可信的操作系统的一些具体技术。

我用比较小的一个操作系统来给你们看一个例子，如果说是在并发系统上，会有一些Spin-lock Module，上面会支持一些Thread Queue，很可能上面会加一些Scheduling Module、Inter-Process Communication和Keyboard Driver等，这是一个操作系统怎么从底层往上搭建的方式。

其中用到的最主要的技术是Certified Abstraction Layers，就是说把所有的程序的模块分成一块块，称为Certified Objects，一个Object就代表每一个模块对外能做什么事情。而且，代码和模块遵循的规范是完全一致的，这样的做法就是让每个模块都有一个抽象状态（Abstract State）和模块能做的基类型操作（Primitives）。

所以，你每次写任何一个软件模块的时候，都会在一个抽象层上做，会使用一些内层。如果你要验证这个模块，就要在上面写它的规范，你要验证的目标就是要保证实现C代码和写的形式化模块之间的关系。

比如说上图显示的是C语言代码中定义的Queue，这是它用的内层，这个C语言代码事实上是拿它来做双向链表，用于实现一个队列，中间还有一个State，上面还有一个head和tail，这样做了之后你可能用其写一些C语言代码。

如果要保证这个代码不会出错，你就得保证其与它上面的规范是一致的。

事实上这是我们所有写程序用的最多的办法，因为你们平时写每一行程序的时候，脑袋里都有一个自己想要实现的东西，所以复杂的系统其实都是在搭一层层的抽象层。构建一个复杂的无人驾驶的汽车，也需要有很多抽象层，只不过是现在我们关注的是在最底层的操作系统的安全。

如果抽象规范写成这样，从队列上拿下一个元素就非常简单，你要保证C代码和函数的规范是具备一致性的，我从队列里拿掉一个元素，C语言就要跑好几步，但是你能保证两者之间是一致的。这样的证明就表示你做了一个Simulation Proof（模拟验证），能保证你写的代码和形式规范之间没有任何Gap，那么黑客就无法攻击系统。

有了这套名为Deep Specification的形式规范，就可以保证你在程序里观察到的行为都能在规范中表达出来。有了它以后，我们能够保证所有想要证明的Property（属性）都可以在规范上提炼出来，便可以做一些操作系统的内核验证。

如上图所示，如果内核代码是这样的，很可能大部分代码会包括内存管理、线程管理、进程管理，还有上层的Trap。

如果先把内存管理的模块拿出来，把它分好层，所谓分层就是保证每一层都只依赖底层，把每一个模块都验证了进而并成一个。这个方式也适合用来验证线程管理模块、进程管理模块、虚拟内存模块等。有了这些模块，我们就可以搭建一个Certified Sequencial kernel。

如果你又要在上面加Hypervisor的功能，比如说虚拟化的模块，那么你只需要做的就是在硬件端有一个支持虚拟化的模块，把硬件的功能体现出来。往上再提升到进程管理，从那个地方就可以开始来验证虚拟化模块用来实现Hypervisor。这个验证以后，就可以得到一个Certified Hypervisor，在上面就可以Boot Linux，而且是多个版本的Linux。

有了这个以后，我们就能把多行代码之间每一块的关系都搞得非常透彻，比如此前提到的3000行代码就可以转变成37层的抽象层，这些抽象层都是逻辑上的抽象层，所以它真正实现的速度和功能跟原来是一样的，用这些抽象层可以把中间各种各样的关系理顺，保证不会出任何的错误。

在这个基础上，我们还可以拿它来实现一些并发的Kernel。大家都知道，未来所有的自动驾驶汽车上用的芯片越来越多的应该是MPSOC，这些多核的CPU带来了很多同步的问题，所有的人都知道并发程序是现在写程序最大的挑战，如果这个问题不解决，接下来整个自动驾驶汽车、无人机都会有很大的局限性。

所以我们现在也做多核内核的验证。多核内核的验证跟刚才用的技术是类似的，我们做的是能够让你把用在串行系统上的验证方法运用到了多核上，我们把多核的机器变得如串型一样，只不过把其他的CPU变成了它的环境。

每一个模块不仅能够保证满足规范，即使有其他并发的进程进行的时候，也不会出现任何问题，黑客无法进行攻击。

我们在验证并发操作系统的工作中发现，哪怕是大家用了十几年的操作系统的教科书里的很多例子，一旦涉及到并发的代码，很多都有错，即使老师讲了很多，学生也看了很多，但我们拿它去验证时，还是会发现一些边角的case没有考虑到，所以我们在验证过程中找到了很多Bug，这些Bug会变成网络安全隐患。

在这个基础上，我们还做了一些Device Driver的验证，这个其实是很有意思的。事实上，我们做操作系统验证的目标不是只验证一个特定操作系统，而是要验证一类平台，这个平台可能不只是几个CPU，比如汽车上会有很多的Device，有很多ECU。所以汽车操作系统不只是简单的Linux就在一个Box上运行。

在这样的Device上也可以用同样的手段建抽象层，这方面的工作我们也做了很多，比如在一个Device Driver的最底层与硬件接触的地方建立起大量的抽象层。此外，我们还可以拿它来验证一些Security，能够在规范的层面上保证任何两个线程之间不会互相影响，也就是说，即使一个黑客控制了其中一个部件，也不能破坏剩下的部件。这在汽车上是非常重要的，因为汽车上有很多部件，如果黑客通过某个部件的操作系统黑进了汽车，很可能会利用其攻击其他部件或者整个主机。

总的来说，虽然我们目前专注在CertiKOS这样一个简单的操作系统上，但也在不断寻求突破，比如在其上实现Real Time的功能，朝着做一个支持多核且非常安全的操作系统的方向前进，这套技术也已经变得越来越成熟。

事实上，这方面的工作以前大部分是在航天领域进行。现在，越来越多的业内人士认为，以往对于航天领域的诸多要求都会慢慢转移到自动驾驶汽车上。

5.

最后想说的是，对于操作系统，中国以往做的工作大部分还只是停留在应用层或系统级别更上的一层，而最核心的部分却没有太多涉足。

如今，新的应用如智慧城市、区块链以及自动驾驶汽车等都已经冒头，原来的那些操作系统已经不完全适用于这些新的应用。但为了能马上推向市场，很多都是稍微改一下便搭载到设备上，其实里面存在很多问题。

所以操作系统已经到了一个拐点，这时候如果有一个能保证安全的操作系统、出现一个新的平台，我相信很多行业都会拥抱这个平台。

*文中图片由雷锋网截自邵中演讲PPT