Software Security

Thomas Jensen

In this course, we will study various techniques for analysing and improving the security propoerties of a program.The techniques include advanced 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 eg 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

Contents

Part1 - Foundations of static analysis

• Inductive definitions and operational semantics
• type systems, unification, sub-typing, polymorphism
• partial orders and lattices, fixpoints, abstract interpretation

Part2 - Security analysis

• Non-interference, taint analysis, information flow analysis
• security monitors, byte code verification, secure compilation to low-level code

Learning outcomes

In this course, the student will acquire knowledge about advanced program analysis and type systems.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.