zlacker

>>kkl+(OP)
Rutkowska is surely doing some of the most interesting research in this field.

>>gaius+Z7
Barely. Most of her work is behind what was done in the 80's and 90's for security kernels then 2000's for separation kernels. I criticized her for not building on proven foundations and methods. She censors my stuff but did eventually say and do some of same things. My Xen gripes, GUI trusted path... these come to mind.

For an example, here's an Orange Book A1-class VMM by legend Paul Karger. He's one of inventors of INFOSEC, genius designer/coder, and high-assurance veteran. Look at the design and assurance sections (p9 onward) of it to see what... in 90's... was necessary to secure a VMM via minimal privilege (POLA), correctness arguments, backdoor prevention, and covert channel suppression. Nothing today in OSS even has this baseline despite us discovering more problems and solutions. Re-reading it now, I noticed they were even doing continuous integration on it well before that became a fad.

http://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-A...

A modern example, one I cited on their mailing list, is INTEGRITY-178B. The features plus assurance activities are a nice illustration of high-assurance approach to microkernels for security or virtualization vs things like Xen. Quite a few things worth copying for security- or reliability-focused OSS projects. Approaches that got open-sourced from CompSci are in links below it.

http://www.ghs.com/products/safety_critical/integrity-do-178...

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=9EE...

http://genode-labs.com/publications/nfeske-genode-fosdem-201...

Note: GenodeOS is a competitor that uses components like above with architecture designed to lower risk in TCB like in high-assurance. It's nice work. Fundamental architecture needs peer review, though, to ensure it has claimed properties.