4 ms·
From the paper "Comprehensive formal verification of an OS microkernel": "We still assume correctness of hand- written assembly code, boot code, management of c
by moblahbl4hblah 12y ago
From the paper "Comprehensive formal verification of an OS microkernel":
"We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"
http://www.nicta.com.au/pub?doc=7371 http://www.nicta.com.au/pub?doc=7371
There's a lot of assuming going on...I'm not saying that what they've done isn't interesting, but as always don't let yourself get carried away.
- deadgrey19 12y agoTo be fair. Every operating system assumes these things. At least the seL4 team has made this explicit. Secondly, there is a tiny amount of this code amounting to a few hundred lines of assembly and there are numerous verified hardware projects underway. Furthermore, as time has gone by, many of the original assumptions have been whittled away. This is by far the most robust operating system ever written.
- moblahbl4hblah 12y agoSure, I agree. There is indeed some work being done in making some of those parts more trustworthy. That being said, it will probably be sometime before that technology is usable by the average person. I'm really interested in seeing what they release.