>> A Secure Operating System is one which will not permit itself to be >> modified by the activity of an application program. these are >> available,-- just not used by the "mainstream” .
> No, they're not. You're talking about a unicorn here. There is > absolutely no operating system that meets this definition. To do this, > the entire OS would need formal Floyd-Hoare proofs from soup to nuts. > 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. See http://ssrg.nicta.com.au/projects/TS/l4.verified/ See also the sub-page titled “What we prove and what we assume”. A microkernel doesn’t provide very much; the secure operating system you desire might need to provide much more than memory management and threading. The verified microkernel only runs single-threaded. If you’re honest, your guarantees have to be very carefully stated. Michael ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ 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
