{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215458,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2007,7]]},"abstract":"<jats:p>\n            As computer systems become increasingly mission-critical, used in life-critical situations, and relied upon to protect intellectual property, operating-system reliability is becoming an ever growing concern. In the past, mission- and life-critical embedded systems consisted of simple microcontrollers running a small amount of software that could be validated using traditional and informal techniques. However, with the growth of software complexity, traditional techniques for ensuring software reliability have not been able to keep up, leading to an overall degradation of reliability. This paper argues that microkernels are the best approach for delivering truly trustworthy computer systems in the foreseeable future. It presents the NICTA operating-systems research vision, centred around the L4 microkernel and based on four core projects. The\n            <jats:italic>seL4<\/jats:italic>\n            project is designing an improved API for a secure microkernel,\n            <jats:italic>L4, verified<\/jats:italic>\n            will produce a full formal verification of the microkernel, Potoroo combines execution-time measurements with static analysis to determine the worst case execution profiles of the kernel, and\n            <jats:italic>CAmkES<\/jats:italic>\n            provides a component architecture for building systems that use the microkernel. Through close collaboration with\n            <jats:italic>Open Kernel Labs<\/jats:italic>\n            (a NICTA spinoff) the research output of these projects will make its way into products over the next few years.\n          <\/jats:p>","DOI":"10.1145\/1278901.1278904","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"3-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["Towards trustworthy computing systems"],"prefix":"10.1145","volume":"41","author":[{"given":"Gernot","family":"Heiser","sequence":"first","affiliation":[{"name":"NICTA and University of New South Wales, Sydney, Australia"}]},{"given":"Kevin","family":"Elphinstone","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales, Sydney, Australia"}]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales, Sydney, Australia"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales, Sydney, Australia"}]},{"given":"Stefan M.","family":"Petters","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales, Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2007,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945462"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/827272.829144"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/362258.362278"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168629"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/871910.871940"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of IASTED Software Engineering and Applications (SEA '04)","author":"Coulson G.","year":"2004","unstructured":"G. Coulson , G. Blair , P. Grace , A. Joolia , K. Lee , and J. Ueyama . A component model for building systems software . In Proceedings of IASTED Software Engineering and Applications (SEA '04) , Cambridge, MA, USA , Nov. 2004 . G. Coulson, G. Blair, P. Grace, A. Joolia, K. Lee, and J. Ueyama. A component model for building systems software. In Proceedings of IASTED Software Engineering and Applications (SEA '04), Cambridge, MA, USA, Nov. 2004."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159850"},{"key":"e_1_2_1_10_1","first-page":"28","volume-title":"Proceedings of the 1st International Workshop on Microkernels for Embedded Systems","author":"Elkaduwe D.","year":"2007","unstructured":"D. Elkaduwe , P. Derrin , and K. Elphinstone . A memory allocation model for an embedded microkernel . In Proceedings of the 1st International Workshop on Microkernels for Embedded Systems , pages 28 -- 34 , Sydney, Australia , Jan. 2007 . NICTA. D. Elkaduwe, P. Derrin, and K. Elphinstone. A memory allocation model for an embedded microkernel. In Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, pages 28--34, Sydney, Australia, Jan. 2007. NICTA."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1361397.1361417"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the USENIX Annual Technical Conference","author":"Fassino J.-P.","year":"2002","unstructured":"J.-P. Fassino , J.-B. Stefani , J. Lawall , and G. Muller . Think: A software framework for component-based operating system kernels . In Proceedings of the USENIX Annual Technical Conference , Monterey, CA, USA , June 2002 . J.-P. Fassino, J.-B. Stefani, J. Lawall, and G. Muller. Think: A software framework for component-based operating system kernels. In Proceedings of the USENIX Annual Technical Conference, Monterey, CA, USA, June 2002."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199805)28:6%3C569::AID-SPE158%3E3.0.CO;2-U"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the USENIX Annual Technical Conference, General Track","author":"Gabber E.","year":"1999","unstructured":"E. Gabber , C. Small , J. L. Bruno , J. C. Brustoloni , and A. Silberschatz . The Pebble component-based operating system . In Proceedings of the USENIX Annual Technical Conference, General Track , Monterey, CA, USA , June 1999 . E. Gabber, C. Small, J. L. Bruno, J. C. Brustoloni, and A. Silberschatz. The Pebble component-based operating system. In Proceedings of the USENIX Annual Technical Conference, General Track, Monterey, CA, USA, June 1999."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/581630.581634"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/976270.976281"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/800122.803950"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 1990 Summer USENIX Technical Conference","author":"Golub D.","year":"1990","unstructured":"D. Golub , R. Dean , A. Forin , and R. Rashid . Unix as an application program . In Proceedings of the 1990 Summer USENIX Technical Conference , June 1990 . D. Golub, R. Dean, A. Forin, and R. Rashid. Unix as an application program. In Proceedings of the 1990 Summer USENIX Technical Conference, June 1990."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018420.1019739"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/858336.858337"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266660"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.326"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/319195.319210"},{"key":"e_1_2_1_27_1","first-page":"113","volume-title":"Proceedings of the USENIX Workshop on Microkernels and other Kernel Architectures","author":"Hildebrand D.","year":"1992","unstructured":"D. Hildebrand . An architectural overview of QNX . In Proceedings of the USENIX Workshop on Microkernels and other Kernel Architectures , pages 113 -- 126 , Seattle, WA, USA , Apr. 1992 . D. Hildebrand. An architectural overview of QNX. In Proceedings of the USENIX Workshop on Microkernels and other Kernel Architectures, pages 113--126, Seattle, WA, USA, Apr. 1992."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378993.379006"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133572.1133615"},{"key":"e_1_2_1_30_1","volume-title":"Proc. 2nd ECOOP Workshop on Programm Languages and Operating Systems","author":"Hohmuth M.","year":"2005","unstructured":"M. Hohmuth and H. Tews . The VFiasco approach for a verified operating system . In Proc. 2nd ECOOP Workshop on Programm Languages and Operating Systems , Glasgow, UK , Oct. 2005 . M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In Proc. 2nd ECOOP Workshop on Programm Languages and Operating Systems, Glasgow, UK, Oct. 2005."},{"key":"e_1_2_1_31_1","first-page":"65","volume-title":"Proceedings of the 15th International Conference on Real-Time and Network Systems RTNS07","author":"John T.","year":"2007","unstructured":"T. John and R. Baumgartl . Exact cache characterization by experimental parameter extraction . In Proceedings of the 15th International Conference on Real-Time and Network Systems RTNS07 , pages 65 -- 74 , Nancy, France , Mar. 2007 . T. John and R. Baumgartl. Exact cache characterization by experimental parameter extraction. In Proceedings of the 15th International Conference on Real-Time and Network Systems RTNS07, pages 65--74, Nancy, France, Mar. 2007."},{"key":"e_1_2_1_32_1","volume-title":"L4.sec: Preliminary Microkernel Reference Manual","author":"Kauer B.","year":"2005","unstructured":"B. Kauer and M. V\u00f6lp . L4.sec: Preliminary Microkernel Reference Manual . Dresden University of Technology , http:\/\/os.inf.tu-dresden.de\/L4\/L4.Sec\/, Oct. 2005 . Last visited 2007-04-10. B. Kauer and M. V\u00f6lp. L4.sec: Preliminary Microkernel Reference Manual. Dresden University of Technology, http:\/\/os.inf.tu-dresden.de\/L4\/L4.Sec\/, Oct. 2005. Last visited 2007-04-10."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/354871.354874"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.08.039"},{"key":"e_1_2_1_35_1","unstructured":"L4Ka Team. L4Ka::Pistachio kernel. http:\/\/14ka.org\/projects\/pistachio\/.  L4Ka Team. L4Ka::Pistachio kernel. http:\/\/14ka.org\/projects\/pistachio\/."},{"key":"e_1_2_1_37_1","first-page":"17","volume-title":"Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation","author":"LeVasseur J.","year":"2004","unstructured":"J. LeVasseur , V. Uhlig , J. Stoess , and S. G\u00f6tz . Unmodified device driver reuse and improved system dependability via virtual machines . In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation , pages 17 -- 30 , San Francisco, CA, USA , Dec. 2004 . J. LeVasseur, V. Uhlig, J. Stoess, and S. G\u00f6tz. Unmodified device driver reuse and improved system dependability via virtual machines. In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation, pages 17--30, San Francisco, CA, USA, Dec. 2004."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800213.806531"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168633"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224075"},{"key":"e_1_2_1_41_1","volume-title":"Programming .NET Components. O'Reilly &amp","author":"L\u00f6wy J.","year":"2003","unstructured":"J. L\u00f6wy . Programming .NET Components. O'Reilly &amp ; Associates, Inc , 2003 . J. L\u00f6wy. Programming .NET Components. O'Reilly &amp; Associates, Inc, 2003."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800214.806541"},{"key":"e_1_2_1_45_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002."},{"key":"e_1_2_1_46_1","volume-title":"CORBA Component Model","author":"Object Management Group","year":"2006","unstructured":"Object Management Group . CORBA Component Model , 2006 . http:\/\/www.omg.org\/cgi-bin\/doc?formal\/06-04-01. Object Management Group. CORBA Component Model, 2006. http:\/\/www.omg.org\/cgi-bin\/doc?formal\/06-04-01."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.2242"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Fourth Symposium on Operating Systems Design and Implementation","author":"Reid A.","year":"2000","unstructured":"A. Reid , M. Flatt , L. Stoller , J. Lepreau , and E. Eide . Knit: Component composition for systems software . In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation , Oct. 2000 . A. Reid, M. Flatt, L. Stoller, J. Lepreau, and E. Eide. Knit: Component composition for systems software. In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation, Oct. 2000."},{"issue":"4","key":"e_1_2_1_49_1","first-page":"305","article-title":"Chorus distributed operating systems","volume":"1","author":"Rozier M.","year":"1988","unstructured":"M. Rozier , V. Abrossimov , F. Armand , I. Boule , M. Gien , M. Guillemont , F. Herrmann , C. Kaiser , S. Langlois , P. L\u00e9onard , and W. Neuhauser . Chorus distributed operating systems . Computing Systems , 1 ( 4 ): 305 -- 367 , 1988 . M. Rozier, V. Abrossimov, F. Armand, I. Boule, M. Gien, M. Guillemont, F. Herrmann, C. Kaiser, S. Langlois, P. L\u00e9onard, and W. Neuhauser. Chorus distributed operating systems. Computing Systems, 1(4):305--367, 1988.","journal-title":"Computing Systems"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:20020198"},{"key":"e_1_2_1_51_1","volume-title":"12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Work-in-Progress Session","author":"Schaefer S.","year":"2006","unstructured":"S. Schaefer , B. Scholz , S. M. Petters , and G. Heiser . Static analysis support for measurement-based WCET analysis . In 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Work-in-Progress Session , Sydney, Australia , Aug. 2006 . S. Schaefer, B. Scholz, S. M. Petters, and G. Heiser. Static analysis support for measurement-based WCET analysis. In 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Work-in-Progress Session, Sydney, Australia, Aug. 2006."},{"key":"e_1_2_1_52_1","volume-title":"www.coyotos.org","author":"Shapiro J.","year":"2006","unstructured":"J. Shapiro . Coyotos. www.coyotos.org , 2006 . J. Shapiro. Coyotos. www.coyotos.org, 2006."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319163"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/645540.657852"},{"key":"e_1_2_1_55_1","unstructured":"Sun Microsystems. Enterprise JavaBeans Specification Version 3.0. http:\/\/java.sun.com\/products\/ejb\/index.jsp.  Sun Microsystems. Enterprise JavaBeans Specification Version 3.0 . http:\/\/java.sun.com\/products\/ejb\/index.jsp."},{"key":"e_1_2_1_56_1","volume-title":"Component Software - Beyond Object-Oriented Programming","author":"Szyperski C.","year":"2002","unstructured":"C. Szyperski , D. Gruntz , and S. Murer . Component Software - Beyond Object-Oriented Programming . Addison-Wesley \/ ACM Press , second edition, 2002 . C. Szyperski, D. Gruntz, and S. Murer. Component Software - Beyond Object-Oriented Programming. Addison-Wesley \/ ACM Press, second edition, 2002."},{"key":"e_1_2_1_57_1","volume-title":"USA","author":"Tuch H.","year":"2005","unstructured":"H. Tuch , G. Klein , and G. Heiser . OS verification --- now! In Proceedings of the 10th Workshop on Hot Topics in Operating Systems, pages 7--12, Santa Fe, NM , USA , June 2005 . USENIX. H. Tuch, G. Klein, and G. Heiser. OS verification --- now! In Proceedings of the 10th Workshop on Hot Topics in Operating Systems, pages 7--12, Santa Fe, NM, USA, June 2005. USENIX."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.825699"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358825"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDSO.2001.4"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2006.49"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1278901.1278904","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1278901.1278904","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:58:23Z","timestamp":1750258703000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1278901.1278904"}},"subtitle":["taking microkernels to the next level"],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":58,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["10.1145\/1278901.1278904"],"URL":"https:\/\/doi.org\/10.1145\/1278901.1278904","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2007,7]]},"assertion":[{"value":"2007-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}