Software Security (SOS)

Official homepage (with schedule)

Description

In this course, we will study various techniques for analysing and improving the security propoerties of a program. The techniques include static type systems, abstract interpretation and run-time monitoring, and the security properties of interest include information-flow (direct and indirect) as well as memory protection and isloation. The course will start by presenting the analysis techniques and the formalism used for defining these analyses. This will build on basic notions of operational semantics and data-flow analysis (obtained e.g. from the M1 courses on those topics). We will then study examples of security verification mechanisms, with an emphasis on information flow analysis. The course will study several programming languages (Java, JavaScript, assembly) and examine the security mechanisms offered by these different programming languages.

Keywords

Software security ; information flow control ; program analysis ; type systems ; abstract interpretation

Prerequisites

Basic notions of operational semantics and data flow analysis

Part 1 - Foundations of static analysis

Inductive definitions and operational semantics
Static type systems : progress, type-preservation, soundness
Partial orders and lattices, data-flow analysis, abstract interpretation

Part 2 - Security analysis

Non-interference, taint analysis, information-flow analysis
Security monitors, bytecode verification

Learning outcomes

In this course, the student will acquire knowledge about advanced program static analysis. The student will learn how to apply these techniques and how these techniques are used to analyse and enforce security policies for protecting a piece of software.

Teachers