Research On Instrumentation Methods In Runtime Monitoring And Verification For C Programs And Applications

With more and more software is applied in social life, the size and complexity of software systems are increasing rapidly, software reliability becomes an important aspect of software development accordingly. Among the exist software verification technologies, as a lightweight software verification method, runtime verification combines the technology of runtime monitoring and the techonolgy of formal specification, so it is rising as a pop research area. The key to runtime verification has two aspects, one for the description of property to be checked and generation of validator, the other one for the instrumentation of monitor and validator. Owing to the increasing size and complexity of software systems, monitoring based on log API or manual code instrumentation is not applicable for the verification of systems from different platforms and different areas. With the development of compiler technology and aspect-oriented programming technology, using compiler to realize the automated instrumentation and aspect-oriented language to describe and modularly manage the instrumentation location is becoming an important research filed for the practical application of runtime verification.This thesis analyzes the compilation process of C programs, LLVM open source compiler framework and its Clang frontend. Based on these tools and the concept of AOP, we design and implement an AOP language MOVEC for C programs, with which monitor instrumentation location's description can be analyzed and realized automatically using source code instrumentation. We also design and implement a validator instrumentation tool for errors such as dividing by zero, integer overflow and value uninitialization which is also based on source code instrumentation. The final experiment of comparison between MOVEC, AspectC, Aspect C++ shows its advantages in higher accuracy, less instrumentation time consumption and less code bloat with no more running time overhead. Another one experiment shows the validity of validator design and instrumentation algorithm. Work in this thesis can be a foundation for the automated, efficient, cross-platform instrumentation for monitor and validator in runtime verification, and promote the practical application of runtime verification.