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|
- 2013-10-24: assigned time for the tutorials and office hours
- 2013-10-12: updated requirements
- 2013-09-24: the website is online
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)
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.
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.