When will an operating system or microkernel be developed that can verify formal proofs of security requirements and allow programs to run in kernel space? Such an OS would require programs to provide a formal proof ensuring that they will never access unallocated memory or violate other critical security constraints. Programs would operate in kernel space, with system calls having the same performance overhead as regular function calls. At a minimum, the OS should be capable to run programs like ssh and grep
1,000@brunoedwards yes. user might want to write a program in such a way that it becomes impossible to prove whether the program ever reaches a specific part of the code or not, and hence it will be impossible to determine the exact preconditions and postconditions for that part of the code. I guess for most of useful programs it will be easy to prove that program satisfies constraints and provide that proof with program