Hi Mike, We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more: https://wiki.sel4.systems/CAmkESVM We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently. Anna. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM. A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall? Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled? Thanks! On Thu, Jun 8, 2017 at 8:10 PM, wrote:

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to. I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented? If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case? On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote:

...

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Kent, Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however. I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM. Is that the right path to head down? On Fri, Jun 16, 2017 at 12:24 AM, wrote:

Hi Mike,

If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig configuration forwards reads and writes to uart hardware to a separate CAmkES component. If you are wanting to trap access to certain mmio registers, then looking at how that project handles access to the UART and CLKCAR devices (on TK1) could be a place to start.

Traps caused by HSTR should end up being sent to the VMM by seL4 as a seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S under "Traps taken to HYP mode" to see where the trap enters the kernel).

Kind regards, Kent McLeod. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, June 16, 2017 5:18 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to.

I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented?

If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case?

On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

...

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote:

...

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Thanks Kent. I was afraid that would be the case. The VMM runs in user mode, right? Can it call those invocations? If so, how? It wasn't immediately obvious to me, and I couldn't find any existing code that looked like it was calling those. On Thu, Jun 22, 2017 at 1:10 AM, wrote:

Hi Mike,

Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to the VCPU which would allow you to use those invocations, but at this stage it isn't supported sorry.

If you wanted, you could look at adding a special case to the above invocations in the kernel (looking in /kernel/src/arch/arm/object/vcpu.c and kernel/include/arch/arm/arch/object/vcpu.h) where you would have to add the assembly to read and write to the registers yourself.

Kind regards, Kent McLeod ________________________________________ From: Mike Clark Sent: Thursday, June 22, 2017 12:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however.

I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM.

Is that the right path to head down?

On Fri, Jun 16, 2017 at 12:24 AM, wrote:

...

Hi Mike,

If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig configuration forwards reads and writes to uart hardware to a separate CAmkES component. If you are wanting to trap access to certain mmio registers, then looking at how that project handles access to the UART and CLKCAR devices (on TK1) could be a place to start.

Traps caused by HSTR should end up being sent to the VMM by seL4 as a seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S under "Traps taken to HYP mode" to see where the trap enters the kernel).

Kind regards, Kent McLeod. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, June 16, 2017 5:18 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to.

I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented?

If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case?

On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

...

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote:

...

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Kent, Thanks, that was very helpful. I was able to add the code necessary to give myself the ability to read and write to the registered that are being trapped. I then use that access to emulate the trapped instructions, then I call ignore_fault. After doing this, my linux VM boots part way, but eventually I get an error: "Assertion failed: seg_size > 0 (/host/camkes-arm-vm/libs/libsel4arm-vmm/src/copyinout.c: copy_in: 249)". The instruction that is being emulated at this point is "mrc p15, 0, r3, c2, c0, 1". Where it dies because of the assertion failure, I noticed that the very next block of code is: if (seg_size <=0) { return -1; } That if statement will never be true because of the assertion right above it. See here: https://github.com/smaccm/libsel4arm-vmm/blob/master/src/copyinout.c#L249 Here is a backtrace of the function calls that got me there: copy_in (copyinout.c) vm_copyin (copyinout.c) maybe_fetch_fault_instruction (fault.c) decode_instruction (fault.c) fault_get_width (fault.c) fault_is_32bit_instruction (fault.c) ignore_fault (fault.c) That call to ignore_fault was added in my trap handler. When I remove my additional trap, that sequence of calls never happens as far as I can tell. My handler is called a number of times before this fault occurs, once with the exact same instruction triggering the trap. Any thoughts? I was very encouraged to get it going as far as it is. I'm wondering if I just hit a case in the code that has an issue. On Fri, Jun 23, 2017 at 3:05 AM, wrote:

Hi Mike,

I've pasted a sample of using those invocations to update banked registers from advance_fault() in libsel4arm-vmm/src/fault.c:

/* register is banked, use vcpu invocations */ seL4_ARM_VCPU_ReadRegs_t res = seL4_ARM_VCPU_ReadRegs(vm_get_vcpu(fault->vm), reg); if (res.error) { ZF_LOGF("Read registers failed"); return -1; } int error = seL4_ARM_VCPU_WriteRegs(vm_get_vcpu(fault->vm), reg, fault_emulate(fault, res.value)); if (error) { ZF_LOGF("Write registers failed"); return -1; }

