• Formal verification
• Security
• HOL4 theorem prover
• Virtualization
• Isolation property
• Runtime monitoring

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.