"against its specification"
Which itself is not know to be bugfree.
(And is 10x the size of the source code and in a language that is less readable than x64 assembler)
Which itself is not know to be bugfree.
(And is 10x the size of the source code and in a language that is less readable than x64 assembler)
Not totally correct, from:
https://sel4.systems/Info/FAQ/proof.html
The binary code of the ARM and RISCV64 versions of the seL4 microkernel correctly implement the behaviour described in its abstract specification and nothing more. Furthermore, the specification and the seL4 binary satisfy the classic security properties called *integrity* and *confidentiality*.
[...]
Previously, in 2009, we had only proved functional correctness between the C code of the kernel and its specification. Now we have additionally shown binary correctness, that is, the compiler and linker need not be trusted, and we have shown that the specification indeed implies strong security properties as intended.
Note that nowhere in that they claim X is secure.
Your claim about "x64 assembler" is dubious.
Hopefully things get better and more practically useful.
It is subjective, and I’ll grant it’s not the most intuitive thing to look at, but I don’t agree it’s worse than assembly. Besides the readability of the specification is not some priori limitation.
Sel4 spec example
definition
set_endpoint :: "endpoint ⇒ data ⇒ state ⇒ state
set_endpoint ep data s ≡ s
(ep := (IdleEP, data))