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.

(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?

(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.

Best,

Oak

--