Accelerating Time-to-Market
Figure 3-2 . Kernel design approaches : Monolithic and microkernel ( taken from seL4 white paper
5 ).
seL4 joined the family of L4 microkernels in 2009 , when it was first released to the public . Since 2014 , it was made available as open-source software ; and , as of 2020 it is officially maintained by the seL4 Foundation . In contrast to previous L4 designs , seL4 was implemented completely from scratch . The developers therefore were able to free themselves from this legacy ( e . g . API and code ), and yet benefit from all the positive and negative experiences of almost 20 years of L4 based kernel design . One of seL4 ’ s outstanding features is provided by its inherent and unique focus on the development of highly secure systems without compromising performance . Therefore , two main security design concepts were introduced : the utilization of capabilities , and the application of formal verification techniques . Within the context of seL4 , capabilities represent a form of access token , which allows for a very fine-grained control over system resources . This supports the kernel ’ s isolation properties . Additionally , with the help of formal verification techniques , the absence of bugs inside the kernel implementation has been mathematically proven with respect to its specification . This is an achievement that still leaves the seL4 kernel as the world ’ s most advanced and most highly assured OS kernel .
Nevertheless , the actual implementation of services directly on top of the seL4 microkernel API itself can be quite a challenging task . To provide easier access to the underlying concepts , various helper libraries were developed , trying to hide the low-level kernel mechanisms of seL4 . This makes the microkernel ’ s security features and its mechanisms ( e . g . IPC , memory management ) easier to use for non-experts . The CAmkES ( Component Architecture for microkernel-based Embedded Systems ) framework extends this approach by providing “ a software development and runtime framework for quickly and reliably building microkernel-based multi-OS systems .” 6
As a result , a layered component architecture for the separation of concerns was established , allowing for model-driven development . This enables the ability to auto-generate CAmkES configuration files from system models , which will reduce configuration complexity .
5
6
July 2022