Verifying programs with complex data structures using Coq

Abstract:

If one had a tool that could verify that a program correctly maintains data structure invariants, it would be very useful for finding bugs. For example, the Heart bleed bug from a couple of years ago can be traced to an invariant violation. The OpenSLL library made an assumption that packet size information stored in two di erent places was consistent. By sending packets which broke this invariant, a hacker was able to steal critical data. Had a tool existed to verify these invariants, this bug would have been caught before the software was released.

The research presented in this abstract aims at creating a tool for first documenting data structure invariants and second to verify them. We have developed a separation logic based language using the Coq theorem prover. This language is sufficient to document most useful invariants. We are working on the verification of a simplified version of the DPLL algorithm to demonstrate the utility of the invariants. The code for this algorithm is around 200 lines of C code. The invariant describing relationship between all the data structures is around 100 lines of Coq code. This invariant describes simple relationship such as the relation between an array storing assignments for boolean variables and a linked list storing the same assignments using pairs with the variable number and value. It also describes more complex relationships such as the 2-watch variable algorithm used to quickly identify unit propagations in DPLL.

One of the keys to make completing the proof tractable is to be able to break it into smaller pieces. In order to do this, we needed to add some constructs tour separation logic framework. These constructs make it easier to represent intermediate states where for example, an intermediate state might be “all invariants hold except that one variable has been assigned a new value.”

Any Coq user who as attempted a non-trivial proof has found that the process is extremely tedious. The author after analyzing some of his own workflow in developing proofs identified a number of areas in which the proof development process could be improved. One key finding is that of developing a large proof (with many lemmas) often requires many iterations of revisions on the statement of the proof. Developing the proof script often reveals errors in the statement of the proof. Changing the statement then requires the proof to be replayed which is very tedious. As part of the research, we introduce a new IDE, CoqPIE that has all the functionality of Proof General or Coq IDE plus many new features to deal with work flow issues. For example, the IDE introduces tools to automatically replay and update proof scripts.

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 is an active iOS developer.  He has 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.  He also does iOS development contracts and has many clients.