On 30 Jan 2021, at 08:26, Bora Agca <[email protected]<mailto:[email protected]>> wrote:
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 9–10. Gernot _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
