Originally posted by liam
View Post
There are limits to the scope of their proofs and the assumptions they make. Specifically, there are the 320 lines of assembly that you mentioned, but also the 1200 lines of boot code and in their handling of virtual memory, where they admit that "in this part of the proof, unlike the other parts, there is potential for human error".
And while bugs in hardware and drivers, or deliberate attempts to compromise the system lay outside the scope of the code, real world systems can and must take these factors into consideration. This is where the qualifier of being "meaningful" and "valuable" come into play. A kernel which assumes bug-free hardware, bug-free drivers, normal operating conditions and no bad actors may be meaningful and valuable from a research standpoint, but is not operationally meaningful. It's like having an ideal unicorn herder.
Leave a comment: