Informazioni sul corso

Time and Location

• Lecture: Wednesdays, 2:00 PM - 4:00 PM
• Exercise Sessions: TBD 

Prerequisites

This advanced course for MSc and PhD students requires having attended the Proofs are Programs course or at least having a working knowledge of the contents of the Logical Foundations book, including familiarity with logic, mechanized proofs, and functional programming in the Coq proof assistant.

Course Description

Complex proofs on paper are difficult to write, check, and maintain. This holds not only for interesting proofs in mathematics, but also for complex formal proofs about interesting programs. For this reason, machine-checked proofs created with the help of interactive tools called proof assistants are gaining increased traction in academia and industry. Proof assistants have been used to prove the correctness and security of realistic compilers, operating systems, cryptographic libraries, or smart contracts, and also to construct machine-checked proofs for challenging mathematical results.

This course will use the Coq proof assistant [2] to lay down the foundations of Programming Languages, Verification, and Security. The Coq proof assistant enables us to program formal proofs interactively and it machine-checks the correctness of the proofs along the way. We will use Coq to define the syntax and semantics of imperative and functional programming languages, to define type systems, and to prove theorems such as type soundness. We will also formalize Hoare Logic and Relational Hoare Logic in Coq and use them to prove the correctness and security of simple imperative programs. Finally, the course will introduce static and dynamic enforcement mechanisms for Secure Information Flow Control and Cryptographic Constant Time as well as their formal noninterference guarantees.

This hands-on course is based on the Programming Languages Foundations online textbook [1], which is itself formalized and machine-checked in the Coq proof assistant. The many exercises in each book chapter are to be solved weekly mostly in Coq, from easy exercises allowing the students to practice concepts from the lecture, building incrementally to slightly more interesting programs and proofs and also to various optional challenges.

Learning Outcomes

After successful completion of this course, students will be able to

• understand how to define in Coq the syntax of simple programming languages, in particular variants of a simple imperative language and of the simply-typed lambda calculus;
• define the big-step and small-step operational semantics of such simple languages;
• formally define type systems for such languages as inductive relations;
• work out the metatheory of such languages, by proving results such as type soundness;
• understand the semantic foundations of Hoare Logic and Relational Hoare Logic;
• use Hoare Logic for verifying the correctness of simple imperative programs, both formally in Coq and informally on paper;
• understand the semantic foundations of Secure Information Flow Control and Noninterference.
• use Relational Hoare Logic for proving program equivalence as well as Noninterference of simple imperative programs;
• be familiar with static and dynamic enforcement mechanisms for Secure Information Flow Control as well as their formal noninterference guarantees (e.g. security type systems, secure multi-execution, etc.);
• understand how to formalize Cryptographic Constant Time in Coq;
• apply different proof techniques in Coq (e.g. induction on rule derivations, proof automation).

Requirements for getting credit points

There will be a mandatory written final exam (120 minutes) that counts for 100% of the grade. In addition there will be weekly exercise sheets that are crucial for preparing for the exam and that, when submitted on time, count for bonus points, up to 20% of the final grade. We will also have an optional midterm exam that helps students practice for the final exam, but only counts for bonus points, up to 10% of the final grade.

To pass the course and receive credit points one has to attend the final exam and the weighed sum of your scores including bonus points (which can add up to a maximum of 130%) has to be at least 50%.

Which students can attend this course and get official credit?

• Computer Science MSc students
• IT Security MSc students
• Mathematics MSc students ("Nebenfach Informatik")
• CASA PhD students -- attendance requirement is to reach 50% of the points in the exercise sheets

BSc students in CS and ITS can only take this as a free elective, ger. “Freier Wahlbereich”. If you are in another program and still want to attend the course for credit please get in touch with us and the examination office.

eCampus page

• TBD

Literature

[1] Software Foundations, Vol. 2: Programming Languages Foundations. Benjamin C. Pierce et al.

[2] The Coq Proof Assistant.

[3] Security Foundations. Catalin Hritcu and Roberto Blanco.