コース情報

Complex proofs on paper are difficult to construct, 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 theorems in mathematics.

This course introduces the Rocq proof assistant [3] and explains how to use it to prove properties about functional programs and inductive relations, how to formally define a simple imperative programming language, and how to securely enforce information-flow control for functional and imperative programs, including against side-channel attacks. The Rocq proof assistant enables us to program formal proofs interactively and it machine-checks the correctness of the proofs along the way. The design of the Rocq proof assistant itself exploits a beautiful connection between programs in typed functional programming languages and proofs in constructive logics, which is known as the Curry-Howard Correspondence [4]. This deep connection between programs and proofs should make this course interesting to not only to computer scientists, but also to mathematicians and other scientists. The goal is to demystify proofs as just programs in an elegant programming language, for which the course provides a gentle introduction. The course also shows that proofs are not only a way to convince a human reader, but they can actually be fully formalized in a proof assistant like Rocq and automatically checked by a computer.

This hands-on course is based on the Logical Foundations [1] and Security Foundations [2] online textbooks, which are themselves formalized and machine-checked in the Rocq proof assistant. The many exercises in each book chapter are to be solved weekly mostly in Rocq, 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

• develop purely functional programs using recursive functions on numbers, lists, maps, and various kinds of trees, including the abstract syntax trees of programs;
• use functional programming concepts such as type polymorphism and higher-order functions, which are increasingly becoming mainstream;
• formally state and prove theorems in the Rocq proof assistant;
• apply different proof techniques in Rocq and in informal paper proofs (e.g. equational reasoning, contradiction, case analysis, induction on natural numbers, lists, and trees, induction on rule derivations, proof automation);
• define new inductive types and relations in Rocq and prove statements about them;
• comprehend how the syntax and semantics of simple imperative programs can be formally defined in Rocq and how to prove theorems about such programs and languages;
• understand how the absence of information leaks can be formalized as a security property called noninterference and enforced using secure-multi execution or simple type systems;
• formalize the Cryptographic Constant-Time semantic security property against certain timing side-channel attacks and enforce it using a simple type system;
• (optional for BSc students) learn about Spectre attacks and how to formalize the Speculative Constant Time property and the Speculative Load Hardening (SLH) program transformation in Rocq.

No Prerequisites

The lecture is intended for a broad range of students, from motivated BSc students to MSc and PhD students. No specific prior knowledge in logic, programming, functional programming, or programming languages is assumed, though a degree of mathematical maturity is helpful.

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 10% 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 120%) has to be at least 50%.

Which students can attend this course and get official credit?

• Computer Science MSc and BSc students
• IT Security MSc and BSc students (ITS BSc students can only take this as a free elective, ger. “Freier Wahlbereich”)
• Mathematics MSc students ("Nebenfach Informatik")
• CASA PhD students (attendance requirement is to reach 50% of the points in the exercise sheets)

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.

Literature

[1] Benjamin C. Pierce et al. Software Foundations, Vol. 1: Logical Foundations: https://softwarefoundations.cis.upenn.edu/lf-current

[2] Catalin Hritcu and Yonghyun Kim. Software Foundations, Vol. 7: Security Foundations: https://softwarefoundations.cis.upenn.edu/secf-current

[3] The Rocq Interactive Theorem Prover: https://rocq-prover.org

[4] Philip Wadler: Propositions as types. Commun. ACM 58(12): 75-84 (2015) https://doi.org/10.1145/2699407