CSI 3118 Tues/Thurs 2:00-3:15pm

Office Hours: By appointment AVW 3417

Schedule | Piazza Discussion | Syllabus | Course Description | Project | Resources

- May 11-13 -
**Take-home exam**

- May 17 -
**Project due**

- May 10 - Project presentation: Nick, Nikos, Phil, Ian

- May 5 - Project presentations: Milod, Ugur, Andrew

- May 3 - Boogie (Phil Nguyen)
- Boogie: A Modular Reusable Verifier for Object-Oriented Programs
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- Apr 28 - Grab bag (Nikos Kofinas)
- Apr 26 - CompCert (Milod Kazerounian)
- Apr 21 - Verdi (Nick Labich)
- Apr 19 - Qed and Why3 (Ugur Koc)

- Apr 14 - VellVM (Andrew Ruef)

- Apr 12 - Verified Software Toolchain

- Verification
of a Cryptographic Primitive: SHA-256 (Ian Sweet)

- Reference: Verified
Software Toolchain

- Apr 7 - Project proposal due
- Details of the format of the proposal given below.

- Paper to read: Propositions as Types
- Apr 5 - Frama-C
- In-class: Frama-C tutorial slides, examples.tgz
- Detailed Frama-C WP tutorial
- WP-plugin user manual
- Mar 29, 31 - F-star
- In class: F-star tutorial
**Homework, due April 12**@ 2pm: Fill in all of the admits in fstar_hw.fst (refer to fstar_hw.txt for help understanding the definitions)

- Mar 24 - Certified
Programming with Dependent Types

- To
**discuss in class**: Chapter 2 (a verified stack compiler) - Homework,
**due April 5**@ 2pm*(Updated 9am, 3/31, to be compatible with Coq 8.4)*

- Mar 22 - Certified
Programming with Dependent Types

- To
**discuss in class**: Sections 13.1, 14.1, 14.2 (Proof automation)

- Files LogicProg.v and Match.v

- Mar 15, 17 -
**Spring Break**(no class!) - Mar 10 - ProofObjects.v (HTML)
- Exercises for class (and homework
**due March 22**@ 2pm): eight_is_even, conj_fact, or_commut'', leibniz_equality - Mar 8 - Dafny

- In class: The Dafny Tutorial
- Required reading (to
**discuss Mar 10**): Ironclad apps: End-to-end Security via Automated Full-System Verification

- Recommended viewing: The
*Loop Invariants*lecture at The Verification Corner - Optional reading: Getting Started with Dafny
- Homework,
**due March 22**@ 2pm. - Mar 3 - Hoare2.v (HTML)
- Exercises for class (and homework,
**due March 8**): if_minus_plus_reloaded, slow_assignment, parity_formal, wp, is_wp_formal (you can skip the units on Formal Decorated Programs and beyond).

- Mar 1 - Hoare.v (HTML) - you might find this crib sheet on notation useful
when working the proofs

- Exercises for class (and homework,
**due March 8**): assertions, valid_triples, hoare_asgn_examples, hoare_asgn_example4, swap_program, if_minus_plus (extra credit: hoare_repeat) - Feb 25 - Equiv.v (HTML)
- Exercises for class (and homework,
**due March 1**): equiv_classes, skip_right, IFB_false, WHILE_true, CIf_congruence. You don't have to read the Optional part about not dealing with Extensionality - Feb 23 - Imp.v (HTML)
- Requires SfLIb.v
- Go through the above file by the start of class, Feb 23. We
will use class time to work on the following exercises (
**due March 1**): optimize_0plus_b, ceval_example2, loop_never_stops, stack_compiler (extra credit: stack_compiler_correct). - Feb 18 - Maps.v (HTML)
- Assignment,
**due Feb 23**: Do all 2-star exercises (there are five of them) - Feb 16 - IndProp.v (HTML)
- Assignment,
**due Feb 23**: Do all 1-star exercises, and ev_sum, ev_ev__ev, total_relation, empty_relation, le_trans, le_plus_l, leb_correct (for this one, you may want to use earlier lemmas), exp_match_ex1, reflect_iff - Feb 11 - Logic.v (HTML)
- Assignment,
**due Feb 16**: Do all non-optional, non-advanced 1-star exercises, and and_exercise, and_assoc, contrapositive, iff_trans, or_distributes_over_and, dist_exists_or, In_map_iff, All, logical_connectives - Feb 9 - Tactics.v (HTML)
- Assignment,
**due****Feb 16**: Do apply_exercise1, apply_rewrite, trans_eq_exercise, plus_n_n_injective, beq_nat_true, gen_dep_practice, bool_fn_applied_thrice, beq_nat_sym - Feb 4 - Poly.v (HTML)
- Review (to do in class): Lists_review.v

