【作者】 赵常智；

【导师】 齐治昌；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2011， 博士

【摘要】 运行时验证是一种轻量级的运行时监控技术。通过持续监控软件系统的运行状态来判定当前系统运行是否满足通过某种高层规约描述的正确性性质。在运行时验证中，通常从高层规约中自动产生运行时监控器。在系统运行过程中，运行时监控器在任何时刻仅能观察到在理想情况下为无穷状态序列的系统执行的有穷前缀。传统的运行时验证技术无法预测被监控软件系统未来可能的执行行为。运行时监控器监控结论的产生仅能依据当前观察的有穷前缀。故仅能检测当前系统执行中的软件失效，而不能预测软件失效的发生。对于部署后软件，及时检测到软件失效固然重要，但预测软件失效并避免其发生更有意义。本文围绕运行时软件失效预测和预防问题，一方面研究软件系统一般时序性质和参数化时序性质的预测语义和预测监控器构造技术，尽可能早的检测软件失效；另一方面，通过前瞻软件行为把控制和反馈的概念引入软件运行过程，提出了软件主动监控的概念和方法，形成由失效预测和预防形成的闭环回路。使得软件运行时验证及主动监控技术成为传统软件分析和验证技术的有效补充，提高部署后软件系统的安全性、可靠性。本文首先基于线性时序逻辑预测语义定义，研究和提出了改进的预测监控器构造方法。运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器。本文提出的构造方法使最终产生的预测监控器规模尽可能小，能有效控制构造过程复杂度，避免状态爆炸从而增强该方法的适用性。以面向线性时序逻辑的运行时验证技术为基础，提出了基于软件系统模型的软件主动监控技术和方法。在系统模型中，不但关心系统状态之间的迁移关系，而且关心驱使状态迁移发生的方法和事件。本文以该模型为基础，提出了如何前瞻系统行为，如何针对运行时监控器监控结论自动产生在特定状态处的调控动作，以及如何采用适当的执行机制使得调控动作能够被及时使能和饨化，从而避免软件失效的方法和技术，形成包含失效预测及预防的闭环回路，使得被监控系统的行为能够向着期望的方向被不断监控和调控。同时本文还证明了，在特定的条件下，主动监控技术总能保证系统的实际运行行为与期望的系统行为之间的一致性。针对描述程序动态属性的特殊需求，本文进一步研究了面向参数化线性时序性质的运行时验证技术，首先综合考虑运行时验证以及参数化线性时序性质描述两方面的特殊需求，提出了既适于运行时验证技术，又能满足参数化性质描述的参数化线性时序逻辑，即PAⅡL，从语法层面保证公式中参数化变量的绑定和使用等基本操作的实施。同时给出了相应的标准语义和预测语义。以此为基础，提出了以交错自动机为中间环节的单一整体参数化预测监控器构造技术，并通过形式化的方法定义了参数化预测监控器的运行过程。该监控器基于参数化系统执行轨迹能够尽可能早的检测当前系统执行中的软件失效。由于PAⅡL逻辑强大的表达能力，使得单一整体参数化预测监控产生过程复杂度比较高及理论比较复杂，本文进一步提出了一种表达能力受限的描述参数化线性时序性质的形式化方法，LTL模板。它与一般的线性时序逻辑存在比较紧密的对应关系。因此，本文研究了如何把参数化系统执行轨迹转化为一组非参数化的程序执行轨迹，从而把面向参数化时序性质的运行时验证问题转化为面向一般线性时序性质的验证问题。这就使得上述关于面向LTL的运行时验证和主动监控技术得以在参数化环境应用。最后，本文以操作系统信息安全访问控制机制为典型应用背景，展示了如何利用上述软件运行时验证和主动在线监控技术和方法框架，在系统运行时过程中，进一步精化sELillLIx操作系统安全策略配置。从而实现进一步提高软件系统信息流安全的目标。验证了本文方法的有效性。更多还原

【Abstract】 Runtime verification (RV) is a lightweight runtime monitoring technique. It aims to check whether an execution of a system under scrutiny satisfies or violates a given correctness property expressed as some types of top-level specification through observing its running continuously. In runtime verification, a correctness property is typically automatically translated into a monitor. During runtime, at any time the monitor can just observe a finite prefix of an execution which should be an infinite states sequence in ideal situation. For traditional techniques of RV, because they are not concerned with and can not look-ahead the future behaviors of the system under scrutiny, the verdicts of monitors are given just on the basis of the current observed finite prefix. Thus, the traditional techniques of RV can just detect the occurrence of failure, but can not predict possible faults in advance effectively. In fact, for deployed software, although it is important to detect the occurrence of failure, it is much more meaningful to predict the fault in advance and prevent it from occurring.In this paper, around the problem on failure prediction and preventention, on one hand, Anticiparoty semantics definition and anticipatory monitor construction for common temporal properties and parameterized temporal properties are reaserched which make failure detection as early as possible. On the other hand, the definitions of control and feedback are imported through looking ahead the future behavior of the system, the definition and method of software active monitoring are proposed. Thus, a closed-loop system is formed which is consisted of prediction and preventention. It’s our purpose to make them to be complementation of other traditional analysis and verification techniques and improve the safety and reliability of deployed software system.Based on anticipatory semantics of linear temporal logic (LTL), this paper presents an improved construction method of anticipatory monitor. An important aspect in RV is that of synthesizing efficient monitor from specification. The proposed method in this paper is not only making the size of the final anticipatory monitor as small as possible, but also controlling the complexity of intermediate steps to prevent the construction process from being affected due to states explosion and improve applicability of the method.On the basis of proposed technique of runtime verification for LTL, this paper presents the technique and method of software active monitoring based on system models. In the model, not only the transitions between states are concerned, but also the methods and events which make the transitions happen are considered. Through the model, the paper presents a series of methods and techniques about how to look-ahead the future behaviors of the system, how to generate the corresponding steering actions connected to given state automatically based on the verdicts of monitors and how to enable and disable the actions in time to prevent the failure from occurring through special execution mechanism. At last, a closed-loop containing failure predication and prevention is generated to control the behaviors of observed system towards desired direction through continuously monitoring and steering. Meanwhile, it is proved that under given condition, active monitoring technique always assure the consistency between the actual execution and expected behaviors of the system.In order to verify the dynamic property, this paper presents RV technique for parameterized linear temporal property further. Based on the consideration about the special requirement of RV itself and the expression of parameterized property, a parameterized linear temporal logic, i.e. PALTL, is proposed which is not only suitable for RV, but also satisfied with the need to describe the parameterized property. It assures that several basic operations such as variables binding and using can be implemented in syntax level. Then, the standard and anticipatory semantics are presented. On the above basis, the paper presents the construction process of a monolithic parameterized anticipatory monitor, and gives the definition of running of the parameterized monitor in formal method. The monitor can detect the failure of current execution based on a parameterized prefix as early as possible.Due to the strong expressiveness of PALTL, it makes the construction process and theory of monolithic monitor is complicated. This paper presents another constrained formal method to describe parameterized linear temporal properties, i.e. LTL Schema. It has close correspondence with LTL. It has explained how to separate a parameterized trace into several non-parametric sub-traces and how to transfer the problem of RV for parametrized temporal properties to the easier verification problem for a corresponding LTL formula on several non-parametric state traces. It makes the techniques about RV and active monitoring can be applied in parametric context.Finally, in the context of access control mechanism for security of operating system, it is showed that based on the technique and framework of RV and active monitoring, the security policy configuration of SELinux can be further refined to improve the security information flow goal during runtime. The effectiveness of the proposed method is verified.更多还原