Foundations of Programming Languages, Verification, and Security (SoSe2025)

Time and Location

• Lecture: Wednesdays, 14:15 - 15:45 (starting on 9 April) 
  • Starting on April 30 the lecture will take place in building MB, floor 5, room SM-MO-506 (an MPI-SP seminar room, the same as for the Q&A session below).
    • Building MB was formerly 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 up 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.
  • 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 lecture physically whenever possible. When you cannot attend the lecture in person here is the Zoom room you can use (also for the exercise sessions): <<please join the course on Moodle for link; non-RUB students can create an account with their email for that>>
• Q&A exercise sessions: Tuesdays, 10:15 - 11:45 (starting on 15 April)
  • The exercise sessions will take place in person in building MB, floor 5, room SM-MO-506 (an MPI-SP seminar room).
    • Building MB was formerly 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 up 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.

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.

Content

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 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 as well as their formal noninterference guarantees. Finally we will formalize Cryptographic Constant Time and Speculative Constant Time and prove in Coq that a software defense called Speculative Load Hardening (SLH) achieves Speculative Constant Time.

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, Speculative Constant Time, and Speculative Load Hardening (SLH) in Coq;
• apply various proof techniques both in Coq and in informal paper proofs (e.g. induction on rule derivations) or just in Coq (e.g. proof automation).

Literature

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

[2] The Coq Proof Assistant: https://coq.inria.fr (recently renamed to Rocq, but we will use v8.18 which is still called Coq)

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

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

• Link to eCampus page