DD2460 Software Safety and Security 7.5 credits
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.
Choose semester and course offering
Choose semester and course offering to see current information and more about the course, such as course syllabus, study period, and application information.
Content and learning outcomes
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.
- 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.
Course disposition
Literature and preparations
Specific prerequisites
Completed course in computer security equivalent to DD2395.
Active participation in a course offering where the final examination is not yet reported in LADOK is considered equivalent to completion of the course.
Registering for a course is counted as active participation.
The term 'final examination' encompasses both the regular examination and the first re-examination.
Recommended prerequisites
Good knowledge and skills in programming, programming languages, and program semantics. Knowledge of first-order logic and finite automata.
Equipment
Literature
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
Grading scale
Examination
- EXA2 - Home exam, 1.0 credits, grading scale: A, B, C, D, E, FX, F
- LAB2 - Laboratory work, 5.0 credits, grading scale: A, B, C, D, E, FX, F
- ÖVN2 - Group presentation and report, 1.5 credits, grading scale: A, B, C, D, E, FX, 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
Opportunity to raise an approved grade via renewed examination
Examiner
Ethical approach
- 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 web
Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.
Course web DD2460Offered by
Main field of study
Education cycle
Add-on studies
Contact
Transitional regulations
The earlier module TEN2 has been replaced by EXA2.
Supplementary information
In this course, the EECS code of honor applies, see:
http://www.kth.se/en/eecs/utbildning/hederskodex
Additional regulations
This course contains group projects and labs. Course registration after the official registration period is not possible, since we need to create the groups in the beginning of the course.