Summary
The sel4 microkernel system was designed to be a highly secure yet open source framework. It functions on a level below the operating system, between the device hardware and user software layers. With one of the largest proofs of security in existence as well as successful real world implementation, this microkernel is one of the best examples of cutting edge yet practical applications of cybersecurity. Optimization of the system is still ongoing.
Presenters
Gernot Heiser, Trustworthy Systems Research Group
Gernot is the Founder of the Trustworthy Systems Research Group (TS), which created seL4. He is Scientia Professor and John Lions Chair of Operating Systems at UNSW Sydney, where he has been teaching operating systems and leading research on L4 microkernels for more than 25 years. Besides that, his focus is on transferring TS technology to the real…
Presentation: The sel4 microkernel – mathematical proof of security
- Sel4 is an open source, high assurance, high performance operating system microkernel. Claimed as the worlds fastest microkernel, it has the most comprehensive mathematical proof of security.
- It is used in safety or security critical systems in automotive, avionics, defense, and space.
- Latency benchmarks as compared to Fisco.OC and Zircon
A microkernel operates underneath the operating system layer and exists between the hardware and user level software of the system.
Sel4 manages access between software within the machine.
Sel4 has a unique verification by mathematical proof. The abstract model was proven by C implementation and binary code. Security enforcement was also proven via availability, confidentiality, and integrity. At over 1 million lines of proofscript, the proof is the largest maintained proof base in an evolving system.
The microkernel is already being used in military grade security settings.
Refits of small and large autonomous systems successfully used the sel4 microkernel for security.
There is still ongoing research into improving sel4. Time protection, systems engineering, and cost reduction are some of the future optimization goals.
Seminar summary by Aaron King.
