1. 2

  2. 1

    Submitting this in response to submissions talking Intel hardware and VMM’s. The high-assurance, security community originally went with separation kernels since they were small enough to bullet-proof them. They did well during security evaluations. The method usually split system into complicated, untrusted components in VM’s with security-critical stuff running directly on separation kernel with mediation of interactions. Especially covert-channel suppression. These ran on simplified hardware such as aerospace-style, PowerPC boards.

    Commercial, government, and academic groups kept trying to implement these on Intel hardware with similar assurance. They did the implementations. The problem is the hardware and firmware of commodity desktops and servers seem to do everything they can to screw up security. Plus, the market prefers feature-packed solutions like Xen platform. So, McDermott et al started the Xenon project many years ago to fork Xen into a medium-assurance product to see what could be done with a whole VMM. They selectively applied techniques from high-assurance, security development and certification. They eventually wrote this paper as a survey of issues and summary of their work. I’m not sure what’s happened from then on as I haven’t checked. Just bumped into the paper again and thought people might find it interesting.

    For open-source, seL4 (General Dynamics) and Muen (ETH) are two examples of separation kernels people could build on now. seL4 has formal verification but not fully EAL7 yet as it’s missing stuff. It can be expanded on. Muen isn’t high-assurance so much as coded in a language (SPARK Ada) that proves absence of most attacks. Genode already integrated both seL4 and Muen with varying levels of support/usability.



    Note that these require middleware on top to enforce security policies. An inter-partition communications system, partitioning networking/filesystem, and a trusted path (see Nitpicker GUI). These at a minimum for usability although I did network appliance designs without a filesystem with just network loading over secure transport.