On 30 Jan 2021, at 08:26, Bora Agca
Hi, i have one question:
since the seL4 was written with a C compiler and it is possible that this
compiler has an in-built backdoor, how can you still claim, that seL4 is
"safe", i.e. non-hackable.
because we prove that the binary is a correct translation of the verified (formalised) C.
The compiler is definitely *not* part of our TCB. [ATM this is true for Armv7 only, but
that part of the verification will be completed for RISC-V soon.]
The white paper (https://sel4.systems/About/seL4-whitepaper.pdf
) explains this on p