麻省理工学院。 讲座课程＃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部分 受众：似乎您尚未谈论如何使用位来存储整数int。
教授：这是一个很好的问题。 确实与您如何定义限制有关，对吗？ 因此，如果从一开始就看一下我们的简单示例，就会发现我们假设我们在小学学习的整数存在。 同时，我们完全决定忽略溢出错误。 如果您关心溢出错误，并且对于您而言重要的是没有此类错误，那么使用数学上的整数将无助于解决问题。
您需要的不是将这些数量表示为整数，而是表示为位向量。 当将它们表示为位向量时，应使用更广泛的视图。 在这里，我们回到SMT求解器。 模块化理论的一个方面是，求解器本身可以使用不同的理论进行扩展。
最受欢迎的理论是固定长度位向量理论。 这意味着，如果您在固定长度位向量的理论中解释公式，则必须首先设置位向量的长度。 也就是说，必须明确指出将用于32位长，8位或64位的位向量。
还有另一种理论称为TOA阵列理论。 我们将讨论更多。 与针对固定长度的事物设计的位向量理论不同，数组理论旨在用于大小事先未知的集合。
现在，实际上，没有人使用数组理论来建模整数，因为它太昂贵了。 当您不知道问题的边界时，谈论问题的代价会更高。 因此，人们通常在讨论整数甚至符号时使用固定长度的位向量理论。
另一个非常普遍的理论是实整数算法，尤其是线性整数算法。
人们非常喜欢这种理论，因为它提供了有效的论据，但是在谈论程序时并不太好，因为在这里您真正关心的是溢出问题。 但是，该理论已广泛用于许多事物。
经常使用的另一种理论是未解释函数的理论。 这个理论是什么意思？
这意味着您具有一定的公式。 在此公式中，您知道自己正在调用一个函数，但是对该函数一无所知，除了以下事实：如果在其中插入一些输入，您将获得相同的输出。
事实证明，这在使用诸如浮点代码，建模，正弦，余弦，平方根之类的事物进行推理时非常有用。 关于此类事情的详细讨论可能非常耗时且昂贵。 但是使用这种理论，您可以说：“看，我真的不在乎正弦函数的作用。 我不在乎她会给出什么。 我只需要知道，如果我在具有特定输入的程序的各个位置调用正弦函数，我将在输出中获得相同类型的数据。 这对于我来说足以说明我的程序。”
因此，在实际系统分析中，最常见的操作是与整数，对数和指针一起工作的位向量。 实际上，指针通常用整数表示，因为有时您不必在指针上设置位向量。 但是有时您必须这样做，然后您就不能再使用整数了。
因此，我们研究了SMT求解器可以为您做什么。 真正如何运作？ 它们内部有什么使它们起作用？
实际上，SMT求解器依靠我们解决SAT布尔公式的可行性问题的能力，依靠仅考虑与布尔约束和布尔变量有关的问题的能力，并告诉我们是否将确保程序分配分配给这些布尔变量的值。
这是许多年来教给高年级学生的东西，说这实际上是NP完成的任务，并且在某些事情归结为SAT的情况下，您不应该这样做。 但是事实证明，我们实际上有非常好的SAT求解器。
因此，我将告诉您SAT求解器如何工作的基本概念。 这是因为您将所有对布尔变量的限制都放入了数据库中。 您可能看不到屏幕上的小写字母，但这就是我所能做的。
我将在操作过程中对此进行评论和讨论，稍后我将发布幻灯片，以便您可以看到那里写的内容。
因此，在SAT任务中，所有这些变量都代表布尔未知数，对吗？ 我们想知道X是否可能同时为真（X = TRUE），Y是否为真，Z是否为真。 这些是我们的未知数。 而且，所有限制都是正常的合取形式。 这意味着我们所有的限制都采用X1 = true或X2 = true或X3 = true的形式。
在这种形式下，我们具有所有局限性，即X1为true或X2为false或X3为false。 您可能还记得离散数学中的任何布尔公式都可以以常规连接形式表示。 这意味着，用于表示布尔公式的任何表示形式都可以轻松转换为这种格式。
因此，我们的数据库具有这种形式的许多限制。 SAT求解器将随机选择这些变量之一，假设它是X1。 他会说：“为什么不将X1设置为true？ 我对这些限制一无所知，因此我可以假设确实如此。” 然后碰巧您将受到限制，例如，声明X1为假或X7为真。
因此，如果您知道X1为真，并且知道X1为假或X7为真，那么您对X7有什么了解？
听众：一定是真的！
教授：是的，一定是对的。 因为否则将无法满足此限制。 因此，现在您已将该值从X1分配到X7。 现在假设您选择另一个随机变量，例如X5。
现在假设您有一个限制条件：X7为false，或者X6为true，或者X5为false。 因此，我有X5 = true和X7 = true。 这意味着X6现在也应该为true。 因为否则将违反此限制。 因此，系统得出结论：X6应该为真，并继续该过程，执行可用的检查并查看所有可用的报价。 系统检查其检查是否暗含了其他东西。 她遵循这些含义，直到发生两件事之一。
首先是您继续遵循后果并尝试随机的事情，最终为每个变量设置值，而不会遇到矛盾。 所以您做对了所有事情。
第二个-您面对矛盾，然后返回使X4为真的条件，不包括使X4为假的条件。 但是每个人都应该知道布尔代数的一个规则：一个变量不能同时为真和假。
它说您面临一个矛盾，您显然在尝试完成的随机任务之一中做错了什么。
让我们分析这个矛盾，看看导致这种矛盾的任务是什么。 根据导致这一矛盾的任务，让我们提出一个新的冲突条款，以概括这一矛盾。
X1为假，X5为假，X9也为假会发生什么？ 本质上，这是基于我从这些随机分配中学到的，在此期间，我发现其中之一必须是真实的，不可能是X1是真实的，X5是真实的，而X9是错误，这不能。
我知道这是不可能发生的，因为当我尝试这样做时，所有事情都“爆炸”了，我以矛盾结束了程序。
因此，SAT求解器会尝试完成随机任务，并检查它们的运行情况。 当他遇到矛盾时，他分析了导致这些矛盾的一系列后果，并最终形成了新的限制，这确保了求解器不会再遇到这个特定的矛盾，这个特定的问题。
因此，我们可以将SAT解算器想象成一个“黑匣子”，它给出了布尔约束并可以判断它是否令人满意。 SMT求解器建立在最好的SAT求解器之上。 他们可以利用SAT解算器的功能，通过面向主题的支持理论推理来解决NP完全问题。
为了了解其工作原理，假设您有这样一个公式。
可以吗 我们能为她找到满意的考验吗？ SMT求解器可以分离出该公式的一部分，这需要使用整数理论进行推理。 我们使用布尔结构来分隔公式。 因此我们有公式F1，F2，F3和F4。
现在，这是一个纯粹的逻辑布尔任务-我可以为此找到满意的任务吗？ SAT求解器可以说：“是的，通过执行F1 = true，F2 = true和F3 = true，我可以找到一些满足此任务的东西。” 这满足布尔公式的规范。
\
因此，现在有一个问题，我们可以向求解器询问特定区域，在这种情况下，它只是线性算术求解器。 因此，我们可以去理论求解器线性求解器，然后说：“ SAT求解器声明这是一个合理的赋值，并且如果我可以使该赋值起作用，那么我的公式将得到满足。”
我可以说F1是X> 5，F2是Y <5，而F3是Y>X。所以我可以问SAT求解器是否可以得到这样的X和Y，使得X> 5，Y是< 5，在这种情况下，Y将> X？ 现在这是一个纯粹的线性算术问题，没有布尔逻辑。
这个问题的答案是什么？ 不行 无法同时满足这些条件。
因此，存在解决线性问题的传统方法。 例如，您可以使用单纯形法来求解线性不等式系统。 有许多方法可用于求解线性不等式系统。
因此，SAT求解器向理论求解器发送理论问题。 最重要的是，理论求解器求解器知道有关这些问题的所有知识，并且可以准确回答这些条件是否有效。
在这种情况下，理论求解器将处理该请求，发现条件的这种分配不起作用，然后返回SAT求解器并说：“您所做的那些事情将不起作用”！
但是他不只是说是或不是，而是解释了为什么有些东西行不通。 根据这些公式不起作用的事实，理论求解器得出结论：F1，F2和F3不能同时存在，并告诉SAT求解器这三个公式是互斥的。
因此，现在我们有了一些可以返回给SAT解算器的信息，并问他：“嘿，您可以给我一个解决方案，该解决方案不仅要满足我们一开始的约束，而且还要满足Theory发现的新约束。解算器“？
现在满足这些限制的还有其他目的吗？
因此，我们放弃了初始限制X> 5，Y <5，Y> X，这不再困扰我们。
我们可以为我们的理论求解器设置一个新的限制-X> 5，Y <5，Y>2。我们可以使Y等于3，并且X等于6，然后它将起作用。 现在您的任务是在理论上满足公式并满足此目的的布尔结构。 这样，系统可以返回并说：“是的，这是满足您所有限制的任务。” 这是理论求解器和SAT求解器之间的交互。 实际上，这意味着能够谈论非常，非常大和非常复杂的布尔公式。 这就是使符号执行成为可能的原因。
现在，我们将考虑下一个问题-如何从程序过渡到我们可以提供给SMT求解器的限制。
受众：构建SMT求解器NP是否完整？
教授： SMT求解器本质上是一个典型的NP完全问题。 但是，如今，大多数求解器都支持某些完全无法解决的理论。
受众：您如何在系统中解决此问题？
教授：好吧，最后，您将获得此程序的限制。 您将把它提供给SMT求解器。 这些都是NP完成的任务，或者它们不令人满意，这意味着如果幸运的话，您将在几秒钟内收到答复。 但是，如果您不走运，则可能需要比创建宇宙所需的时间更长的时间。
观众：线性系统的任务是否未通过SAT？
教授：是的，确实如此。 但是，现有的工程工具使其不那么常见。 我们不解决SAT的随机问题，也不解决位向量的完全随机问题。
我们解决具有特定结构的问题，以便一个人可以看到它并确信它会起作用。 我们正在尝试在他的脑海中产生一些争论，以了解为什么这样做有效。 SAT求解器使用此结构。 您的问题可能具有一百万个布尔变量，但实际上，这些变量中的大多数都非常依赖于彼此的值。 因此，问题中的自由度数量实际上比数百万个变量所暗示的数量少得多。
听众：您说的这不是考试题，而是现实生活。 一旦有人建立了这个系统，它就应该起作用并且有意义。 因此，这可能不会成为不必要的理论依据。
教授：就是这样。 因此，实际上，在使用此工具时，通常要做的就是设置超时。 通常，所有事情都会发生，因为指数并不意味着您不能这样做。 指数，即当一个功能受另一功能限制时，仅表示存在一堵砖墙，这些事物将在其前面起作用，并且它们将非常快速地起作用。 指数向两个方向起作用。
当您离开这堵墙时，事情会迅速发展，但是当您解决较小或更简单的问题时，这些问题也会非常迅速地加速发展。 这意味着许多问题很快就会解决。 然后问题超时发生。 关键是要设计事物，以便使那些很快就能解决的问题带来切实的好处。 这些问题将使您指出系统的安全漏洞，错误，以前可能没有探索过的路径，或者如果您以前没有调查过这些输入就会违反您的路径。
因此，我们知道如何从一个公式，一组限制到一个回答：“是的，这个公式有一个解决方案，而这里就是一个解决方案。” 否则他会说：“这个公式不能令人满意，因为没有任何输入可以满足您的任务。” 那么我们如何从程序中获取公式呢？
当执行符号执行时，您将转到分支，并且不知道它将往哪个方向运行。 在这种情况下，有两种选择。 — , , , .
, , . , SMT-. . , .
: « , , , , ».
, , . . , .
, . , , . , – , . ? , .
, , t=0 false.
, , ? : , , .
, , , , , , .
, , t = 0, x, y 0. , . , , X , Y.
, X > Y.
55:00
MIT « ». 10: « », 3该课程的完整版本可
在此处获得 。
, . ? ? ,
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月免费，在六个月内付款，您可以
在此处订购。
戴尔R730xd便宜2倍？仅在荷兰和美国，我们有2台Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100电视（249美元起）！阅读有关如何构建基础架构大厦的信息。使用Dell R730xd E5-2650 v4服务器花费9000欧元（一分钱）的c类？