Skip to main content.
Language-based Security
Advanced Lecture in Winter Term 2008/09

Teaching Assistants
Fabienne Eigner (fabie
fm12agzhs7
nne@stu
28vrgfd8eh
d.uni
1ypamgsx5r
-saarland.de)
Kim Pecina (pecina@
iondy7zngw
mmc
6islj6zaap
i.uni-s
omedo8ez9w
aarland.de)
Lecture
Wednesday 14-16, E1.3, HS 002
Turorial
Monday 14-15, E 1.3, SR 14
Course Material
Slides and papers suggested during the course
Language
English
Contact
maffei@cs.un
qruzndwtos
i
h8s93vpjrg
-sb.de
34pjxu72dz

Latest News

Course Material

LBS Reference containing the grammar, the semantics, and the typing rules of the type systems and calculi covered in the lecture.
Examples used in the ProVerif lecture: Example 1 Example 2 Example 3 Example 4

Date Topics Slides Homework Solutions References
10/22/2008 Introduction Information Flow PDF, PDF-4up
PDF, PDF-4up
Language-Based Information-Flow Security
(Sabelfeld and Myers, 2003)
10/29/2008 A Type System for Secure Information Flow PDF, PDF-4up PDF PDF Principles of Secure Information Flow Analysis
(Smith, 2006)
11/5/2008 Probabilistic Non-interference PDF, PDF-4up PDF PDF Probabilistic Noninterference for Multi-threaded Programs
(Sabelfeld and Sands, 2000)
11/12/2008 Tools: Visualizer for Information Leaks and Jif PDF, PDF-4up Link Visualizer (Martin Bättig, 2005)
Jif
11/19/2008 Typed Assembly Language (TAL-0) PDF, PDF-4up PDF PDF Chapter 4 of Advanced Topics in Types and Programming Languages (Benjamin Pierce)
TAL home page
11/26/2008 Typed Assembly Language (TAL-1) PDF, PDF-4up PDF PDF Chapter 4 of Advanced Topics in Types and Programming Languages (Benjamin Pierce)
TAL home page
12/03/2008 Proof Carrying Code (Part I) PDF, PDF-4up PDF PDF Chapter 5 of Advanced Topics in Types and Programming Languages (Benjamin Pierce)
PCC home page
12/10/2008 Proof Carrying Code (Part II)
Edinburgh Logical Framework
PDF, PDF-4up PDF PDF Chapter 5 of Advanced Topics in Types and Programming Languages (Benjamin Pierce)
PCC home page
12/17/2008 Applied Pi-calculus (Part I) PDF, PDF-4up PDF PDF Mobile Names, New Values, and Secure Communication (Abadi and Fournet, 2001)
01/14/2009 Applied Pi-calculus (Part II) PDF, PDF-4up PDF PDF
01/21/2009 ProVerif (Part I) PDF, PDF-4up PDF TGZ ProVerif
01/28/2009 ProVerif (Part II)
Electronic Voting (Part I)
PDF, PDF-4up
PDF, PDF-4up
PDF PDF
TGZ
ProVerif
Analysis of an electronic voting protocol in the applied pi-calculus (Kremer and Ryan, 2005)
02/04/2009 Electronic Voting (Part II) PDF, PDF-4up Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol (Michael Backes, Matteo Maffei and Dominique Unruh, 2008)
Automated Verification of Electronic Voting Protocols in the Applied Pi-calculus (Michael Backes, Catalin Hritcu, and Matteo Maffei, 2008)
02/11/2009 Refinement Types PDF, PDF-4up A Type Discipline for Authorization in Distributed Systems (Cedric Fournet, Andy Gordon, Sergio Maffeis, 2007)

Office hours

Dr. Matteo Maffei will be available for your questions on Tuesday from 3pm to 4pm in building E 1.1, room 2.16.

Kim Pecina will be available for your questions on Monday from 1pm to 2pm in building E 1.1, room 2.15.

Description

What is language-based security?
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 modern attacks (e.g., worms and virus) 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 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.

Who should attend this course?
Would you like to...

If you are interested in some of the aforementioned topics, then this course is for you!

Prerequisites

Basic knowledge of operational semantics is useful, but not utterly necessary, as it can be acquired during the course.

Quizzes and Exam

The back-up exam will take place on 2nd of April from 14:00-16:00 sharp in lecture hall 002 in E 1.3. Everybody admitted to the final exam is also admitted to the back-up exam. If you passed both the final and the back-up exam, the better of the two grades will count as your final grade.
Please notify us if you intend to take the back-up exam to give us an indication on how many people will participate.

The exam inspection is scheduled for Thursday, 5th of March from 10:00 to 12:00 in room 2.18 building E 1.1.

Percentage < 50.0% ≥ 50.0% ≥ 54.5% ≥ 59.0% ≥ 63.5% ≥ 68.0% ≥ 72.5% ≥ 77.0% ≥ 81.5% ≥ 86.0% ≥ 90.5%
Grade 5.0 4.0 3.7 3.3 3.0 2.7 2.3 2.0 1.7 1.3 1.0

Every second week, starting from 12.11.2008, there will be a brief quiz in the fist part of the tutorial (approx. 15 minutes). Quizzes will affect your final grading by 30%, and you need an overall quiz-grading of at least 50% to pass the course. Your overall quiz-grade is determined by dropping the quiz with the lowest grading, and calculating the average of the remaining quizzes. The final exam will be a written test of two hours. It will make up 70% of your final grade and you need at least 50% to pass the course.