5 ms·

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 clob

by 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
  - deleted 2y ago
    [deleted]
  - deleted 2y ago
    [deleted]
  - ryao 2y ago
    See the FAQ entry on seL4 having zero bugs: https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... Most who read that would expect the bug fixed in the linked GitHub PR to be impossible. The loophole was that the specification had a flaw, which was only mentioned as a vague hint about “unexpected features”.
    - Veserv 2y ago
      You keep dancing around the question of it being a memory corruption despite confidently asserting it as a clear, indisputable fact. Please support your claim by identifying the specific memory safety property that was violated and how it was violated.
      - ryao 2y ago
        I provided citations. Use them and do your own research. I think you will find the answers in what the seL4 developers published, but I have no interest in spending days or even weeks pointing to things until you are satisfied.
        Veserv 2y ago
        You made a strong claim which you have failed to support adequately and yet have continued to double down on. I did my research and presented my own interpretation which fundamentally disagrees with your interpretation. You have refused to address it, instead continuing to assert your interpretation without further detail. That does not prove my interpretation is correct, but it does indicate that the citations and evidence you have provided do not clearly lead to your conclusion and you neither identify the errors of my interpretation or directly demonstrate the correctness of your interpretation which could be done by demonstrating a simple counter-example demonstrating what memory is corrupted. You claim it is indisputable fact, yet you claim it would take "days or even weeks" to present a clear example of the corruption. I do not see how you can claim the bug is clearly and indisputably a memory corruption bug that anybody can see from the citations you provided when it would take even you so long to provide a clear example.
froh 2y ago
that's not how that works. writing into memory that doesn't belong to you is memory corruption. in this case: kernel (induced) memory corruption. and it's really a bad thing: functional safety technically boils down to the job of the kernel to provide "spatial and temporal freedom from interference", meaning all subsystems are isolated from each other. no "process" can write to another process, no process can starve another process. in this perspective, the kernel is another (special and privileged) process on the system. a kernel that randomly writes to user space processes is inherently unsuitable for functional safety. it's a huge no no. a failure in the goals and purpose of the kernel. and finding this here specifically was heavily shaking up confidence in formal specifications and formal proofs of compliance to these specs.
- Veserv 2y ago
  Again, the nature of the bug has not been appropriately established. It appears to me to be a bug where a output register that the kernel is expected to write is written with a incorrect, but legal value in certain cases. If my interpretation is correct, which it might not be, that is just a wrong output not a "memory corruption". The claim of "memory corruption" needs a clear detailed explanation of what memory safety property is violated and how it violates that. Second, no. The spatial separation guarantees you want from a kernel are that a domain can not induce spatial interference in a different domain that is isolated from the former. Internal memory corruption of a user domain, even uncontrolled asynchronous corruption by the kernel, makes it not very useful, but does not violate the protection property. This is a case where it is important to distinguish between "safety" and "usability". It is "safe", but not very "usable". If your memory corruption only occurs during specified system calls, then that problem is further reduced making it easier to "use" the system. If the memory corruption is highly constrained, say it only corrupts in-bounds of passed in pointers, then it is easier to "use" once again. If there is no memory corruption, but it instead sometimes outputs invalid garbage, that is easier to "use" once again. If it outputs legal, but incorrect values, that is easier to "use" once again. None of these affect "system safety", but all are important bugs to fix to enable to creation of functional, usable systems.
  - froh 2y ago

by Veserv 2y ago

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
- deleted 2y ago
  [deleted]
- deleted 2y ago
  [deleted]
- ryao 2y ago
  See the FAQ entry on seL4 having zero bugs: https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... Most who read that would expect the bug fixed in the linked GitHub PR to be impossible. The loophole was that the specification had a flaw, which was only mentioned as a vague hint about “unexpected features”.
  - Veserv 2y ago
    You keep dancing around the question of it being a memory corruption despite confidently asserting it as a clear, indisputable fact. Please support your claim by identifying the specific memory safety property that was violated and how it was violated.
    - ryao 2y ago
      I provided citations. Use them and do your own research. I think you will find the answers in what the seL4 developers published, but I have no interest in spending days or even weeks pointing to things until you are satisfied.
      - Veserv 2y ago
        You made a strong claim which you have failed to support adequately and yet have continued to double down on. I did my research and presented my own interpretation which fundamentally disagrees with your interpretation. You have refused to address it, instead continuing to assert your interpretation without further detail. That does not prove my interpretation is correct, but it does indicate that the citations and evidence you have provided do not clearly lead to your conclusion and you neither identify the errors of my interpretation or directly demonstrate the correctness of your interpretation which could be done by demonstrating a simple counter-example demonstrating what memory is corrupted. You claim it is indisputable fact, yet you claim it would take "days or even weeks" to present a clear example of the corruption. I do not see how you can claim the bug is clearly and indisputably a memory corruption bug that anybody can see from the citations you provided when it would take even you so long to provide a clear example.

froh 2y ago

that's not how that works. writing into memory that doesn't belong to you is memory corruption. in this case: kernel (induced) memory corruption. and it's really a bad thing: functional safety technically boils down to the job of the kernel to provide "spatial and temporal freedom from interference", meaning all subsystems are isolated from each other. no "process" can write to another process, no process can starve another process. in this perspective, the kernel is another (special and privileged) process on the system. a kernel that randomly writes to user space processes is inherently unsuitable for functional safety. it's a huge no no. a failure in the goals and purpose of the kernel. and finding this here specifically was heavily shaking up confidence in formal specifications and formal proofs of compliance to these specs.

Veserv 2y ago
Again, the nature of the bug has not been appropriately established. It appears to me to be a bug where a output register that the kernel is expected to write is written with a incorrect, but legal value in certain cases. If my interpretation is correct, which it might not be, that is just a wrong output not a "memory corruption". The claim of "memory corruption" needs a clear detailed explanation of what memory safety property is violated and how it violates that. Second, no. The spatial separation guarantees you want from a kernel are that a domain can not induce spatial interference in a different domain that is isolated from the former. Internal memory corruption of a user domain, even uncontrolled asynchronous corruption by the kernel, makes it not very useful, but does not violate the protection property. This is a case where it is important to distinguish between "safety" and "usability". It is "safe", but not very "usable". If your memory corruption only occurs during specified system calls, then that problem is further reduced making it easier to "use" the system. If the memory corruption is highly constrained, say it only corrupts in-bounds of passed in pointers, then it is easier to "use" once again. If there is no memory corruption, but it instead sometimes outputs invalid garbage, that is easier to "use" once again. If it outputs legal, but incorrect values, that is easier to "use" once again. None of these affect "system safety", but all are important bugs to fix to enable to creation of functional, usable systems.
- froh 2y ago