Let me know if this answers your question.

Kind regards, Kent. ________________________________________ From: Mike Clark Sent: Friday, June 23, 2017 4:29 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Thanks Kent. I was afraid that would be the case.

The VMM runs in user mode, right? Can it call those invocations? If so, how? It wasn't immediately obvious to me, and I couldn't find any existing code that looked like it was calling those.

On Thu, Jun 22, 2017 at 1:10 AM, wrote:

...

Hi Mike,

Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to the VCPU which would allow you to use those invocations, but at this stage it isn't supported sorry.

If you wanted, you could look at adding a special case to the above invocations in the kernel (looking in /kernel/src/arch/arm/object/vcpu.c and kernel/include/arch/arm/arch/object/vcpu.h) where you would have to add the assembly to read and write to the registers yourself.

Kind regards, Kent McLeod ________________________________________ From: Mike Clark Sent: Thursday, June 22, 2017 12:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however.

I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM.

Is that the right path to head down?

On Fri, Jun 16, 2017 at 12:24 AM, wrote:

...

Hi Mike,

If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig configuration forwards reads and writes to uart hardware to a separate CAmkES component. If you are wanting to trap access to certain mmio registers, then looking at how that project handles access to the UART and CLKCAR devices (on TK1) could be a place to start.

Traps caused by HSTR should end up being sent to the VMM by seL4 as a seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S under "Traps taken to HYP mode" to see where the trap enters the kernel).

Kind regards, Kent McLeod. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, June 16, 2017 5:18 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to.

I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented?

If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case?

On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

...

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote:

