After successfully completing the course, you will be able to:
- discuss programming language techniques to implement domain-specific languages and their tradeoffs.
- understand how programming language techniques can be used to improve the security of software systems.
- design and implement domain-specific languages, analyses, and transformations to address specific problems, such as security bugs.
- understand and explain fundamental aspects of security attacks (e.g., undefined behavior, memory vulnerabilities, sandbox breakout, information leaks, side channels).
- understand and explain basic mathematical concepts (e.g., lattices, fixed points, traces) underlying domain-specific languages, analyses, and properties.
- develop formal models that describe the behavior and the security requirements of a system.
- develop formal specifications of domain-specific languages and prove that they achieve desired security properties using program semantics.
Written exam; lab assignments.
A repair test requires at least a 4 for the original test.
Building secure systems is notoriously hard. Despite every security patch, attackers always seem to find new exploits.|
A huge part of the problem is that developers do not have the right tools to write secure software. They build complex software systems that handle sensitive data using programming languages that do not account for security or privacy.
Thus, developers can too easily introduce bugs that attackers can exploit as security vulnerabilities to breach their systems.
Domain-specific languages can help developers address the security and privacy problems of their systems through security-oriented abstractions that make it easy to detect and eliminate security bugs.
This course studies techniques to design and implement domain-specific languages and analyses, with a focus on software security.
In the first part of the course, we will learn basic program analysis techniques and apply them to automatically prevent sandbox breakouts and information leaks in cryptographic code.
We will then cover lightweight techniques to embed domain-specific analyses into general-purpose languages. We will apply these techniques to develop information-flow tracking languages that can enforce data confidentiality by construction in untrusted third-party code.
The course combines theoretical foundations and hands-on experience.
We will learn how to design programming languages and analyses using formal semantics and how to specify and establish their security guarantees.
The practical assignments will provide experience implementing static analyzers and domain-specific languages.
Combined lectures, exercises, lab sessions.
Slides and the following book: Nielson, Flemming, Nielson, Hanne R., Hankin, Chris, "Principles of Program Analysis", Corr. 2nd printing, ISBN: 3-540-65410-0.
Other material may be made available throughout the course.
Note that basic knowledge of and experience with the Haskell programming language is important to do the practical assignments; this is a prerequisite to follow the course.
Note, though, also that you are not expected to have done the course on Advanced Functional Programming.