Software Runtime Verification Based On Aspect-oriented Programming

As software systems are more and more pervasive in everyday life, it is becom-ing increasingly necessary to guarantee the security and reliability of software systems.Current software quality control techniques, such as software test, program analysis andmodelchecking,cannotguaranteethatdeployedsoftwaresystemsareerrorfree. Runtimeverification is a lightweight verification technology, which does not assume a deployedsoftware is correct, but continuously checks whether a software execution satisfies or vio-lates a given critical property. Runtime verification techniques are widely used to preventdamages from happening and are quite effective in practice.The techniques of Aspect-Oriented Programming (AOP) based runtime verificationtreat runtime verification as a cross concern. AOP can modularize runtime verificationconcern, andthejoinpointmodelusedinAOPlanguagesisnaturallycorrespondingtotheevents monitored in runtime verification. Most mainstream runtime verification frame-works are implemented in AOP languages.As the monitored program is evolving and AOP based runtime verification tech-niques inject monitors into programs in an oblivious way and generally can arbitrarilymodify the monitored program, those features bring big challenges to use them correctly.In this paper, we try to resolve the problems that hinder users from effectively and cor-rectly adopting the AOP based runtime verification techniques. The main contributionsinclude:1. We propose an event pattern language for runtime verification. Based onthe characteristics of selecting the event sequences in runtime verification, we propose anew event pattern selection language. This event pattern language is composed by twolevel operators. The lower level operators use restricted pointcuts to select single events.The restricted pointcuts only use the local information from the event environment. Thehigher level operators fully leverage the control flow and the data flow relation amongevents to select event sequences. Compared with other event pattern languages used incurrent runtime monitoring frameworks, our language can express a wider spectrum ofevent sequences.2. We propose predictive semantics for LTL formulae used in runtime verifi-cation. Current runtime verification techniques generally assume that monitored events arrive one at a time. But if we can do a static analysis on monitored programs, we mayfind that some monitored event sequences are predictable when their first elements hap-pen. Thus we can help the monitor to find whether an execution satisfies or violates aproperty in advance. We give a formal definition to this method and implement a tool.We use the tool to carry out some experiments on several real and large-scale projects.The result demonstrates that our method is generally applicable in these projects.3. We define two types of conflicts in and between runtime monitors and theircorresponding detection algorithms. There might be an inconsistency between an in-tended monitor property and the actually implemented monitor property because of thecomplexity of the pointcuts used to select monitored events. If there are several monitorsinjected into a monitored program, it is a big challenge for developers to master the fi-nal runtime behavior. To address this problem, we define two kinds of conflicts: one isinside a runtime monitor; the other one is between runtime monitors. We also give theircorresponding detection algorithms. These algorithms are implemented based on an opensource runtime verification framework and several real cases are examined. The resultsdemonstrate that this approach can help users to use runtime verification techniques moreeffectively.4. Weproposeaclassificationmethodforruntimemonitorsandthecorrespond-ingdetectionmethod. Currentmainstreamruntimeverificationframeworksenableusersto arbitrarily modify monitored programs when their executions satisfy or violate mon-itor properties. The original properties of the monitored program may be broken. Wepropose a classification method for runtime monitors based on their impacts on the prop-erties of monitored program. We also present a method to automatically detect the classof a monitor. The monitor’s class can help users to select runtime monitors more wisely.