Not logged in
Log in now
Create an account
Subscribe to LWN
LWN.net Weekly Edition for May 16, 2013
A look at the PyPy 2.0 release
PostgreSQL 9.3 beta: Federated databases and more
LWN.net Weekly Edition for May 9, 2013
(Nearly) full tickless operation in 3.10
development follows "formalized or semi-formalized methods."
Doesn't that rule out the Linux kernel (and therefore anything build on top of it) straight away?
Mandrake shoots for EAL5
Posted Sep 30, 2004 13:17 UTC (Thu) by pdc (guest, #1353)
I don't know how much of the system needs to be in the formal-methods category. Perhaps only the SELinux subsystem needs to have formal proofs, on the grounds that it then has oversight on the rest of the kernel. Maybe it already does (I do not know much about the SELinux internals, and it would depend on what counts as a proof).
True formal methods cannot be used direcly on anything with the scope of an operating-system kernel; I think that most research uses formally-verified tools to verify software that is then itself used to verify the rest of the system. Maybe this means the semi-formal methods could include creating new security-auditing code-checkers?
Copyright © 2013, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds