Using symbolic execution to test monitor specifications

Abstract

In security critical applications, monitors are used to increase the level of confidence during runtime. Their main job is to extract information from a running application and use it to detect and possibly mitigate any specification violation. Monitors are typically specified and compiled automatically from high level specification languages. However, particularly for novel users, ensuring that the specifications are correct is a major concern and might consume a lot of time. Creating a system which can automatically generate a report indicating whether the identified monitors exhibit the expected behaviour or not, would be of precious feedback for the monitor developer. This project aims to investigate whether symbolic execution techniques can be successfully used to automatically force the system under test to go through all the states specified in the monitors, with the aim of generating a report which can be used to verify the mentioned monitor specifications.