*耶鲁大学邵中教授在CCF-GAIR 2017大会现场 雷锋网按：2017年7月9日，中国计算机学会（CCF）主办、雷锋网（公众号：雷锋网）与香港中文大学（深圳）承办的第二届全球人工智能与 机器人 ( 行情 300024 ,诊股)峰会（CCF-GAIR 2017）进入到最后一天的议程。自

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

　　雷锋网按：2017年7月9日，中国计算机学会（CCF）主办、雷锋网（公众号：雷锋网）与香港中文大学（深圳）承办的第二届全球人工智能与机器人(行情300024,诊股)峰会（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语言代码。

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

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