3 ms·

> 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 hig

> 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.

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.