SOFTWARE CORRECTNESS, SECURITY, AND RELIABILITY

Questo insegnamento appartiene ai percorsi "Software Development and Engineering" e "Cybersecurity" del corso di laurea magistrale in Computer Science, ed offre contenuti e metodologie relative metodi e strumenti per la verifica del software.

L'obiettivo dell'insegnamento è formire una panoramica delle principali tecniche per l'analisi e la verifica di codice sorgente. L'affidabilità del software dipende fortemente dalla correttezza delle sue componenti. Il corso sottolinea i vantaggi ed i limiti delle tecniche di analisi statica rispetto alle tecniche di testing, e discute le metriche e gli standards per l'assicurazione di qualità dei prodotti software. Al termine del corso gli studenti saranno in grado di utilizzare e di estendere un analizzatore statico per la verifica di codice sorgente.

In particolare il corso contribuisce a far sì che lo studente raggiunga i seguenti obiettivi di apprendimento:
- è in grado di verificare i requisiti funzionali e non funzionali di un sistema software
- sa condurre ricerche ed esperimenti per valutare le proprietà di sicurezza dei sistemi informatici
- è in grado di accedere alla letteratura scientifica per individuare potenziali soluzioni a problemi con metodi innovativi allo stato dell'arte.

Strutture Algebriche di base, Linguaggi di Programmazione

1. Semantics-based techniques for correctness and security analysis
Trace Semantics and Fixpoints
Dataflow Analysis
Abstract Interpretation
Numerical and String domains for source code verification

2. Software Quality Assurance
Software quality metrics
Software quality standards
Software quality management
Software Safety and Reliability

Xavier Rival and Kwangkeun Yi, "Introduction to Static Analysis An Abstract Interpretation Perspective", MIT Press, 2020, ISBN: 9780262043410
G.Schulmeyer, “Handbook of Software Quality Assurance”, 2007, ISBN-13: 978-1596931862
P.Cousot, "Principles of Abstract Interpretation, MIT Press, 2021

Ogni settimana verrà assegnato un task che via via accompagnerà lo studente all'utilizzo di un analizzatore statico a livello professionale.
L'esame finale consisterà nella discussione di un progetto finale (che potrà essere svolto anche in coppia), in continuità con i task individuali svolti durante il corso.
Ciascun task avrà una valutazione (in decimi) in base al numero di test superati.
La valutazione finale terrà conto per un 30% della valutazione media dei task e per il 70% della correttezza e della completezza del progetto realizzato e della relativa documentazione.

orale

Lezioni frontali, lavori di gruppo, revisione degli esercizi proposti
Tutto il materiale didattico sarà messo a disposizione sulla piattaforma Moodle.

Questo insegnamento tratta argomenti connessi alla macroarea "Capitale umano, salute, educazione" e concorre alla realizzazione dei relativi obiettivi ONU dell'Agenda 2030 per lo Sviluppo Sostenibile