CMSC 838G, Spring 2016

Mechanized Proof and Verified Software


Instructor Michael Hicks
CSI 3118 Tues/Thurs 2:00-3:15pm
Office Hours: By appointment AVW 3417
Schedule | Piazza Discussion | Syllabus | Course Description | Project | Resources

Schedule

Upcoming

Current

The initial material is based on Software Foundations (v4.0), but is slightly more recent. Therefore, some of the future material linked on the Software Foundations web site may change; the above-linked material is primary. Discussions and announcements on Piazza (sign up, if you haven't already). See Resources section below for useful information on Coq and Proof General.

Course Description

Overview

Most software is rigorously tested before it is deployed. But testing is not enough, not even in practice, as the well-known litany of bugs and security vulnerabilities in mature software attests. If you want high assurance that your software does what it is supposed to (or that it does not do what it is not supposed to), you need to look beyond testing. This course is focused on technology to assist in the development of high-assurance proofs about important properties of software, e.g., those regarding its security.

Outline

This course will be divided into roughly three parts.

During the first part, we will focus on developing formal proofs using the Coq proof assistant. Normally, when we think of a "proof", we think of an informal English description of an argument. But such English descriptions may have mistakes that go undetected, and so informal proofs do not provide the high assurance we want. To do better, a "proof" will be a formal object that we will construct with the assistance of Coq, which will ensure that the proof is valid. By valid, we simply mean that each step in the proof follows from the basic rules of a given (higher-order) logic, and that taken together, the steps allow us to conclude that the given property holds.

Modern proof assistants, such as Coq, provide a uniform environment for writing code, models of systems and mathematical objects, logical specifications, and proofs. Programs in Coq are written in a typed, functional language similar to OCaml, except that the type system is much more powerful. That extra power is used to reflect specifications and logical (math) properties as types, while proofs are represented as functional expressions that build evidence of the validity of a given specification. In this fashion, Coq is able to reduce proof-checking to a form of type-checking. In other words, the type-checker of Coq prevents you from assembling a purported proof unless the proof is actually valid.

We will use portions of Pierce et al's Software Foundations as our roadmap for experience with Coq. We may also refer to parts of Chlipala's Certified Programming with Dependent Types.

For the second part, we will widen the net and look at different tools and technologies, in particular, at Bedrock, F-star, Dafny, Frama-C, and perhaps other tools, depending on the interests of the students in the class. We expect to spend a 2-3 class lectures or so on each of these. The goal here is to learn enough about each tool to get a sense of its strengths and weaknesses, especially as compared to other tools. Students will participate in presenting tools they find most interesting.

The final phase of the course will be focused on individual projects. By this point, students will have learned enough about the space of possibilities to pick a topic area to dig into more deeply, e.g., by using it to build some verified software, or to formalize an idealized system and prove metatheoretic properties about it. While students are working on their projects, class time will consist for further delving into the advanced topics begun in the second third of the class.

Syllabus

Prerequisite: There is no official prerequisite for this class (beyond an undergraduate CS degree); we will attempt to make it largely self-contained. However, as Coq is a functional programming language, some familiarity with functional programming will be important (ideally, with OCaml). Students should also feel comfortable with mathematical thinking and pencil-and-paper proofs (or be willing to put in the time to get better). We will also be reading some technical papers from the programming languages research literature, so having taken CMSC 631 will be helpful. That said, we will review programming languages concepts crucial for understanding particular papers prior to reading them. Contact the instructor if in doubt.

Grading: Graded work is as follows:

Presentations: Students making presentations will be graded on the following criteria: Remember that you will likely be able to explain more detail than you can hope to cover in a single lecture. This is one reason that it's hard work to prepare a good presentation: not only do you need to understand the paper, but you need to filter out the irrelevant details and amplify the key arguments. You'll probably have omit entire sections of the paper from your talk -- don't worry about it. Simply mimicking the structure of the paper ("regurgitating it") tends to produce a disconnected sequence of boring facts. A good talk should tell a story; every idea should be motivated, and all facts should fit together in a coherent picture. Telling such a story in a short time often requires creating your own explanations, motivation, and examples. I would recommend reading some advice by Simon Peyton Jones on giving good presentations.

Academic Dishonesty: The university policy on academic dishonesty is strictly followed. All graded materials (whether exams, summaries, presentations, or projects) must be strictly individual efforts. In the case of a group project or assignment, only collaborations within the group are permitted.

Project

Each student will complete a final project. Projects, done individually or in groups, will be defined according to the participants' own interests. A student may choose to work on verified data structures or algorithms, protocols, etc., or may formalize some basic results from mathematics, programming languages theory, etc. (e.g., perform the formalization in a published paper in Coq, reproducing its results with higher assurance).

Possible project topics should be discussed with the instructor prior to submitting a proposal, to make sure they are in scope. The final project writeup is due May 17. The project proposal should be submitted by April 7, by e-mail. It should be 1-2 pages in length, and consist of the following components:

One example project might be to mechanize the metatheory of Miller et al's paper on authenticated data structures (ADS). The first paragraph of the proposal would review what Miller's scheme is. The second would state the goal for the project: To mechanize the metatheory of the paper; in particular to mechanize, in F* (say), the definitions of the operational semantics, type system, auxiliary mathematics, and proof of security and correctness. Then would come the bullet list, listing the tasks to be undertaken each week. Finally would come the listing of the deliverable: A report describing the artifact produced and the process and pitfalls, along with the artifact itself and how the instructor can use it to check the results.

Resources

Using Coq

Reading papers

Here is some useful advice about how to read papers. Once you get in the groove, you should expect to spend 1-3 hours per paper (you do not need to understand every detail, especially for the longer papers).