3 ms·

"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 a

"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)

fooker 2y ago
This is the price of contemporary formal methods. Hopefully things get better and more practically useful.
flawsofar 2y ago
All code is either useless or unreadable
simplereally 2y ago
Is the specification really 10x the size of the source code, or are you including the proof of the specification? Your claim about "x64 assembler" is dubious.
naasking 2y ago
> Which itself is not know to be bugfree. Not totally correct, from: https://sel4.systems/Info/FAQ/proof.html 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. So the specification has indeed been proven to be free of certain security bugs.
- daghamm 2y ago
  It is always X meets Y under the assumption Z. But what if Y is incomlete or Z is invalid? Note that nowhere in that they claim X is secure.
  - naasking 2y ago
    "Secure" is ambiguous, so of course they wouldn't claim X, whatever that is, is "secure". For instance, a microkernel does not provide cryptographic confidentiality, but some readers include such properties under the umbrella of "secure", so using that term would be dumb. When talking about proofs you describe the specific properties proven in a way that leaves no ambiguity.
WhitneyLand 2y ago
I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. 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 where set_endpoint ep data s ≡ s (ep := (IdleEP, data))

"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)

fooker 2y ago

This is the price of contemporary formal methods. Hopefully things get better and more practically useful.

flawsofar 2y ago

All code is either useless or unreadable

simplereally 2y ago

Is the specification really 10x the size of the source code, or are you including the proof of the specification? Your claim about "x64 assembler" is dubious.

naasking 2y ago

> Which itself is not know to be bugfree. Not totally correct, from: https://sel4.systems/Info/FAQ/proof.html 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. So the specification has indeed been proven to be free of certain security bugs.

daghamm 2y ago
It is always X meets Y under the assumption Z. But what if Y is incomlete or Z is invalid? Note that nowhere in that they claim X is secure.
- naasking 2y ago
  "Secure" is ambiguous, so of course they wouldn't claim X, whatever that is, is "secure". For instance, a microkernel does not provide cryptographic confidentiality, but some readers include such properties under the umbrella of "secure", so using that term would be dumb. When talking about proofs you describe the specific properties proven in a way that leaves no ambiguity.

WhitneyLand 2y ago

I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. 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 where set_endpoint ep data s ≡ s (ep := (IdleEP, data))