ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| FORMAL METHODS FOR SECURE SYSTEMS | ING-INF/05 | LEZIONI | 90 |
|
By the end of the course, students will have acquired knowledge about the theoretical foundation of formal methods and the methodologies and tools to model, analyse and formally prove security of computer-based systems. The course covers practical application of the theory to the following security issues: data confidentiality; malware detection; and cyber-physical systems security. Moreover, students will acquire knowledge on dependability, on fault tolerance techniques and on model-based quantitative evaluation of dependability.
The assessment of the knowledge will be the subject of the evaluation at each exam session. Students knowledge will be assessed on their ability to discuss the fundamental concepts of the course using the appropriate terminology, to solve exercices on the application of the formalisms studied and to present a project carried out in group.
The course enables students to (i) formal modelling of hardware and software components, and attacks; (ii) formal verification of security properties of a system using basic techniques. This includes the application of: model checking, theorem proving, abstract interpretation. Moreover, students will be able to use formal approaches to reliability modeling and evaluation of computer-based systems: combinatorial models and state-based models (stochastic nets). Finally, students will acquire the awareness of international standards for safety and security applied in industry.
During the laboratory sessions, small example will be carried out in order to understand how to use the verification tools. Students will present and discuss their activity on the project periodically, showing the methodology and tools applied to solve the specific problem. The student will have to prepare and present a written report.
Students will acquire a rigorous approach to system modelling and analysis. Students will develop an awareness of security issues in safety critical systems. Students will acquire ability in the formalization, evaluation and verification process.
During the discussion of the project, the accuracy and precision of the activities, together with the correctness of the proposed solution will be evaluated.
None.
None.
None
Face to face lectures with slides.
Hands-on activities using either computers in the classroom or students’ personal computers, based on material provided by the teacher.
Web site of the course for downloading teaching materials.
Background on formal methods: Automata theory, logic, program semantics.
Automated verification: model checking, theorem proving, abstract interpretation.
Dependability and security: non-malicious/malicious faults, errors and failures. Availability, Reliability, Safety, Confidentiality, Integrity, Maintainability. Security Aware Hazard Analysis and risk assessment.
Quantitative evalutation: Fault/Attack-trees, stochastic nets.
Security issues: data confidentiality; malware detection; and cyber-physical systems security.
Standards: ISO 26262 "Road vehicles – Functional safety"
D.P. Siewiorek, R. S. Swarz
Reliable Computer Systems (Design and Evaluation)
Prentice Hall, 1998 (part)
A. Avizienis, J.C. Laprie, B. Randell, C. Landwehr.
Basic Concepts and Taxonomy of Dependable and Secure Computing.
IEEE Transactions on Dependable and Secure Computing, Vol. 1, N. 1, 2004
The teacher will provide lecture slides and handouts.
Attendance is not mandatory but highly recommended.
The exam is made up of one written test, one practical test and one oral test.
The written test consists of exercises to demonstrate in-depth knowledge of formal methods and security issues.
The practical test consists of a project carried out in group on the application of one specific modelling/veriifcation technique to a cyber-security specific problem. The project is carried out under the guidance of the teachers, and it must be completed and delivered to teachers at least one week before the examination.
The oral test consists of an interview. The student is requested to demonstrate his/her knowledge of the course material.
To attend the oral test, it is necessary to pass the written and the practical test.
-------------------------------
Because of the COVID-19 pandemic, the exam has been changed into an online exam with (1) a presentation and discussion of a technical project and (2) an oral examination.
None.
