麻省理工学院。 讲座课程＃6.858。 “计算机系统的安全性。” Nikolai Zeldovich，James Mickens。 2014年
计算机系统安全是一门有关开发和实施安全计算机系统的课程。 讲座涵盖了威胁模型，危害安全性的攻击以及基于最新科学研究的安全技术。 主题包括操作系统（OS）安全性，功能，信息流管理，语言安全性，网络协议，硬件安全性和Web应用程序安全性。
第1课：“简介：威胁模型”
第1 部分 /
第2 部分 /
第3部分第2课：“控制黑客攻击”，
第1 部分 /
第2 部分 /
第3部分第3讲：“缓冲区溢出：漏洞利用和保护”
第1 部分 /
第2 部分 /
第3部分讲座4：“特权分离”，
第1 部分 /
第2 部分 /
第3部分讲座5：“安全系统从何而来？”
第1 部分 /
第2部分讲座6：“机会”
第1 部分 /
第2 部分 /
第3部分讲座7：“本地客户端沙箱”
第1 部分 /
第2 部分 /
第3部分讲座8：“网络安全模型”
第1 部分 /
第2 部分 /
第3部分讲座9：“ Web应用程序安全性”
第1 部分 /
第2 部分 /
第3部分讲座10：“符号执行”
第1 部分 /
第2 部分 /
第3部分 大家早上好，我是Armando Solar-Lesam，今天我将做有关象征性表演的演讲。 在座的这些人中谁最熟悉这个词或曾经听说过这个词？ 我只想了解我们的听众。 因此，让我们开始吧。 我掉了好几次笔记本电脑，所以加载时间很长。
符号执行是现代程序分析的主力军。 这是一种起源于研究的方法，然后开始在许多应用中使用。 例如，今天在Microsoft，有一个名为SAGE的系统，它可以与许多重要的Microsoft软件一起使用，从Power Point到Windows本身，以真正发现安全问题和漏洞。
有许多学术项目对现实世界产生了重大影响，例如使用符号执行来检测开源软件中的重要错误。 符号执行作为一种技术的美丽之处在于，与测试相比，它使您有机会想象程序在潜在的可能的无限输入数据集中将如何运行。 这使我们能够研究输入数据的数组，即使存在大量的测试人员，这对于通过随机测试进行研究也是完全不切实际和不切实际的。 另一方面，与更传统的静态分析方法相比，它具有以下优点。 在调查问题时，符号执行可以创建输入和跟踪，可以在真实程序中运行并基于此输入运行该程序的执行路径。 然后，我们可以确定真正的错误，并使用传统的调试机制开始对其进行修复。 当您在工业开发环境中可能没有时间去处理代码中的每个小问题时，这特别有价值。
例如，您确实希望能够区分实际问题和误报。 如何运作？
要真正了解它是如何工作的，从正常执行开始很有用。 如果我们将符号执行视为对传统的简单执行的概括，那么了解它的外观就很有意义。 因此，我将使用这个非常简单的程序来说明我们今天要谈论的许多事情。
在这里，我们摘录了几个分支中的一个非常简单的代码，并声明了，如果在某些条件下，值t <x，则这是一个错误的语句。 我们想找出是否可以提出这一说法。 有可能吗 是否有任何输入会使该语句失败？
我可以做的一件事是使用输入数据的特定值来检查该程序的执行情况。 假设我们使用X = 4和Y = 4的输入。如程序开始时所宣布的，T的值为零。
因此，在我们开始正常执行之前，让我们先了解这里的重点。 我们需要对程序的状态有所了解，对吗？ 无论是执行常规执行还是执行符号执行，我们都需要某种方法来表征程序的状态。 在这种情况下，它是一个简单的程序，它不使用堆，不使用堆栈，并且这里没有函数调用。
因此，状态可以通过这三个变量以及知道我在程序中的位置来充分表征。 因此，如果我从4、4和0开始执行并到达分支的末尾，那么我将检查表达式：4大于4？ 显然不是。
现在，我将在T = Y处执行程序，即T不再为0，而是值为4。这是程序的当前状态，现在我可以评估该分支。
T <X是真的吗？ 不行 我们躲开了子弹，虚假的陈述没有用。 在这个私人执行中没有问题。
但这并没有告诉我们任何其他执行方式。 我们知道，当值X = 4和Y = 4时，程序将不会失败。 但是，这并不能告诉我们如果输入值为2和1会发生什么。
使用这些输入值，执行将以不同的方式进行。 这次我们看到T = X，在执行此行之后，T将取等于2的值。此执行中是否有任何问题？ 这样的输入会出现断言错误吗？
好吧，让我们看看。 因此，如果T为2并且X为2，则T不小于X。看来我们再次躲过了子弹。 对不对 因此，这里有两个特定的输入值，程序可以在这些输入值下正常运行。 但是实际上，它并没有告诉我们任何其他输入值。
因此，符号执行的思想是我们要超越具有一组输入数据的程序的执行。 我们希望能够在使用非常大的数据集（在某些情况下，使用无限数量的可能的输入值）时真正谈论程序的行为。 其主要思想如下。
对于这样的程序，其状态由以下三个不同变量的值确定：X，Y和T，并知道我当前在程序中的位置。 但是现在，除了X和Y的特定值之外，我还有一个符号值，只是一个变量。 一个允许我命名该值的变量，用户将其用作输入。 这意味着程序状态不再通过将变量名与特定值匹配来表征。 现在，这是变量名到这些符号值的映射。
可以将符号值视为公式。 在这种情况下，X的公式等于X，Y的公式只是Y，而T的公式实际上等于0。我们知道对于每个输入值，您所做的都无关紧要。 第一条语句之后的T的值为0。
那就是现在变得有趣的地方。 我们到达了这个分支，它说如果X大于Y，我们将朝一个方向前进。 如果X小于或等于Y，我们将朝另一个方向前进。
我们对X和Y有什么了解吗？ 我们对他们了解什么？ 至少我们知道它们的类型，我们知道它们在min int和max int之间会有所不同，但这就是我们所了解的全部。 事实证明，我们所知的信息不足以说明该分支机构的发展方向。 她可以往任何方向走
我们可以做很多事情，但是目前我们能做什么？ 尝试做出最疯狂的猜测。
受众：我们可以在两个分支上跟踪程序的执行情况。
教授：是的，我们可以跟踪两个分支的进度。 翻转硬币，然后根据跌落的方式选择一个或另一个分支。
因此，如果我们要遵循两个分支，则必须首先遵循一个，然后再遵循另一个，对吗？ 假设我们从这个分支开始-T =X。 我们知道，如果到达这个位置，T将与X具有相同的含义。我们不知道该值是什么，但是我们有一个名称-这就是脚本X。
如果我们走相反的分支，那会发生什么？ T的值等于其他值，对吧？ 在此分支中，T的值将为Y的符号值。
那么，当我们到达程序中的这一点时，这个T值意味着什么？ 也许是X，也许是Y。我们不确切知道这个值是什么，但是为什么不给它起个名字呢？ 称它为t
0 。 关于t
0，我们知道什么？ 在什么情况下，t
0等于X？
本质上，我们知道如果X大于Y，则变量等于X，如果X小于或等于Y，则变量等于Y。因此，我们定义了一个值，将其称为t
0 ，并具有逻辑属性。
因此，在程序的这一点上，我们为T的值命名，即t
0 。 我们在这里做了什么？ 我们使用了if语句的两个分支，然后计算了符号值，看看在什么条件下将执行程序的一个分支，并在另一个条件下执行该分支。
现在到了应该问T是否可以小于X的地步了。现在T的值是t
0 ，我们想知道t
0是否可以小于X？ 记住我们检查的第一个分支-我们询问了有关X和Y的问题，但对它们一无所知，只是它们的类型为int。
但是有了t
0 ，我们对此确实了解很多。 我们知道在某些情况下它将等于X，在某些情况下将等于Y。因此，现在它给我们提供了一组可以求解的方程式。 那么，知道t
0满足所有这些条件，我们可以说t
0是否小于X。 因此，我们可以将此表示为一个限制，表明t
0是否可能小于X。如果X大于Y，则t
0等于X，如果X小于或等于Y，则意味着t
0 =是的
所以我们有一个方程。 如果有解决方案，则有可能找到满足该方程的t
0值，X值和Y值，则我们将识别出这些值，并将它们输入程序中，然后在执行时，如果t <x和“当断言为false时将爆炸。
那么我们在这里做了什么？ 我们执行了该程序，但没有将变量名映射到特定值，而是给这些变量名提供了符号值。 实际上，他们给了他们其他变量名称。 在这种情况下，我们的其他变量名称是脚本X，脚本Y，t
0 ，此外，我们还有一组方程式，显示这些值之间的关系。 我们有一个方程式，告诉我们在这种情况下t
0与X和Y之间的关系。
这个方程的解使我们能够回答这个分支是否可以执行的问题。 看一下等式-是否可以采用此分支？ 似乎不是，因为我们正在寻找t
0小于X的情况，但是如果在第一个条件下t
0 = X，则表达式t
0 <X将不成立。
因此，这意味着当X> Y时，这不会发生，因为t
0 = X且它不能同时等于或小于X。
但是，如果t
0 = Y会怎样？ 在这种情况下，t
0可以小于X吗？
不，它绝对不能，因为我们知道X <Y。因此，如果t
0小于X，那么它也将小于Y。但是我们知道在这种情况下t
0 =Y。 ，此条件无法满足。 因此，这里我们有一个没有解的方程式，在方程式中包含什么值都没有关系。
您无法解决它，这告诉我们，无论我们将什么输入X和Y传递给程序，如果t <x，它都不会向下跳转。
现在请注意，在此处创建此参数时，我基本上暗示了您对整数，数学整数的直觉。 在实践中，我们知道机器整数的行为并不完全像数学整数那样。 在某些情况下，适用于数学整数数据类型的定律不适用于程序化int。
因此，在求解这些方程式时，我们必须非常小心，因为我们必须记住，这些不是我们在小学中学到的整数。 这些是机器使用的32位整数。 发生错误的原因很多，因为程序员是用数学整数来考虑代码的，而不是意识到诸如溢出之类的事情会导致数学输入的不同程序行为。
我在这里描述的另一件事是一个纯粹的直观论证。 我将指导您完成该过程，并演示如何手动进行，但这绝不是算法。 但是，这种符号执行概念的优点在于可以将其编码为算法。 而且您可以机械地解决它，这不仅使您可以针对10行程序，而且可以针对数百万个程序执行此操作。 这使我们能够使用与本例相同的直观推理，并讨论使用不同输入值运行该程序时会发生什么。 这些考虑因素可以扩展并扩展到非常大的程序。
受众：如果程序不支持某种类型的变量的输入，该怎么办？
教授：这是一个很好的问题！ 假设我们有相同的程序，但不是t = x，而是t =（x-1）。 然后，凭直觉，我们可以想象现在该程序可以“爆炸”了，对吧？
因为当程序以这种方式运行时，t实际上将小于x。 这样的程序会怎样？ 我们的符号状态将是什么样？ 当x大于y时t
0将是什么？ 当t =（x-1）时，我们根据另一个值校正方程中的线。 现在程序可能会失败，然后您去找开发人员并告诉他：“嘿，当x大于y时，此函数可能会爆炸”！
开发人员看了看后说：“哦，我忘了告诉你-实际上，永远不会使用参数调用此函数，而x大于y。 “由于某些历史原因，我只是写了它，所以不用担心，如果您不告诉我，我将不会记住它。”
假设我们假设x小于或等于y。
这是我们履行职能的前提或协议。 该函数承诺会做某事，但前提是该值满足此假设。 但是，如果不满意，该函数会说：“我不在乎会发生什么。 我保证，只有满足这一假设，才会有任何错误。”
那么，当我们求解方程式时，我们如何编码该约束？ 本质上，我们有一组约束告诉我们该分支是否可行。 除限制外，我们还必须确保满足先决条件或假设。
问题是，我是否可以找到满足所有这些限制并同时具有所需属性的x和y？ 您可以看到，此限制X≤Y表示满足此限制的情况与不满足此条件的情况之差。
在进行分析时，这是一个非常重要的问题，尤其是当您要在单个功能级别同时进行时。 建议您在编写此函数时了解程序员的想法。 因为如果您对这些假设一无所知，您可能会认为有一些输入会使程序失败。
如何以机械方式做到这一点？ 这个问题有两个方面。 第一方面-您实际上是如何提出这些公式的？
在这种情况下，直观上很清楚我们是如何得出这些公式的，我们只需手动对其进行组合即可。 但是如何机械地创建这些公式？
第二个方面-拥有这些公式后如何解决？ 是否有可能真正解决这些描述程序是否崩溃的公式？
让我们从第二个问题开始。 我们可以使用这些公式来减少问题，这些公式包括整数推理和位向量。 创建程序时，您需要照顾数组，函数，因此，您会得到庞大的公式。 是否可以机械地解决它们？
我们今天谈论的许多技术都是实用的工具，与开发逻辑问题求解器的巨大进步有关。 特别是，有一类非常重要的求解器，称为SMT，或“模块化理论的可求解器”。 SMT求解器是考虑了逻辑公式基础的逻辑公式的可解性。
许多人声称此名称不是特别好，但已被固定为最常用的名称。
SMT求解器是一种算法，由于该算法，输出端的此逻辑公式将为您提供以下两种选择之一：它满足其目的或不满足。 , , .
. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».
, , , , : « ». , , .
27:30
MIT « ». 10: « », 2该课程的完整版本可
在此处获得 。
, . ? ? ,
30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB DDR4).
VPS（KVM）E5-2650 v4（6核）10GB DDR4 240GB SSD 1Gbps至12月免费，在六个月内付款，您可以
在此处订购。
Dell R730xd 2 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?