On 1 Sep 2016, at 18:29 , Horace Blanc wrote:

Hi,

I would like to have more information concerning the design of the hypervisor functionality in the sel4 project on ARMv7 architectures. From what I read (FAQ/announcement from Adrian Danis in this mailing list), sel4 can run an application called VMM which adds that functionality. Here are my questions: 1) Did the design of this functionality require any change in the sel4 microkernel or is it just the VMM in userland that permits it? (what was in the arm_hyp branch that is now in master?)

The hypervisor extensions to the architecture introduce new hardware state that the kernel needs to manage. Specifically it must forward virtualisation exceptions to the VMM (basically new exception modes).

2) Does this mean that it is a type-2 hypervisor? Do the guest OS run on top of the VMM?

No to the first question, yes (in a way) to the first. SeL4 is the hypervisor, it runs native.

3) How are the virtualization extentions of ARM used? More precisely what runs on the different protection levels (PL0, PL1 and PL2)?

seL4 runs in hype mode. The VMM as well as the guest OS run in kernel mode (but isolated from each other). Apps run in user mode.

4) To what extent is this hypervisor design pure? Do the guest OS know that it is running on top of seL4?

It’s “pure” in the sense that an unmodified guest binary will run in a VM. Whether the guest can tell that it is being virtualised is a different question, and there are arguments that it is practically impossible to prevent it from being able to tell (see [Garfinkel & Rosenblum, 2005], https://www.usenix.org/legacy/events/hotos05/prelim_papers/garfinkel/garfink...) Gernot