- Assignment,
**due Feb 9**: Do all 1-star exercises, mumble_grumble, poly_exercises, rev_app_distr, split, flat_map. Extra credit: do church_numerals. - Feb 2 - Lists.v (HTML)
- Review (to do in class): Induction_Basics_review.v

- Assignment,
**due Feb 9**: Do all 1-star exercises, all recommended exercises, and list_exercises and beq_natlist. - Jan 28 - Induction.v (HTML)
- Assignment,
**due Feb 2**(at 2pm): Do all 1-star exercises in Induction.v, as well as basic_induction, double_plus, mult_comm, more_exercises (only the first three), and binary_commute - Jan 26 - Preface (HTML) and Basics.v (HTML)
- Assignment,
**due Feb 2**(at 2pm): Do all 1-star exercises in Basics.v, as well as mult_S_1, andb_true_elim2, and boolean_functions

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.

- Project proposal, April 7

- Take-home final exam, May 11-13
- Project final writeup, May 17

**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:

- Homeworks (40%) There will be several problem sets in Coq in
the first 1/3 of the course, and 1-2 other problem sets during
the last third.

- Class participation (5%). Students are expected to come to
class and participate in discussions. Many times, class periods
will involve lectures and exploration of new tools, and students
will be expected to contribute presentations about tools of
interest. Grading criteria for in-class presentations are given
below.

- Project (25%). Students will propose projects approximately two months into the semester, to be completed by the end of the semester (during its last 5 weeks). More details below.
- Final Exam (30%). There will be a comprehensive final exam, which will count for comp credit.

**understanding**: does the presenter understand the material?**thoughtfulness**: does the presenter have insights and opinions beyond what was in the paper?**background/perspective**: did the presenter read background papers?**clarity**: can the audience understand the presentation? is the "big picture" clear? are there useful examples?**materials**: do the slides or use of blackboard illustrate and support the talk? are there diagrams to help convey the technicalities? (when your talk gets into deep territory, a diagram is worth 10K words)**delivery**: has the the presenter practiced?**non-regurgitation**: did the presenter do something beyond simply typing sections of the paper as bullet points? did the presenter motivate the ideas in their own words or just state ideas from the paper verbatim?**answering questions**: can the presenter handle questions from the audience?

**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:

- Problem context and project goal (1-2 short paragraphs).
- Approach (1 paragraph)
- Per-week timeline (bullet list covering 6 weeks, up to May 17)
- Final deliverable, if any, to accompany final report (bullet)

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.

- Coq homepage

- Tactic cheat sheet (thanks to Arthur Azevedo de Amorim and Robert Rand)
- Proof General,
and documentation.
Useful key bindings:

- C-c C-RET : Processes (or reverts) to the cursor
- C-c C-n : Processes the next definition/element
- C-c C-u : Undoes processing of the last element
- C-c C-BS : Undoes
*and deletes*the last element

- C-c C-b : Processes the entire buffer
- C-c C-r : Reverts all processing so far

- C-C C-. : Enables "electric period" (or disables it) --
immediately processes up to . when entered.

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

- How to read a technical paper by Jason Eisner (JHU)
- How to Read a Paper by Michael Mitzenmacher (Harvard)
- Efficient Reading of Papers in Science and Technology by Michael J. Hanson (and updated by Dylan J. McNamee)