Sistema ETD

banca dati delle tesi e dissertazioni accademiche elettroniche

 

Tesi etd-11182014-105609


Tipo di tesi
Tesi di laurea magistrale
Autore
CHFOUKA, HIND
URN
etd-11182014-105609
Titolo
The Prosper run-time monitor: design and formal verification
Struttura
INFORMATICA
Corso di studi
INFORMATICA
Commissione
relatore Corradini, Andrea
relatore Guanciale, Roberto
controrelatore Prof. Baiardi, Fabrizio
Parole chiave
  • Formal verification
  • Security
  • HOL4 theorem prover
  • Virtualization
  • Isolation property
  • Runtime monitoring
Data inizio appello
05/12/2014;
Disponibilità
completa
Riassunto analitico
Un runtime monitor è uno strumento che può essere usato per garantire una proprietà di sicurezza su una risorsa di sistema. Un comune approccio consiste in avere il runtime monitor come un modulo di sicurezza del kernel del sistema operativo. Questo approccio soffre di alcune problematiche che possono compromettere l'integrità del modulo di sicurezza. In un ambiente virtualizzato, un approccio alternativo è quello di sfruttare la proprietà di isolamento per garantire la protezione del modulo di sicurezza stesso. In questa tesi viene presentato un runtime monitor che si appoggia su Prosper hypervisor, un virtual machine monitor per embedded systems formalmente verificato. Il runtime monitor presentato è in grado di garantire delle proprietà di sicurezza tramite il monitoraggio delle hypercalls fornite dall'hypervisor al sistema operativo. Adottando un metodologia formale, viene discusso quale tipo di proprietà è possibile garantire con il runtime monitor di Prosper e viene identificata una proprietà di sicurezza che permette di proteggere il sistema operativo da attacchi di tipo code-injection. Questo è possibile grazie ad un meccanismo di validazione delle hypercalls che viene formalmente identificato. Il lavoro di tesi viene concluso presentando una verifica formale del meccanismo di validazione, dimostrando che la proprietà di sicurezza è valida su tutti gli stati raggiungibili dal sistema.
File