Operating systems kernels are the main target of malevolent attacks since, if successful, such attacks give a complete control on the computer. Since most existing operating systems kernels are very complex, they are vulnerable to these attacks, and many malicious programs like "rootkits" have been developed by malicious hackers for this purpose.

From the detailed analysis of the way rootkit-based attacks access the kernel and then corrupt its addressing space, we have proposed a protection scheme for Linux that relies on using a hardware-supported hypervisor (HyTux), which exploits the virtualization capabilities of the underlying CPU. HyTux is a lightweight hypervisor that implements protection mechanisms in a mode more privileged than the Linux kernel. Therefore, it cannot be bypassed by the possibly compromised kernel itself. This approach to protect operating system kernels mainly consists in preserving some kernel constraints (the address of the system calls table, for example, whose modification could lead to a loss of integrity of the kernel control flow). The preservation of these constraints is automatically made by the hypervisor and cannot be bypassed by the kernel.

The kernel constraints are, up to now, found "by hand". We plan to develop a formal model in order to represent interactions between the hardware platform and the different software layers (hypervisor, kernel and user space layers) in such a way that these constraints can be expressed as soon as the stage of kernel specification. We also currently investigate other complementary protection mechanisms such as :

• the protection of the DMA (Direct Memory Access) I/Os through the IOMMU chipset included in recent PC architectures ;

• the verification of kernel module loading thanks to the Trusted Plateform Module (TPM) and the Intel Trusted Execution Technology (TXT).