凯萨琳Fisher博士加入了Darpa作为2011年计划经理。她的研发利益与编程语言和高保证系统有关。亚博体育官网亚博体育苹果app官方下载费舍尔博士从塔夫茨大学加入了Darpa。此前，她担任AT＆T实验室的技术人员的主要成员。费舍尔博士在斯坦福大学获得了计算机科学的哲学哲学和斯坦福大学数学和计算科学学士学位。
卢克·穆罕沃斯：Kathleen，你是Darpa的节目经理HACMS.旨在使用“清洁板岩，基于方法的方法”方法构建满足“适当安全性和安全性能”的网络 - 物理系统。亚博体育苹果app官方下载我的第一个问题类似于一个我格雷格问Morrisett关于安全的计划，旨在为“适用于弹性和安全系统的清洁板岩设计”：在HACMS的情况下，为什么采取“清洁板岩”的方法如此重要，并从地上设计系统的安全和安全性亚博体育苹果app官方下载（以及功能正确）？
凯瑟琳费舍尔：研亚博体育官网究人员一直在努力证明几十年来正确的程序，直到最近（成功的例子包括Nicta）Sel4 Microkernel.和inria的验证c编译器的compcert）.在这个过程中得到的教训之一是，验证现有代码比验证编写的代码要困难得多。
这有几个原因。首先，许多必须保持程序正确的不变量通常只存在于程序员的头脑中。当试图在事后验证一个程序时，这些不变量已经丢失，验证者需要很长时间才能重新发现。其次，有时代码可以以多种方式编写，其中有些方式比其他方式更容易验证。如果程序员知道他们必须验证代码，他们会选择容易验证的方式。
路加福音：哈珀(2000)引用一个旧消息由肯·弗里斯到了安全关键邮件列表：
认为必须将正式证明应用于智能系统让我感冒。亚博体育苹果app官方下载如何为在持续学习过程中有能力改变自己的东西提供满意的保证？
显然，我们不能为整个宇宙写一个正式的规范，并根据它正式地验证一个系统，那么什么类型的(正式的)事情呢亚博体育苹果app官方下载可以我们要确保越来越强大的自动系统的可取行为吗?亚博体育苹果app官方下载
凯萨琳验证自适应或智能系统是一项困难的挑战。亚博体育苹果app官方下载它是一个积极的研究课题，特别是在航空电子工业。亚博体育官网一种方法是使用Simplex体系结构，在该体系结构中监视智能系统，以确保其处于安全范围内。亚博体育苹果app官方下载如果智能系统看起来要离开信封，监视器就亚博体育苹果app官方下载会将控制转移到一个基本系统。在这种方法中，必须直接验证监视器、开关代码和基本系统，而不是智能系统。亚博体育苹果app官方下载目前的技术可以检验这些更小的部件。
路加福音：您之前说过“验证现有代码比验证验证的验证代码更难。”这表明需要在需要非常高的系统安全性时，例如，亚博体育苹果app官方下载对于自动驾驶仪软件，需要大量的额外工作，因为一个人必须从头开始设计一个系统“从地上开始”的安全性和验证。亚博体育苹果app官方下载
此外，我的印象是设计可核心安全的智能系统所需的工作往往比设计智能系统所需的工作更为“串行”，而无需如此高度可验证的安全性。亚博体育苹果app官方下载在设计一个不需要特别是“安全”的智能系统时，例如，亚博体育苹果app官方下载一个亚博体育苹果app官方下载系统智能地选择用于显示网站访问者的广告，人们可以从这里和那里搭配一系列代码，并在某些数据集中测试结果，然后在现实世界中运行系统“。但是，需要以非常精确的方式建立一个可判定的安亚博体育苹果app官方下载全系统，根据以前的选择，许多算法设计选择，以及许多研究洞察依赖于之前的见解等的形状，似乎是项目亚博体育官网设计不可判断安全的智能系统比设计可验证安全智能系统的项目更轻松地平行。亚博体育苹果app官方下载
这也是你的印象吗?你要怎么修改我的账号?
凯萨琳你的评估是准确的。基本上，如果您的代码有广泛的可接受的行为，并且如果它的错误行为没有特别糟糕的后果，那么编写代码就会容易得多。
我要小心并行化。它通常用于指零件与其他部分同时运行的程序，如多个计算机或芯片。它还可以指并行工作的程序员。使用它的方式，它读取就像你的意思是，当我认为你的意思是说代码是并行编写的时，代码并行运行。两者都更容易获得非高保证码，但您正在制作的论据将其自身带到“并行写入”解释。
路加福音:在可验证的网络物理系统安全方面，您观察或预期有哪些定性或定量趋势?亚博体育苹果app官方下载例如:你认为研究亚博体育官网能力和智力网络物理系统的发展速度超过了对它们的亚博体育苹果app官方下载研究亚博体育官网安全和验证性？相对于另一个(安全性和可验证性)，具体来说，就网络物理系统而言，一个(能力和亚博体育官网智力)投入了多少资金和质量调整后的研究时间?亚博体育苹果app官方下载对于每一项而言，有多少低挂的果实似乎已经被摘走了，比如，额外的进展单位需要比以前的单位更多的资金和研究时间?亚博体育官网
凯萨琳总的来说，对能力的研究超过了亚博体育官网对如何确保这些能力安全的相应研究。一个给定能力的安全性问题在该能力被证明是可能的之前并不有趣，所以最初研究人员和发明者自然更关注新能力，而不是与其相关的安全性。亚博体育官网因此，一旦新功能被发明出来并证明是有用的，安全性就必须跟上。
此外，根据定义，新功能添加了有趣和有用的新功能，这些新功能通常会提高生产率、生活质量或利润。安全除了确保某物按预期的方式工作之外，什么也没有增加，所以它是一个成本中心而不是利润中心，这往往会抑制投资。
我不知道如何将数据收集，以显示对能力与安全性的研究级别。亚博体育官网我不确定美元总数会揭示。亚博体育官网即使在安全性上花费了更多的资金，安全性仍然可以滞后，即使在安全性上花费了更多的资金，如果安全性比对能力更昂贵。
路加福音：确保具有非常有限的行为和最有限的决策能力的系统安全行为是一项挑战，并相当于确保具有更大的自主能力的系统的安全亚博体育苹果app官方下载行为。您认为确保网络实际系统安全行为的前景是什么，因为它们具有足够的智力和自主权，以便例如为例如ev。亚博体育苹果app官方下载更换工厂工人，更换出租车司机，更换战场部队等几十年来？
凯萨琳如你所说，用定义良好的行为来确保简单系统的安全行为要容易得多。亚博体育苹果app官方下载尽管如此，很明显，我们将为各种各样的活动部署越来越复杂的网络物理系统，我们将需要能够确保这些系统足够安全。亚博体育苹果app官方下载我认为技术的结合将使我们能够达到这一目标，尽管还需要大量的额外研究。亚博体育官网这些技术包括:1)基于模型的设计，2)程序合成，3)安全性和安全意识的组合，以及4)基于简单的架构。基本上，我们将需要从简单的组件和简单的架构开始，然后利用它们来构建越来越复杂的系统。亚博体育苹果app官方下载
路加福音： 谢谢！
你喜欢这个帖子吗?你可以享受我们的其他谈话帖子，包括：
