资讯 人工智能
此为临时链接,仅用于文章预览,将在时失效

耶鲁大学终身教授邵中:「没有 bug」的操作系统是如何炼成的?| CCF-GAIR 2017

作者:奕欣
2017/05/31 09:35

a2+b2=c2

毫无疑问,勾股定理是固若金汤的真理,因此也不存在被推翻的可能性。

而在颠扑不破的数学真理之外,这个世界上还存在着病毒,不论是猖獗不已的勒索蠕虫,或是防不胜防的「全家桶」流氓软件,都在无孔不入地寻找软件的漏洞。

那么,世界上是否可能有一种软件「没有 bug」,就像真理般没有漏洞、不可攻破?

耶鲁大学终身教授、FLINT 实验室主任邵中教授坚定地告诉雷锋网:有。

耶鲁大学终身教授邵中:「没有 bug」的操作系统是如何炼成的?| CCF-GAIR 2017

「防黑客攻击」的操作系统

邵中教授是计算机程序语言设计领域的国际权威,他所研发的 SML/NJ 已经成为了 SML 语言最流行的编译器。而目前,邵中教授在耶鲁大学所做的有关 CertiKOS 操作系统的关键研究,就是让系统软件变得更加可靠安全,「保证这些软件不会出错,把里面的 bug 都去掉。」

耶鲁大学终身教授邵中:「没有 bug」的操作系统是如何炼成的?| CCF-GAIR 2017

所谓「没有 bug」的操作系统,严格意义来说,指的是能够防黑客攻击的软件体系。邵中教授告诉雷锋网,这个问题从根本上可以通过编程或者程序的设计来实现。

这听上去有些不可思议,但「完美的」操作系统是真实存在的。

「这与我们小时候做数学证明有点类似。以勾股定理为例,我们证明这个定理时,不会将所有的边都穷尽列举出来,而是通过一组引理经过逻辑演绎进行证明。也就是说,我们将程序当成一个数学公式,保证在任何情况下,所有的输入都会按照设计者所想的那样执行,即与原本设计的功能保持一致。如果保持一致,那么就表示它不可能有病毒可以侵入。」邵中教授这样告诉雷锋网 AI 科技评论。

这就是保障程序不出错的关键方法,也是邵中教授所提倡的「certified software with mechanized proofs」(可信软件)的核心要义,它也已经成为国际上非常活跃的一个研究分支。

但计算机编程与数学证明的不同之处在于,系统软件的结构设计非常复杂,可能达到上万行底层的汇编代码。那么,如果程序设计者要实现十个功能,那么必须保证在任何情况下,这段代码会严格按照这十个功能去执行,这依然是非常具有挑战性的一个事情。

那么在如此庞大的信息体系中,如果程序设计者每设计一个系统,便要将可能涉及的定理从头证明一次,这样的工作量显然是不现实的。计算机发展到现在,每一次进步都是在把人类生活当中的每一样东西放到虚拟世界里。而在构建了形式化证明工具(proof assistant)时,设计者能将程序的逻辑证明过程存在计算机中,在写形式规范之时,可以通过调用的方式直接生成程序,同时又可以生成证明。

「我们所做的这种软件一旦被证明,这些代码里就不可能有任何的 bug。因为如果有 bug,那么就意味着这个证明是不对的,如果证明不对,说明数学上的逻辑就不对了。而如果数学逻辑有不对的地方,可能这就不是一个程序设计问题,而是一个颠覆数学圈的问题了(笑)。」

自动驾驶的安全问题

邵中教授非常关注操作系统的安全应用问题,他认为随着人工智能、物联网、自动驾驶的发展,软件对安全也会有越来越高的需求。而自动驾驶作为多家汽车厂商竞逐的热点,它的安全性便成了一个不可忽视的议题。中国科恩实验室曾通过安全漏洞,在无物理接触的情况下攻破特斯拉;切诺基吉也曾经被美国网络安全专家查利·米勒和克里斯·瓦拉塞克「黑」过。如果被不法之徒抓到可趁之机,后果不堪设想。

