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,000Does the proof have to be already present in the program and only checked in the kernel, as opposed to the kernel doing the proving ala ebpf? There's a full tradeoff continuum here, and there's no clear line between "proving from hints" and "checking a proof". See the discussion around SAT solver proof formats, where some require significant computation for "checking".
@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