NDAK14002U Static program analysis and language-based security
Volume 2014/2015
Content
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-basedsecurity
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.
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
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-basedsecurity
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.
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.
Literature
Papers from the scientific
literature.
Academic qualifications
Semantics and Types
(course in block 1) is recommended, but not required.
Teaching and learning methods
Lectures plus written and
programming exercises.
Workload
- Category
- Hours
- Exercises
- 100
- Lectures
- 30
- Preparation
- 76
- Total
- 206
Sign up
Self Service at
KUnet
Exam
- 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
- NDAK14002U
- Credit
- 7,5 ECTS
- Level
- 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
- Study Board of Mathematics and Computer Science
Contracting department
- Department of Computer Science
Course responsibles
- Fritz Henglein (8-716e7770756e7277496d7237747e376d74)
Saved on the
23-06-2014