3 ms·

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 rea

by 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
  fascinating. maybe terminology issues? where I come from, the kernel must not, ever, write to unwanted locations, even if in theory it could. wrong data as you point out is a completely different point of discussion, that could be a bug in the function which may or may not be safety critical , but hey, depending on the function you call, a wrong value could also come from some other process and the kernel is just the messenger of false data, not it's origin. no, "wrong value" that's not what I mean. and a bug in the user process, writing data to the wrong place, also is not what I'm talking about. what I consider violation of the functional safety requirement of spatial freedom form interference on the kernel is and unexpected "wrong location": the kernel "surprise surprise" writing to some address or some register (!) the kernel was not supposed to modify --- these _both_ are a violation of spatial freedom from interference, in the functional safety sense, to my limited understanding. "your dance area, my dance area" type of violations. this reading comes from discussions about how if at all it might be possible to achieve this with a monolithic FOSS Linux kernel. There the page table can be set up to give quite some protections, even protecting user space from the kernel, but then who ensures the page tables aren't corrupted "somehow" by some rando kernel module? And similar discussions exist to reliably save and restore user space registers on context switches to the kernel... but that's not what I wanted to get into, my point rather is: user space must be safe not only from other processes but also from the kernel. and that's something a microkernel can prove much easier than a monolith.
  - Veserv 2y ago
    It is a nuanced point. Certainly, you want to have a API that conforms to specifications and does not ruin your desired program invariants. But what if it does? What if you make a specification error? How do you modularize your specification so errors in one part of the specification do not invalidate the rest? For instance, suppose I have a kernel with spatial safety. I then add the system call, “Corrupt random memory in my own process at a random time”. Is that kernel still safe? All that function can do is destroy the invariants of the calling program. It can not turn a innocent isolated program malicious no matter how malicious another process is or became. What if nobody calls that function? It would certainly be hard to use such a function for any purpose. It may allow a malicious input crafted by a communicating malicious process to cause a problem in a innocent, but incorrect program. But a correct, isolated program, using APIs correctly would be unaffected no matter what any program does even with access to that new “memory corruption on demand” API. So, in this case, it would be fair and reasonable to classify the kernel as safe despite having a absurd system call in its specification. And, as basically any other API with a memory corruption is going to be less absurd, it only makes sense to classify those as “safe”, though very likely “unusable” or “hard to use”. The distinction then becomes being able to cause memory corruption in isolated, correct programs. In that case, a program is no longer safe even if it proves itself correct. You must prove the entire system is correct and all other programs correct to establish any guarantees about any individual program. You can no longer “isolate” or “separate” your analysis which makes the problem even more intractable. That is the first problem you want to solve which is what this definition is intended to achieve.

by froh 2y ago

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
fascinating. maybe terminology issues? where I come from, the kernel must not, ever, write to unwanted locations, even if in theory it could. wrong data as you point out is a completely different point of discussion, that could be a bug in the function which may or may not be safety critical , but hey, depending on the function you call, a wrong value could also come from some other process and the kernel is just the messenger of false data, not it's origin. no, "wrong value" that's not what I mean. and a bug in the user process, writing data to the wrong place, also is not what I'm talking about. what I consider violation of the functional safety requirement of spatial freedom form interference on the kernel is and unexpected "wrong location": the kernel "surprise surprise" writing to some address or some register (!) the kernel was not supposed to modify --- these _both_ are a violation of spatial freedom from interference, in the functional safety sense, to my limited understanding. "your dance area, my dance area" type of violations. this reading comes from discussions about how if at all it might be possible to achieve this with a monolithic FOSS Linux kernel. There the page table can be set up to give quite some protections, even protecting user space from the kernel, but then who ensures the page tables aren't corrupted "somehow" by some rando kernel module? And similar discussions exist to reliably save and restore user space registers on context switches to the kernel... but that's not what I wanted to get into, my point rather is: user space must be safe not only from other processes but also from the kernel. and that's something a microkernel can prove much easier than a monolith.
- Veserv 2y ago
  It is a nuanced point. Certainly, you want to have a API that conforms to specifications and does not ruin your desired program invariants. But what if it does? What if you make a specification error? How do you modularize your specification so errors in one part of the specification do not invalidate the rest? For instance, suppose I have a kernel with spatial safety. I then add the system call, “Corrupt random memory in my own process at a random time”. Is that kernel still safe? All that function can do is destroy the invariants of the calling program. It can not turn a innocent isolated program malicious no matter how malicious another process is or became. What if nobody calls that function? It would certainly be hard to use such a function for any purpose. It may allow a malicious input crafted by a communicating malicious process to cause a problem in a innocent, but incorrect program. But a correct, isolated program, using APIs correctly would be unaffected no matter what any program does even with access to that new “memory corruption on demand” API. So, in this case, it would be fair and reasonable to classify the kernel as safe despite having a absurd system call in its specification. And, as basically any other API with a memory corruption is going to be less absurd, it only makes sense to classify those as “safe”, though very likely “unusable” or “hard to use”. The distinction then becomes being able to cause memory corruption in isolated, correct programs. In that case, a program is no longer safe even if it proves itself correct. You must prove the entire system is correct and all other programs correct to establish any guarantees about any individual program. You can no longer “isolate” or “separate” your analysis which makes the problem even more intractable. That is the first problem you want to solve which is what this definition is intended to achieve.