乔纳森·米伦报道

路加福音Muehlhauser当前位置由于您是隐蔽信道通信领域相对较早的研究人员，我想问您关于该领域的亚博体育官网早期，通常被认为是始于兰普森(1973)．你知道第一次隐蔽信道攻击是什么时候“在野外”被发现的吗?我的印象是兰普森发现了几个普遍问题几十年在它被发现在野外被利用之前;是这样吗?

乔纳森•米伦:我们可能永远不会知道真正的隐蔽信道攻击是什么时候第一次被注意到，或者什么时候第一次发生。当信息被隐蔽通道窃取时，原始数据仍然存在，因此窃取行为不会引起注意。即使袭击被发现，受害者和施暴者一样不愿承认。对于机密信息来说，这当然是一种情况，因为已知的攻击通常比它所危害的信息的级别要高。我所掌握的1999年之前的真正攻击的唯一证据来自于Robert Morris(资深)，他是UNIX安全领域的先驱，曾有一段时间是国家计算机安全中心的首席科学家，该中心在组织上隶属于NSA。他在一个安全研讨会上说，确实发生过袭击。他什么也不说了;这么多钱可能很难获得许可。

路加福音:从您自己的角度来看，自您写了“隐蔽信道通信”之后，最有趣的发展是什么?20年的隐蔽通道建模和分析“1999年?

乔纳森这是一个很难回答的问题，有几个原因。像许多已经存在多年的亚博体育官网研究领域一样，隐蔽信道研究已经分裂成几个专业。其中的一些子主题是无干扰模型、通过类型理论的基于语言的信息控制、隐写术等。

虽然专业化是深入发展的必要条件，但我希望更多地关注关于隐蔽渠道的务实的“那又怎样”问题。例如，信息流安全通常定义为不干涉，但不幸的是，可以通过几种微妙不同的方式来定义它。它们都依赖于某种形式的行为等价性，这是一个强有力的条件，保证未经授权的观察者无法知道何时有更有特权的用户出现。关于被保护方的数据或行为，哪怕是一点点或一点点的信息，都被认为是太多了。然而，我们真正想知道的是，是否可以建立一个循环信道，产生大量或无限数量的信息。此外，香农意义上的信息可能有用，也可能没用。其中一篇论文引起了我的注意用信念量化信息流，因为它处理的是信息的准确性。

另一个务实的问题是系统功能的可信性。亚博体育苹果app官方下载一般来说，我不相信依赖于访问控制软件或其编写语言设计的安全方法。即使是操作系统内核以下的固件和硬件也是可疑的。亚博体育苹果app官方下载在过去的几年里,我的主要研究兴趣是在可信计算,作为支持可信平台亚博体育官网模块,功能可用,但很大程度上未使用在现代平台——密码地检查系统软件的完整性的引导序列从防伪TPM。亚博体育苹果app官方下载而且，这样做之后，我们只知道系统软件是真实的，而不是它是正确的或不受隐蔽渠道的影响。亚博体育苹果app官方下载令人鼓舞的是，在软件和硬件验证方面的工作仍在继续，但常用的系统仍超出其能力范围。亚博体育苹果app官方下载

复杂性是安全的敌人。您必须依赖的越多，就越不可能很好地理解它以排除漏洞。一些推论:您的安全策略越复杂，它的健壮性就越差，因为它需要更复杂的软件。支持安全性的系统组件越专门化，它作为攻击目标的吸引力就亚博体育苹果app官方下载越大。我认为乐观的观点是，如果我们使用一个典型的复杂的现代系统，隐蔽通道是我们最不需要担心的!亚博体育苹果app官方下载

路加福音:从你几十年的计算机安全经验来看，你是否知道这样的情况，有人担心计算机安全或安全挑战，虽然不是迫在眉睫，但可能是在一到二十年后，他们决定开始做研究，准备迎接这个挑战-亚博体育官网例如，也许是因为他们认为解决方案需要10年或20年的“连续”研究和/或工程工作，每一块都是在它之前的基础上建立起来的，他们希望准备好迎接即将到来的挑战?亚博体育官网在我看来，兰普森对“限制问题”的早期识别可能就是这样一个例子，但也许我误解了历史。

乔纳森:在计算机安全领域，通常发生的情况是，有人意识到一个漏洞已经存在，但不清楚需要多长时间，恶意方就会利用它。推迟相关研究和开发开始的另一个因素是，旨在消除漏洞的长期努力是有风险的，其结果可能不充分或在亚博体育官网未来因不同的问题而黯然失色。

如果困难是社会性的，比如更新标准，那么困难是真实存在的，但是基本的工程知识在早期就已经存在了。例如,TCP序列号为会话劫持攻击1985年被莫里斯指出,利用由米特尼克在1995年1996年导致Bellovin标准建议,直到最近的可用性加密认证和IPv6带来了广泛的解决方案触手可及。

如果困难是在工程上，比如开发安全内核和击败特洛伊木马的强制访问策略，或者安装和使用tpm，那么就需要转移一个行业，一个由新产品的商业可行性需求驱动的行业。在所有这些努力之后，一些弱点仍然存在。

