CIS 700: Software and Compiler Verification

University of Pennsylvania     Fall 2005

315 Levine Hall
Monday and Friday 1:30 - 3:00pm
Instructor: Steve Zdancewic



Synopsis

Software flaws, such as buffer overflows, account for the vast majority of security vulnerabilities exploited by viruses, worms and other forms of malicious software that are becoming pervasive and costly. Buggy code creates other expenses as well: for developers, additional costs include debugging, testing, and patching; for consumers, additional costs include lost productivity and lost revenue due to down time. The U.S. Dept. of Commerce Planning estimates that reduction in easily avoidable program errors could save between $22 and $60 billion per year in the U.S. alone.

Programming languages and compilers researchers have attacked the problem of preventing software flaws from many angles, including type systems and other static analyses. However, to ensure that no bugs are introduced into the deployed system, some form of verification must be applied at all levels, from the source program and its specification, to the final assembly code running on the hardware. Applying formal verification techniques of this kind on the large scale are beyond our current technology, but much progress has been made since the problem was first articulated in the 1960's. Building a "verifying compiler" (one that proves the generated program is correct with respect to a formal specification) has been proposed by Tony Hoare as a Grand Challenge problem for Computer Science, and there is much active work in the area.

This course will survey the historic and current approaches to verifying compilation, focusing on the programming language and compiler aspects of the problem, but also touching on related subjects such as theorem proving and software model checking. The course material will primarily focus on the research literature, with papers presented both by the instructor and class participants. The reading selection will range from classics, such as Tony Hoare's 1969 paper "An Axiomatic Basis for Computer Programming" to more recent work such as Morrisett et al.'s "From System F to Typed Assembly Language".

Grades will be based on class participation, the presentation of papers in class, and (possibly) a course project.


Course Schedule

Date Topic Presenter
Sept. 7 Introduction / Axiomatic Semantics
The Verifying Compiler: A Grand Challenge for Computing Research (Hoare, 2003)
Zdancewic
Sept. 12 Axiomatic Semantics
An Axiomatic Basis for Computer Programming (Hoare, 1969)
Zdancewic
Sept. 14 Weakest Preconditions / Verification Conditions
Winskel, Chs. 6 & 7

The characterization of semantics Chapter 3 of "A Discipline of Programming" (Dijkstra, 1976)

Zdancewic
Sept. 19* Separation Logic: A Logic for Shared Mutable Data Structures (Reynolds, 2002) Brian Aydemir
Sept. 21* Separation Logic and Abstraction (Parkinson & Bierman, 2005) Alwyn Goodloe
Sept. 26* BI as an Assertion Language for Mutable Data Structures (Ishtiaq & O'Hearn, 2001)

The logic of bunched implications (O'Hearn & Pym, 1999)

Karl Mazurak
Sept. 28* Proof-Carrying Code (Necula, 1997)  
Oct. 3* From System F to Typed Assembly Language (Morrisett et al., 1999)  
Oct. 5* Foundational Proof-Carrying Code (Appel, 2001)  
Oct. 10* A Certifying Compiler for Java (Colby et al., 2000)  
Oct. 12* Proof Generation in the Touchstone Theorem Prover (Necula & Lee, 2000)  
Oct. 17 No class -- Fall Break  
Oct. 19 Report from the verified software meeting Zdancewic
Oct. 24 Extended Static Checking for Java (Flanagan et al., 2002) Sebastian Burckhardt
Oct. 26 An Overview of JML Tools and Applications (Burdy et al, 2005)

Lessons from the JML Project (Leavens and Clifton, 2005)

Margaret Delap
Oct. 31 The Spec# Programming System: An Overview (Barnett, Leino, and Schulte, 2004)

Verification of Object-oriented Programs with Invariants (Barnett et al., 2004)

Pavol Cerny
Nov. 2 Praxis SparkAda publications

Correctness by Construction: Developing a Commercial Secure System (Hall and Chapman, 2002)

Is Proof More Cost-effective than Testing? (King et al., 2000)

Justin Smith
Nov. 7 Enhancing Server Availability and Security Through Failure-Oblivious Computing (Rinard et al., 2005) Brian Aydemir
Nov. 9 A Language-based Approach to Functionally Correct Imperative Programming (Westbrook, Stump, and Wehrman, 2005) Geoff Washburn
Nov. 14 Dynamically discovering likely program invariants to support Program Evolution (Ernst, et al., 2001) Zdancewic
NOTE: Meet in room 512.
Nov. 16 A Logical Analysis of Aliasing in Imperative Higher-order Functions (Berger, Honda, and Yoshida, 2005) Alwyn Goodloe
Nov. 21 Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant (Leroy, 2006) Aaron Bohannon
Nov. 23 No class -- Thanksgiving Break  
Nov. 28 Lazy Abstraction (Henzinger, et al., 2002) Sebastian Burckhardt
Nov. 30 Shape Analysis (Wilhelm, Sagiv and Reps, 2000) Jeff Vaughan
Dec. 5 Synthesis of Interface Specifications for Java Classes (Alur et atl., 2005) Pavol Cerny
Dec. 7 Discussion about Software Verification Zdancewic
* Prof. Zdancewic will be absent