Type Systems for Security Verification

Advanced Lecture, Winter 2014/15

Instructor Prof. Dr. Matteo Maffei, Dr. Catalin Hritcu (INRIA, Paris-Rocquencourt)
Teaching Assistant Niklas Grimm
Dates Block course, daily for two weeks, March 16-27, 9am-1pm.
Place E1.3, Room 003
Form/Credits Advanced Course, 6 ECTS
Language English

Description

Type systems constitute a state-of-the-art static analysis technique for security-critical code. They can certify the security of all possible program executions at compilation time, thereby avoiding run-time overhead typical of monitoring techniques; they enjoy modularity, and thus scale well to large programs; and they can be used to verify a number of different security properties, both trace- and indistinguishability-based ones.

The lecture will provide hands-on experience on F*, a new ML-like functional programming language designed with program verification in mind. It has a powerful refinement type-checker that discharges verification conditions using the Z3 SMT solver. F* has been successfully used to verify nearly 50,000 lines of code, ranging from cryptographic protocol implementations to web browser extensions, and from cloud-hosted web applications to key parts of the F* compiler itself. The newest version on F* erases to both F# and OCaml, on which it is based. It also compiles securely to JavaScript, enabling safe interoperability with arbitrary, untrusted JavaScript libraries.

The initial part of the course is based on the F* tutorial, which was also used for teaching at the Joint EasyCrypt-F*-CryptoVerif School 2014 and at POPL 2015.

Course Materials

The course materials are available here .

Grading

The grading is based on homework (2/3) and project (1/3).

Requirements

A background in functional programming languages and verification is very helpful for this advanced course. It is thus highly recommended to have attended some related courses, such as Introduction to Computational Logic, Semantics, Parametricity and Modular Reasoning, Security, and Logics in Security. Motivated students without this background are also welcome to the course, but we certainly expect more spirited efforts from you.

Registration

Students should register for the course through the HISPOS system. In addition, we will be using Piazza to publish lecture notes and assignments as well as for class discussion. Therefore, students should also register in Piazza for the course here. Please let us now if you face any problem with registration.