The course covers several fundamental techniques for the analysis of programs, with a focus on safety and security. The techniques are based on types and logics for programs, and allow to discover certain types of illicit behaviour or deduce the absence of such behaviour. We consider several successful tools implementing such techniques.
Information per course offering
Information for Autumn 2024 Start 28 Oct 2024 programme students
Headings with content from the Course syllabus FDD3463 (Spring 2022–) are denoted with an asterisk ( )
Content and learning outcomes
Course disposition
This course is taught simultaneously with the Master’s-level course DD2460 (Software Safety and Security). The Ph.D. course differs in the following ways:
1. The report and final presentation, as well as the tutorial labs designed to learn the different tools, are individual assignments.
2. Instead of solving pre-defined guided assignments in verification, the students will develop a formal model and a software-level model of an algorithm, architecture, or protocol that they are working on as part of their research. The high-level model will be developed in Event-B, NuSMV, or a similar tool that is suitable for formal verification; the low-level model (which may include only a part of the high-level model) will be written in a programming language like Java and verified with a tool like JPF or PAT.
Course contents
Part I. Introduction to safety and security. Part II. Temporal logics, modeling, model checking, formal specification. Tool: NuSMV. Part III. System modeling with Event-B. Tool: Rodin. Part IV. Concurrency, network programming. Tool: Java Pathfinder (JPF). Part V. Memory safety, fuzzing Tools: memory checker, fuzzer.
Intended learning outcomes
After passing the course, the student should be able to: explain safety and security aspects for systems, construct models of systems, specify and analyse safety and security properties, apply analytical tools on software systems, evaluate and compare different approaches to verification and validation of software systems, in order to as citizen and expert be able to discuss software safety and security, in professional life and/or research projects be able to formally express safety and security related properties, be able to use and adapt various tools and technologies to verify such properties.
Literature and preparations
Specific prerequisites
Completed course in computer security equivalent to DD2395. For the Ph.D. course, the candidate needs at least a design of a research idea to be able to formalize it in a model.
Recommended prerequisites
Good knowledge and skills in programming, programming languages, and program semantics. Knowledge of first-order logic and finite automata.
Equipment
Software installations are provided on KTH’s lab computers or available through links on Canvas.
Literature
Research papers, book excerpts, tool documentation, and web pages; provided on Canvas.
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
Grading scale
P, F
Examination
EXA1 -
Examination,
7.5 credits,
grading scale: P, F
Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.
The examiner may apply another examination format when re-examining individual students.
Opportunity to complete the requirements via supplementary examination
No information inserted
Opportunity to raise an approved grade via renewed examination
All members of a group are responsible for the group's work.
In any assessment, every student shall honestly disclose any help received and sources used.
In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.
Further information
Course room in Canvas
Registered students find further information about the implementation of the course in the course room in Canvas. A link to the course room can be found under the tab Studies in the Personal menu at the start of the course.
