|
Todays commercial processors provide various hardware capabilities for monitoring and protecting systems from cyber intrusions. One technique suggested in the literature is to utilize hardware assisted virtualization (HAV) capabilities of modern processors and a hypervisor to provide security protections for a virtualized operating system (OS) and applications. Under this design, however, the security of the hypervisor is critically important. We use a formally verified microkernel (the security embedded L4, or seL4, microkernel) as a security hypervisor in order to provide a strong foundation for building security protections. We report on a series of experiments that measure the overheads associated with adding security protections into a system via our security hypervisor. Our security hypervisor uses common capabilities found in HAV extensions of modern processors to regain execution control every time the guest OS performs a context switch. This enables the hypervisor to perform additional security checks before running applications, including code verification and data integrity checks. Utilizing HAV in this manner adds significant overhead to guest OS context switches, an average of 6X in our experiments. To understand how this overhead affects system performance, we conducted experiments to measure the performance of a webserver under heavy traffic load. The system performance overhead with the context switch hooks in place was negligible. Therefore, utilizing HAV with a formally verified microkernel hypervisor is a viable and resource-effective method for enabling security protections.
|
