Using Coq to Verify DPLL

Abstract

Most large software systems have complex data structures with complex invariants. Many bugs can be traced to code that does not maintain these invariants. As an example, the Heartbleed bug can be traced to an attacker sending a packet that violates an invariant that is assumed to be true in the OpenSSL code. Often these invariants are not well documented. However, maintaining them is necessary for correct operation of the software.

In order to develop techniques for verifying complex invariants, we are in the process of developing a verification of a simplified DPLL algorithm. We have a C implementation of this algorithm which is about 200 lines of code. The code implements the two watch variable algorithm for efficient unit propagation. Our proof verifies that the code properly maintains the watch variable invariant. This invariant is described using separation logic and consists of 100 lines of Coq code.

The verification uses our PEDANTIC framework which is designed for verifying the correctness of C-like programs using the Coq theorem prover. PEDANTIC is designed to prove invariants over complex dynamic data structures such as inter-referencing trees and linked lists. The language for the invariants is based on separation logic. The PEDANTIC tactic library has been constructed to allow program verifications to be done with reasonably compact proofs.

While working on the DPLL example, we have found existing Coq IDE tools to not be well suited for some of the tasks needed for a complex verification task. For example, if while verifying an entailment, we find an error in the invariant, then all theorems that have been completed need to be modified and their scripts revised. It would be nice to have an intelligent replay that can guess at changes that need to be made to the scripts. We are in the early stages of developing an IDE based on Python. In addition to replay, the IDE will present a scripting language in which programs can be written to automate some editing tasks. We will an overview of this IDE in our poster.

For more information on this research, check out the website at http://www.cs.jhu.edu/~roe.

Presenter Bio

Kenneth Roe is a PhD student at Johns Hopkins. He returned to graduate school in 2010 after working in the industry for many years. With this work experience, he has a good understanding of the key challenges in developing commercial quality software. This understanding guides his research in formal methods. In addition, Kenneth Roe runs a small business selling iPhone apps. His most successful app, Smart Recorder, has over 1,000,000 device installs and has over 40,000 regular users.