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.
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.
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.
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:
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.
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.
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).