NSCPHD1237 Static program analysis and language-based security

Volume 2014/2015
Content

The overall goal of the course is to introduce students to (1) semantics-based methods for program analysis, with (2) applications to software security. 

Part 1. Static program analysis


This part provides the student with the fundamental notions of static program analysis (operational semantics, abstract interpretation, type systems) and shows how these techniques can be used to reason about the behavior of  software. The goal of the course is to enable the students to define the operational semantics of a simple programming language and to design type systems and data flow analyses for this language in a systematic way. We present a variety of analyses, including the Java byte code verifier, alias analysis and relational analysis based on polyhedra.

Part 2. Language-based security

In the second half of the course we give a detailed presentation of the theory of abstract interpretation and study the JavaScript language from a semantics-based point of view.  This part provides shows how program analysis techniques can be used to improve the security of software. The goal of the course is to enable the students to define the operational semantics of a programming language and to design type systems and data flow analyses for this language. In the second part of the course we will present a variety of analyses used for improving software security, including the Java byte code verifier, information flow analysis and analysis problems related to binary code and JavaScript.

Learning Outcome

Knowledge:

Fundamentals of operational semantics, abstract interpretation, type systems, language-based software security.

Skills:

Design type systems, semantics and a data-flow analysis for a realistic programming language, specifically Java and JavaScript.

Competences:

Reasoning about the run-time behavior of software to improve and, in part, guarantee software security.

Papers from the scientific literature.

Semantics and Types (course in block 1) is recommended, but not required.
Lectures plus written and programming exercises.
Also listed as MS course NDAK14002U
  • Category
  • Hours
  • Exercises
  • 100
  • Lectures
  • 30
  • Preparation
  • 76
  • Total
  • 206
Credit
7,5 ECTS
Type of assessment
Continuous assessment
Active participation in class, plus 4-6 mandatory theoretical and programming exercises
Marking scale
passed/not passed
Censorship form
No external censorship
Several internal examiners
Re-exam
Resubmission of mandatory assignments (written exercises), plus 30 minutes' oral exam without preparation.
Criteria for exam assesment

Active participation in class, plus acceptable answers to at least 50% of mandatory exercises.