Scheda programma d'esame
FORMAL METHODS FOR SECURE SYSTEMS
CINZIA BERNARDESCHI
Anno accademico2021/22
CdSCOMPUTER ENGINEERING
Codice909II
CFU9
PeriodoSecondo semestre
LinguaItaliano

ModuliSettore/iTipoOreDocente/i
FORMAL METHODS FOR SECURE SYSTEMSING-INF/05LEZIONI90
CINZIA BERNARDESCHI unimap
Obiettivi di apprendimento
Learning outcomes
Conoscenze

 

 

 

Knowledge

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.

 

Assessment criteria of knowledge

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.

Skills

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.

Assessment criteria of skills

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.

Behaviors

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.

Assessment criteria of behaviors

During the discussion of the project, the accuracy and precision of the activities, together with the correctness of the proposed solution will be evaluated.

 

Prerequisites

None.

Teaching methods

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.

Syllabus

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"

Bibliography

 

  • Flemming Nielson, Hanne Riis Nielson, Formal Methods, Springer, 2019

  • John Knight. Fundamentals of Dependable Computing for Software Engineers, Chapman & Hall, 2012

  • 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

  • M. Nicol, W.H. Sanders, K.S. Trivedi. Model-Based Evaluation: From Dependability to Security. In: IEEE Transactions on Dependable and Secure Computing, vol. 1 (1), 2004

The teacher will provide lecture slides and handouts.

Non-attending students info

Attendance is not mandatory but highly recommended.

Assessment methods

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.

 

Notes

None.

Ultimo aggiornamento 24/02/2022 09:08