6 ms·

Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was

by ryao 2y ago

Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public: https://github.com/seL4/seL4/pull/243 https://github.com/seL4/seL4/pull/243 https://github.com/seL4/l4v/pull/453 https://github.com/seL4/l4v/pull/453 You will find a number of other memory related bugs in its issue tracker: https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Abug%20 https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab... Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug". I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software. Finally, to answer your question. The specification that seL4 meets is published on github: https://github.com/seL4/l4v https://github.com/seL4/l4v

isubasinghe 2y ago
I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.
- vacuity 2y ago
  Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.
  - deleted 2y ago
    [deleted]
- ryao 2y ago
  This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?
  - isubasinghe 2y ago
    There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?". I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not. I would need to have a look at the source code and proofs to confirm.
    - ryao 2y ago
      How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?
senderista 2y ago
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.
Veserv 2y ago
I do not see how that is a kernel memory corruption. I do not understand the code in context, but it appears to just be a case where the kernel incorrectly clobbered a userspace register which could result in incorrect userspace code execution. A error in that class would not inherently violate the system safety properties of the kernel itself. If so, that would only fall under a functional specification problem in the userspace API making it hard to use the userspace API in the intended/desired way. That would make it hard to use the kernel and verify your system using the kernel, but it would not constitute a kernel memory corruption which is what safety specifications and proofs of the kernel itself would be concerned with.
- ryao 2y ago
  I said that a memory corruption flaw was found in seL4. This is a fact. If you read the patch, you will see that a message that was just created had been being overwritten (which is explained in a code comment). This occurs inside the seL4 kernel code, and the proof previously permitted this behavior (according to one of the developers’ comments on the PR). The proof had to be amended to disallow this (which is the second PR). You should see this in the links.
  - Veserv 2y ago
    You can not just assert it is a memory corruption without explaining how it is a memory corruption. It appears to be a case where a wrong, but legal output is being stored. That does not, inherently, constitute a memory corruption. For example, suppose I have a sorting function. I pass it a vector of integers by reference and I intend it modify it into a sorted vector of integers. Instead, that function zeros every element of my vector. That is a sorted vector, so it technically meets the specification. That function “corrupted” the contents of my vector. That is not a “memory corruption” bug. That is just a plain bug where I output the wrong thing into memory. A memory corruption bug needs to violate the explicit or implicit invariants of the memory being “corrupted”. Out-of-bounds write, use-after-free, bypassing class interface, unguarded shared parallel access, etc. Writing incoherent, but legal values through provided pointers to uniquely owned memory is wrong, but not “memory corruption”. Furthermore, this is not a definition game where we are disagreeing on the definition of “memory corruption”. They do not claim blanket safety from “memory corruption” which may be a class up to interpretation. They claim safety from [1]: buffer overflows, null pointer dereferences, pointer type confusion, memory leaks, and other specifically named and defined forms of memory corruption errors. Please identify which specific enumerated memory safety property was violated. Again, I am not asserting it is not a memory corruption bug of some class. But it is very unclear from the patch and comments that the stated bug was actually a memory corruption without significantly more contextual detail. I literally do kernel development professionally and even I can not tell from the patch out-of-context; there is no way almost anybody else would be able to tell without more detail. [1] https://sel4.systems/Info/FAQ/proof.html https://sel4.systems/Info/FAQ/proof.html
ptman 2y ago
seL4 in Rust?
amw-zero 2y ago
We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs. What's important is how many bugs there are for each unit of "effort." For example, if this were hypothetically the only bug that was ever found, then that would be a pretty damn good argument that formal verification is effective. Because the bug rate of other non-verified operating systems is much higher.

by ryao 2y ago

isubasinghe 2y ago

I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.

vacuity 2y ago
Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.
- deleted 2y ago
  [deleted]
ryao 2y ago
This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?
- isubasinghe 2y ago
  There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?". I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not. I would need to have a look at the source code and proofs to confirm.
  - ryao 2y ago
    How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?

senderista 2y ago

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.

Veserv 2y ago

I do not see how that is a kernel memory corruption. I do not understand the code in context, but it appears to just be a case where the kernel incorrectly clobbered a userspace register which could result in incorrect userspace code execution. A error in that class would not inherently violate the system safety properties of the kernel itself. If so, that would only fall under a functional specification problem in the userspace API making it hard to use the userspace API in the intended/desired way. That would make it hard to use the kernel and verify your system using the kernel, but it would not constitute a kernel memory corruption which is what safety specifications and proofs of the kernel itself would be concerned with.

ryao 2y ago
I said that a memory corruption flaw was found in seL4. This is a fact. If you read the patch, you will see that a message that was just created had been being overwritten (which is explained in a code comment). This occurs inside the seL4 kernel code, and the proof previously permitted this behavior (according to one of the developers’ comments on the PR). The proof had to be amended to disallow this (which is the second PR). You should see this in the links.
- Veserv 2y ago
  You can not just assert it is a memory corruption without explaining how it is a memory corruption. It appears to be a case where a wrong, but legal output is being stored. That does not, inherently, constitute a memory corruption. For example, suppose I have a sorting function. I pass it a vector of integers by reference and I intend it modify it into a sorted vector of integers. Instead, that function zeros every element of my vector. That is a sorted vector, so it technically meets the specification. That function “corrupted” the contents of my vector. That is not a “memory corruption” bug. That is just a plain bug where I output the wrong thing into memory. A memory corruption bug needs to violate the explicit or implicit invariants of the memory being “corrupted”. Out-of-bounds write, use-after-free, bypassing class interface, unguarded shared parallel access, etc. Writing incoherent, but legal values through provided pointers to uniquely owned memory is wrong, but not “memory corruption”. Furthermore, this is not a definition game where we are disagreeing on the definition of “memory corruption”. They do not claim blanket safety from “memory corruption” which may be a class up to interpretation. They claim safety from [1]: buffer overflows, null pointer dereferences, pointer type confusion, memory leaks, and other specifically named and defined forms of memory corruption errors. Please identify which specific enumerated memory safety property was violated. Again, I am not asserting it is not a memory corruption bug of some class. But it is very unclear from the patch and comments that the stated bug was actually a memory corruption without significantly more contextual detail. I literally do kernel development professionally and even I can not tell from the patch out-of-context; there is no way almost anybody else would be able to tell without more detail. [1] https://sel4.systems/Info/FAQ/proof.html https://sel4.systems/Info/FAQ/proof.html

ptman 2y ago

seL4 in Rust?

amw-zero 2y ago

We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs. What's important is how many bugs there are for each unit of "effort." For example, if this were hypothetically the only bug that was ever found, then that would be a pretty damn good argument that formal verification is effective. Because the bug rate of other non-verified operating systems is much higher.