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:
“Our Indian said that he was a doctor, and could tell me some medicinal use for every plant I could show him ... proving himself as good as his word. According to his account, he had acquired such knowledge in his youth from a wise old Indian with whom he associated, and he lamented that the present generation of Indians “had lost a great deal.””
—Henry David Thoreau (1817–1862)
“But why should not the New Englander try new adventures, and not lay so much stress on his grain, his potato and grass crop, and his orchards,—raise other crops than these? Why concern ourselves so much about our beans for seed, and not be concerned at all about a new generation of men?”
—Henry David Thoreau (1817–1862)