3 ms·

> If you build a bridge to a specification and the bridge collapses, does saying that the specification was wrong in any way lessen the reality that the bridge

> If you build a bridge to a specification and the bridge collapses, does saying that the specification was wrong in any way lessen the reality that the bridge failed? You framed this as a loss of confidence in the techniques that prove the absence of various flaws. This bug should not undermine such confidence as the bug was always in the place (the spec) that would allow such bugs.

ryao 2y ago
When seL4’s proof was published, people regarded seL4 to be flawless software and the fact that a problem in the specification would lead to issues was largely disregarded. Now that it is clear that the specification has had problems, seL4 should not be considered issue free, since there is no proof that its specification is issue free and there is proof that its authors made a nonzero number of mistakes. Anyone minimizing the impact of this flaw by saying “the specification was at fault here” completely misunderstands why the rest of the industry thought highly about these techniques in the first place. They had promised to produce flaw free software. Now that it is clear that is not true, the level of confidence the industry places in these techniques naturally needs to be adjusted. We cannot ignore the massive caveat of the specification needing to be flaw free anymore.
- naasking 2y ago
  > When seL4’s proof was published, people regarded seL4 to be flawless software No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true. > the level of confidence the industry places in these techniques naturally needs to be adjusted No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with.
  - froh 2y ago
    the point are people not using formal methods yet. automotive for example continues amazing aspire iso 26262 rain dances to tell themselves systems were safe. and does not allow to replace that with formal specs and proofs of compliance. that's just complementary the "real safety work" has to be done with paperwork v model tracing.
  - ryao 2y ago
    No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true. A number of people who read that interpreted it to mean seL4 is flawless. Now that flaws have been found, those people have had to re-evaluate their views. Those who understood seL4’s guarantees correctly are an extreme minority. No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with. >99.99% of the industry does not use formal methods, so those that understood the guarantees were weak enough to allow “impossible bugs” in the real world were an extreme minority. The rest of us had the view that I described. You can deride people who do not do formal verification, but I guarantee everything you use has unverified code written by people who do not do formal verification. If we restricted computers to formally verified code, we would not have working computers, embedded or otherwise.

ryao 2y ago

When seL4’s proof was published, people regarded seL4 to be flawless software and the fact that a problem in the specification would lead to issues was largely disregarded. Now that it is clear that the specification has had problems, seL4 should not be considered issue free, since there is no proof that its specification is issue free and there is proof that its authors made a nonzero number of mistakes. Anyone minimizing the impact of this flaw by saying “the specification was at fault here” completely misunderstands why the rest of the industry thought highly about these techniques in the first place. They had promised to produce flaw free software. Now that it is clear that is not true, the level of confidence the industry places in these techniques naturally needs to be adjusted. We cannot ignore the massive caveat of the specification needing to be flaw free anymore.

naasking 2y ago
> When seL4’s proof was published, people regarded seL4 to be flawless software No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true. > the level of confidence the industry places in these techniques naturally needs to be adjusted No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with.
- froh 2y ago
  the point are people not using formal methods yet. automotive for example continues amazing aspire iso 26262 rain dances to tell themselves systems were safe. and does not allow to replace that with formal specs and proofs of compliance. that's just complementary the "real safety work" has to be done with paperwork v model tracing.
- ryao 2y ago
  No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true. A number of people who read that interpreted it to mean seL4 is flawless. Now that flaws have been found, those people have had to re-evaluate their views. Those who understood seL4’s guarantees correctly are an extreme minority. No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with. >99.99% of the industry does not use formal methods, so those that understood the guarantees were weak enough to allow “impossible bugs” in the real world were an extreme minority. The rest of us had the view that I described. You can deride people who do not do formal verification, but I guarantee everything you use has unverified code written by people who do not do formal verification. If we restricted computers to formally verified code, we would not have working computers, embedded or otherwise.