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

本篇文章4189字，读完约10分钟

*耶鲁大学邵忠教授在2017年ccf-gair会议上

据雷锋说。网站:2017年7月9日，由中国计算机联合会主办，雷锋主持的第二届全球人工智能与机器人峰会。(公开号码:雷锋。和香港中文大学(深圳)进入了最后一天的议程。作为人工智能最重要的分支之一，自主驾驶在今天已经得到了广泛而深入的讨论。

事实上，自主驾驶的每个环节都必须面对网络安全问题。耶鲁大学的邵忠教授作为计算机编程语言设计方面的权威专家，应邀在会议上发表主旨演讲，解释他正在开发的“反黑客”操作系统certikos背后的概念。

1.

众所周知，无论是区块链、机器人还是自动驾驶，它的核心软件都有一个操作系统。一旦操作系统遭到黑客攻击，上层的安全性就无法保证。因此，自主车辆的信息安全是一个巨大的挑战。

近年来，业内有很多黑客攻击汽车的案例，他们可以轻而易举地控制十英里外的汽车，而不用靠近它们。这些攻击无法快速修复，而且每年都会发生。此外，还有软件、物联网病毒等。一直困扰着网络设备，即使只有一个组件受到攻击，其后果也是不可想象的。

最近，《纽约时报》的一篇文章提到，自动驾驶系统比你看到的手机和电脑系统要复杂得多，上面有无数的网络接口。一旦受到攻击，就无法修复。这辆车很可能成为黑客的武器，危及公共安全。

2.为了从根本上解决这些问题，邵忠带领耶鲁大学的团队启动了一个研发项目，并重新设计了操作系统——黑客无法攻击。

目前，当通用软件出错时，测试是用来发现错误位置，并知道在特定的执行状态和攻击下会发生什么。如果你想解决错误，你不能使用测试。你唯一能做的就是正式验证。那么，我们如何使用正式的方法来验证新的无缺陷操作系统呢？

所谓的形式化方法，就像中学里的数学证明一样，一个简单的数学定理需要用一页纸来验证它的可能性和成功性。然而，不管是否能够完成，形式验证应该证明程序满足其规范，并且在任何执行条件下，面对某种类型的攻击都没有错误，这就是形式验证的效果。

为什么到目前为止还没有成功地将正式验证应用到每个业务部门？有几个主要原因。

首先，应该有正式的支持来写证据。例如，下图显示了2009年操作系统会议上第一个经过验证的操作系统内核。有7500行代码，但光是为它工作就花了11个人工年，其中500行汇编代码和1000多行C语言代码都没有经过验证，这说明工作量很大。

另一个问题是，当用户通常写C语言代码时，它有多清晰？c语言不是一种特别好的语言。一旦用于编写操作系统的底层，C语言代码、汇编代码以及C语言代码和汇编代码的混合代码就可以共存，这是高度依赖的。一旦这些代码连接在一起形成一个复杂的系统，就不可能保证它们不会出错。

除了这个问题，所有的操作系统，特别是新的多核cpu平台，也使用并发，这通常有几个版本，很难验证它。

因此，当前系统所能达到的程度与理想状态仍有很大差距。物联网和自动驾驶平台等系统将变得越来越复杂，差距将会扩大。

3.我们想要做的系统是解决所有这些挑战。我们使用的技术是经过认证的抽象层。

经过认证的抽象层不仅用于现有系统，而且还用作开发新系统的新技术，目的是使差距越来越小。

怎么做？我们会有模块，每个小模块都被想象成一个代码，每个软件模块在编写时都会实现一些新的功能。因此，对于m1，每个经过验证的模块被称为经过验证的抽象层，它们之间将有一个模拟的关系。如果它们都建立在一个抽象层上，它们可以组合在一起。

如果这些代码是用C语言编写的，并且已经过验证符合这些规范，那么它们可以由编译器编译以生成汇编代码，这些代码也是经过完全验证的，因为该编译器可以确保生成的代码与原始代码完全一致。这样，可以形成一个大系统，并且它可以以模块化的方式形成一个大系统。

我们的项目是在两三年前完成的，增加了支持中断，这可以确保车内的组件不会相互影响。最近，我们正在做并发内核，它可以在多核上运行，每个内核都可以运行一个linux系统。因此，我们能够证明的不仅仅是功能，而且它不会消亡，黑客能够攻击的所有普通意义上的模块都将被移除。

整个认证是通过coq认证助理进行的，该助理还获得了2014年(acm软件系统奖)。

在具体应用中，certikos可以用于机器人和智能系统，也可以用于无人驾驶飞行器。Certikos的优势在于，它可以确保操作系统内核中没有可能被黑客攻击的模块。

4.接下来，我们将介绍一些具体的技术，如果我们想建立这样一个经过验证和信任的操作系统。

让我给你看一个相对较小的操作系统的例子。如果它是一个并发系统，将会有一些自旋锁模块，它将支持一些线程队列，并且很可能会添加一些调度模块、进程间通信和键盘驱动程序。这是一种如何自下而上构建操作系统的方法。

使用的最重要的技术是经过认证的抽象层，这意味着所有的程序模块都被分成块，这些块被称为经过认证的对象，一个对象代表每个模块在外部可以做什么。此外，代码和模块遵循相同的规范，因此每个模块都有一个抽象状态和模块可以做的原语类型。

因此，每次你写任何软件模块的时候，你都会在一个抽象层上写，并使用一些内部层。如果你想验证这个模块，你应该把它的规格写在上面。验证的目标是确保C代码和编写的正式模块之间的关系。

例如，上图显示了用C语言代码定义的队列，这是它的内层。事实上，这个C语言代码使用它作为一个双链表来实现一个队列，中间有一个状态，头和尾都在上面。完成后，您可以用它来编写一些C语言代码。

如果您想确保该代码是无错误的，您必须确保它与上面的规范一致。

事实上，这是我们用来编写程序的最常见的方式，因为当你编写程序的每一行时，你的头脑中总是有你想要实现的东西，所以复杂的系统实际上是在构建抽象层。要建造一辆复杂的无人驾驶汽车，有许多抽象的层面，但现在我们关心的是底层操作系统的安全性。

如果抽象规范是这样写的，那么从队列中取出一个元素是非常简单的。您必须确保C代码和函数的规范是一致的。如果我从队列中取出一个元素，C语言将运行几个步骤，但是您可以保证这两个步骤是一致的。这种证明意味着你已经做了一个模拟证明，可以确保你写的代码和正式的规范之间没有差距，所以黑客不能攻击系统。

有了这个被称为深度规范的正式规范，您可以确保您在程序中观察到的行为可以在规范中表达出来。有了它，我们可以确保我们想要证明的所有属性都可以从规范中提取出来，然后我们可以对操作系统进行一些内核验证。

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

如果您先取出内存管理模块并将其分成层，所谓的分层就是确保每一层只依赖于底层，并验证每个模块，然后将其合并为一个模块。该方法也适用于验证线程管理模块、进程管理模块和虚拟内存模块。有了这些模块，我们可以构建一个经过认证的顺序内核。

如果您想添加虚拟机管理程序功能，如虚拟化模块，那么您所需要做的就是在硬件端有一个支持虚拟化的模块来显示硬件功能。升级到流程管理，然后您可以开始验证虚拟化模块是否用于实施虚拟机管理程序。经过这种验证，您可以获得一个经过认证的虚拟机管理程序，您可以在其上引导linux，并且有多个版本的linux。

有了这个，我们就可以彻底了解每一段多行代码之间的关系。例如，前面提到的3000行代码可以转换成37层抽象层，这些抽象层都是逻辑抽象层，所以它的实际速度和功能与以前一样。有了这些抽象层，中间的各种关系可以被理顺，不会出错。

在此基础上，我们还可以用它来实现一些并发内核。众所周知，未来越来越多用于所有自动驾驶汽车的芯片应该是mpsoc。这些多核处理器带来了许多同步问题。每个人都知道并发程序是现在编写程序的最大挑战。如果这个问题得不到解决，未来整个自动驾驶汽车和无人驾驶飞机将会有很大的局限性。

所以现在我们也做多核内核的验证。多核内核的验证类似于刚刚使用的技术。我们所做的是使您能够将串行系统中使用的验证方法应用于多核。我们让多核机器像一根弦，除了其他处理器成为它的环境。

每个模块不仅可以保证它符合规范，而且即使有其他并发进程，也不会有问题，黑客也不能攻击。

在验证并发操作系统的工作中，我们发现，即使是大家已经使用了十多年的操作系统教科书中的许多例子，在涉及到并发代码时，也有许多是错误的。虽然老师说了很多，学生读了很多，但是当我们用它来验证的时候，我们还是发现有些地方没有考虑到，所以我们在验证的过程中发现了很多漏洞，这些漏洞会成为网络安全的隐患。

在此基础上，我们还对设备驱动做了一些验证，这其实很有趣。事实上，我们操作系统验证的目标不是只验证一个特定的操作系统，而是验证一种平台，它可能不仅仅是几个CPU。例如，汽车里会有许多装置和许多电子控制单元。因此，汽车操作系统不仅仅是一个简单的linux，而是运行在一个盒子上。

我们也可以用同样的方法在这样的设备上构建一个抽象层，我们已经在这方面做了大量的工作，比如在设备驱动的底层与硬件接触的地方构建大量的抽象层。此外，我们还可以使用它来验证一些安全性，这可以确保任意两个线程在规范级别上不会相互影响，也就是说，即使黑客控制了其中一个组件，他也不能破坏剩余的组件。这在汽车中非常重要，因为汽车中有许多部件。如果黑客通过一个组件的操作系统入侵汽车，他们很可能会用它来攻击其他组件或整个主机。

总的来说，虽然我们关注的是certikos这一简单的操作系统，但我们也在不断寻求突破，比如在其上实现实时功能，向支持多核的安全操作系统迈进，这一技术也越来越成熟。

事实上，这个领域的大部分工作以前都是在航空航天领域进行的。现在，越来越多的业内人士认为，航空航天领域的许多需求将逐渐转向自主飞行器。

5.最后，对于操作系统，中国过去所做的大部分工作只停留在较高层次的应用层或系统层，而核心部分涉及不多。

如今，智能城市、区块链和自动驾驶汽车等新应用已经起飞，原有的操作系统并不完全适用于这些新应用。然而，为了能立即进入市场，他们中的许多人都是在设备上进行了一点改造。事实上，里面有很多问题。

因此，操作系统已经到了一个拐点。此时，如果有一个安全的操作系统和一个新的平台出现，我相信很多行业都会拥抱这个平台。

*文中的图片被雷锋截获。来自邵忠演讲ppt

雷锋原创文章。严禁擅自转载。详情请参考转载说明。