seL4 won't run on latest keystone version

[swidi]

Describe the bug
seL4 won't run with the latest keystone version. The kernel has been compiled just as described and runs well on the old keystone version. Host application has been adapted to the new SDK:

#include "keystone.h"
#include "edge_call.h"

int main(int argc, char** argv)
{
    Keystone::Enclave enclave;
    Keystone::Params params;

  params.setFreeMemSize(512*1024*1024);
  params.setUntrustedSize(1024);
  
  enclave.init(argv[1], argv[2], argv[3], params);
  enclave.registerOcallDispatch(incoming_call_dispatch);                                                                                                      
  edge_call_init_internals(                                                                                                                                   
    (uintptr_t)enclave.getSharedBuffer(), enclave.getSharedBufferSize());       
  enclave.run();

  return 0;
}

Screenshots or Error Log

# ./sel4/sel4.ke 
Verifying archive integrity... MD5 checksums are OK. All good.
Uncompressing Keystone vault archive
[  275.107139] keystone_enclave: shared buffer size is not multiple of PAGE_SIZE

No error, just nothing happens after extraction. Unfortunately, debugging of enclave applications is not possible, so I cannot provide any more info.

Additional context
I am working on a research project with the goal of having OP-TEE as an enclave besides Linux, having seL4 as an enclave would serve as a good reference.

[finmackandal]

Hi, I cannot say much about current Keystone and seL4 compatibility.

However, FWIW, you can debug the enclaves in QEMU using gdb-multiarch (fairly recent version is needed, eg. >= 12.1):
First starts QEMU in debug mode with scripts/run-qemu.sh -debug, then open gdb in another terminal and use the following snippet as starting point:

gdb \
       -ex "set arch riscv"\
       -ex "target remote localhost:$QEMU_GDB_PORT"\
       -ex "set confirmation off"

from here can use add-symbol-file to add the binaries/symbols and place breakpoints.

[swidi]

Thank you, but GDB seems to only help until the program counter is inside the enclave.
I tried to break at sbi_sm_run_enclave and then stepped a little until the PC moves to 0xffffffffc0000000. When I continue and Ctrl+C again, the PC has not moved. So, I believe, this is where it hangs.

Unfortunately, GDB is unable to access the memory in that location, so I don't know what exactly is happening:

(gdb) x/10i $pc
=> 0xffffffffc0000000:	Cannot access memory at address 0xffffffffc0000000

This is why I think that Enclaves themselves are not debuggable. I also found this open issue about this: keystone-enclave/keystone-sdk#6
But maybe something else is wrong, the PC just jumps to an impossible location due to whatever reason and this is why I can't debug it.

Hi, I cannot say much about current Keystone and seL4 compatibility.

However, FWIW, you can debug the enclaves in QEMU using gdb-multiarch (fairly recent version is needed, eg. >= 12.1): First starts QEMU in debug mode with scripts/run-qemu.sh -debug, then open gdb in another terminal and use the following snippet as starting point:

gdb \
       -ex "set arch riscv"\
       -ex "target remote localhost:$QEMU_GDB_PORT"\
       -ex "set confirmation off"

from here can use add-symbol-file to add the binaries/symbols and place breakpoints.

Hi, I cannot say much about current Keystone and seL4 compatibility.

However, FWIW, you can debug the enclaves in QEMU using gdb-multiarch (fairly recent version is needed, eg. >= 12.1): First starts QEMU in debug mode with scripts/run-qemu.sh -debug, then open gdb in another terminal and use the following snippet as starting point:

gdb \
       -ex "set arch riscv"\
       -ex "target remote localhost:$QEMU_GDB_PORT"\
       -ex "set confirmation off"

from here can use add-symbol-file to add the binaries/symbols and place breakpoints.

[finmackandal]

I usually put breakpoints at privilege modes entry points because single stepping between them never worked for me.
After sbi_sm_run_enclave the enclave starts its execution with the Supervisor (seL4 in your case I guess), so I would put a breakpoint at one of its early called functions.

Generally speaking, this should be this way regardless of the enclave you have.

Note, that 0xffffffffc0000000 is a virtual address and the CPU is managing physical addresses at the SM. That might be the reason it cannot access that address.

[grg-haas]

Hi @swidi ! The original issue that you're facing (keystone_enclave: shared buffer size is not multiple of PAGE_SIZE) I believe is most likely caused by this line

params.setUntrustedSize(1024);

RISC-V typically uses 4kB pages, so I'd recommend bumping your untrusted size to at least that value.

@finmackandal is correct in that enclaves can be debugged, but this can get a little tricky when things are not working correctly. In your specific case, you say that you get to 0xffffffffc0000000 successfully (which is the runtime's entry point) but then things hang. I've seen situations like this before, especially when combined with GDB not being able to access the memory, when PMP is somehow misconfigured. You can use scripts/gdb/pmp.py to debug this. Specifically, in GDB at that point, do:

source scripts/gdb/pmp.py
pmp-dump

And this will show you the current PMP configuration. In your case, I have a gut instinct that PMP is not getting correctly configured since your untrusted size is not a multiple of the page size. If you fix that, I wouldn't be too surprised if your runtime starts working as well. Keep me updated!

[swidi]

Thank you guys, that was already quite helpful. You were right about debugging enclaves being possible in general, it works well with the example applications and Eyrie. I can easily break at a function within the EApp and debug from there.

With seL4 or a small baremetal example that I am currently trying, though, it seems like the entry function is never reached. Could it be that the loader.bin only works with Eyrie? It is part of the Eyrie repository after all.

@grg-haas Indeed setting the untrusted size to a different value resolved the warning message. Unfortunately, the runtime did not start working.

PMP seems to be the same, both for the working hello world example and the non working seL4 or baremetal test:

pmp-dump
PMP reg 0 NAPOT
	cfg	0x18 
	addr	0x2003ffff = 0x80000000 -> 0x80200000
PMP reg 2 TOR
	cfg	0xf RWX
	addr	0x30039000 = 0xa0000000 -> 0xc00e4000
PMP reg 7 NAPOT
	cfg	0x1f RWX
	addr	0x41107fff = 0x104400000 -> 0x104440000

However, I don't know enough about RISC-V to be able to interpret this.

---

For reference, my 'baremetal example' looks like this:

	.global _start
	.section .text.bios

_start:	addi a0, x0, 0x68
	li a1, 0x10000000
	sb a0, (a1) # 'h'

	addi a0, x0, 0x65
	sb a0, (a1) # 'e'

	addi a0, x0, 0x6C
	sb a0, (a1) # 'l'

	addi a0, x0, 0x6C
	sb a0, (a1) # 'l'

	addi a0, x0, 0x6F
	sb a0, (a1) # 'o'
	
loop:	j loop

With the linker script adapted from Eyrie:

#define RISCV_PAGE_SIZE ()

OUTPUT_ARCH( "riscv" )

SECTIONS
{
  . = 0xffffffffc0000000;
  PROVIDE(rt_base = .);
  .text : {
    *(.text._start)
    *(.text.bios)
    *(.text)
  }
  . = ALIGN(1 << 12);
  .rodata :
  {
    *(.rdata)
    *(.rodata)
  }
  .data : { *(.data) }
  .bss : { *(.bss) }
  . = ALIGN(1 << 12);
  .kernel_stack : {
    . += 8 * (1 << 12);
    PROVIDE(kernel_stack_end = .);
  }

  _end = .;
}

[grg-haas]

Hmmmm, so with this example I could see a couple of issues. First, it seems that you are storing to the address 0x10000000, which I don't believe is mapped by default. I could imagine that this access leads to a store fault, which then (since you don't install an exception handler), could pretty catastrophically lock up your enclave.

Here's what I'd be interested in to debug this:

1. If you set a breakpoint on 0xffffffffc0000000, do you actually get to it? If so, please run pmp-dump at that point and send me the results.
2. If so, what's the value in stvec (the S-mode exception vector base address)? Set a breakpoint on it (even if it is 0x0).
3. If you run stepi a few times starting at 0xffffffffc0000000, does it immediately hang? Or do you actually manage to execute at least one instruction? Or do you hit the breakpoint on the stvec value? Or neither?

[swidi]

