组合验证法在计算机系统验证中的应用

112理论计算机科学电子笔记70第4期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html16页组合验证法在计算机系统验证中的JoshuaLevy和HassenSadi和TomasE. Uribe系统设计实验室SRI InternationalMenlo Park，CA.94025flevy，saidi，uribesdl.sri.com摘要验证允许检查无法完全在线验证的系统属性当系统包含复杂的第三方组件（如通用操作系统和软件库）时，以及当感兴趣的属性包括安全性和性能时，尤其如此。目前的挑战是找到可靠的方法来监测这些属性在现实的系统。尤其重要的是，必须保证在实际发生侵犯人权行为时予以报告例如，如果安全违规是由一系列不在其模型中的系统事件引起的，则监视器可能无法检测到我们描述了如何结合运行时监视器的不同功能，如内存管理，安全相关的事件，性能数据和更高级别的时间属性可以导致更有效的运行时验证。在讨论了一些基本的概念相结合，相关的监视器，我们说明了他们的应用程序在SRI开发的入侵容忍Web服务器体系结构1引言大多数计算机系统在投入使用之前不能完全检验。完备的系统的高度复杂性使它们超出了详尽的形式化分析工具的范围，如模型检查器和theo-rem证明器。此外，许多系统依赖于第三方组件，而第三方组件的完整规范（甚至源代码）都不可用。最后，大多数形式化分析工具的本质要求它们检查1 这项研究由DARPA赞助，合同号为N66001-00-C-8058。本文中的观点是作者的观点，不一定反映支持机构的观点。c2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。利维，Sa迪和乌里韦113而不是系统本身。如果这个模型是不准确的，重要的方面的实际系统的行为可以overlooked。用于认证系统的规范可能不完整、错误，或者做出了被运行时环境违反的隐含假设。验证通过检查实际的系统执行是否满足所需的属性来解决其中的一些问题。与检查系统（模型）的所有计算是否满足属性不同，运行时验证检查系统执行时生成的特定计算是否正确，避免了限制穷举验证工具可伸缩性的状态空间爆炸。然而，在分析系统的运行时行为时，仍然必须做出重要的选择，包括执行运行时验证的抽象级别，它有多详细和全面，以及期望保持什么规范或属性例如，支票的便利性常常被用来换取效率。在许多情况下，在单个抽象级别上监视操作是不够的。同样地，监测可以不限于单个组件或操作的单个方面。监视机制的正确行为可能取决于必须单独监视的属性。当该系统旨在主要用于以下用途时，这些问题尤为严重保留安全属性。恶意攻击者可能试图击败或绕过监视机制本身，成功的攻击可能会使打算报告它的监视器失效。在本文中，我们讨论并说明了运行时验证如何从多个抽象级别的多个监视器的组合使用许多专门的监视器可以更好地了解系统中的事件。通过组合监视器提供的信息，可以在运行时检查与系统的不同方面相关的更强的属性。由单独的监测器产生的模块化便利了监测信息和机制的共享和再利用。概述：我们在第2节和第3节中提出了一些初步的定义。第4节描述了我们的目标应用程序，一个入侵容忍服务器。第5节提供了一组组合显示器的示例。第6节介绍结论以及相关和未来的工作。2预赛我们感兴趣的分布式系统，这可能是由多台机器，每个运行多个进程，连接到一个网络的运行时属性检查。虽然我们并不试图将这项任务利维，Sa迪和乌里韦114在本文件中，我们将在下文中说明它应处理的一些方面系统状态：非正式地，系统状态由所有机器的状态和网络状态对于一个特定的机器，系统状态可以在不同的抽象层次上描述。在硬件级别，它由处理器、寄存器和内存的状态给出。在操作系统级别，它是操作系统和当前运行的进程对于给定的进程或线程，（局部）状态由其程序变量、执行堆栈和控制位置的值给出。系统变量应该足以描述所有考虑的组件和抽象。定义2.1系统状态是一组系统变量V的赋值。固定系统变量的集合是一种建模选择，并且意味着选择某个最低抽象级别（例如CPU寄存器和内存位置），但是在定义我们下面的术语时很有用定义2.2系统的运行是系统状态的一个不间断序列r：s0; s1; s2;：状态和运行可以映射到更高的抽象级别，抽象变量是根据一套原始的具体系统来定义的变量。这引起了许多问题，例如抽象变量的范围问题[15]：在实践中，抽象状态的定义将是模块，进程或子例程的本地。当本地进程不运行时，抽象值将被忽略。一般来说，抽象变量和具体变量之间的映射是不固定的（例如，程序变量指的是从程序的一次运行到下一次运行的不同存储器位置，并且其他值可以被动态地绑定）。不同层次的可观测性：通常，当我们关注系统的某个特定方面时，只有系统状态的一个子集是可见的。例如，应用程序可能不知道完整的OS状态是什么，包括什么其他进程正在运行。操作系统可能知道所有正在运行的进程，但可能无法直接访问特定进程的内部状态定义2.3（局部视图）给定一个系统状态s和一组（可能是抽象的）变量L，我们写s j L来表示s在L中的变量中引起的赋值，即状态的局部视图。我们允许L中的在它们还没有被初始化的状态）。时间粒度：一般来说，组件或监视器只能观察某些系统转换，并且可能忽略转换。而且，软件抽象级别的转换可以对应于硬件级别的多个步骤，并且此外，可以中断和恢复。例如，应用程序级监视器将不知道何时调用中断。利维，Sa迪和乌里韦115出于这个原因，我们可以预期大多数被监控的属性都是口吃不变的[1]。以前的工作已经确定了过程级、语句级和警告级监控之间的区别[11]。每一个都在开销、实现复杂性和精度之间提出了不同的权衡。我们的目标是在所有这些级别上都允许wmonitor，以及其他更一般定义的抽象级别。3监视器监视器是一个模块，它在特定的抽象级别上观察给定的一组系统变量，收集有关这些变量的信息，并使这些信息中的一些可用于其他监视器和组件。特别是，我们希望监视器报告违反预期的系统属性。定义3.1“属性”是系统的一组运行。 对于游程r，我们假设r是“的模型，并且写rj=”，如果r2“。 我们写rj="，或者等价地rj=“，如果r62”。描述这些属性的一种常见方法是使用线性时间时序逻辑（L TL）[16]。属性可以被分类为属于安全或活性类[2]，其中安全属性是那些可以通过运行的nite pre x检测到故障的属性。停止并发出警告或警报的监视器通过定义来检查安全属性。(On另一方面，并非所有的安全属性都是可监测的[23]。有一些系统属性不能表示为运行集，包括可能性和一般分支时间时间属性[3，6]。这包括许多安全属性，例如各种不干扰公式[25]。我们将专注于发现财产违法行为，而不是财产执法[21]。定义3.2监控器M具有一组可观察的状态变量V M和一组辅助变量O M，它们对外部模块可见。监视器通过对VM中的变量进行采样并更新OM中的变量来操作，并且当它认为已经发生违规时发出警报。给定一个系统运行s0; s1; s2;：，监视器会看到一系列状态si0;si1;si2 * 仅限于变量VM，即，si0jVM;si1 jVM;si2 jVM：其中0Iji j+1对于所有j0.假设辅助变量OM是系统变量V的全局集合的一部分。利维，Sa迪和乌里韦116实际上，VM中的变量 是最好的定义l ocall y，而不是在全球，但低层次的系统变量。例如，当我们在变量n ts中将高水平的velc ode注释为c heck时，就是这种情况。我们不对监控器M可以使用什么机制来观察变量VM或可以具有什么内部状态M做出任何假设。大多数监视器可以被假设为nite-state，尽管软件监视器可以具有无界堆栈（例如[24]中使用的下推自动机）。一个简单的形式化的监控器的例子是一个nite-state自动机，它描述了一个特定级别的系统抽象的时间安全属性[7 ]，并通过代码注释与系统组成。在实践中，监视器的功率和可靠性可能会有所不同。定义3.3（监控器特征）我们说监控器M相对于一个 属性y'是 完 全的 ， 如 果 对于任意一个运行r，rj='，M保证发出警报。如果每当M报告警报时，则rj =“”（无假警报），则监视器M相对于属性“是健全的。不完整监视器的一个例子是可以跳过所选抽象级别的步骤，从而错过违反所需属性的状态。许多入侵检测系统是不完整和不健全的监视器的例子：它们可能产生错误警报，并且无法报告违规行为。还要注意，由监视器检查的属性在监视器实现中可能是隐式的，并且在声明形式（诸如时态逻辑公式）中不可用。如果监视器的执行被停止，则可以使其失效。从技术上讲，如果修改观察到的变量的执行步骤也被停止，则监视器旨在检查的安全属性可能不会被违反。 对于通过源代码注释检查应用程序内部一致性的监视器来说就是这种情况。我们将在下面更详细地调查这个问题。假设保证规范：我们可以以假设保证的方式指定监控器的属性[1]。定义3.4给出系统S、监视器M和特性1 第二，我们写['1]M['2]以指示M是可靠的，并且当被限制为满足“1”的运行时，相对于“2”是完整的，假设M未被禁用。也就是说，M被保证充分地报告违反了'2foranyrun，其中'1 保持。请注意与标准霍尔三元组描述的部分正确性的类比因此，M可以可靠地监视“（”总正确性”）被分解为两个属性：第一个可以写为[true]M[“]，并包括可靠性。 第二条规定，M不能在S的运行中被禁用。利维，Sa迪和乌里韦117M1MM如果我们写[[M]]来表示监控器M不发出警报的运行集合，则['1]M['2]可以表示为（'1\[[M]]）'2。定义3.5（监视器组成）如果M1 和m2是S中的监视器，我们写为M1M2以指示当出现M1或M2时发出警报的监视器 是的。正式通知，如果M1 证明了P成立，而 M2 c he cksQ，thenM1M2c hecksP^Q：如果组合监视器不发出警报，则P和Q都保持。我们也有[[M1 M2]]=[[ M1]]\[[ M2]]：然后我们可以编写简单的规则，例如和[P1]M1[Q1];[P2]M2[Q2][P1^ P2]（M1M2）[Q1^Q2][P]M1['];[']M2[Q][P]（M1M2）['^Q][P1]M1[Q1];P！ P1; Q1！Q[P]M1[Q]其中一般的S-时间有效性要求的前提[16]。通过这种方式，可以将运行时和静态验证相结合。上述规则都是一个一般规则的实例[Ai]Mi[Gi] ;（Vi（Ai！ Gi））！ A！G[A]（M1： Mn）[G]在下面的部分中，我们描述了在实践中可以通过共享信息以及结合警报来紧密结合监视器的方法3.1组合键正如我们所讨论的，监视器可以嵌入到应用程序代码中，也可以嵌入到操作系统中;它们可以是一个单独的进程，也可以由观察网络和接口的单独模块组成。上面描述的组合操作符仅意味着各种监视器警报是联合的。在实践中，监测人员可以分享和交流其他信息。我们考虑的监视器组合模式如图1所示。从N到M的箭头表示M的可观测变量包括N的一些辅助变量，is，ON\VN 不是emp ty。2 在所有情况下，我们假设监视器报警2一般来说，可能会出现循环信息流，其中O\V和O\V2M 2 1非空。但是，在这种情况下，将M1和M2利维，Sa迪和乌里韦118补偿：被覆盖更正：更强的属性尊敬的：工作再利用、效率Fig. 1. 监视器组合（信息流）是连在一起的 描述的组合模式为：互 补监视器：在这种情况下，监视器M1和M2独立地检查其属性.净效应是获得监控器M1 M2，如前一节所述请注意，即使监视器在运行时不通信，其设计也可以利用其他监视器存在的事实例如，M1的正确 行 为 可 能 取 决 于 由 M2 检 查 的 假 设 ， 正 如 我 们 将 在 第 5 节 中 看 到的那样。相关性：给定监控器M1和M2，监控器M3通过在其可观测变量中包括M1和M2的一些辅助变量来关联它们的活动。 这允许检查比仅由M1和M2检查的那些更强的属性。相关性：相关性的一种特殊情况，其中一个监视器检查依赖于其他监视器传递的信息的属性。这种组合可以提高总体监测子系统的效率，允许再利用潜在的昂贵的监测数据。4应用：DIT服务器架构我们的动机和示例应用程序是设计和实现一个入侵容忍Web服务器体系结构[22]。依赖型入侵容忍（DIT）体系结构如图2所示。 一个或多个冗余容限代理管理用户请求，并将它们转发到冗余应用服务器组。DIT系统的目标是以合理的成本发布具有高度完整性和可用性的Web内容。这是通过使用低成本的COTS软件，相对较低的保证，在高保证入侵容忍设计。该体系结构是基于观察，COTS Web服务器软件的功能lled和复杂的，往往包含安全漏洞。然而，不同的程序和操作系统具有不同的漏洞，因此，在不同平台上具有不同Web服务器的系统应该提供更大的可用性和完整性保证，假设可靠的机制用于从冗余服务器收集响应，验证它们，并将它们转发到客户端。利维，Sa迪和乌里韦119COTS应用服务器代理客户图二、容侵服务器体系结构示意图同行专业人士图三. 代理实现此功能由代理执行，该代理驻留在运行少量自定义代码的硬化平台上。代理软件的简单性和自定义特性使其比应用服务器更易于加固。代理接受客户端请求，将它们转发到多个应用服务器，并比较应用服务器返回的内容。如果足够多的人同意，代理将确认的答案发送给客户端。一个协议机制决定了哪些服务器被查询由代理为每个客户端请求，以及如何充分的协议是确定的。例如，特定的机制可以指定每个请求被转发到随机选择的三个不同的应用服务器，并且在结果被发送回客户端之前，在三个应答中代理服务器和应用服务器通过由入侵检测系统（IDS）监控的专用网络进行通信。协议机制随着时间的推移而变化，例如报告不一致和IDS警报。图3显示了我们的代理实现的主要组件。机制管理器负责执行内容协定协议，领导人IDs应用服务器代理服务政权经理警报经理挑战-响应IDs客户TS利维，Sa迪和乌里韦120无效请求开始图四、通用内容协议如图4所示。警报管理器从IDS子系统和挑战-响应协议获取输入，并在需要更改时通知机制管理器。挑战-响应协议作为附加的完整性检查不断地执行。它提供了一个相对高的延迟检查的完整性，代理和服务器上的LE和目录，通过周期性地发出质询，该质询必须通过计算质询和给定LE的单向函数来回答挑战-响应协议还提供了活性检查：如果没有收到响应，则会发出警报。这是一个专用监视器的示例，它可以帮助确保其他监视器处于活动状态并正常工作。 (Note该协议的成功破坏很可能被IDS子系统检测到。5组合示例我们现在描述各种运行时监视器组合的示例。代码注释和进程监视：在运行时验证程序执行的一种常见方法是源代码注释。 这最适用于在源语言和程序设计的上下文中容易表达的属性，例如简单的断言，以及可以用一些辅助变量表达的时态属性。将运行时版本嵌入到程序本身允许密切和准确的监控，但不能保证属性对于整个系统保持不变，除非保证带注释的源代码实际上正在运行。当使用通用操作系统时，这是不平凡的，并且可能会危及安全性。然而，接受请求有效福尔瓦德请求到n个服务不充分的协议足够的协议问更多服务器发送对客户的回应识别可疑服务器足够的协议限制达到服务不可用利维，Sa迪和乌里韦121确实存在捕获这种违规的机制，例如在基于主机的入侵检测系统中使用的机制操作系统进程可以被监视，这样入侵者（或故障）就很难在不被发现的情况下停止或终止程序。设P1 是源代码一致性属性，而P2 B是系统属性，说明应用程序正在运行。 在该示例中，代码注释监视器MA相对于内部属性P1是完整的，但相对于系统级属性P1、P2不是完整的，因为MA 不能保证P2。 因此，我们需要监视器的补充组合，以捕获对更全局的系统属性的违反。这样的组合用于DIT代理设计中。代码注释检查关于变量的断言并监视请求处理线程的执行，而单独的监视器ME用于验证整个多线程进程的不间断执行。后一种监视器通过许多Unix类型操作系统中存在的/proclestrom机制访问相当防篡改的内核信息。这一论点的形式化是[true]MA[P1];[true]ME[P2][true]（MAME）[P1^P2]此外，我们使用StackGuard [4]来确保代理代码中不会出现缓冲区。这可以看作是第三个补充监测。注意，MA和ME观察不同的状态变量集。MA检查应用软件变量的属性，例如源代码变量和执行堆栈，而ME监视操作系统的状态。这说明了如何检查一个属性，涉及到许多种状态变量是更容易通过分解成子属性，每一个涉及一个更有限的变量集，监视器更容易建立。计数连接：作为监视器之间相关性的一个例子，考虑一个从网络接受客户端连接并提供响应的服务器程序。 如果运行程序的机器是专用服务器，那么到机器的网络连接数应该等于程序所服务的客户端的数量。 违规表示服务器软件中存在错误或未经授权的连接。为了准确地监视正在服务的请求的数量，我们需要一个服务器软件的监视器，它是通过注释代码获得的。为了计算整个系统的实际客户端连接数，我们需要一个基于操作系统的监视器。最后，第三个监视器接受前两个监视器的输入，并检查它们是否一致。我们目前正在将这样一个监视器合并到DIT代理中，/proc提供系统连接信息，如前一个示例所述到服务器进程的连接数也可以从利维，Sa迪和乌里韦122外部，而不改变程序;我们的方法具有能够验证附加属性的优点，例如，为每个连接发送有效响应。资源和性能监控：相关性的一个更一般的例子涉及与资源使用和性能相关的属性的验证性能和资源使用可以各自独立地监控，最有可能使用不同的机制。但是涉及这两种类型信息的属性也是有用的。给定一个简单的服务器应用程序，其中客户端请求预计具有大致相等的成本，我们可能希望检查内存和CPU使用率与当前连接的客户端的数量成比例违反此属性可能表示内存泄漏、服务器操作中的错误，或者客户端超出了预期或可接受的资源分配。组合监视器以实现网络安全：监视器的组合当然不限于由单个机器组成的系统可以监视联网的计算机集合，监视器验证各种平台、网络及其组合操作的状态和操作。虽然网络中的信息流的数量和通信中的信任级别通常比单个计算机上的软件组件之间的信息流和通信中的信任级别更有限，但是有效地组合单独的监视器的必要性越来越大，因为需要不同的机制来监视不同的平台和网络本身。检查网络系统中可能存在的安全违规行为的网络入侵检测系统已经很常见[19]。由于它们是为通用网络设计的，并且由于通用网络数据的量和复杂性，网络IDS不验证网络操作的大多数方面，而是专注于特定的违规行为，例如包含已知攻击的分组的存在，或者分组的特定类型和序列。然而，在需要验证更强网络安全属性的应用中，网络监视可以与其他类型的监视器组合以提高准确性。作为一个简单的例子，考虑一个数据库，在rewall后面，可以通过身份验证Web服务器访问。如果监视器是与每个请求相关联的用户的ware，并且当用户使用身份验证机制登录时，则对到数据库的内部网络连接的监视通过验证查询在登录之后和徽标之前，雷沃会被抓住。检查DIT系统中的请求转发：最后，让我们概述一下在DIT系统设计中，监视器如何结合起来验证关键属性P：P：代理将客户端请求发送到一组正确的应用服务器。代理服务器程序维护两个关键的内部值：（i）列表利维，Sa迪和乌里韦123图五. DIT监视器的服务器被认为是未受损的，因此可以查询，以及（ii）当前的制度，它确定了未受损的服务器的数量，应查询每个客户端请求。P意味着请求被发送到适当数量的被认为是未受损的不同应用服务器，或者如果没有足够的这样的服务器，则根本不发送请求属性P可以用几个其他属性来表示P1：公共服务器正在运行.P2：根据设计规范，每个区域的过渡都是可以的.P3：实际上遵循了当前的制度（即， 代理发送等于当前机制中指定的请求的数目）。P4：被认为有问题的服务不被查询.P1{P4}意味着P（假设系统启动时的状态是正确的）.属性P1由前面描述的基于OS的/proc监视器ME来验证。警报管理器的接口允许使用接口监视器MI来监视状态转换，只要代理服务器运行，接口监视器MI就工作MI能够通过检查每个转换对规范，i阳离子，描述了当政权被允许改变，以验证P2该规范说明了当观察到不一致时如何增加该机制，以及如果未受损服务器的数量下降到该机制所需的数量以下，则如何减少该机制触发跃迁的事件可以在界面上观察到。为了验证请求的数量实际上与当前状态匹配，在连接到内部网络的单独机器上运行的网络监视器MN进行监视以查看哪些应用服务器是每个转发的请求的接收者。监视器将其与当前制度和当前未受危害的服务器列表进行比较，该列表在来自MI的网络消息中接收。（MN） 也检测不存在SU CH消息）。 这种情况下，MN既包括P3，也包括P4。本示例中监视的系统变量的相关类型(i) 代理上的OS变量（/proc）(ii) 应用软件变量（代理代码）利维，Sa迪和乌里韦124(iii) 方案状态变量（当前机制和未压缩服务器的当前列表）(iv) 网络变量（发送的数据包、它们的来源和目的地）P1涉及第一组系统变量，P2涉及第二组变量，P3和P4都涉及最后两组变量。总而言之，图5以图表形式显示了三台监视器之间的信息。表明三个监视器结合起来验证P的形式论证是 ：[true]MN[P3^P4];[true]ME[P1];[P1]MI[P2][true]（MEMI）[P1^P2]P1 P2P3P4！ P;[true]（MEMIMN）[P1^P2^P3^P4] [true]（MEMIMN）[P]当然，还有一项任务是确保这三个监测员不会受到干扰，在这种情况下，我们认为这将通过其他正式或非正式的论点来确定。6结论我们认为，在实际的系统中，运行时监视器在不同的操作水平必须结合起来。在制度设计、监督层次和监督机制的选择上，应考虑监督组合的效果。组合监视器的优点可以总结如下：(i) 额外的监视器可以覆盖缺失的属性，例如未检查的假设（协作）(ii) 通过共享信息，可以监控更强的属性（验证）(iii) 提高监测机制在有效实施和合并监测方面存在许多实际挑战。例如，将期望具有支持在不同抽象级别处实现的监视器之间的信息交换的安全内核模块。6.1相关工作运行时监视器的组合在以前的工作中还没有得到解决，虽然已经做了很多工作来开发和测试个人的moni- toring机制。我们提到了一些与我们所讨论的技术和应用相关的技术。利维，Sa迪和乌里韦125入侵检测可以被视为一类重要的运行时监控和验证，特别是在基于规范的IDS [12，13]的情况下。给定潜在入侵的具体说明，设计时验证还可以帮助识别安全漏洞和漏洞利用。在C程序中缺乏类型安全导致了臭名昭著的安全aws，如buer over erows，被Code Red蠕虫利用[18]。有几个工具可以满足在运行时检查C和C++程序的类型安全属性的需要。CCured类型系统[17]使用静态和运行时指针分析的组合来捕获类型错误。Cyclone [10]是一种更强类型的C语言方言，它插入了额外的运行时检查。StackGuard [4]是一种编译器安全机制，可以捕获许多buer over ow攻击（我们用于代理编译）。MaC语言[15，11]提供了一种用于描述监视器的形式语言Alamo监视器架构[9，8]对C代码进行了更详细的分析，导致代码效率较低用于检测C和C++代码并分析结果的技术在[14]中给出。futurework：我们的正式框架可以扩展到显式地包括抽象层，包括变量，组件和监视器之间的抽象和关系。假设保证证明符号可以类似地扩展。我们还没有讨论设计问题，比如设计师如何知道使用什么显示器以及如何组装它们。然而，这种运行时验证的方法可以很好地补充设计方法，包括设计时验证。O线验证和分析可以尽可能彻底地应用，然后可以选择和组装运行时监视器来检查所有剩余的关键属性。监视器的选择也可以遵循设计保证参数，该参数描述了为什么电弧结构满足所需的操作和安全要求[5]。正如我们在第2节中指出的，一些重要的安全属性不是迹集[25，20]。因此，仅运行时检查无法保证这些属性。验证必须与设计时分析相结合，以确保这些属性。未来工作的另一个方向是扩展我们的框架以包括财产强制执行，正如[21 ]的安全自动机所做的那样;我们目前的重点是检测安全财产违规行为。最后，另一个挑战是扩展我们的框架，以包括实时属性和监视器，并访问全局或本地系统时钟。实时约束允许将许多不定时的进度属性表示为定时的安全属性，从而可以对其进行监控.利维，Sa迪和乌里韦126确认我们感谢Magnus Almgren、Nikolaj Bj rner、Steven Cheung、YvesDeswarte、Bruno Dutertre和Alfonso Valdes的评论和反馈。引用[1] Abadi，M.和L. Lamport，Composing speciations，ACM T ransactionsonProgramming Languages and Systems14（1992），pp.1{60.[2] 阿尔彭湾和F.B. 谢文龙，《生态安全与活性》，《分布式计算》，第2卷，1987年，页。117{126.[3] Ben-Ari ， M. ， Z. Manna 和 A. Pnueli ， 分 支 时 间 的 时 间 逻 辑 ， ActaInformatica20（1983），pp. 207{226.[4] 考恩角，C. Pu，D.作者：J. Bakke，S.贝蒂，A.格里尔山口Wagle，Q.Zhang和H.Hinton，StackGuard：自动自适应检测和预防缓冲器溢出攻击，在：Proc. 第七届USENIX安全会议，1998年，pp. 63{78.[5] 道 森 ， S. ， J. 利 维 河 Riemenschneider ， H.Sadi ， V.Stavridou 和A.Valdes，入侵容忍的设计保证论证，在：入侵容忍系统研讨会，DSN2002年，2002年，第10页。C{8{1{C{8{5。[6] Emerson，E. A.和J. Y. Halpern，“ 有时”和“不是永远”revisite d ：在branching时间与线性时间，ACM杂志33（1986），页。151{178.[7] Geilen，M.，关于时序逻辑特性监视器的构造，理论计算机科学电子笔记55（2001），R V '01|第一次研讨会上的验证。[8] Je ery，C.，Alamo执行监视器架构，电子笔记理论计算机科学30（2000）。[9] Je ery，C.L.，W. Zhou，K.Templer和M.刘晓波，一种新的程序设计方法，计算机科学与工程，2000，第10页。67{74.[10] 吉姆，T.，G. Morrisett，D.格罗斯曼，M.Hicks，J.Cheney和Y.王文，《旋风：C语言的一种基本形式》，载于：美国科学院国际技术会议， 2002年。[11] 金，M.，运行时形式化分析的信息抽取”，博士学位。论文，CIS部门宾夕法尼亚大学（2001年）。[12] Ko，C.，\分布式系统中安全关键程序的执行监控：基于规范的方法，博士学位。毕业论文，计算机科学，加州大学戴维斯分校（1996）。[13] Ko，C.，M. Ruschitzka和K. Levitt，分布式系统中安全关键流程图的执行监控：基于规范的方法，在：IEEE安全和隐私，1997年，pp. 175{187.利维，Sa迪和乌里韦127[14] Kortenkamp，D.，T.米拉姆河西蒙斯和J. L.张文，张文，等.计算机理论与应用.北京：清华大学出版社，2001|第一次研讨会上的宣传。[15] 李岛，加-地S. Kannan，M.金河，澳-地Sokolsky和M.李文，基于形式化规范的并行计算，并行分布式计算技术与应用国际会议，1999年。[16] 曼纳角，巴西-地 和A. P nueli.，技术验证分析，载：国际计算机软件性能研讨会（TACS'94），LNCS789（1994），pp. 726{765.[17] Necula、G. C.的方法，S. McPeak和W. Weimer，CCured：《语言的类型安全记录》，载于《语言程序设计原则》（2002年）。[18] 佩 尔 梅 河和M.Mairet ， .ida\CodeRed”worm，SecurityAdvisoryAL20010717 ， eEyeDigitalSecurity （ 2001 ） ，http://www.eeye.com/html/Research/Advisories/AL20010717.html.[19] Porras，P.和P. Neumann，EMERALD：事件监控，使异常现场干扰的响应成为可能，在：第20届国家信息系统安全会议的开幕式上，巴尔的摩，MD，1997年，第110页。353{365.[20] Rushb y，J.， 安全需求规范：如何和什么？2001年，美国印第安纳州印第安纳波利斯信息服务需求工程研讨会[21] 施耐德，F.B、可执行的安全策略，信息和系统安全3（2000），pp。30{50.[22] Valdes，A.， M. Almgren，S. 张，Y。 德瓦特湾 Dutertre，J. Levy，H. Sa di，V.Stavridou和T. E.陈文辉，一种基于网络的入侵容忍服务器体系结构，计算机科学与技术研究所，北京，2001。[23] Viswanathan，M.，\F oundations for the Run-time Analysis of Softw areSystems，”Ph.D.论文，计算机与信息科学，宾夕法尼亚大学（2000）。[24] 瓦格纳，D。和D. Dean，通过静态分析进行入侵检测，在IEEE安全和隐私研讨会上，2001年，第100页。156{169.[25] Zakinthinos，A.，\“论证券性质的构成”，博士。论文，多伦多大学电子与计算机工程系（1996）。