Research On Key Techniques Of Software Monitoring Based On Runtime Verification

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.