> 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.
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
