ECTS - University of Pisa
Lo studente che completa l'insegnamento con successo avrà conoscenze su (i) principi fondamentali della dependability di sistemi basati su computers (ii) metodi formali per la modellazione e la verifica di programmi e sistemi (iii) strumenti per analizzare e provare formalmente proprietà di security di sistemi. Verranno approfonditi i seguenti problemi di security: data confidentiality; malware detection; and cyber-physical systems security. Inoltre, lo studente avrà conoscenze sulle tecniche di fault tolerance e sulla valutazione quantitativa della dependability basata sui modelli.
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; malware detection; 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.
Le conoscenze saranno verificate sull'abilità di illustrare i concetti fondamentali oggetto del corso usando la corretta terminologia, di risolvere esercizi sull'applicazione dei formalismi studiati e di presentare un progetto svolto in gruppo.
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.
Il corso fornirà gli studenti le capacità di (i) modellazione formale di componenti hardware e software, e di attacchi di sicurezza; (ii) verifica formale di proprietà di cybersecurity di un sistema usando tecnique di base. Inoltre, gli studenti saranno in grado di di usare approcci formali per modellare e valutare la dependability di sistemi basati su computers: modelli combinatori, modelli state-based. Infine, gli studenti acquisiranno la conoscenza degli standard internazionali per la safety e la security in ambito industriale.
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. Finally, students will acquire the awareness of international standards for safety and security applied in industry.
Durante le sessioni di laboratorio verranno utilizzati semplici esempi per imparare a progettare sistemi dependable e per utilizzare strumenti di verifica formale. Gli studenti presenteranno e discuteranno la loro attività sul progetto periodicamente, mostrando la metodologia e gli strumenti applicati per risolvere il problema specifico. Gli studenti dovranno preparare un report scritto e fare una presentazione.
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.
Durante la discussione del progetto, verrà valutata la correttezza della soluzione proposta, insieme con l'accuratezza delle attività.
During the discussion of the project, the correctness of the proposed solution, together with the accuracy and precision of the activities, will be evaluated.
Nessuno
None.
Lezioni in presenza con l'ausilio di lucidi.
Attività pratiche basate su materiale fornito dal docente, utilizzando omputers del laboratorio o personali dello studente.
Il materiale del corso sarà disponibile sul sito web del corso.
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.
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 of dependability: Series/Parallel models, fault/attack-trees, stochastic nets.
Background on formal methods: Automata theory, logic, program semantics.
Automated verification: model checking, theorem proving, abstract interpretation.
Security issues: Threat analysis and Risk assessment. Data confidentiality; malware detection; and cyber-physical systems security.
Standards: ISO 26262 "Road vehicles – Functional safety", ISO/SAE 21434:2021 "Road vehicles — Cybersecurity engineering"
Dependability and security: non-malicious/malicious faults, errors and failures. Availability, Reliability, Safety, Confidentiality, Integrity, Maintainability. Security Aware Hazard Analysis and risk assessment.
Background on formal methods: Automata theory, logic, program semantics.
Automated verification: model checking, theorem proving, abstract interpretation.
Quantitative evalutation: Series/Parallel models, Fault/Attack-trees, stochastic nets.
Security issues: Threat analysis and Risk assessment. Data confidentiality; malware detection; and cyber-physical systems security.
Standards: ISO 26262 "Road vehicles – Functional safety", ISO/SAE 21434:2021 "Road vehicles — Cybersecurity engineering"
Lucidi delle lezioni e materiale delle attività pratiche fornite dal docente.
The teacher will provide lecture slides and handouts.
La frequenza non è obbligatoria ma è fortemente raccomandata.
Attendance is not mandatory but highly recommended.
L'esame consiste in un test pratico e in una prova orale.
Il test pratico consiste di un progetto svolto in gruppo sull'applicazione di una tecnica specifica di modellazione/verifica ad un probema di cyber-security. Il progetto è svolto sotto la guida del docente, e deve essere completato e consegnato prima dell'esame.
La prova orale consiste in una discussione sugli argomenti del corso. Allo studente è richiesto di dimostrare le sue conoscenze sul materiale del corso.
Per sostenere la prova orale, è necessario avere superato la prova scritta.
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 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.
Nessuna.
None.
