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|
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 course materials are available here .
The grading is based on homework (2/3) and project (1/3).
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.
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.