Language-Based Security

Advanced Lecture, Winter 2013/14

Instructor Prof. Dr. Matteo Maffei
Teaching Assistant Ilya Grishchenko
First Lecture Wednesday, October 16, 2013 2-4 pm
Time and Place Wed 2-4 pm, E1.3 (HĂ–RSAAL III), room 0.03.1
First Tutorial Tuesday, October 29, 2013 2-4 pm
Time and Place Tue 2-4 pm, E1.7 (MMCI), room 3.23
Office Hours Mon 4-6 pm, E1.7 (MMCI), room 2.09
Form/Credits Advanced Lecture, 6 ECTS
Language English
Contact ilyagri(at)mpi-inf.mpg.de

Latest News

  • 2013-10-24: assigned time for the tutorials and office hours
  • 2013-10-12: updated requirements
  • 2013-09-24: the website is online

Description

The former security mechanisms were typically defined and implemented at the level of operating systems. However, the increasing complexity of modern operating systems and security requirements makes the enforcement of security by exclusively reasoning at operating-system level very difficult. For instance, many attacks (think, e.g., of worms, malicious apps, cryptographic protocol vulnerabilities) work at application-level and, consequently, typically succeed in circumventing low-level security policies (e.g., file access permissions) by running on behalf of trusted users. An elegant and very effective approach for tackling this problem is to specify and verify security policies at application-level and, more precisely, on the programming languages used for developing the applications of interest. For this reason, this area is known as language-based security.

This course will present methods and tools to certify security and privacy properties of programs, distributed systems, and mobile apps. We will focus, in particular, on static analysis techniques (e.g., type systems and abstract interpretation), which work by analyzing the program code and performing an abstraction of its semantic behavior. The advantage of these techniques is that they provide security guarantees at installation time, without causing any run-time overhead.

In this course, you will learn how to

  • verify security and privacy properties of cryptographic protocols (e.g., how to use a type system to analyse real-world protocols like Kerberor or SSH)
  • verify security properties at source-code level (e.g., on F# and C programs)
  • verify security properties at assembly-code and byte-code level (e.g., how to check whether or not your Android apps leak sensitive data)
  • use general-purpose program verification tools (e.g., refinement type systems, Z3, and others)

The lecture notes and assignments will be placed on Piazza.

Assignments, Exams, and Grading

Assignments will be handed out every second week.

In order to be admitted to the exam, you have to get 50% of the points in the assignments overall.

To pass the course you have to score 4.0 or better in the exam. The exam will be oral or written depending on the number of participants.

Requirements

You should enjoy math and theoretical computer science!

This will be an advanced course and we expect some background in security and semantics. It would be ideal if you have taken one of these lectures at Saarland University or during your previous studies somewhere else. Motivated students without this background are anyway welcome to the course, although they might have to put some more spirited efforts.

How to register

As usual, you have to register in the LSF/HISPOS system of the university. There is no internal registration required. However, in order to access the material like lecture notes and assignments, you will have to sign on to Piazza.