Quote:
Originally Posted by jggimi
Consider the size of the "proof" that would be required. seL4 is a micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.
|
Paper from around 2009 states that:
http://web1.cs.columbia.edu/~junfeng...apers/sel4.pdf
Quote:
seL4, a third-generation microkernel of L4 prove-
nance, comprises 8,700 lines of C code and 600 lines
of assembler.
|
and assembly code actually was not formally verified.
Generally speaking general purpose operating systems are not bug free. However I think that it would be possible that some small parts of it can be formally verified. There is a concept of privilege separation. It is implemented in OpenSSH daemon and Chromium. There is small, trusted part of program and a few other parts which are untrusted and large. It would be very interesting if somebody could write formally verified small, trusted part of these projects. It would be interesting if somebody could write formally verified pledge kernel's subsystem.