Linguaggi di programmazione per la sicurezza

"il corso ha un duplice obiettivo: presentare le principali tecniche di programmazione sicura nei linguaggi più usati per lo sviluppo di applicazioni e fornire le conoscenze necessarie per la progettazione di software sicuro e per l'analisi di sicurezza del codice sorgente attraverso walkthrough, test e tecniche formali di verifica e di analisi statica e dinamica del flusso esecutivo.

Ricevimento

Lunedì dopo la lezione o su appuntamento

Programma lezioni con slides

Introduzione al corso	19 settembre 2005	intro_corso
Type safety e linguaggi programmazione sicura	19 e 26 sett 05 esercizi in lab 4 ott	safe programming
Uso di Cyclone	I parte 26 sett. 05	cyclone_tutorial
Java Basic: da C a Java	fino a stringhe 4 ott completato il 10 ott	da C a java
testing: concetti base	17 ottobre	Introduzione
testing basato su programmi	19 ottobre	clicca qui
usare emma	24 ottobre	slides con esercizi e istruzioni esercizio: - flusso di controllo - codice java
eXtreme Programming JUnit in JBuilder con esempio e soluzione	14 Novembre	slides con le due parti insieme
Design By Contract (tm)	21 Novembre	slides dbc slide su jml
Verifica formale di programmi Altro materiale: capitolo10Finkel, appunti	28 Novembre (e 5 Dic)	slides
Ciclio di vita del sw e ruolo della specifica (prof. Riccobene)	5 Dicembre	slides
Finite State Machines (prof. Riccobene)	12 Dicembre	slides
Testing per FSM	19 Dicembre	slides motres, capitolo 4

Codice

esempio2.c ed esempio3.c : dangling pointers in C

Indice del materiale ad accesso riservato

I Compitino testo d'esame : soluzioni

II Compitino testo d'esame (a breve le soluzioni)

Esame 15 /2 /2006 : risultati (per la registrazione, martedì 21 mattina o per appuntamento)

Modalità d'esame

L'esame consiste nell'accertare le conoscenze teoriche e le capacità pratiche nell'uso di strumenti.
Si può passare con i due compitini o con l'esame. Un progetto, da concordare con il docente, e' facoltativo e da' diritto ad alcuni punti in più.

ATTENZIONE: per l'esame useremo eclipse invece che JBuilder (che non funziona più). Qui alcune indicazioni su come usare Eclipse:

Come creare un progetto e un file

New -> Project -> Java project -> scegli un nome
			       -> dove c'è JDK Compliance -> using project compliance -> seleziona 5.0 (per avere le classi di Java 5)

Lascia "create project in the workspace": questo crea una directory:
C:\Documents and Settings\esamelps2005\workspace\<<NOME>>
dove <<NOME>> è il nome del progetto 
nella quale ci sono i class e i java. D'ora in poi chiamo questo diretcory DJ

New -> java class - > lascia vuoto package
 			-> Name (senza spazi)
			-> seleziona main per avere il metodo main

Come creare test con JUnit

Seleziona la classe per cui vuoi creare i casi di test, tasto destro -> new -> JUnit Test Case
Si apre un dialogo (seleziona tearDown, setUp e main se vuoi avere questi metodi - non è necessario in genere per piccoli esercizi)
fai next -> seleziona il metodo per cui vuoi creare i casi di test

Riempi il metodo (JBuilder ti aiutava, con eclipse devi fare tu).
Ad esempio se hai un metodo foo della classe Es1 che prende un array di Stringhe, avrai un metodo testFoo in cui devi testare foo. 
Puotresti scrivere istruzioni di questo genere:

  public void testFoo() {

    String[] b = new String[0];
    expectedReturn = null;
    actualReturn = Es1.foo(b);
    assertEquals("return value", expectedReturn, actualReturn);

    String[] c = {
        "cane", "grattacielo", "blu"}; ;
    expectedReturn = "blu";
    actualReturn = Es1.foo(c);
    assertEquals("return value", expectedReturn, actualReturn);
  }

usa le istruzioni assertEquals e così via di Junit (vedi i lucidi)

Per eseguire i test fai 
tasto destro sulla classe -> run As -> Junit Test

Usare Emma

eclipse non produce un jar ma solo il .class nella directory DJ

copia emma.jar nelle directory DJ, apri una finestra dos e fai cd fino a quel punto

lancia emma in questo modo:

java -cp emma.jar emmarun -cp . <<NOMECLASSE>>

Nota che <<NOMECLASSE>> va scritto senza .class

per avere l'output in html con i sorgenti colorati:

java -cp emma.jar emmarun -cp . -sp . -r html <<NOMECLASSE>>