a2+b2=c2 ；
毫无疑问，勾股定理是固若金汤的真理，因此也不存在被推翻的可能性。
而在颠扑不破的数学真理之外，这个世界上还存在着病毒，不论是猖獗不已的勒索蠕虫，或是防不胜防的「全家桶」流氓软件，都在无孔不入地寻找软件的漏洞。
那么，世界上是否可能有一种软件「没有 bug」，就像真理般没有漏洞、不可攻破？
耶鲁大学终身教授、FLINT 实验室主任邵中教授坚定地告诉雷锋网：有。
「防黑客攻击」的操作系统
邵中教授是计算机程序语言设计领域的国际权威，他所研发的 SML/NJ 已经成为了 SML 语言最流行的编译器。而目前，邵中教授在耶鲁大学所做的有关 CertiKOS 操作系统的关键研究，就是让系统软件变得更加可靠安全，「保证这些软件不会出错，把里面的 bug 都去掉。」
所谓「没有 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-GAIR 2017 大会，目前六折票正在火热销售中，详情可访问大会官网了解。
