L4 microkernel family (English Wikipedia)

Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–188.
Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock, David; Chakravarty, Manuel M. T. (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop. Portland, Oregon. pp. 60–71.

dl.acm.org

Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109–114.
Sewell, Thomas; Myreen, Magnus; Klein, Gerwin (June 2013). "Translation Validation for a Verified OS Kernel". ACM SIGPLAN Conference on Programming Language Design and Implementation. Seattle, WA, USA. doi:10.1145/2491956.2462183.

apple.com

"iOS Security, iOS 12.3" (PDF). Apple Inc. May 2019. Archived (PDF) from the original on 24 June 2020.

ares-os.org

"Helios". ares-os.org. Retrieved 20 February 2023.

b-labs.com

dev.b-labs.com

"B Labs | Mobile Virtualization solutions, Android and Linux virtualization for the ARM architecture". Archived from the original on 2 February 2014. Retrieved 2 February 2014.

blackhat.com

Mandt, Tarjei; Solnik, Mathew; Wang, David (31 July 2016). "Demystifying the Secure Enclave Processor" (PDF). BlackHat USA. Las Vegas, Nevada, USA. Archived (PDF) from the original on 21 October 2016.

csiro.au

ts.data61.csiro.au

Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kernel design for isolation and assurance of physical memory. 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. Archived from the original on 22 February 2020. Retrieved 22 February 2020.

doi.org

Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology. 20 (5): 654–664. CiteSeerX 10.1.1.59.6766. doi:10.1007/s11390-005-0654-4. S2CID 1121537.
Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems. 2008: 1–14. doi:10.1155/2008/234710 (inactive 1 November 2024). S2CID 7430332.{{cite journal}}: CS1 maint: DOI inactive as of November 2024 (link)
Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kernel design for isolation and assurance of physical memory. 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. Archived from the original on 22 February 2020. Retrieved 22 February 2020.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). "Comprehensive Formal Verification of an OS Microkernel". ACM Transactions on Computer Systems. 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342.
Sewell, Thomas; Myreen, Magnus; Klein, Gerwin (June 2013). "Translation Validation for a Verified OS Kernel". ACM SIGPLAN Conference on Programming Language Design and Implementation. Seattle, WA, USA. doi:10.1145/2491956.2462183.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.
Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). ACM SIGPLAN Notices. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archived (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.

fortune.com

Elmer-DeWitt, Philip (28 October 2014). "Forecast: Apple will ship 310 million iOS devices in 2015". Fortune. Archived from the original on 27 September 2015. Retrieved 25 October 2015.

gdmissionsystems.com

"Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems. Archived from the original on 15 November 2017. Retrieved 26 April 2018.

github.com

"jserv/codezero: Codezero Microkernel". GitHub. Archived from the original on 15 August 2015. Retrieved 20 October 2020.
"F9 Microkernel". GitHub. Retrieved 20 October 2020.

hypervisor.org

"NOVA Microhypervisor website". Retrieved 9 January 2021.

kit.edu

os.itec.kit.edu

Liedtke, Jochen (December 1995). "On μ-Kernel Construction". Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on 25 October 2015.

l4dev.org

"Code Zero : Embedded Hypervisor and OS". Archived from the original on 11 January 2016. Retrieved 25 January 2016.

l4ka.org

l4ka.org: L4Ka::Pistachio microkernel Quote: "...The variety of supported architctures makes L4Ka::Pistachio an ideal research and development platform for a wide variety of systems..."

linuxfoundation.org

"Security Gets Support of Linux Foundation" (Press release). Linux Foundation. 7 April 2020. Archived from the original on 15 March 2016.

nicta.com.au

"NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. 24 November 2005. Archived from the original on 25 August 2006.
"Secure operating system developed by NICTA goes open source" (Press release). NICTA. 29 July 2014. Archived from the original on 15 March 2016.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.

ssrg.nicta.com.au

van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. Archived from the original on 1 March 2015. Retrieved 25 October 2015.

ok-labs.com

"Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. Archived from the original on 11 February 2012.
"Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 27 March 2012. Archived from the original on 2 July 2012.

pdx.edu

web.cecs.pdx.edu

Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). ACM SIGPLAN Notices. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archived (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.

psu.edu

citeseerx.ist.psu.edu

Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology. 20 (5): 654–664. CiteSeerX 10.1.1.59.6766. doi:10.1007/s11390-005-0654-4. S2CID 1121537.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). "Comprehensive Formal Verification of an OS Microkernel". ACM Transactions on Computer Systems. 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.

