Johann Schumann高保证系统亚博体育苹果app官方下载

||谈话

约翰舒曼肖像约翰·舒曼博士是一个成员强大的软件工程组RSE美国宇航局艾米斯。他获得了他的住士学位(2000)慕尼黑技术大学,德国应用自动定理普通在软件工程中的应用。他的博士论文(1991)是关于高性能并行定理的证明。Schumann博士从事软件和系统健康管理的研究,先进亚博体育官网的空中交通管制算法和自适应系统的验证和亚博体育苹果app官方下载验证,空中交通管制系统和无人机事件数据的统计数据分析,数据分析和状态估计的可靠代码生成。Schumann博士的一般研究兴趣集中在正式和亚博体育官网统计方法的应用,以改进先进的安全和安全关键软件的设计和可靠性。

他受雇于SGT,Inc。作为计算科学的首席科学家

卢克·穆罕沃斯: 在丹尼等人。(2006),你和你的合著者解释:

软件认证旨在表明,有问题的软件实现了一定的质量,安全或安全性。其结果是证书,即,独立认为所申请物业的证据。认证方法很广泛......但是通过基于正式方法的方法实现了最高程度的信心,并使用证明证书的逻辑和定理来实现。

我们开发了一种认证方法,其中... [表现出]航空航天软件的安全性,这些软件已从高级规格中自动产生。我们的核心思想是扩展代码生成器,使其同时生成代码和详细的注释......实现了全自动的安全证明。验证条件生成器(VCG)处理注释的代码,并产生一组安全义务,如果代码是安全的,则可以提供。然后,自动定理箴言(ATP)然后排除这些义务和证明,可以通过独立的证明检查器验证,作为证书......

... [我们]建筑区分信赖不可信的受信任的组件必须是正确的,因为其结果中的任何错误都可能危及系统提供的保证;亚博体育苹果app官方下载不受信任的组件不会影响可靠性,因为它们的结果可以由受信任的组件检查。

你还可以使用这个有用的例子:

认证体系架构,Denney等亚博体育苹果app官方下载人(2006)

为什么问题规范和合成系统不受信任,在您的认证系统架构中?亚博体育苹果app官方下载


约翰舒曼理想情况下,图中的整个体系结构只包含受信任的组件。这样就可以确保在验证过程中不会发生任何不好的事情。不幸的是,像程序综合系统或一个完整的自动化定理证亚博体育苹果app官方下载明程序这样的软件系统不能用当前的技术进行正式验证。他们的代码有数万行。因此,我们使用了一个问题复杂性不对称的技巧:例如,一个软件找到一个大数的质因数是复杂的;它的验证是复杂和费时的。另一方面,检查每一个单独的结果是微不足道的:只是把因素相乘。这样的检查器很容易实现和验证。因此,如果我们现在使用未验证的质数因子查找器,并且对每个结果运行快速且小型的已验证检查器,我们就可以知道质数因子查找器是否正确工作。这里重要的是:每个结果都需要运行检查器,但由于检查器速度很快,这并不重要。 Similar situation here: synthesis system and prover are复杂,但证明检查器不是。VCG具有中等复杂性,可以验证。整个系统的实际瓶颈是您必须相信您的安全政策和域理论。亚博体育苹果app官方下载两者都可以是更大的逻辑公式。在我的经验中:如果公式超过5行,则很可能包含一个错误。不幸的是,没有简单的方法。


卢基:直观地,与通过正常工程方法和广泛测试开发的系统相比,您认为通过正式方法(如您自己的过程)开发亚博体育苹果app官方下载了多少“更安全”吗?对你的知识有这种假设有任何经验考验?


约翰:直觉上,我认为在软件开发和V&V中使用形式化方法(FM)可以大大提高安全性。然而,这里有一些问题/考虑:

  • Using FMs to verify that certain, well understood safety properties are never violated (e.g., no buffer overflow, no divide-by-zero, no uninitialized variables) is extremely beneficial (see recent security problems — a lot of those have to do with such safety properties). Some technologies for that task (e.g., static analysis) have already achieved much in that direction.
  • 即使假设工具在那里,也必须问:我可以指定所有必要的安全属性?是软件的规范,我对此进行了基于FMS的验证,正确和一致吗?正确的,一致和完整的规范非常难以写入 - 因此对于任何合理复杂性的软件,我将假设在代码中有规范中至少存在许多错误。
  • 在我看来,FMs应该和传统的方法(包括测试)一起使用,和动态监测一起使用。例如,一个正式的无缓冲区溢出证明应该能够减少(但不能消除)大量的测试。由于测试只能是有限的,所以应该使用动态监视(又名运行时验证(RV)或软件运行状况管理(SWHM))来对未预见到的软件行为(例如,由潜伏的bug或在未预料到的环境中操作引起的)作出反应。RV和SWHM本身大多基于形式化方法。

