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