Third Generation
Recent work on microkernels has been focusing on formal specifications of the kernel API, and formal proofs of security properties of the API. The first example of this is a mathematical proof of the confinement mechanisms in EROS, based on a simplified model of the EROS API. More recently, a comprehensive set of machine-checked proofs has been performed of the properties of the protection model of seL4, a version of L4.
This has led to what is referred to as third-generation microkernels, characterised by a security-oriented API with resource access controlled by capabilities, virtualization as a first-class concern, novel approaches to kernel resource management, and a design goal of suitability for formal analysis, besides the usual goal of high performance. Examples are Coyotos, seL4, Nova, and Fiasco.OC.
In the case of seL4, complete formal verification of the implementation has been achieved, i.e. a mathematical proof that the kernel's implementation is consistent with its formal specification. This provides a guarantee that the properties proved about the API actually hold for the real kernel, a degree of assurance which goes beyond even CC EAL7.
Read more about this topic: Microkernel
Famous quotes containing the word generation:
“Every generation revolts against its fathers and makes friends with its grandfathers.”
—Lewis Mumford (1895–1990)
“My generation had Doris Day as a role model, then Gloria Steinem—then Princess Diana. We are the most confused generation.”
—Erica Jong (b. 1942)