Jonathan Millen在隐秘的频道通信中

卢克·穆罕沃斯：由于您是一个相对早期的研究员在封闭渠道通信领域，我想向您询问该领域的早金宝博娱乐期，这通常被称为已经开始Lampson（1973）。你知道第一个隐蔽的频道攻击何时被发现“在野外”？我的印象是，Lampson确定了一对夫妇的一般问题几十年在它被注意到在野外被注意到之前;是对的吗？

Jonathan Millen.：我们可能永远不会知道真正的隐蔽频道攻击是首先注意到，还是第一次发生时。当信息被隐蔽通道窃取时，原始数据仍然存在，因此盗窃可以不受注意。即使发现攻击，受害者也像肇事者一样不愿意承认它。这肯定是具有分类信息的情况，因为已知的攻击通常被归类于其妥协的信息。我1999年之前唯一的证据来自罗伯特·莫里斯（高级），是UNIX安全的先驱，以及一段时间，是国家计算机安全中心的首席科学家，在组织内部在NSA中。他在一个安全的研讨会上陈述了真正的攻击。他不会说什么;对于那么多，这可能很困难。

卢基：从您自己的角度来看，自从你写道以来，封面频道通信中有哪些最有趣的发展是什么“20年封闭信道建模和分析“1999年？

乔纳森：由于几个原因，这是一个棘手的问题。与多年来一直存在的许金宝博娱乐多研究领域一样，隐蔽的渠道研究已经分成了几种专业。一些副主题是非干扰模型，基于语言的信息控制通过类型理论，隐写术等。

虽然专业化是深入进步所必需的，但我希望更多地关注务实的“那么”关于隐秘渠道的问题。例如，信息流安全通常在非干扰方面定义，不幸的是，可以以多种不同的方式定义。所有这些都依赖于某种形式的行为等价，这是一个强大的条件，保证了未经授权的观察者无法判断出现更多特权的用户。甚至一点，或一点的一部分，有关受保护方的数据或行动的信息也被认为是过多的。然而，我们真正想知道的是可以设置复发频道，产生大量或无限的信息。此外，Shannon Sense中的信息可能是也可能没有用。一篇吸引着我的注意力是“用信仰量化信息流量“，由Clarkson，Myers和Schneider，2009年，因为它处理了信息的准确性。

另一个务实的问题是系统功能的可信度。金宝博官方一般来说，我不信任依赖于访问控制软件的安全方法或写入它的语言的设计。即使是操作系统内核下方的固件和硬件也是可疑的。金宝博官方在过去几年中，我的主要研究兴趣是受信任的计算，如可信平台模块的金宝博娱乐支持，其能力 - 在现代平台中可用但在很大程度上未使用 - 通过以篡改开始，通过引导序列加工检查系统软件的完整性金宝博官方-Resistant TPM。尽管如此，我们只知道系统软件是真实的，而不是它是正确的或没有隐蔽频道的真实性。金宝博官方它令人鼓舞的是，在软件和硬件验证方面的工作仍在继续，但常用的系统仍然超出其范围。金宝博官方

复杂性是安全的敌人。你必须越过的越多，你可以更少理解它足以排除漏洞。几个配子：安全策略的复杂就越复杂，它的强劲越弱，因为它需要更复杂的软件。并且更专业的系统组件是支持安全性，它越有吸引力是攻击的金宝博官方目标。我认为这是乐观的看法是，如果我们使用通常复杂的现代系统，秘密频道是我们最不担心的！金宝博官方

卢基: From your many decades of experience in computer security, do you know of cases where someone was worried about a computer security or safety challenge that wasn’t imminent but maybe one or two decades away, and they decided to start doing research to prepare for that challenge anyway — e.g. perhaps because they expected the solution would require a decade or two of “serial” research and/or engineering work, with each piece building on the ones before it, and they wanted to be prepared to meet the challenge near when it arrived? Lampson’s early identification of the “confinement problem” looks to me like it might be one such example, but maybe I’m misreading the history there.

乔纳森：在计算机安全中，通常发生的是有人意识到漏洞已经存在，但它不清楚恶意派对利用它需要多长时间。另一个因素延迟相关研究和开发的发病是，旨在消除漏洞的长期努力是风险的，其结果可能因未来不同问金宝博娱乐题而不足或黯然失色。

如果困难是社会，例如获得标准更新，难度是真实的，但基本的工程知识大多是早期可用的。For example, the TCP sequence number attack for session hijacking was pointed out by Morris in 1985, taken advantage of by Mitnick in 1995, led to Bellovin’s standards-related recommendations in 1996, and only recently has the availability of encryption-based authentication and IPv6 brought a widespread solution within reach.

如果难度是在工程中，如安全内核的开发和强制性访问政策击败木马，或者安装和使用TPMS时，有一个行业被移动，一个由新的商业可行性的需求驱动产品。毕竟努力，一些漏洞仍然存在。

