Reducing TCB size by using untrusted components: small kernels versus virtual-machine monitors