On 07/16/15 09:58, Robert J. Hansen wrote: >> This has been done for the seL4 microkernel. Indeed the formal >> verification embodies a verification down to the actual machine code >> (ARM). There have been isolation and non-interference properties >> proved of this kernel. > > Yes, and I'm very impressed by the fortitude of the seL4 developers. :) > > A microkernel is not a complete operating system, though. I stand by my > original statement that there are no operating systems that have been > formally proven, although there have been some heroic efforts in proving > small but essential components like microkernels, cryptographic code, > and the like.
For that matter, there is only one PROCESSOR that has ever been formally proven correct. That is the '80s RSRE VIPER processor, which is/was a 386-class processor that was *specifically* designed from the start by the Royal Signals and Radar Establishment in such a way that it would be possible to formally prove that its design was correct (see http://link.springer.com/chapter/10.1007%2F978-1-4613-2007-4_2). I don't know whether it is still in use, but you can't buy it in any commodity computing device. It was intended for military and civil-aviation applications in which it was considered crucial that the design be error-free. -- Phil Stracchino Babylon Communications [email protected] [email protected] Landline: 603.293.8485
signature.asc
Description: OpenPGP digital signature
_______________________________________________ enigmail-users mailing list [email protected] To unsubscribe or make changes to your subscription click here: https://admin.hostpoint.ch/mailman/listinfo/enigmail-users_enigmail.net
