Editing L4 microkernel family (section)

== High assurance: seL4 ==
In 2006, the [[NICTA]] group commenced a from-scratch design of a [[Microkernel#Third generation|third-generation microkernel]], named seL4, with the aim of providing a basis for highly secure and reliable systems, suitable for satisfying security requirements such as those of [[Common Criteria]] and beyond. From the beginning, development aimed for [[formal verification]] of the kernel. To ease meeting the sometimes conflicting requirements of performance and verification, the team used a [[middle-out]] software process starting from an executable [[specification]] written in the language [[Haskell]].<ref name=Derrin_EKCC_06>
{{cite conference
 |last1=Derrin |first1=Philip
 |last2=Elphinstone |first2=Kevin
 |last3=Klein |first3=Gerwin
 |last4=Cock |first4=David
 |last5=Chakravarty |first5=Manuel M. T.
 |date=September 2006
 |title = Running the manual: an approach to high-assurance microkernel development
 |book-title = ACM SIGPLAN Haskell Workshop
 |pages = 60–71
 |location = [[Portland, Oregon]]
 |url = http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956
}}</ref>
seL4 uses [[capability-based security]] access control to enable formal reasoning about object accessibility.

A [[formal proof]] of functional correctness was completed in 2009.<ref name="Klein_EHACDEEKNSTW_09">
{{cite conference
 |last1 = Klein |first1 = Gerwin
 |last2 = Elphinstone |first2 = Kevin
 |last3 = Heiser |first3 = Gernot |author3-link = Gernot Heiser
 |last4 = Andronick |first4 = June
 |last5 = Cock |first5 = David
 |last6 = Derrin |first6 = Philip
 |last7 = Elkaduwe |first7 = Dhammika
 |last8 = Engelhardt |first8 = Kai
 |last9 = Kolanski |first9 = Rafal
 |last10 = Norrish |first10 = Michael
 |last11 = Sewell |first11 = Thomas
 |last12 = Tuch |first12 = Harvey
 |last13 = Winwood |first13 = Simon
 |date = October 2009
 |title = seL4: Formal verification of an OS kernel
 |book-title = 22nd ACM Symposium on Operating System Principles
 |location = Big Sky, MT, USA
 |url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
 |url-status = live
 |archive-url = https://web.archive.org/web/20110728022610/http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
 |archive-date = 2011-07-28
}}</ref>
The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as [[deadlock (computer science)|deadlock]]s, [[livelock]]s, [[buffer overflow]]s, arithmetic exceptions or use of [[Uninitialized variable|uninitialised variables]]. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.<ref name="Klein_EHACDEEKNSTW_09" /> The work on seL4 won the 2019 [[ACM SIGOPS]] Hall of Fame Award.

seL4 takes a novel approach to kernel resource management,<ref name="Elkaduwe_DE_08">
{{cite conference
 |last1 = Elkaduwe |first1 = Dhammika
 |last2 = Derrin |first2 = Philip
 |last3 = Elphinstone |first3 = Kevin
 |date = April 2008
 |title = Kernel design for isolation and assurance of physical memory
 |location = Glasgow, UK
 |doi = 10.1145/1435458
 |url = https://ts.data61.csiro.au/publications/nictaabstracts/Elkaduwe_DE_08.abstract.pml
 |conference = 1st Workshop on Isolation and Integration in Embedded Systems
 |access-date = 2020-02-22
 |archive-date = 22 February 2020
 |archive-url = https://web.archive.org/web/20200222061257/https://ts.data61.csiro.au/publications/nictaabstracts/Elkaduwe_DE_08.abstract.pml
 |url-status = dead
|url-access = subscription
 }}</ref> exporting the management of kernel resources to user level and subjects them to the same [[capability-based security|capability-based]] access control as user resources. This model, which was also adopted by [[Barrelfish (operating system)|Barrelfish]], simplifies reasoning about isolation properties, and was an enabler for later proofs that seL4 enforces the core security properties of integrity and confidentiality.<ref name="Klein_AEMSKH_14">
{{cite journal
 |last1 = Klein |first1 = Gerwin
 |last2 = Andronick |first2 = June
 |last3 = Elphinstone |first3 = Kevin
 |last4 = Murray |first4 = Toby
 |last5 = Sewell |first5 = Thomas
 |last6 = Kolanski |first6 = Rafal
 |last7 = Heiser |first7 = Gernot |author7-link=Gernot Heiser
 |date = February 2014
 |title = Comprehensive Formal Verification of an OS Microkernel
 |journal = ACM Transactions on Computer Systems
 |volume = 32
 |issue = 1
 |pages = 2:1–2:70
 |doi = 10.1145/2560537
 |citeseerx = 10.1.1.431.9140
 |s2cid = 4474342
}}</ref> The NICTA team also proved correctness of the translation from the programming language [[C (programming language)|C]] to executable [[machine code]], taking the [[compiler]] out of the [[trusted computing base]] of seL4.<ref name="Sewell_MK_13">{{cite conference
 |last1 = Sewell |first1 = Thomas
 |last2 = Myreen |first2 = Magnus
 |last3 = Klein |first3 = Gerwin
 |date = June 2013
 |title = Translation Validation for a Verified OS Kernel
 |book-title = ACM SIGPLAN Conference on Programming Language Design and Implementation
 |location = Seattle, WA, USA
 |doi = 10.1145/2491956.2462183
 |url = https://dl.acm.org/doi/pdf/10.1145/2491956.2462183
|url-access = subscription
 }}</ref>
This implies that the high-level security proofs hold for the kernel executable. seL4 is also the first published protected-mode OS kernel with a complete and sound [[worst-case execution time]] (WCET) analysis, a prerequisite for its use in hard [[real-time computing]].<ref name="Klein_AEMSKH_14"/>

On 29 July 2014, [[NICTA]] and [[General Dynamics C4 Systems]] announced that seL4, with end to end proofs, was now released under [[open-source license]]s.<ref name=seL4_OSS>
{{cite press release
 |title = Secure operating system developed by NICTA goes open source
 |url = https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |date = 29 July 2014
 |publisher = [[NICTA]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20160315212902/https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |archive-date = 15 March 2016
}}</ref>
The kernel [[source code]] and proofs are [[Software license|licensed]] under [[GNU General Public License#Version 2|GNU General Public License version 2]] (GPLv2), and most [[Library (computing)|libraries]] and [[Programming tool|tools]] are under the [[BSD licenses#2-clause|BSD 2-clause]]. In April 2020, it was announced that the seL4 Foundation was created under the umbrella of the [[Linux Foundation]] to accelerate development and deployment of seL4.<ref name=seL4_Foundation>
{{cite press release
 |title = Security Gets Support of Linux Foundation
 |url = https://www.linuxfoundation.org/press/press-release/sel4-microkernel-optimized-for-security-gets-support-of-linux-foundation/
 |date = 7 April 2020
 |publisher = [[Linux Foundation]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20160315212902/https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |archive-date = 15 March 2016
}}</ref>

The researchers state that the cost of formal software verification is lower than the cost of engineering traditional "high-assurance" software despite providing much more reliable results.<ref>{{cite journal |last1=Klein |first1=Gerwin |last2=Andronick |first2=June |last3=Elphinstone |first3=Kevin |last4=Murray |first4=Toby |last5=Sewell |first5=Thomas |last6=Kolanski |first6=Rafal |last7=Heiser |first7=Gernot |author7-link=Gernot Heiser |year=2014 |title=Comprehensive formal verification of an OS microkernel |url=http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf |journal=ACM Transactions on Computer Systems |volume=32 |page=64 |doi=10.1145/2560537 |url-status=live |archive-url=https://web.archive.org/web/20140803122308/http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf |archive-date=2014-08-03 |citeseerx=10.1.1.431.9140 |s2cid=4474342}}</ref> Specifically, the cost of one [[source lines of code|line of code]] during the development of seL4 was estimated at around {{US$|400}}, compared to {{US$|1000}} for traditional high-assurance systems.<ref>{{Cite AV media |last=Heiser |first=Gernot |author-link=Gernot Heiser |date=16 January 2015 |url=https://www.youtube.com/watch?v=lRndE7rSXiI |title=seL4 Is Free: What Does This Mean for You? |publisher=Linux.conf.au |place=Auckland, New Zealand}}</ref>

Under the Defense Advanced Research Projects Agency ([[DARPA]]) High-Assurance Cyber Military Systems (HACMS) program, NICTA together with project partners [[Rockwell Collins]], Galois Inc, the [[University of Minnesota]] and [[Boeing]] developed a high-assurance drone using seL4, along with other assurance tools and software, with planned technology transfer onto the optionally piloted autonomous [[Boeing AH-6]] Unmanned Little Bird helicopter being developed by Boeing. Final demonstration of the HACMS technology took place in Sterling, VA in April 2017.<ref name=hacms_demo>
{{cite press release
 |title = DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms
 |url = https://www.rockwellcollins.com/Data/News/2017-Cal-Yr/GS/FY17GSNR38-HACMS.aspx
 |date = 24 April 2017
 |publisher = [[Rockwell Collins]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20170511155335/http://rockwellcollins.com/Data/News/2017-Cal-Yr/GS/FY17GSNR38-HACMS.aspx
 |archive-date = 11 May 2017
}}</ref> DARPA also funded several [[Small Business Innovative Research]] (SBIR) contracts related to seL4 under a program started by [[John Launchbury]]. Small businesses receiving an seL4-related SBIR included: DornerWorks, Techshot, Wearable Inc, Real Time Innovations, and Critical Technologies.<ref name=sbir_sel4>
{{cite web
 |url = https://sbirsource.com/sbir/people/81829-dr-john-launchbury
 |title = DARPA Agency Sponsor Dr. John Launchbury
 |author = <!-- Unstated -->
 |date = 2017
 |website = SBIRSource
 |access-date = 16 May 2017
 |url-status = live
 |archive-url = https://web.archive.org/web/20170929000603/https://sbirsource.com/sbir/people/81829-dr-john-launchbury
 |archive-date = 29 September 2017
}}</ref>

In October 2023, [[Nio Inc.]] announced that their seL4-based SkyOS operating systems will be in mass-produced electric cars from 2024.<ref>{{Cite web |title=News about seL4 and the seL4 Foundation |url=https://sel4.systems/news/2023#nio-skyos |access-date=2024-09-20 |website=sel4.systems}}</ref>

In 2023, seL4 won the [[ACM Software System Award]].