计算机科学家可以通过开发强大的通用工具和技术，具有基本计算机科学目标 - 没有问题的工具。由此，我的意思是验证工具和模型检查器以及加密算法和应用程序。当新的问题和设计理念出现时，这些工具可以缓解工程负担。这些工具的发展应该有几十年的研究建筑在事后工作，应该鼓励和支持能够成功开展这项活动的人。金宝博娱乐

卢基：您提到验证工具和模型检查。我最近在计算机安全和安全社区中发表了重要人物（我没有许可给出她的名字）关于常见的方法，即正式方法可以捕获角落错误，这不仅仅是通过测试测试。她提到，如果正式方法社区曾经过正式的方法，以谨慎的实验表明，验证真的确实捕获了无法通过测试发现的错误，她不知道。你知道任何这样的示威活动吗？如果没有，怎么会怎么样你为安全和安全目的描述正式方法的价值吗？

乔纳森：对我来说，请求仔细的实验​​似乎是不公平的，以证明与测试相比证明正式方法。这是一个原因，指出了正式方法用于安全内核验证，是实际开发的很少的安全内核，因此任何实验结果都不会存在统计学意义。

在正式规格历史的一开始是由大卫Parnas进行的一个实验，由发明概念“正式的非本质规范”。¹事实上，我们许多人首先提到了这样的规格作为“Parnas规范”，但他让它知道（通过Peter Neumann）他不赞成。Parnas的实验是一个小型课堂实验，旨在调查，而不是验证正式规格的效果，而是说明规范确定实施的合理思想。Parnas’ classroom experiment, in which several groups were given the same specification to implement, disproved that (or at least cast doubt on that) because different groups implemented their specified task in very different ways, despite the very detailed constraints on input-output behavior in the specification. (I heard the experiment described at a conference presentation by Parnas, but I can’t find the paper or the citation now.)

这一结果对我来说是有用的几年后，当DoD赞助商认为，分析安全内核的正式规范应该是比程序本身的分析，即使分析证明没有访问控制违规和存储渠道，因为该规范允许读者推断执行的实施功能，这些功能会告诉他们关于时间和其他频道。我指出，Parnas已经给出了他们的恐惧没有合理的证据。

正式方法的一个指标，特别是模型检查的一个指标，是它在CPU的设计中经常使用，这具有相当复杂的内部策略来管理内存和注册缓存。（用快速谷歌找到一个引文来确认这是“英特尔的十五年正式财产核查“，凭借Intel Research Pittsbu金宝博娱乐rgh的Imor Fix，在2008年出版的Springer-Verlag书中，25年的模型检查。）

卢基: You also wrote that “Computer scientists can help by developing powerful general-purpose tools and techniques… [e.g.] verification tools and model checkers, as well as encryption algorithms and applications… Development of these tools deserve decades of research building on prior work, and those who are capable of conducting this activity successfully should be encouraged and supported.”

您希望收到更多的外部发展人才和资金的软件系统安全或安全工具的一些具体例子是什么？金宝博官方例如。概率模型 - 检查员或验证的程序综合图书馆，或者您认为最紧急或不足的任何内容。

乔纳森：我的肠道反应是上述所有内容。涉及特定工具时，我们每个人都有基于我们所需要的，我们使用的是什么，以及最可访问的偏好。当我在Sri International时，我使用了PVS定理箴言，后来，斯里的SAL环境，举办了多种模型检查算法。这两者都受益于最高的人才;挑战是，工作从未完成，特别是如果它是一个繁荣的，使用过错的系统。金宝博官方资金来源通常强调紧急申请或全新的想法，因为它们应该忽略了保持软件套件了解硬件，操作系统，算法的演变所需的稳定，不宣传的作品，所以金宝博官方上。即使有强大的用户社区，支持正式方法的工具也没有与Windows，Apple的OS X和其他商业系统的收入相同的机会。金宝博官方

顺便提一下，虽然我已经强调了通用工具，但这并不意味着我是针对专为特定应用而设计的工具，如安全性。毕竟，我在协议安全分析仪（称为约束求解器）上花了很少的时间。然而，专业工具，以简洁度和可读性的利益，从具有强大的基元的表现力语言构建 - 对于我的申请，Prolog，特别是SWI-Prolog。

但是：谨慎一句话：在它下面构建分析工具的分析工具是一件事，另一方面是另一方面建立一种据说安全的系统。金宝博官方从学习隐蔽频道中学到的一课是安全界面下的整个系统是潜在的漏洞来源。金宝博官方那么我们如何构建安全系统？金宝博官方我认为，主要要求，很简单：不要让敌人编程你的电脑（持有数据的电脑）。但我们怎样才能防止这一点？这是艰难的部分。

卢基：谢谢，乔纳森！

1. Parnas（1972）。↩