我不知道任何这样的经验测试 - 他们很难以无偏见的方式进行。致力于成本和可靠性建模(例如,B. Boehm)可能会提供一些洞察力,但我需要看看。


卢基:您认为正式的验证方法最终将如何有效地处理更复杂的安全属性,如火车、飞机和汽车的避碰,以及Asimovian属性(一个拉WELD&ETZIONI.)对于与人类亚博体育苹果app官方下载互动的系统?


约翰:有几个示例,其中正式的方法已成功用于复杂系统的规范和/或开发。亚博体育苹果app官方下载例如,B方法(与Z方法相关的工具支持的方法)已被用于巴黎地铁(第14行)上的自动列车控制。空中客车正在使用正式方法,如抽象解释(Cousot),以便他们开发安全关键的飞机软件。

TCAS系统(交通亚博体育苹果app官方下载避碰系统)是商用飞机上的一个国际系统,用于警告飞行员在空中(不到一分钟的距离)发生碰撞的危险。这个复杂的系统(飞机需要使亚博体育苹果app官方下载用一个详细的通信协议来解决彼此之间的冲突)已经被详细研究,并有正式的规范/分析(例如,Leveson, Heimdahl和其他)。

在我看来,形式化方法足够强大,可以用来指定/验证复杂的系统。亚博体育苹果app官方下载然而,尤伯林根事故表明,这个系统不是故障安全的。亚博体育苹果app官方下载这里的“系统亚博体育苹果app官方下载”指的是:实际的硬件/软件,飞行员(他们从TCAS系统和空中交通管制系统得到了相互矛盾的信息),航空公司(据说该公司告诉飞行员不要理会警告,选择最赚钱的航线),以及瑞士空中交通管制部门,该部门人手不足。

对我来说,似乎在混合控制系统中的人类行为的准确建模和预测(人类运营商拥有所有/部分控制)仍然是一个大型未解决的问题。亚博体育苹果app官方下载

一个完全自动化的系统(例如,无人机)亚博体育苹果app官方下载可能安全地处理这种情况,但一般有几个主要问题:

    1. 接受问题(我们会挂载一个UA,我们会在我们的车的轮子中抵御我们的车轮吗?)。据说,当Bart首次引入无人驾驶训练时,他们不被通勤者接受,他们不得不把司机放回火车上。
    2. 如何在“混合模式”环境下安全操作?例如,一些汽车是自动驾驶的,一些汽车是手动驾驶的,或者商用飞机与通用航空和无人机系统的对比。亚博体育苹果app官方下载人类操作员可能会犯(愚蠢的)错误或以意想不到的方式作出反应。自动化系统也可能会有出乎意料亚博体育苹果app官方下载的反应,例如,因为一个软件错误。
    3. 如何处理系统安全性?亚博体育苹果app官方下载许多增加安亚博体育苹果app官方下载全的系统目前很容易受到恶意攻击的影响:例如,ADS-B系统,该系统应该替代老化ATC系统的部分使用未加密的协议;UAS飞机可以欺骗(见由伊朗捕获的CIA UA);现代汽车可以轻松攻击。

虽然在复杂系统的严格的追踪和规范中发生了很多事情,但在我们甚至接近谈论机器人规律时需要解决许多问题。亚博体育苹果app官方下载

如何在操作失误后安全地恢复一个复杂的系统?亚博体育苹果app官方下载假设一辆装有驾驶辅助系统(例如,自适应巡航控制,检测不安全的变道)的车里的驾驶员。亚博体育苹果app官方下载自动系统如何应对迫在眉睫的问题,而不让司机惊慌亚博体育苹果app官方下载失措,犯更多错误?

如何在系统硬件或软件中存在问题后安全恢亚博体育苹果app官方下载复系统?当发动机在Qantas A380上爆炸时,那些根据400个诊断和错误消息的指挥,他们必须处理(幸运的是他们有时间)。一些信息彼此矛盾或者会难以执行。

这表明以复杂系统的简洁和正确的状态信息呈现操作员仍然是一个大问题。亚博体育苹果app官方下载

在飞行员降落A380后,他们无法转动发动机。机器智能的第一个迹象“不要杀了我”?


卢克:谢谢你,约翰!