Testi
  1. Mark G. Graff, Kenneth R. van Wyk. Secure Coding: Principles and Practices. O'Reilly, 2003.
  2. John Viega, Gary McGraw. Building secure software : how to avoid security problems the right way. Addison-Wesley, 2002.
  3. John C. Mitchell. Concepts in programming languages. Cambridge University Press, 2003.
  4. Ghezzi Carlo, Jazayeri Mehdi, Mandrioli Dino. Ingegneria del software. Fondamenti e principi. Pearson Education Italia, 2004, 2ª ed.
  5. Glenford J. Myers, Corey Sandler, Tom Badgett, Todd M. Thomas. The Art of Software Testing. John Wiley & Sons; 2 edition, 2004.
  6. Broy, M.; Jonsson, B.; Katoen, J.-P.; Leucker, M.; Pretschner, A. (Eds.). Model-Based Testing of Reactive Systems. Springer Verlag, LNCS 3472, 2005.
Programma 

1.      Sicurezza del software.
Proprietà del software sicuro. (parti 2.1 e 2.2 di [4]; cap. 1 di [2])
Ciclo di vita del software: fasi di sviluppo del software, modelli di ciclo di vita. (cap. 7 di [4] : parti 7.1 - 7.4)
La sicurezza nel ciclo di vita del software. (cap. 2 di [2])
Ciclo di vulnerabilità del SW ed attacchi a livello di progettazione, di implementazione ed di funzionalità. (
La lezione del Y2K.) (cap. 1 di [1])
Fattori di vulnerabilità.
Casi di studio: Arianne e TCP SYN.


 

2.      Architetture e tecnologie sicure.
Principi di architetture sicure.
Linee guida e principi per architetture sicure.
Criteri di scelta di tecnologie sicure.
Il caso di studio di Java sandbox.

 

3.      Specifica e progettazione di software sicuro.
Proprietà di specifiche di software sicuro.
Metodi di specifica.
Macchine a stati finiti.
Proprietà delle macchine a stati finiti e
sequenze particolari di esecuzione.
Macchine a Stati Finiti Estese.
Communicating Machines.
Macchine di stato UML.
Design by contract e il tool JML.
Tutorial di JML

      Esercizi su Macchine a Stati Finiti  (aggiornato)


 

4.      Implementazione.
Linee guida per la programmazione sicura. Tipici errori.
Sicurezza dei linguaggi di programmazione. Alcune violazioni di sicurezza in C. Programmi sicuri in C.
Dalla specifica al codice: macchine a stati finiti in Java.

 

5.      Testing.
Il testing nel ciclo di vita del software. Tipi di testing. Tecniche per la validazione e verifica. I limiti del testing.
Testing basato sui programmi. Grafo di flusso di un programma.
Copertura delle istruzioni e degli archi. Copertura delle decisioni e delle condizioni. I metodi MCC e MCDC.
Testing basato su specifiche.
Valutare la copertura con Emma. Tutorial di Emma. Il tool JUnit. Il caso di studio del CoffeeMaker.
Questa lezione verrà ripetuta in data 10 Gennaio 2007, ore 9-11, lab. Ovest.
Codice del CoffeeMaker.



Esami