redox-os.org

"RedoxOS". RedoxOS.

rockwellcollins.com

"DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms" (Press release). Rockwell Collins. 24 April 2017. Archived from the original on 11 May 2017.

sbirsource.com

"DARPA Agency Sponsor Dr. John Launchbury". SBIRSource. 2017. Archived from the original on 29 September 2017. Retrieved 16 May 2017.

sel4.systems

"News about seL4 and the seL4 Foundation". sel4.systems. Retrieved 20 September 2024.

semanticscholar.org

api.semanticscholar.org

Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology. 20 (5): 654–664. CiteSeerX 10.1.1.59.6766. doi:10.1007/s11390-005-0654-4. S2CID 1121537.
Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems. 2008: 1–14. doi:10.1155/2008/234710 (inactive 1 November 2024). S2CID 7430332.{{cite journal}}: CS1 maint: DOI inactive as of November 2024 (link)
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). "Comprehensive Formal Verification of an OS Microkernel". ACM Transactions on Computer Systems. 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.

sigops.org

Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. Archived (PDF) from the original on 28 July 2011.

sr.ht

git.sr.ht

"~sircmpwn/helios – An experimental microkernel – sourcehut git". git.sr.ht. Retrieved 20 February 2023.

tu-dresden.de

os.inf.tu-dresden.de

"DROPS – Overview". Dresden University of Technology. Archived from the original on 7 August 2011. Retrieved 10 August 2011.
"Announce: Introducing Codezero". Dresden University of Technology.

usenix.org

Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: A system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264–278. Archived from the original on 17 February 2007.

web.archive.org

Liedtke, Jochen (December 1995). "On μ-Kernel Construction". Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on 25 October 2015.
"Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems. Archived from the original on 15 November 2017. Retrieved 26 April 2018.
"Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. Archived from the original on 11 February 2012.
"DROPS – Overview". Dresden University of Technology. Archived from the original on 7 August 2011. Retrieved 10 August 2011.
Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: A system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264–278. Archived from the original on 17 February 2007.
van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. Archived from the original on 1 March 2015. Retrieved 25 October 2015.
"NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. 24 November 2005. Archived from the original on 25 August 2006.
"Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 27 March 2012. Archived from the original on 2 July 2012.
"iOS Security, iOS 12.3" (PDF). Apple Inc. May 2019. Archived (PDF) from the original on 24 June 2020.
Mandt, Tarjei; Solnik, Mathew; Wang, David (31 July 2016). "Demystifying the Secure Enclave Processor" (PDF). BlackHat USA. Las Vegas, Nevada, USA. Archived (PDF) from the original on 21 October 2016.
Elmer-DeWitt, Philip (28 October 2014). "Forecast: Apple will ship 310 million iOS devices in 2015". Fortune. Archived from the original on 27 September 2015. Retrieved 25 October 2015.
Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. Archived (PDF) from the original on 28 July 2011.
Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kernel design for isolation and assurance of physical memory. 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. Archived from the original on 22 February 2020. Retrieved 22 February 2020.
"Secure operating system developed by NICTA goes open source" (Press release). NICTA. 29 July 2014. Archived from the original on 15 March 2016.
"Security Gets Support of Linux Foundation" (Press release). Linux Foundation. 7 April 2020. Archived from the original on 15 March 2016.
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.
"DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms" (Press release). Rockwell Collins. 24 April 2017. Archived from the original on 11 May 2017.
"DARPA Agency Sponsor Dr. John Launchbury". SBIRSource. 2017. Archived from the original on 29 September 2017. Retrieved 16 May 2017.
Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). ACM SIGPLAN Notices. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archived (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.
"jserv/codezero: Codezero Microkernel". GitHub. Archived from the original on 15 August 2015. Retrieved 20 October 2020.
"Code Zero : Embedded Hypervisor and OS". Archived from the original on 11 January 2016. Retrieved 25 January 2016.
"B Labs | Mobile Virtualization solutions, Android and Linux virtualization for the ARM architecture". Archived from the original on 2 February 2014. Retrieved 2 February 2014.

worldcat.org

search.worldcat.org

Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). ACM SIGPLAN Notices. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archived (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.

wrmlab.org

"WrmOS". Retrieved 20 October 2020.
"w4linux is paravirtualized Linux kernel working on WrmOS". Retrieved 20 October 2020.

youtube.com

Heiser, Gernot (16 January 2015). seL4 Is Free: What Does This Mean for You?. Auckland, New Zealand: Linux.conf.au.