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.commailto: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
-
Bora Agca -
Gernot Heiser