...

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Kent, I did what you suggested. This is the line that I am hitting a return -1 statement on (https://github.com/smaccm/libsel4arm-vmm/blob/master/src/copyinout.c#L192). The value of HSR on this particular trap is 0x0fe20861. Here are the values of the various registers at that point (which I got from print_fault): r0: 0xee519780 r1: 0x0 r2: 0x0 r3: 0x80004059 r4: 0x0 r5: 0xee521000 r6: 0xee519280 r7: 0xee519780 r8: 0xee519380 r9: 0xee519540 r10: 0xee522b00 r11: 0x1 r12: 0x0 pc: 0xc001dff8 r14: 0xb6e1bc10 sp: 0xbeb63d24 cpsr: 0x600b0013 I'll let you know if I find out anything else in my debugging. On Sun, Jun 25, 2017 at 8:42 PM, wrote:

Hi Mike,

Looking at your back-trace and the code, it appears that during the process of mapping in the memory in order to read the instruction to calculate the instruction width copy_in_page() fails to map the page in. To debug where that failure is occurring it may be worthwhile inserting some ZF_LOGF("") (from #include ) lines before the return -1 statements inside the copy_in_page function.

The code path that you are hitting is because the instruction you are trapping doesn't have a valid syndrome. Because in the past we never handled emulating instructions that didn't have a valid syndrome, the vmm would usually print an error in decode_instruction() in fault.c:286 and stop executing after one fault. It is not unlikely that you have found an issue with the implementation of the copy_in/copy_out because it hasn't been exhaustively tested very much.

My initial thought is that it could be vspace_get_cap returning seL4_CapNull due to some book keeping issue in the vspace (where the cap information should be stored).

I'd be interested to hear more about what is causing the fault.

Kind regards, Kent

________________________________________ From: Mike Clark Sent: Saturday, June 24, 2017 5:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I was able to add the code necessary to give myself the ability to read and write to the registered that are being trapped.

I then use that access to emulate the trapped instructions, then I call ignore_fault.

After doing this, my linux VM boots part way, but eventually I get an error: "Assertion failed: seg_size > 0 (/host/camkes-arm-vm/libs/libsel4arm-vmm/src/copyinout.c: copy_in: 249)".

The instruction that is being emulated at this point is "mrc p15, 0, r3, c2, c0, 1".

Where it dies because of the assertion failure, I noticed that the very next block of code is:

if (seg_size <=0) { return -1; }

That if statement will never be true because of the assertion right above it. See here: https://github.com/smaccm/libsel4arm-vmm/blob/master/src/copyinout.c#L249

Here is a backtrace of the function calls that got me there:

copy_in (copyinout.c) vm_copyin (copyinout.c) maybe_fetch_fault_instruction (fault.c) decode_instruction (fault.c) fault_get_width (fault.c) fault_is_32bit_instruction (fault.c) ignore_fault (fault.c)

That call to ignore_fault was added in my trap handler. When I remove my additional trap, that sequence of calls never happens as far as I can tell. My handler is called a number of times before this fault occurs, once with the exact same instruction triggering the trap.

Any thoughts? I was very encouraged to get it going as far as it is. I'm wondering if I just hit a case in the code that has an issue.

On Fri, Jun 23, 2017 at 3:05 AM, wrote:

...

Hi Mike,

I've pasted a sample of using those invocations to update banked registers from advance_fault() in libsel4arm-vmm/src/fault.c:

/* register is banked, use vcpu invocations */ seL4_ARM_VCPU_ReadRegs_t res = seL4_ARM_VCPU_ReadRegs(vm_get_vcpu(fault->vm), reg); if (res.error) { ZF_LOGF("Read registers failed"); return -1; } int error = seL4_ARM_VCPU_WriteRegs(vm_get_vcpu(fault->vm), reg, fault_emulate(fault, res.value)); if (error) { ZF_LOGF("Write registers failed"); return -1; }

Let me know if this answers your question.

Kind regards, Kent. ________________________________________ From: Mike Clark Sent: Friday, June 23, 2017 4:29 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Thanks Kent. I was afraid that would be the case.

The VMM runs in user mode, right? Can it call those invocations? If so, how? It wasn't immediately obvious to me, and I couldn't find any existing code that looked like it was calling those.

On Thu, Jun 22, 2017 at 1:10 AM, wrote:

...

Hi Mike,

Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to the VCPU which would allow you to use those invocations, but at this stage it isn't supported sorry.

If you wanted, you could look at adding a special case to the above invocations in the kernel (looking in /kernel/src/arch/arm/object/vcpu.c and kernel/include/arch/arm/arch/object/vcpu.h) where you would have to add the assembly to read and write to the registers yourself.

Kind regards, Kent McLeod ________________________________________ From: Mike Clark Sent: Thursday, June 22, 2017 12:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however.

I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM.

Is that the right path to head down?

On Fri, Jun 16, 2017 at 12:24 AM, wrote:

...

Hi Mike,

If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig configuration forwards reads and writes to uart hardware to a separate CAmkES component. If you are wanting to trap access to certain mmio registers, then looking at how that project handles access to the UART and CLKCAR devices (on TK1) could be a place to start.

Traps caused by HSTR should end up being sent to the VMM by seL4 as a seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S under "Traps taken to HYP mode" to see where the trap enters the kernel).

Kind regards, Kent McLeod. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, June 16, 2017 5:18 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to.

I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented?

If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case?

On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

...

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote: > Hi Mike, > > Unfortunately we haven't yet written any documentation on the VMM internals > or how it works. You are actually the first person to express interest in > this. Will try to make it a higher priority to write at least a brief > overview of the structure. For now my advice is to be familiar with CAmkES, > have a built version of the VMM so that you can code search for generated > code and then start exploring from either > https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... > or > https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... > depending on whether you are asking about the arm or x86 VMM. > > Adrian > > > On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote: > > Is there any documentation on how the VMM works? If I wanted to start > hacking on the VMM and extend its capability, where should I start > looking to learn how it works, etc? > > That might be a pretty broad topic, because there are lots of ways the > VMM can be extended, I'm sure. Broad is fine, until I get things more > figured out. > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel > >

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Hi Mike, It is interesting that vspace_get_cap() is returning a null cap. Given that the VM is faulting on that instruction it therefore must be mapped in to the guest, and if it is mapped into the guest, the guest vspace should return the cap for the mapping. sel4utils_get_cap() is the function for the implementation of the vspace that the vmm uses. You could dig around in there and related functions to try and figure out what is going on. Is there a chance that you could provide some sample code that demonstrates this problem and I can see if I can recreate it myself? Kind regards, Kent _______________________________________ From: Mike Clark Sent: Monday, June 26, 2017 10:52 PM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation Something else I just realized. I'm calling a print_fault on these new traps I added. All of the ones that handle just fine have an FSR value that looks like 0x03800047 or 0x03870007. The one that results in the failed assertion has FSR of 0x47. On Mon, Jun 26, 2017 at 8:31 AM, Mike Clark wrote:

Kent,

I did what you suggested. This is the line that I am hitting a return -1 statement on (https://github.com/smaccm/libsel4arm-vmm/blob/master/src/copyinout.c#L192).

The value of HSR on this particular trap is 0x0fe20861.

Here are the values of the various registers at that point (which I got from print_fault):

r0: 0xee519780 r1: 0x0 r2: 0x0 r3: 0x80004059 r4: 0x0 r5: 0xee521000 r6: 0xee519280 r7: 0xee519780 r8: 0xee519380 r9: 0xee519540 r10: 0xee522b00 r11: 0x1 r12: 0x0 pc: 0xc001dff8 r14: 0xb6e1bc10 sp: 0xbeb63d24 cpsr: 0x600b0013

I'll let you know if I find out anything else in my debugging.

On Sun, Jun 25, 2017 at 8:42 PM, wrote:

...

Hi Mike,

Looking at your back-trace and the code, it appears that during the process of mapping in the memory in order to read the instruction to calculate the instruction width copy_in_page() fails to map the page in. To debug where that failure is occurring it may be worthwhile inserting some ZF_LOGF("") (from #include ) lines before the return -1 statements inside the copy_in_page function.

The code path that you are hitting is because the instruction you are trapping doesn't have a valid syndrome. Because in the past we never handled emulating instructions that didn't have a valid syndrome, the vmm would usually print an error in decode_instruction() in fault.c:286 and stop executing after one fault. It is not unlikely that you have found an issue with the implementation of the copy_in/copy_out because it hasn't been exhaustively tested very much.

My initial thought is that it could be vspace_get_cap returning seL4_CapNull due to some book keeping issue in the vspace (where the cap information should be stored).

I'd be interested to hear more about what is causing the fault.

Kind regards, Kent

________________________________________ From: Mike Clark Sent: Saturday, June 24, 2017 5:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I was able to add the code necessary to give myself the ability to read and write to the registered that are being trapped.

I then use that access to emulate the trapped instructions, then I call ignore_fault.

After doing this, my linux VM boots part way, but eventually I get an error: "Assertion failed: seg_size > 0 (/host/camkes-arm-vm/libs/libsel4arm-vmm/src/copyinout.c: copy_in: 249)".

The instruction that is being emulated at this point is "mrc p15, 0, r3, c2, c0, 1".

Where it dies because of the assertion failure, I noticed that the very next block of code is:

if (seg_size <=0) { return -1; }

That if statement will never be true because of the assertion right above it. See here: https://github.com/smaccm/libsel4arm-vmm/blob/master/src/copyinout.c#L249

Here is a backtrace of the function calls that got me there:

copy_in (copyinout.c) vm_copyin (copyinout.c) maybe_fetch_fault_instruction (fault.c) decode_instruction (fault.c) fault_get_width (fault.c) fault_is_32bit_instruction (fault.c) ignore_fault (fault.c)

That call to ignore_fault was added in my trap handler. When I remove my additional trap, that sequence of calls never happens as far as I can tell. My handler is called a number of times before this fault occurs, once with the exact same instruction triggering the trap.

Any thoughts? I was very encouraged to get it going as far as it is. I'm wondering if I just hit a case in the code that has an issue.

On Fri, Jun 23, 2017 at 3:05 AM, wrote:

...

Hi Mike,

I've pasted a sample of using those invocations to update banked registers from advance_fault() in libsel4arm-vmm/src/fault.c:

/* register is banked, use vcpu invocations */ seL4_ARM_VCPU_ReadRegs_t res = seL4_ARM_VCPU_ReadRegs(vm_get_vcpu(fault->vm), reg); if (res.error) { ZF_LOGF("Read registers failed"); return -1; } int error = seL4_ARM_VCPU_WriteRegs(vm_get_vcpu(fault->vm), reg, fault_emulate(fault, res.value)); if (error) { ZF_LOGF("Write registers failed"); return -1; }

Let me know if this answers your question.

Kind regards, Kent. ________________________________________ From: Mike Clark Sent: Friday, June 23, 2017 4:29 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Thanks Kent. I was afraid that would be the case.

The VMM runs in user mode, right? Can it call those invocations? If so, how? It wasn't immediately obvious to me, and I couldn't find any existing code that looked like it was calling those.

On Thu, Jun 22, 2017 at 1:10 AM, wrote:

...

Hi Mike,

Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to the VCPU which would allow you to use those invocations, but at this stage it isn't supported sorry.

If you wanted, you could look at adding a special case to the above invocations in the kernel (looking in /kernel/src/arch/arm/object/vcpu.c and kernel/include/arch/arm/arch/object/vcpu.h) where you would have to add the assembly to read and write to the registers yourself.

Kind regards, Kent McLeod ________________________________________ From: Mike Clark Sent: Thursday, June 22, 2017 12:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Kent,

Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however.

I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM.

Is that the right path to head down?

On Fri, Jun 16, 2017 at 12:24 AM, wrote:

...

Hi Mike,

If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig configuration forwards reads and writes to uart hardware to a separate CAmkES component. If you are wanting to trap access to certain mmio registers, then looking at how that project handles access to the UART and CLKCAR devices (on TK1) could be a place to start.

Traps caused by HSTR should end up being sent to the VMM by seL4 as a seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S under "Traps taken to HYP mode" to see where the trap enters the kernel).

Kind regards, Kent McLeod. ________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, June 16, 2017 5:18 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to.

I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented?

If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case?

On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

...

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote: > Hi Mike, > > We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more: > > https://wiki.sel4.systems/CAmkESVM > > We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently. > > Anna. > > > ________________________________________ > From: Devel on behalf of Mike Clark > Sent: Friday, 9 June 2017 10:56 PM > To: Danis, Adrian (Data61, Kensington NSW) > Cc: devel@sel4.systems > Subject: Re: [seL4] vmm documentation > > Okay, so I'll start with something more concrete that should help me > understand a few things. Let's say I wanted to implement a hypercall > and for the purposes of this discussion, let's assume ARM. > > A user process on the Linux VM can issue a hypercall with the HVC > instruction, right? Where would I need to add code to the VMM to > handle this hypercall? > > Also, it is my understanding that certain instructions will cause a > trap into the VMM. Where is that handled? > > Thanks! > > On Thu, Jun 8, 2017 at 8:10 PM, wrote: >> Hi Mike, >> >> Unfortunately we haven't yet written any documentation on the VMM internals >> or how it works. You are actually the first person to express interest in >> this. Will try to make it a higher priority to write at least a brief >> overview of the structure. For now my advice is to be familiar with CAmkES, >> have a built version of the VMM so that you can code search for generated >> code and then start exploring from either >> https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... >> or >> https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... >> depending on whether you are asking about the arm or x86 VMM. >> >> Adrian >> >> >> On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote: >> >> Is there any documentation on how the VMM works? If I wanted to start >> hacking on the VMM and extend its capability, where should I start >> looking to learn how it works, etc? >> >> That might be a pretty broad topic, because there are lots of ways the >> VMM can be extended, I'm sure. Broad is fine, until I get things more >> figured out. >> >> _______________________________________________ >> Devel mailing list >> Devel@sel4.systems >> https://sel4.systems/lists/listinfo/devel >> >> > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

I don't think this is possible with how seL4 manages the page tables in the ARM hyp model (Someone who is more familiar with this may need to correct me here). You may be able to achieve the same result by telling Linux that there is some device memory somewhere there is not and rely on a data abort to trap to hyp mode? Kent. ________________________________________ From: Devel on behalf of Mike Clark Sent: Thursday, June 29, 2017 5:17 AM To: devel@sel4.systems Subject: Re: [seL4] vmm documentation There is something else I want to try to do. I got the inspiration from here: https://community.arm.com/processors/f/discussions/4065/trap-to-hypervisor-i... It looks like from the ARM Reference manual that if I set the two least-significant bits of an entry in the first or second level translation table to be b00, then there will be a page fault any time that page is accessed. How would I do this in seL4 from the VMM? Is that currently possible to do? Thanks! On Thu, Jun 8, 2017 at 12:26 PM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel