It is common to prove hardware correctness these days.
Wikipedia mentions two verified operating systems, but I don’t know what has been verified about them, probably that certain kinds of privilege escalation are not possible. A problem is that one would like to run legacy machine code or C that is not specified, thus cannot be verified. Verification of the memory protection would show that such processes cannot interfere with each other. One can also deal with this by moving to languages without pointer arithmetic. Java makes a lot of security guarantees, but I don’t know if anyone has verified them for a runtime. A similar project that has been verified is Microsoft’s Singularity. The boast is that it provably does not need run-time memory protection.
Of course, it is very difficult to model user interactions and prevent processes from tricking the user into letting them interfere with each other.
Don’t deduce anything about the difficulty from the lack of deployment. The incentives for security are pretty low. The incentives for backwards compatibility are pretty high.
Try wikipedia on formal methods..
It is common to prove hardware correctness these days.
Wikipedia mentions two verified operating systems, but I don’t know what has been verified about them, probably that certain kinds of privilege escalation are not possible. A problem is that one would like to run legacy machine code or C that is not specified, thus cannot be verified. Verification of the memory protection would show that such processes cannot interfere with each other. One can also deal with this by moving to languages without pointer arithmetic. Java makes a lot of security guarantees, but I don’t know if anyone has verified them for a runtime. A similar project that has been verified is Microsoft’s Singularity. The boast is that it provably does not need run-time memory protection.
Of course, it is very difficult to model user interactions and prevent processes from tricking the user into letting them interfere with each other.
Don’t deduce anything about the difficulty from the lack of deployment. The incentives for security are pretty low. The incentives for backwards compatibility are pretty high.