Corso di Metodi Formali

Corso di Laurea in Informatica - Università di Verona
Corso di

AVAS - Analisi e Verifica Automatica di Sistemi


Introduzione:

Un aspetto fondamentale della moderna scienza dei calcolatori è quello di fornire strumenti per poter ragionare sulle proprietà dei programmi. Le proprietà più interessanti sono quelle legate alla semantica dei programmi, ovvero a ciò che i programmi fanno indipendentemente dalla loro rappresentazione in un dato linguaggio di programmazione. Ad esempio, nei moderni sistemi distribuiti WWW è spesso necessario assicurare un corretto e sicuro flusso di informazioni affinchè non vengano violate privacy o venga compromessa la sicurezza dei sistemi di elaborazione. Analogamente, nei compilatori è importante conoscere il flusso delle informazioni all'interno delle varie strutture del programma (ovvero la semantica del programma) per potere trasformare questo al fine di ottenere un programma semanticamente equivalente ma migliore in prestazioni. Questi problemi sono risolti da strumenti largamente utilizzati nei moderni browsers e compilatori per verificare ed ottimizzare il codice importato dall'esterno o prodotto in fase di compilazione. Tuttavia, la natura indecidibile dei problemi legati alla semantica dei linguaggi di programmazione, impone una necessaria approssimazione nella fase di analisi e verifica formale. Nel corso vengono studiati i principali metodi formali per costruire sistematicamente strumenti per l'analisi statica e la verifica automatica di proprietà di programmi scritti in un linguaggio di programmazione (qualunque esso sia) mediante tecniche di approssimazione semantica. A partire da una semantica molto concreta (vicina all'esecuzione reale dei programmi) di un generico linguaggio di programmazione, verranno introdotti strumenti e tecniche per specificare, verificare ed approssimare proprietà di programmi. In particolare verranno affrontati i problemi di sicurezza del software (information flow analysis, code obfuscation, software watermarking e malware detection).

Il Corso:

  • Docente: Roberto Giacobazzi (E-mail roberto.giacobazzi@univr.it);
  • Ricevimento studenti: Lunedi, 15-18
  • Credito: 1UD (5 crediti)
  • Prerequisiti: Conoscenza di: Logica, Fondamenti dell'Informatica e Linguaggi (III anno).
  • Modalità d'Esame: Orale con discussione di una tesina (applicata o teorica) su un argomento dato dal docente.

  • Programma

  • Introduzione all'analisi e verifica di sistemi complessi
  • Posets, CPO, Reticoli, e Teoremi di punto fisso
  • Specifiche e proprietà di programmi
  • Logica di Hoare e verifica di programmi sequenziali
  • Astrazione e connessioni di Galois
  • Correttezza e astrazione di sistemi
  • Approssimazione semantica: Interpretazione astratta
  • Alcuni domini per l'analisi statica: Intervalli, congruenze, poliedri, aprrossimazioni in virgola mobile (Eric Gobault)
  • Elementi di Sicurezza del Software (Isabella Mastroeni)
  • Fondamenti normativi sulla protezione del Software
  • Tecniche di Software Watermarking
  • Tecniche di Code Obfuscation (Mila Dalla Preda)

  • Riferimenti bibliografici

  • H. A. Priestley, "Ordered sets and complete lattices" PDF
  • Burris and Sankappanavar, "A Course in Universal Algebra." PDF
  • Davey and Priestley, "Introduction to Lattices and Order", Cambridge, 1992
  • J.B. Nation, "Notes on Lattice Theory." PDF
  • Nielson, Nielson and Hankin, "Principles of Program Analysis", Springer-Verlag, 1999
  • Winskel, "The formal Semantics of Programming Languages" MIT Press, 1993
  • F. Nielson and H.R. Nielson, " Semantics with Applications" accessibile via web
  • Cousot and Cousot, "Abstract Interpretation of Logic Programs." PS

  • Slides utilizzate e materiale collegato

    Slides di Patrick Cousot
  • Introduzione Parte I
  • Introduzione Parte II
  • Mathematical Foundation Parte I
  • Mathematical Foundation Parte II
  • Galois connections
  • Fixpoint Theory Parte I
  • Fixpoint Theory Parte II
  • Abstraction
  • Sicurezza
  • Sicurezza: Introduzione
  • Sicurezza Parte I (slides) e (testo)
  • Sicurezza Parte II (slides) e (testo)
  • Domini astratti
  • Floating-Point Computations
  • Protezione del Software
  • Fondamenti Normativi

  • Alcuni puntatori collegati al corso:
  • Ariane 5; Una buona ragione per studiare i metodi formali (estratto da A $500 million mistake).
  • Semantics and Abstract Interpretation at Ecole Normale Superieure (Home page di P. Cousot).
  • Alcune tesi di Laurea disponibili.
  • Interessi di ricerca di Roberto Giacobazzi.
  • Altri puntatori.

  • Ritorna alla mia Home Page.