ECTS - University of Pisa
By the end of the course, students will have acquired knowledge about dependability of computer-based systems, theoretical foundation of formal methods and methodologies and tools to model, analyse and formally prove security. The course covers practical application of the theory to the following security issues: data confidentiality; security protocols; and cyber-physical systems security. Moreover, students will acquire knowledge on fault tolerant computing, 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.
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"
The teacher will provide lecture slides and handouts.
Attendance is not mandatory but highly recommended.
The exam is made up of one practical test and one oral test.
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 practical test.
None.
