Using Lightweight Specifications with Fuzzing and Symbolic Execution to Reveal Security and Semantic Bugs

Security and Semantic bugs exist in software systems, and discovering them is time-consuming, complicated, and challenging. Several static and dynamic techniques are presented for discovering bugs. However, finding a bug is still a challenging topic. In this work, we investigate developing a prototype tool that uses the benefits of using the lightweight specification, fuzzing, and symbolic execution for discovering security and semantic bugs in an arbitrary Java program. This proposal aims to extend Badger, meaning both SPF and Kelinci, with the ability of handling both pre and postconditions using the runtime assertion checker of OpenJML with the lightweight specification. Also, using and extending Debug.assume()'' andDebug.assert()'' mechanisms in SPF that they work like precondition and postcondition, respectively.