Greg Morrisett.是哈佛大学计算机科学计算机科学教授的艾伦B.。他收到了他的B.。1989年里士满大学数学与计算机科学，及其博士学位。来自1995年的卡内基梅隆。1996年，他在康奈尔大学举行了立场，在2003年至04年学年，他休假并访问了微软欧洲研究实验室。亚博体育官网2004年，他搬到了哈佛，他曾担任计算机科学和工程的副院长，他目前正在担任哈佛大学的计算和社会研究。亚博体育官网
Morrisett为他的编程语言，型系统和软件安全性的研究获得了许多奖项，包括科学家和工程师的总统早亚博体育官网期职业奖，IBM教师奖学金，NSF职业奖和Alfred P. Slo亚博体育苹果app官方下载an奖学金。
他担任职能编程杂志的首席编辑，也是编程语言和系统和信息处理字母上的ACM交易的助理编辑。亚博体育苹果app官方下载他目前为委员会的编辑委员会担任ACM期刊，作为研究的联合主编，突出了ACM的通信专栏。亚博体育官网此外，Morrisett还致力于DARPA信息科学和技术研究（ISAT）集团，NSF计算机和信息科学和工程（CISE）咨询委员会，Microsoft Research的技术咨询委员会和微软的Trusthworthy计算学术咨询委员会。亚博体育官网
卢克·穆罕沃斯： 其中一个有趣的项目你所涉及的是安全的，DARPA资助的项目“专注于清洁的板岩设计，适合弹性和安全系统。”亚博体育苹果app官方下载这个项目的动机是什么，特别是它的“清洁石板”方法？
Greg Morrisett.：我认为从DARPA的角度来看，主要的力量是我们在保护系统方面所做的事情是不起作用的。亚博体育苹果app官方下载我怀疑来自国家和其他组织的成功攻击的一些高调问题使他们绝望地尝试新的和不同的东西。
与此同时，遗产软件（和潜在的硬件）越来越高兴是问题的重要组成部分。例如，如果我们所有的关键软件都以类型安全的语言编码，那么大量的低级问题（例如，缓冲区溢出）将会消失。所以我认为这是整个崩溃计划背后的思考，有20个不同的团队尝试了一系列想法。
我们的特定项目（安全）采取了非常激进的方法，希望重新思考一切：语言，操作系统，甚至硬件，以及强调正式试图获得一些保证的方法。亚博体育苹果app官方下载The team has designed some very interesting hardware that (a) effectively enforces type-safety at the machine level (i.e., object-level integrity, pointers as capabilities, etc.), and (b) provides novel support for doing fine-grained end-to-end information flow tracking. We’ve also designed a high-level, dynamically-typed language (Breeze) that has pervasive information flow tracking built in. This means that we can tell which principal actors may have influenced the construction of any value in the system. We’re now building compiler support for Breeze and systems-level software (e.g., scheduler, garbage collector, etc.) to bridge the high-level code and the hardware.
与此同时，我们一直试图应用正式的模型和推理，以便证明系统模型的关键属性。亚博体育苹果app官方下载例如，我们已经从一开始就拥有机器检查的（核心）语言的安全证明，并且当前正在构建硬件的核心模型，并尝试建立类似的属性。
卢基：你能解释一下，最好用例子，你的意思是“机器级别的类型安全”和“细粒度的端到端信息流跟踪”？
格雷格：因此，让我们首先从“类型安全”开始。在此上下文中，我简单意味着我们在内存中的不同值之间进行区分，并且机器只允许适当的操作应用于适当的值。例如，我们在指向对象（给定大小）和整数之间的指针之间的区别，并且该计算机仅允许您相对于指针加载/存储（以及它在其指向的对象的范围内）。如果您尝试相对于整数加载/存储，它将陷阱。同样，我们区分了对代码和数据的引用，因此您只允许跳转或呼叫对代码的引用，而不是数据。这些基本的完整性属性阻止了依赖于违反抽象的一系列基本攻击（例如，代码注入，缓冲区溢出等）
With respect to “information flow control” (IFC): we want to enforce policies like “unauthorized principal actors, say a web site with whom I’m communicating, should never learn my private information, say my users’ social security number of password”. The hard part is the “learn no information” as opposed to literally passing the data. If, for instance, I reverse your password and send it out, or take every other letter from your password, we want those to be seen as violations as well as explicitly copying the data. (There are much more subtle ways to communicate information as well.)
正式，我们的目标是，如果我将密码更改为任意字符串，则“未经授权的主要参与者”的观察应该是相同的。技术术语是“不干涉”。
我们实现IFC的方式是通过用信息流控制策略标记每条数据。组合两条数据（例如添加两个数字）时，我们有用于计算新策略的规则，以便在新生成的值上放置。例如，如果添加“秘密”和“公共”号码，则结果保守归类为“秘密”。
卢基： 在一个博客文章，我警告读者在安全或安全保障的100％保证的情况下，没亚博体育苹果app官方下载有系统是“可证明的安全”或“可被证明的安全”，因为例如。安全/安全定义可能会巧妙错误，或者特定的安全减少可能会有错误。这些事情发生了。我说“相反，这些方法意味着提供比我们更有信心，否则相同，给定的系统是安全的[或安全]亚博体育苹果app官方下载。“
您是否同意这种特征？而且，在术语问题上：您认为术语与“可证明的安全”和“可怕的安全”是过于误导的，或者他们只是专家常规术语的另一个不可避免的例子，通常但不可避免地被非专家错误地解释了？
格雷格：是的，我完全同意你的博客帖子！系统的所有“正确性证明”将受到建模环境，并指定我们的意思是正确的。亚博体育苹果app官方下载对于真实的系统，建亚博体育苹果app官方下载模永远不会是足够的，并且正规化正确性的概念可能像重新实现系统一样复杂。
我确实认为建立环境的明确模型，并撰写正式规格并构建正式证明具有很多价值。如您所知，它确实有助于增加信心。并且，它有助于识别假设。很多次，攻击者会看看你的假设，并试图违反他们获得购买。因此，通过建模识别假设是一个很好的运动。
经历正式证明的过程也会导致很多良好的建筑洞察力。例如，当我们试图为谷歌的本土客户端检查器构建正确性证明时，我们意识到我们手头的工具会太难。所以我们提出了一种更简单的算法和架构，这更容易证明正确。它也结果更快！这在技术文件中详述：Rocksalt：更好，更快，SFI更强大的X86。
最后，所有这些都是在设计中爬行复杂性的巨大推动力。我认为出现了很多问题，因为软件是如此柔软，我们编写了很多代码而不深入思考它应该（不）做什么。
回到您的问题，以及我们是否应该使用“可证实安全”一词：可能不是。我想使用“认证代码”一词，因为我们正在经历一个非常严格的认证过程。但遗憾的是，“认证”一词表示意味着我们遵循一些官僚的开发过程，实际上并不是安全的安全或可靠性。所以我向更好的术语开放了建议。
卢基：哈珀（2000）引号旧消息由肯·弗里斯到了安全关键邮件列表：
认为必须将正式证明应用于智能系统让我感冒。亚博体育苹果app官方下载如何为在持续学习过程中有能力改变自己的东西提供满意的保证？
您如何考虑将正式方法应用于越来越聪明，自治系统的机会和限制？亚博体育苹果app官方下载
格雷格：我会诚实地说，我还没有想到这一点。也许我正在努力的最接近的事情正在尝试为加密方案进行信息 - 理论上的安全性，并在该设置中构建正式证明。这是一个我认为加密/理论界提供足够的结构，我们可以希望取得进步，但即使在这里，我们在基础上都有各种各样的摇摇欲坠的假设。
我怀疑，对于智能和自主系统的工作（特别是在网络物理领域），第一个真正的挑战是构建适当的模型，亚博体育苹果app官方下载这些模型是潜在的失败模式的过度逼近，并尝试找到易于与之合作的东西，类似加密尝试模型对手的方式。
卢基：一般来说，对于需要满足高标准的安全亚博体育苹果app官方下载性的系统，您认为我们认为我们可以采取最多是设计的现有系统有效的和“螺栓安全到它们上”，而且需要从地上建造东西以安全？也许一些具体的例子通知你的观点？
格雷格：我认为重新架构和重新编码的东西几乎总是在与螺栓接近相比的安全方面取胜。一个很好的例子是qmail.这被设计为Sendmail的安全替代品，并且相比之下，具有良好的架构，使最容易获得大多数事情，包括尤其是配置。据我所知，Qmail（一个整数溢出）只有一个错误，可能会导致安全问题，而有许多问题与sendmail（我丢失了计数。）
但是，最终，安全性是几乎所有系统的次要考虑因素。亚博体育苹果app官方下载尽管我希望我们可以丢弃所有的代码，并花时间重新建立时间并重新编码大量的东西（特别是使用更好的语言技术），它太贵了。例如，Windows XP超过5000万行代码（我不知道Win7或Win8有多大），所以重新编码Windows不是一个现实的可能性。
我们所需要的是人们现在可以购买的工具和技巧，并帮助阻止遗留系统问题。亚博体育苹果app官方下载理想情况下，这些同样的工具应该给你一个“支付你的付费”的物业：一点努力为你买了一些保证，而且更多的努力给你买了更多。
一个很好的例子是我们开始查看遗留C / C ++代码的静态分析工具，例如覆盖物，HP / Fortify或Microsoft的Preamet / Prefix / Slam /等。这些是自动识别潜在错误的工具，反过来可能导致漏洞。今天，如果您在随机堆的C / C ++代码上运行这些工具，您会发现它提供了许多误报。但如果你努力尽量减少那些警告，那么你会发现该工具变得更加有效。而且，对于新的代码，它可以很好地工作，只要你注意警告和工作来摆脱它们。
卢基：谢谢，格雷格！
你喜欢这篇文章吗？你可以享受我们的其他谈话帖子，包括：