邵中教授告诉雷锋网 AI 科技评论,自动驾驶的系统有多元性,且需要与多个领域进行紧密合作,因此车载系统软件的最底端必须是可靠安全的。「人类在逐步依赖计算机控制的设备时,软件是第一步,核心软件里一定不能有任何的 bug。我们第一步要把最底端(的架构)做安全,虽然不见得所有的零件与软件都能保证安全,但它至少能保证一旦出错,底端架构能够观察与监控部件,且不让出错部件影响其它的地方。」

如果有了这样完美的软件,又会对自动驾驶产生怎样的影响呢?邵中教授提及了两个有意思的领域。

一个是保险领域。有了安全可靠的软件,保险费用及投保主体势必会发生变化。「如果坐车的人不开车,而自动驾驶汽车不可能永远不出问题,那么谁会为保险而买单?我想汽车制造商会把保险变成汽车成本的一部分。那么,如果汽车本身的 bug 越少,那么它的保费自然越便宜。因此,有了安全可靠的软件,同样能带来经济上的好处。」

第二个是法律伦理方面。就像「电车问题」一样,如果是人做抉择,可能只是一瞬间的反应,但如果把这个选择权交给自动驾驶汽车,又需要如何用程序来限定它的行为?人与人之间的约束是通过法律来达成,而人与机器自然也会有一些形式规范存在。「法律条款与我们所说的形式规范,其实是一个东西。只不过前者可能是用法律语言写出来,而后者是用数学语言写出来。这一点对于我们做科研的人而言就非常有意思。」

在今年 7 月 7 日的 CCF-GAIR 2017 大会,邵中教授也将亲临自动驾驶分会场,与我们分享他在软件安全性的真知灼见。

可信软件,任重道远

不过,伴随而来的一些困难与挑战也让可信软件的应用带来了困难。

首先,可信软件的发展是一个循序渐进的过程。原来的软件系统已经沿用了 30 年,已经在不断的迭代中形成了属于自己的生态系统。而新软件一开始的功能相对有限,因此这个演变的过程肯定需要一些时间。

「但我认为,人类对软件安全的追求肯定是不会停止的,一旦技术上具有可行性,那么所有的人都不会希望自己用的是一个会被勒索的、会被黑客攻击的软件。」

其次,人工智能的大环境尚不成熟,很多商业化应用目前还没有发展到考虑安全的阶段,也没有足够的人才能做这件事情。以自动驾驶为例,现在有很多企业还处于第一步,即在没有黑客攻击的前提下先让车跑起来的状态。「防黑客攻击,听上去像是下一步的事情。但我觉得安全性的确是不能往后推移的。一旦汽车上路了,还是会有很多问题存在。」

此外,研发可信软件的成本还是非常高的,目前主要集中于高校研究。这也是邵中教授今年 7 月受邀参加 CCF-GAIR 2017 大会的另一个原因,他希望在这个千人盛会上,通过表达自己的想法与思考,与多方寻求可能的合作。

邵中教授一直坚信,设计安全可靠的程序,才是实现人工智能的必由之路。「所有的人工智能到最后,都是用程序来实现的。这就是一个搞懂不同模块之间关系的过程。而实现复杂人工智能功能的一个过程,就是从根本上弄懂底层这些功能的机制是如何实现的。那么,保证安全可靠的目的,就是要彻底弄懂功能之间的关系,让它们的逻辑非常清晰,没有矛盾。」如果你想更深入地了解邵中教授的观点,欢迎来到 7 月 7 日-9 日中国计算机学会(CCF)主办,雷锋网与香港中文大学(深圳)承办的第二届 CCF-GAIR全球人工智能与机器人峰会,目前六折票正在火热销售中,详情可访问大会官网了解。

耶鲁大学终身教授邵中:「没有 bug」的操作系统是如何炼成的?| CCF-GAIR 2017

长按图片保存图片,分享给好友或朋友圈

耶鲁大学终身教授邵中:「没有 bug」的操作系统是如何炼成的?| CCF-GAIR 2017

扫码查看文章

正在生成分享图...

取消
相关文章