4 ms·
Layers are useful for containing failures. What will happen when you get an undetected memory read error? A precondition of the proofs just left.
by jws 12y ago
Layers are useful for containing failures. What will happen when you get an undetected memory read error? A precondition of the proofs just left.
- TheLoneWolfling 12y agoHmm. Yeah, that would be a problem, wouldn't it. There are failures that cannot be proven to not occur at compile time, namely, as you mention, hardware errors. ECC will prevent some of these, but not all. So perhaps it should still be layered at the hardware level. (Reminds me of the JVM exploit that relied on waiting for random bitflips in RAM.) (Of course, this is a problem for traditional OSs as well, although the vulnerable area of memory (ring0 data structures / stack / etc) is smaller.) I wonder. It might be possible to express some of that in the proof requirements - "this program must not write to memory owned by another process even if a single bitflip occurs anywhere" - although that would probably balloon the complexity of the proof.