I suppose it depends on what counts as 'semi-formalized'. It might be that part of the job is creating a 200-page SSADM description of the present Linux kernel-development process, thus retroactively making it semi-formalized...?
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 © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds