Greetings

I want to modify the sel4 kernel to compute a checksum over the executable of the first process before executing it. The goal is to ensure that we execute the correct first process. What I'm doing right now is modify try_init_kernel() in kernel/src/archarm/kernel/boot.c by adding the following lines:

for(i=ui_p_reg_start, i<ui_p_reg_end; i++) { checksum += *((char*) (i)); }

My questions are the following:

(1) Is this a right place to perform the checksum (inside try_init_kernel())? I assume in this function, seL4 kernel already takes over and thus this should do the job.

I am making checksum checking three times: Two times over physical addresses (before and after the try_init_kernel), and one check over virtual:

printf("pre init hash = %x\n",fhash(ui_p_reg_start, ui_p_reg_end - ui_p_reg_start)); <..> result = try_init_kernel(ui_p_reg_start, ui_p_reg_end, pv_offset, v_entry); if (!result) { fail ("Kernel init failed for some reason :("); }

schedule(); activateThread(); <..> printf("post init hash = %x\n",fhash(ui_p_reg_start, ui_p_reg_end - ui_p_reg_start)); printf("virt hash = %x\n",fhash(0x00400000, ui_p_reg_end - ui_p_reg_start));

(2) Based on my understanding, what I did was computing the checksum over the entire image (which may includes executable of other processes as well). Is there a way to just read the executable of the first process and ignore the rest in seL4 kernel?

You should add some software to read elf headers, I guess

(3) I'm also curious: where/when does the seL4 kernel start the root process? I see the end of the same file (boot.c) that it just calls try_init_kernel() but does not load the root process.

try_init_kernel prepares context of the ‘root process’ (and some other things) via create_initial_thread() and after that kernel switches into it.