Foundations of Programming Languages, Verification, and Security (WiSe 2023/24)

Time and Location

  • Lecture: Thursdays, 10:00 AM - 12:00 PM (from 12 Oct to 1 Feb)
  • Exercise Sessions: Wednesdays, 2:00 PM - 4:00 PM (from 18 Oct to 31 Jan)

For everyone's benefit, we would like this to remain a mostly in-person course, so to get the best out of it, we encourage everyone to attend the course physically whenever possible.

Both the lecture and the exercise sessions will take place in building MB, foor 5, room SM-MO-506 (an MPI-SP seminar room).

  • Building MB is also known as Technologiezentrum Ruhr (or TZR). Please enter via the main MB entrance, which faces the MC building and the parking lots between MC and MB. Then take the glass elevator right next to the entrance (or the stairs) to floor 5. On floor 5 enter the open door of the Max Planck Institute for Security and Privacy (MPI-SP) and the seminar room is only a few steps away. Should the MPI-SP door be closed, please ring the bell and someone will open for you.

When you cannot attend in person you will be able to join via Zoom (please enroll for the course on Moodle to see the link).

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 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: variants of a simple imperative language and 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).

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.

Requirements for getting credit points

There will be a mandatory written final exam (120 minutes) that counts for 60% of the grade and weekly exercise sheets that have to be submitted on time and that count for 40% of the 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. One can additionally get bonus points up to 5% of the final grade by solving all exercise sheets.

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 115%) 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 (where because of bonus points the maximum is 112.5%)

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

Literature

  1. Software Foundations, Vol. 2: Programming Languages Foundations. Benjamin C. Pierce et al.
  2. The Coq Proof Assistant.
Semester: WT 2023/24