Software Security (SOS)


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.


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


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.


Thomas Jensen (responsible), Delphine Demange