研究人员致力于消除计算机错误的工具

当您的计算机崩溃时,失去一个小时的工作已经够糟糕的了-但是在医疗保健和航空业等环境中,软件故障可能会带来更为严重的后果。

消除计算机错误

在一个臭名昭著的案例中,计算机错误导致癌症患者从放射治疗机中接收致命的过量药物。在最近的头条新闻中,埃塞俄比亚和印度尼西亚的飞机失事归咎于有缺陷的软件。

努力消除计算机错误

现在,史蒂文斯理工学院的研究人员与耶鲁大学合作,正在开发可大大降低灾难性计算机灾难发生可能性的工具。

由史蒂文斯(Stevens)计算机科学助理教授埃里克·科斯金宁(Eric Koskinen)领导的这项工作不仅旨在确保程序在特定情况下正确运行,而且还使用算法确定在任何情况下在逻辑上是否有可能使软件产生不需要的内容。结果。

“我们的目标是100%保证您永远不会遇到错误,” Koskinen说。

Koskinen的团队得到了海军研究办公室(Office of Naval Research)超过250万美元的支持,为该计划的两个版本之间的差异建模。这很有用,因为程序员通常是在现有软件的基础上进行工作,而不是从头开始编写代码,并且可以将错误从一个版本引入另一个版本。

这种方法对军方特别有价值,因为国防机构经常从私人承包商那里购买软件,然后在将其部署到关键任务状态之前进行内部更改。

Koskinen说:“他们需要一种方法来确认自己在内部正确进行了更改,并且没有引入新的问题。”

时间逻辑

为了从数学上证明计算机程序永远不会存在任何类型的错误,无论是在预期的还是无法想象的任何情况下,Koskinen的团队都使用了一种称为时态逻辑的策略。

该团队而不是仔细检查每行代码以寻找语法差异,而是由史蒂文斯(Stevens)二进制分析专家助理徐准(Jun Xu)组成的团队研究程序在一段时间后的行为方式。这个想法是要证明,无论程序运行多长时间,都没有逻辑上的方法可以返回不想要的结果。

对程序的结构和行为建模,而不是遍历每行代码很重要,因为完全相同的代码行在不同的上下文中可能具有不同的效果,就像看起来很不同的代码行可以完成相同的事情一样。

Koskinen解释说,这就像研究法律文档一样:更改一个单词看似微不足道,但可以更改文档的整体含义。时态逻辑有助于对程序的潜力进行建模,从而获得对程序实际功能的强大见解。

使用封闭源

该小组的方法还可以消除现有商业软件中源代码不可用的错误。如果没有源代码,则团队只能使用源代码的二进制版本比较计算机程序。他说:“如果您看不到源代码,就很难知道该漏洞是否真的已被消除。”

“我们正在构建的技术将做到这一点:如果您拥有自己信任的软件版本,我们的技术将能够帮助您发现更改-软件更新中的漏洞或插入到可执行程序中的恶意软件-并决定是否信任新版本。”

一个工具包正在开发中

Koskinen的团队还正在开发一个工具包,其他研究人员和公众将可以使用该工具包来测试软件-他们正在扩大其方法以与更大的程序和更复杂的故障一起使用。 “这些都是困扰现代计算机系统的大问题,” Koskinen说。

“这些问题只会在医疗保健,航空,自动驾驶汽车等领域变得越来越关键,因此至关重要的是,我们开发实用技术以使计算机控制系统无错误且使用安全。”

分享这个