侵权投诉
技术:
GPU/CPU 传感器 基础元器件 网络通信 显示 交互技术 电源管理 材料 操作系统 APP 云技术 大数据 人工智能 制造 其它
应用:
可穿戴设备 智能家居 VR/AR 机器人 无人机 手机数码 汽车 平衡车/自行车 医疗健康 运动设备 美颜塑身 早教/玩具 安防监控 智能照明 其它
当前位置:

OFweek智能硬件网

交互技术

正文

没有bug的操作系统是如何炼成的?浅访耶鲁大学终身教授邵中

导读: 世界上是否可能有一种软件「没有 bug」,就像真理般没有漏洞、不可攻破?耶鲁大学终身教授、FLINT 实验室主任邵中教授坚定地告诉说:有。

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

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

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

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



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

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



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

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

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

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

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

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

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

1  2  下一页>  
声明: 本文由入驻OFweek公众平台的作者撰写,除OFweek官方账号外,观点仅代表作者本人,不代表OFweek立场。如有侵权或其他问题,请联系举报。

我来说两句

(共0条评论,0人参与)

请输入评论

请输入评论/评论长度6~500个字

您提交的评论过于频繁,请输入验证码继续

暂无评论

暂无评论

文章纠错
x
*文字标题:
*纠错内容:
联系邮箱:
*验 证 码: