| | 27 | * 16h15-17h00 Matthieu Lemerre (CEA LIST), Nikolai Kosmatov (CEA LIST), and Céline Alec (CEA LIST), '''Verified Secure Kernels and Hypervisors for the Cloud'''[[BR]]Cloud-computing systems share hardware resources (CPU time and memory) between mutually untrusted applications. As such, they must provide isolation barriers between these applications, but must also secure resource sharing such that applications cannot stop, slow down, or provoke incorrect resource accounting of other applications. These isolation barriers are implemented by a trusted operating system kernel, which must be built according to security principles. Confidence in the system can be further increased with the help of tools for formal verification and proof of programs. Using these tools is eased because thorough application of security principles leads to a small system, but still poses many challenges for formal verification, like concurrency and the need to model the behavior of the hardware. This paper shows how modern tools for proof of programs can be applied to verification of secure kernels and hypervisors for the Cloud. We illustrate this approach on a critical module of a prototype Cloud hypervisor, called Anaxagoros, using the Frama-C software verification platform. |
![(please configure the [header_logo] section in trac.ini)](http://traclifo.univ-orleans.fr/INEX/chrome/site/lifo.png)