计算机科学家可以通过开发具有基本计算机科学目标的功能强大的通用工具和技术来提供帮助——这些工具不依赖于问题。这里，我指的是验证工具和模型检查器，以及加密算法和应用程序。当新问题和设计想法出现时，这些工具可以减轻工程负担。这些工具的开发需要在以前的工作基础上进行几十年的研究，应该鼓励和支持那些有能力成功开展这一活亚博体育官网动的人。

路加福音您提到了验证工具和模型检查器。最近，我与计算机安全和安全领域的一位重要人物(我不知道她的名字)谈论了一种普遍的说法，即正式的方法可以捕获那些仅通过测试不太可能捕获的角落漏洞。她提到，如果正式方法社区曾经让正式方法进行仔细的实验，以证明验证确实能够捕获测试不太可能发现的bug，她并不知道这一点。你是否知道有类似的示威活动?如果没有，怎么能你描述为安全和保障目的的正式方法的价值?

乔纳森在我看来，要求通过仔细的实验来证明正式方法与测试相比较是不公平的。当正式的方法被推荐用于安全内核验证时，其中一个原因被指出，那就是很少有安全内核被真正开发出来，所以任何实验结果在统计上都没有意义。

David Parnas在正式规范历史的初期做了一个实验，他被一些人认为发明了“正式非程序规范”的概念。¹事实上，我们很多人一开始把这种规范称为“帕纳斯规范”，但他(通过Peter Neumann)让大家知道他不赞成这种做法。Parnas的实验是一个小型课堂实验，目的不是调查正式规范验证的有效性，而是调查规范决定实现的似是而非的想法。在帕纳斯的课堂实验中，几个小组被要求执行相同的规范，这证明了这一点(或至少引起了怀疑)，因为不同的小组以非常不同的方式执行他们指定的任务，尽管规范中对输入-输出行为有非常详细的限制。(我在帕纳斯的一次会议报告中听到了这个实验的描述，但我现在找不到论文或引文了。)

几年之后，这个结果对我很有用，因为国防部的赞助人认为，对安全内核的正式规范的分析应该比程序本身的分类更高，即使分析证明没有违反访问控制和存储通道，因为规范允许读者推断实现的特性，这些特性将告诉他们有关时间和其他通道的信息。我指出，帕纳斯提供的证据表明，他们的担心是没有道理的。

形式化方法(特别是模型检查)的价值的一个指标是，它在cpu的设计中经常被使用，cpu有相当复杂的内部策略来管理内存和寄存器缓存。(我找到了一个引用，用一个快速的谷歌来确认这是“在英特尔做了十五年的正式财产验证，由英特尔匹兹堡研究所的Limor Fix在2008亚博体育官网年出版的斯普林格-弗拉格出版社的书中写道，25年的模型检验．)

路加福音:您还写道:“计算机科学家可以通过开发强大的通用工具和技术来提供帮助……[例如]验证工具和模型检查器，以及加密算法和应用程序……开发这些工具需要在之前的工作基础上进行数十年的研究，亚博体育官网那些有能力成功开展这项活动的人应该受到鼓励和支持。”

您希望获得比当前更多的开发人才和资金的软件系统安全或安全工具的一些具体例子是什么?亚博体育苹果app官方下载例如，概率模型检查器，或用于程序合成的验证库，或任何您认为最紧迫或资金不足的东西。

乔纳森我的本能反应是，以上都是。当谈到特定的工具时，我们每个人都有自己的偏好，基于我们需要什么，我们使用过什么，以及什么是最容易获得的。当我在SRI国际时，我使用了PVS定理证明程序，后来又使用了SRI的SAL环境，其中包含了几种类型的模型检查算法。这两者都得益于最高水平的人才;挑战在于，这项工作永远不会完成，尤其是如果它是一个蓬勃发展、被充分利用的系统。亚博体育苹果app官方下载资金来源通常强调紧急的应用程序或全新的想法，这是他们应该做的，但他们往往忽略了保持软件套件与硬件、操作系统、算法发展等相关的最新进展所需的稳定、不浪漫的工作。亚博体育苹果app官方下载支持正式方法的工具并不像Windows、苹果的OS X和其他商业系统那样有同样的收入机会，即使拥有强大的用户社区。亚博体育苹果app官方下载

顺便说一下，虽然我强调了通用工具，但这并不意味着我反对为特定应用程序(如安全性)设计的工具。毕竟，我在协议安全分析器(称为约束求解器)上花了相当多的时间。然而，专门的工具由于构建在具有强大原语的表达性语言的基础上(对于我的应用程序Prolog，特别是SWI-Prolog)，因此在简洁性和可读性方面受益颇多。

不过，需要注意的是:构建一个具有复杂系统的分析工具是一回事，以这种方式构建一个假定安全的系统是另一回事。亚博体育苹果app官方下载从研究隐蔽通道中得到的教训是，安全接口下的整个系统是漏洞的潜在来源。亚博体育苹果app官方下载那么我们如何建立安全的系统呢?亚博体育苹果app官方下载我认为主要的要求很简单:不要让敌人给你的电脑(存放你数据的电脑)编程。但是我们怎样才能防止这种情况发生呢?这是最难的部分。

路加福音:谢谢,乔纳森!

1. 帕尔曼党注册(1972)．↩