Program Repair Using Datalog-Based Static Analysis

Abstract:

Automated program repair is an emerging technology for automated rectification of errors and vulnerabilities in programs. In past work, it is driven by correctness criteria expressed as tests. In this thesis, we study how static analysis reports can be used to guide program repair. This is an alternate approach. Static analyzers have usage in industry and may allow for higher level repairs to be accomplished. Many static analyzers can be encoded in Datalog owing to the least fixed-point semantics of Datalog. Based on this observation, we propose a symbolic execution of the Datalog program to extract repairs via a surgery of Datalog facts. We show how such a core approach has many applications such as null pointer dereference analysis guided repair, or repair of Application Programming Interface (API) misuses. Finally, we show how we can use Datalog programs with stratified negation to represent temporal logic properties. These are then used to automatically fix vulnerabilities in reactive programs such as internet facing widely used protocol implementations such as OpenSSL. Our approach integrates vulnerability detection and repair, potentially reducing the exposure time of critical software systems to security risks.