5 ms·

The PRs make it clear that this was a bug in the spec, and the implementation behaved according to spec.

ryao 2y ago
That resulted in a memory corruption flaw in the C code. 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?
- snvzz 2y ago
  Many bridges had to collapse until we learned how to build them. As for seL4, the proofs (which are actually the state of the art in that field, yet definitely can be further perfected) are just one of the pillars supporting it e.g. the size of the TCB is another. We do not give up on the goal because there was a mistake once. Nor is the goal not worthy; this is the absolute best the world has atm.
  - ryao 2y ago
    I did not suggest giving up, but I did suggest that seL4 is not immune to the bugs it’s advertising claims to avoid.
- indolering 2y ago
  What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. Indeed, each release is expected to introduce new bugs and vendors typically sell service contracts based on the perpetual brokenness of existing software engineering processes. Whereas formally verified software typically has single digit numbers of bugs ... ever. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land.
  - mmooss 2y ago
    > Cartels and governments regularly hack phones and spy on and even kill activists. Your comment implies SeL4 will prevent these things from happening. Isn't that going way too far? It's a nice start, but we're nowhere near securing things on that level. Without looking into it, I'd put more faith in iPhone's lockdown mode.
    - indolering 2y ago
      We have a long way to crawl, but process isolation is the bedrock of all other security guarantees.
      - ryao 2y ago
        Tell me how process isolation prevents SQL injection. I could ask about any of a great variety of security issues, but I think SQL injection is a great choice for debunking “process isolation is the bedrock of all other security guarantees”. We do not have to worry because we have process isolation is basically this: https://web.archive.org/web/20240123122515if_/https://www.syslog.com/~jwilson/pics-i-like/kurios119.jpg https://web.archive.org/web/20240123122515if_/https://www.sy... I suspect you did not mean to say that, but your comments can be interpreted to mean that, especially when you suggest people will die if seL4 is not used as if nothing else matters, and inject that into a discussion of whether seL4’s is free of flaws (it is not). Using seL4 is like flattening the ground on which a building foundation will sit. Just because the ground was flattened to within microns of flatness does not mean there is nothing else wrong with the foundation and building that are built on it. Perhaps I am being pedantic, but you deserve this after suggesting the mere act of giving an opinion on seL4 made me an accessory to murder.
        throwway120385 2y ago
        The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.
- naasking 2y ago
  > 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

That resulted in a memory corruption flaw in the C code. 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?

snvzz 2y ago
Many bridges had to collapse until we learned how to build them. As for seL4, the proofs (which are actually the state of the art in that field, yet definitely can be further perfected) are just one of the pillars supporting it e.g. the size of the TCB is another. We do not give up on the goal because there was a mistake once. Nor is the goal not worthy; this is the absolute best the world has atm.
- ryao 2y ago
  I did not suggest giving up, but I did suggest that seL4 is not immune to the bugs it’s advertising claims to avoid.
indolering 2y ago
What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. Indeed, each release is expected to introduce new bugs and vendors typically sell service contracts based on the perpetual brokenness of existing software engineering processes. Whereas formally verified software typically has single digit numbers of bugs ... ever. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land.
- mmooss 2y ago
  > Cartels and governments regularly hack phones and spy on and even kill activists. Your comment implies SeL4 will prevent these things from happening. Isn't that going way too far? It's a nice start, but we're nowhere near securing things on that level. Without looking into it, I'd put more faith in iPhone's lockdown mode.
  - indolering 2y ago
    We have a long way to crawl, but process isolation is the bedrock of all other security guarantees.
    - ryao 2y ago
      Tell me how process isolation prevents SQL injection. I could ask about any of a great variety of security issues, but I think SQL injection is a great choice for debunking “process isolation is the bedrock of all other security guarantees”. We do not have to worry because we have process isolation is basically this: https://web.archive.org/web/20240123122515if_/https://www.syslog.com/~jwilson/pics-i-like/kurios119.jpg https://web.archive.org/web/20240123122515if_/https://www.sy... I suspect you did not mean to say that, but your comments can be interpreted to mean that, especially when you suggest people will die if seL4 is not used as if nothing else matters, and inject that into a discussion of whether seL4’s is free of flaws (it is not). Using seL4 is like flattening the ground on which a building foundation will sit. Just because the ground was flattened to within microns of flatness does not mean there is nothing else wrong with the foundation and building that are built on it. Perhaps I am being pedantic, but you deserve this after suggesting the mere act of giving an opinion on seL4 made me an accessory to murder.
      - throwway120385 2y ago
        The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.
naasking 2y ago
> 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.