NSCPHD1237 Static program analysis and language-based security
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.
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.
- Category
- Hours
- Exercises
- 100
- Lectures
- 30
- Preparation
- 76
- Total
- 206
- Credit
- 7,5 ECTS
- Type of assessment
- Continuous assessmentActive 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.
Course information
- Language
- English
- Course code
- NSCPHD1237
- Credit
- 7,5 ECTS
- Level
- Ph.D.Full Degree Master
- Duration
- 1 block
- Placement
- Block 2
- Schedule
- B (Mon 8-12 + Tues 13-17 + Fri 8-12)
- Course capacity
- No limit
- Study board
- Natural Sciences PhD Committee
Contracting department
- Department of Computer Science
Course responsibles
- Fritz Henglein (8-7b78817a7f787c8153777c417e8841777e)