Fwd: Regarding Ken Thompson's Reflecting on trusting trust...
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. Best regards and thanks in advance ___________________________ Bora Agca Diplom Informatiker Oracle Certified Programmer Java SE 6
On 30 Jan 2021, at 08:26, Bora Agca <agca.software@gmail.com<mailto:agca.software@gmail.com>> 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
participants (2)
-
Bora Agca -
Gernot Heiser