You might be right about the address thing!

I was able to break on 0xffffffffc0000000, and I do actually get to it. I am even able to print instructions at this address, and it seems like the binary is correctly loaded! :)

(gdb) x/10i 0xffffffffc0000000
=> 0xffffffffc0000000:	li	a0,104
   0xffffffffc0000004:	lui	a1,0x10000
   0xffffffffc0000008:	sb	a0,0(a1)
   0xffffffffc000000c:	li	a0,101
   0xffffffffc0000010:	sb	a0,0(a1)
   0xffffffffc0000014:	li	a0,108
   0xffffffffc0000018:	sb	a0,0(a1)
   0xffffffffc000001c:	li	a0,108
   0xffffffffc0000020:	sb	a0,0(a1)
   0xffffffffc0000024:	li	a0,111

However, when I step through, only the first three instructions are executed. After sb, it jumps back to the start. I am not very experienced with this but my intuition is that you are indeed right about the address not being mapped, so it tries to write to it but fails and returns to the start as a sort of default exception behavior. As you can see, stvec points there as well.

(gdb) pmp-dump
PMP reg 0 NAPOT
	cfg	0x18 
	addr	0x2003ffff = 0x80000000 -> 0x80200000
PMP reg 2 TOR
	cfg	0xf RWX
	addr	0x3002f800 = 0xa0000000 -> 0xc00be000
PMP reg 7 NAPOT
	cfg	0x1f RWX
	addr	0x41107fff = 0x104400000 -> 0x104440000

(gdb) p/x $stvec
$12 = 0xffffffffc0000000

This is starting to make sense now. However, for seL4, I still can't read from 0xffffffffc0000000:

Thread 4 hit Breakpoint 12, 0xffffffffc0000000 in ?? ()
(gdb) x/10i $pc
=> 0xffffffffc0000000:	Cannot access memory at address 0xffffffffc0000000
(gdb) pmp-dump
PMP reg 0 NAPOT
	cfg	0x18 
	addr	0x2003ffff = 0x80000000 -> 0x80200000
PMP reg 2 TOR
	cfg	0xf RWX
	addr	0x30068000 = 0xa0000000 -> 0xc01a0000
PMP reg 7 NAPOT
	cfg	0x1f RWX
	addr	0x41107fff = 0x104400000 -> 0x104440000

Perhaps the binary just isn't loaded there. I have followed the instructions from here, and it does say that it is deprecated in keystone 0.5. I wonder what changed from there. Surely the loading mechanisms is different now since we have a seperate loader binary. When I take a look at the patch applied to seL4, it does seem like it is loaded at 0xffffffffc0000000, though I can't say for sure as I am not experienced enough.

[swidi]

I think I found out why I can't access that region for seL4. Objdump revealed that the code is mapped at a very different location:

Disassembly of section .boot:

ffffffff80000000 <_start>:
ffffffff80000000:       0001c197                auipc   gp,0x1c
ffffffff80000004:       21618193                addi    gp,gp,534 # ffffffff8001c216 <__global_pointer$>
ffffffff80000008:       00001137                lui     sp,0x1

And indeed, I can examin this memory location with GDB and find the instructions. So, it seems like the jump-in address has changed from the old to the new keystone version. Now I just need to find out how to change either the location of seL4 or the location where the loader jumps to...

[grg-haas]

Ahhhh, I see what you're saying. You have both your baremetal example which stores hello to 0x10000000, and seL4 which is a separate example.

I believe this is where the address to return to is loaded:

keystone/runtime/loader-binary/loader.S

Line 36 in e310f6a

li t0, RUNTIME_VA_START

And this is the function that actually does ELF loading:

keystone/runtime/loader/loader.c

Line 17 in e310f6a

int loadElf(elf_t* elf, bool user) {

One thing you could check when running seL4 is set a breakpoint on 0xffffffffc0000000, but then do x/10i 0xffffffff80000000 to see if the seL4 instructions were actually loaded there. If so, then all you should need to do is change the RUNTIME_VA_START define to point to 0xffffffff80000000 instead. If not, then you might need to look at loader.c and figure out why the loader is not correctly parsing the seL4 ELF file.