凯瑟琳博士费舍尔2011年加入DARPA，担任项目经理。她的研究金宝博娱乐和开发兴趣与编程语言和高保证系统有关。金宝博官方Fisher博士从塔夫茨大学(Tufts University)加入DARPA。在此之前，她曾担任AT&T实验室技术人员的主要成员。Fisher博士获得Stanford University的计算机科学博士学位和数学和计算科学学士学位。
路加福音Muehlhauser:凯瑟琳，你是DARPA的项目经理HACMS该项目旨在构建满足“适当安全和安全属性”的网络物理系统，使用“全新的、正式的基于方法的方法”。金宝博官方我的第一个问题类似于我问Greg Morrisett.有关安全在HACMS的情况下，为什么采取“干净的设计”的方法如此重要，并从头开始设计系统的安全性和安全性(以及功能正确性)?金宝博官方
凯瑟琳·费雪研究金宝博娱乐人员几十年来一直试图证明这些程序是正确的，但直到最近才取得了很少的成功(成功的例子包括NICTA的程序seL4微核和法国的验证C编译器）。在此过程中学到的一个经验教训是，验证现有代码比验证验证的验证代码更难。
有几个原因这一点。首先，许多必须持有要正确的程序的不变性通常仅存在于程序员的头部。在尝试验证事实后验证程序时，这些不变性丢失，并且可能需要很长时间才能重新发现。其次，有时代码可以以多种方式编写，其中一些比其他方式更容易验证。如果程序员知道他们必须验证代码，他们将选择易于验证的方式。
卢基：哈珀（2000）引用A.旧消息作者是肯·弗里斯安全关键邮件列表：
对于必须将形式证明应用于智能系统的想法，我没有兴趣。金宝博官方在一个持续的学习过程中，你如何提供令人满意的保证?
显然，我们无法编写整个宇宙的正式规范，并正式验证系统的系统，那么哪种（正式）的东西金宝博官方能够我们确保从越来越能力的自治系统中确保所需的行为？金宝博官方
凯瑟琳：验证自适应或智能系统是一个艰难的挑战。金宝博官方它是积极研究的主题，特别是在航空电子工业中。金宝博娱乐一种方法是使用Simplex架构，其中监视智能系统以确保其在安全信封内。金宝博官方如果智能系统很可能会离开包围，则监视器金宝博官方将控制转移到基本系统。在这种方法中，监视器，交换代码和基本系统必须直接验证，但不是智能系统。金宝博官方验证这些较小的碎片在当前技术的范围内。
卢基:您前面说过“验证现有代码比验证编写的代码要困难得多。”这表明，当需要非常高水平的系统安全时，例如自动驾驶软件，就需要大量额外的工作，因为基本上必金宝博官方须从头开始设计一个系统，“从头开始”，并牢记安全性和验证。
此外，我有一个印象，设计一个可验证的安全智能系统所需要的工作，在本质上往往比设计一个没有如此高程度可验证安全的智能系统所需要的工作更“串行”。金宝博官方当设计一个智能系统,不需要特别“安全”,如系统智能地选择网站金宝博官方访问者播放的广告,一个从这里能够拼凑出的代码和测试结果在一些数据集,然后运行系统“在现实世界中。”但一个可验证的安全系统需要以一种非常精确的方金宝博官方式构建，许多算法设计选择取决于之前的选择，许多研究见解取决于之前见解的形状，等等。金宝博娱乐这样看来，设计一个非可验证安全的智能系统比设计一个可验证安全的智能系统更容易并行。金宝博官方
这也是你的印象吗？您如何修改我的帐户？
凯瑟琳：您的评估是准确的。基本上，如果您的代码具有广泛的可接受行为，如果如果不对行为不当，则编写代码的更容易。
我要小心平行化这个词。它通常用于指部分与其他部分同时运行的程序，比如在多台计算机或芯片上。它还可以引用并行工作的程序员本身。你使用它的方式，它读起来就像你说代码是并行运行的，而我认为你的意思是代码是并行编写的。这两种方法对于非高度保证的代码来说都比较容易，但是您所提出的论点有助于“并行编写”的解释。
卢基：您在可劣地安全的网络系统系统方面观察或预测或预测您的定性或定量趋势是多少？金宝博官方例如：您认为对此进行研究金宝博娱乐能力和情报网络 - 物理系统正在超越他们的研究金宝博官方金宝博娱乐安全和可验证性？特定于网络物理系统，相对于其他（安全和验证），将有多少资金和质量调整的研究人金宝博娱乐员小时（能力和智能），专门用于网络 - 物理系统？金宝博官方似乎已经采取了多少低悬垂的水果，使得其他进展单位需要更多的资金和研究人员时间比以前的单位更多？金宝博娱乐
凯瑟琳：一般来说，研究能力将相应的金宝博娱乐研究分为如何使这些能力安全。在展示可能的情况下，给定能力的安全问题并不感兴趣，因此最初研究人员和发明人自然更加专注于新的能力而不是在其相关安全性上。金宝博娱乐因此，一旦新的能力已经发明并显示有用，安全通常必须赶上。
此外，根据定义，新功能增加了有趣和有用的新功能，这些功能通常会提高生产力，生活质量或利润。安全性除了确保其所在的方式之外，没有任何东西增加，所以它是一个成本中心而不是盈利中心，这往往会抑制投资。
我不知道如何收集数据来显示对能力和安全研究的投资水平。金宝博娱乐我不确定总金额是否能说明问题。金宝博娱乐即使在安全方面投入了更多的资金，如果安全研究的成本高于能力研究，安全研究仍可能落后于能力研究。
卢基确保一个行为非常有限、决策能力非常有限的系统的安全行为是一个挑战，而确保一个具有更大自主能力的系统的安全行为则金宝博官方是另一个挑战。你认为在未来的几十年里，随着网络物理系统被赋予足够的智能和自主性，以取代工厂工人、出租车司机、战场部队等，确保其安全行为的前景如何?金宝博官方
凯瑟琳：正如您所说，在具有明确定义的行为的简单系统的安全和安全行为要容易得多。金宝博官方也就是说，很明显，我们将为各种活动进行越来越复杂的网络物理系统，我们需要能够确保这些系统足够安全和安全。金宝博官方我认为技术的组合将使我们能够实现这一目标，尽管需要大量额外的研究。金宝博娱乐这些技术包括：1）基于模型的设计，2）编程合成，3）安全和安全感知组成，4）基于单纯的架构。基本上，我们需要从简单的组件和简单的体系结构开始，然后利用它们构建越来越复杂的系统。金宝博官方
卢基:谢谢!
你喜欢这篇文章吗？你可以享受我们的另一个对话的帖子,包括:
