Latest News
- The final exam will take place on February 28th, from 11am to 13:00am, E 1.3, HS 003
- Discussion Board is open.
- Registration is open. De-registration is possible until November 20th, 2006.
Course Material
| Date | Topics | Slides | Homework | Solutions | References |
| 18.10.2006 | Introduction Untyped lambda-calculus |
PDF,PDF-4up
PDF,PDF-4up |
Chapter 5 of Types and Programming Languages (Benjamin Pierce) | ||
| 25.10.2006 | Simply typed lambda-calculus | PDF,PDF-4up | Chapter 9 of Types and Programming Languages (Benjamin Pierce) | ||
| 8.11.2006 | Information flow | PDF,PDF-4up | Try this exercise | Language-Based Information-Flow Security (Sabelfeld and Myers, 2003) and Principles of Secure Flow Analysis (Geoffrey Smith, 2006) | |
| 15.11.2006 | Information flow (arrays and threads) |
PDF,PDF-4up | Lenient Array Operations for Practical Secure Information Flow (Zhenyue Deng and Geoffrey Smith, 2004) and Principles of Secure Flow Analysis (Geoffrey Smith, 2006) | ||
| 22.11.2006 | Jif: Java +information flow | PDF,PDF-4up | Try this exercise | ZIP | Jif web page and Protecting Privacy using the Decentralized Label Model (Andrew C. Myers and Barbara Liskov, 2000) |
| 29.11.2006 | Typed Assembly Language: TAL-0 | PDF,PDF-4up | Chapter 4 of Advanced Topics in Types and Programming Languages (Benjamin Pierce) and TAL home page | ||
| 6.12.2006 | Typed Assembly Language: TAL-1 | PDF,PDF-4up | Chapter 4 of Advanced Topics in Types and Programming Languages (Benjamin Pierce) and TAL home page | ||
| 13.12.2006 | Java Security | PDF,PDF-4up | Securing Java: getting down to Business with Mobile Code (McGraw and Felten), Java Security (Oaks), How the Java virtual machine handles method invocation and return (Bill Venners, 1997), Java Bytecode Verification: Algorithms and Formalizations , (Xavier Leroy, 2003) | ||
| 20.12.2006 | Java Security | PDF,PDF-4up | Merry Christmas... | ...and happy new year! | Securing Java: getting down to Business with Mobile Code (McGraw and Felten), Language-based security for mobile code, with applications to smart cards (Xavier Leroy, 2005), and Understanding Java Stack Inspection (Wallach and Felten, 1998) |
| 10.1.2007 | Security Protocols (Part I) | PDF,PDF-4up | Handbook of Applied Cryptography (McGraw and Felten), SPORE: Security Protocols Open Repository, and A Survey of Authentication Protocol Literature: version 1.0 (Clark and Jacob, 1997) | ||
| 17.1.2007 | Security Protocols (Part II) Concurrency and Spi-calculus |
PDF,PDF-4up
PDF,PDF-4up |
The polyadic pi-calculus: a tutorial (Robin Milner, 1991), A calculus for cryptographic protocols: the spi-calculus (Martin Abadi and Andrew Gordon, 1998) | ||
| 24.1.2007 | Types for Secrecy | PDF,PDF-4up | Secrecy by Typing in Security Protocols (Abadi, 1999), Dynamic Typing for Cryptographic Protocols (Maffei, 2006) | ||
| 31.1.2007 | Authentication Specifications and Types for Authenticity (introduction) | PDF,PDF-4up | Read this paper | A Hierarchy of Authentication Specifications (Gavin Lowe, 1997), Types and Effects for Asymmetric Cryptographic Protocols (Gordon and Jeffrey, 2003) | |
| 7.2.2007 | Static Types for Authenticity | PDF,PDF-4up | Types and Effects for Asymmetric Cryptographic Protocols (Gordon and Jeffrey, 2003) | ||
| 14.2.2007 | Dynamic Types for Authenticity | PDF,PDF-4up | Dynamic Typing for Cryptographic Protocols (Maffei, 2006) |
Office hours
The tutor will be available for your questions on Tuesday from 10am to 11am in building E 1 1, Room U 18.Dr. Matteo Maffei will be available for your questions on Wednesday from 3pm to 4pm in building E 1 1, Room U 22.
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 very difficult the
enforcement of security by exclusively reasoning at operating-system
level.
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.
What is this course about? (please check
for updates)
The course is composed of three parts. The first part will introduce
some
basic notions on lambda calculus, showing the relationship with modern
programming languages such as Java. Furthermore, we will explain some
basic
aspects on type theory, a well-known static analysis technique for
enforcing
safety properties on modern programming languages.
The second part addresses several security issues exploited by modern
attacks
(e.g., memory safety, buffer overflows, the trustiness of distributed
code),
showing how program weaknesses can be detected by means of static
analysis
techniques, with a particular focus on type systems.
The third part concerns the safety of cryptographic protocols, the
de-facto standard of communication over untrusted networks. In particular, we
will present the spi-calculus, a process calculus for modelling distributed
cryptographic communication, and recent static analysis techniques for
proving safety properties over cryptographic protocols.
Finally, we will outline Java security. (e.g., Java bytecode
verifier, security manager, stack inspection.)
Prerequisites
Basic knowledge of operational semantics and type theory is
useful, but not utterly necessary, as it can be acquired during the
course.
Furthermore, you should be interested in some of the following:
- Obtaining a deeper understanding of programming language-based concepts for computer security.
- The design and implementation of security mechanisms.
- Mathematical concepts underlying program verification.
- Computer science research in the area of programming languages and security.
Quizzes and Exam
Every second weak, starting from 08.11.2006, 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.
yFurther Reading
Further reading will be suggested during the course.