Kevin Elphinstone
Associate Professor
Research Interests
Kevin works on operating system microkernels and the infrastructure required to support larger systems upon them. His current focus includes secure embedded operating systems suitable for formal verification, and for being the basis of secure systems for embedded devices. He also has interests in componentised operating systems, operating systems in general, security, real-time systems, computer architecture as it pertains to operating systems, and virtualisation.
Contact Details
| Phone: | +61 2 9490 5874 |
|---|---|
| Email: | k.elphinstone@unsw.edu.au |
More contact information is available at the Contact page.
Kevin Elphinstone is seconded to CSIRO from the University of New South Wales. He is a core member of the Trustworthy Systems project, with particular responsibility for systems design and implementation issues, OS security and real-time issues.
His teaching focusses on operating systems at the undergraduate and postgraduate level. His courses have a reputation for being extremely challenging and rewarding. See COMP3231 and COMP9242 for details.
Dr Elphinstone has been involved in architecting several operating systems including being the chief architect of the seL4 microkernel; a member of L4Ka microkernel team, an architect of the SawMill multi-server OS, and the Mungi single address space OS.
Projects
Current |
Past |
Dr Elphinstone led the seL4 project and is involved in the L4.verified projects, and is now looking towards creating a new class of trustworthy embedded systems based on a formally verified microkernel.
See the research pages for more details.
Collaborations
- ETH Zurich
- DSTO
Career Summary
Prior to joining CSIRO, Dr Elphinstone was a research associate in the System Architecture Group at the University of Karlsruhe, Germany. Before that, was a visiting scientist at the IBM TJ Watson Research Center, New York.
Qualifications
Dr Elphinstone has a Bachelor degree in Electrical Engineering, a Bachelor degree in Computer Science, and a PhD in Computer Science from the University of New South Wales (UNSW), Australia.
Affiliations
Dr Elphinstone is a member of the ACM, and the Special Interest Group in Operating Systems (SIGOPS).
Program Committees and Editorial Boards
- 2014 EuroSys
- 2013 Symposium on Operating Systems Principles
- 2012 EuroSys
- 2011 Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT)
- 2010 Asia-Pacific Workshop on Systems
- 2010 USENIX Annual Technical Conference
- 2009 European Workshop on System Security (EuroSec)
- 2008 Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT)
- 2007 Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT), co-chair
- 2007 Workshop on Microkernels for Embedded Systems, chair
Recognition and Awards
2012 Vice-Chancellor’s Awards for Initiatives that Enhance Learning (shared with Gernot Heiser)
Publications
- Google Scholar profile
- Best Papers
- TS Group Papers (2019, 2017, 2016, 2015, 2014, 2013, 2012, 2010, 2009, 2008, 2007, 2006, 2005, 2004, 2003, 1999, 1998, 1997, 1996, 1994, 1992)
- Papers not affiliated with TS (2007, 2001, 2000, 1999, 1996)
- Research Theses Supervised
Best Papers
|
 |
Gernot Heiser and Kevin Elphinstone L4 microkernels: The lessons from 20 years of research and deployment ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016 |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
|
 |
Kevin Elphinstone and Gernot Heiser From L3 to seL4 – what have we learnt in 20 years of L4 microkernels? ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013 |
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
Trustworthy Systems Group Papers
2019
|
|
|
Yanyan Shen, Gernot Heiser and Kevin Elphinstone Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019 |
2017
|
|
|
Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser A performance evaluation of rump kernels as a multi-server OS building block on seL4 Asia-Pacific Workshop on Systems (APSys), India, September, 2017 |
2016
|
|
|
Gernot Heiser and Kevin Elphinstone L4 microkernels: The lessons from 20 years of research and deployment ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016 |
2015
|
|
|
Yanyan Shen and Kevin Elphinstone Microkernel mechanisms for improving the trustworthiness of commodity hardware European Dependable Computing Conference, pp. 12, Paris, France, September, 2015 |
|
|
|
Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser For a microkernel, a big lock is fine Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015 |
2014
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
2013
|
|
|
Kevin Elphinstone and Gernot Heiser From L3 to seL4 – what have we learnt in 20 years of L4 microkernels? ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013 |
|
|
|
Kevin Elphinstone and Yanyan Shen Improving the trustworthiness of commodity hardware with software Workshop on Dependability of Clouds, Data Centers and Virtual Machine Technology (DCDV), pp. 6, Budapest, Hungary , June, 2013 |
|
|
|
Tudor-Ioan Salomie, Gustavo Alonso, Timothy Roscoe and Kevin Elphinstone Application level ballooning for efficient server consolidation EuroSys Conference, pp. 337–350, Prague, Czech Republic, April, 2013 |
2012
|
|
|
Stefan M. Petters, Kevin Elphinstone and Gernot Heiser Trustworthy real-time systems Advances in Real-Time Systems, pp. 191–206, Springer, 2012 |
2010
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Systems Software Verification, pp. 9, Vancouver, Canada , October, 2010 |
|
|
|
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–10, Chicago, IL, USA, October, 2010 |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an operating-system kernel Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010 Research Highlights paper |
2009
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
|
|
|
Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009 |
|
|
|
Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 – formally verifying a high-performance microkernel International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009 |
|
|
|
Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone Towards real multi-criticality scheduling IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155–164, Beijing, China, August, 2009 |
2008
|
|
|
Stefan M. Petters, Martin Lawitzky, Kevin Elphinstone and Ryan Heffernan Fitting an EDF based scheduling approach to componentised real(-time) systems IEEE Real-Time Systems Symposium, Barcelona, Spain, November, 2008 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel design for isolation and assurance of physical memory 1st Workshop on Isolation and Integration in Embedded Systems, pp. 35–40, Glasgow, UK, April, 2008 |
2007
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy queueing and direct process switch — merit or myths? Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 69–77, Pisa, Italy, December, 2007 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007 |
|
|
|
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
|
|
|
Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Workshop on Hot Topics in Operating Systems (HotOS), pp. 19–24, San Diego, USA, May, 2007 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel International Workshop on Microkernels for Embedded Systems, pp. 28–34, Sydney, Australia, January, 2007 |
2006
|
|
|
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: An approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006 |
|
|
|
Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 2006 |
|
|
|
Kevin Elphinstone and Scott Brandt Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications Technical Report, NICTA, July, 2006 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel data – first class citizens of the system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , pp. 39–43, Victor Harbor, South Australia, Australia, January, 2006 |
2005
|
|
|
Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005 |
|
|
|
Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser User-level device drivers: Achieved performance Journal of Computer Science and Technology, Volume 20, Number 5, pp. 654–664, September, 2005 |
|
|
|
Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser User-level device drivers: Achieved performance Technical Report PA005043, NICTA, July, 2005 |
2004
|
|
|
Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004 |
|
|
|
Kevin Elphinstone and Stefan Götz Initial evaluation of a user-level device driver framework Proceedings of the 9th Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004 |
2003
|
|
|
Andreas Haeberlen and Kevin Elphinstone User-level management of kernel memory Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
1999
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual: MIPS R4x00, version 1.11, kernel version 79 Sydney, Australia, May, 1999 |
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Proceedings of the 4th Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999 |
1998
|
|
|
Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke The Mungi single-address-space operating system Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998 |
1997
|
|
|
Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger Achieved IPC performance (still the foundation for extensibility) Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997 |
1996
|
|
|
Jerry Vochteloo, Kevin Elphinstone, Stephen Russell and Gernot Heiser Protection domain extensions in Mungi Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 161–165, Seattle, WA, USA, October, 1996 |
|
|
|
Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space Proceedings of the 7th International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996 |
1994
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single-address-space operating system Proceedings of the 17th Australasian Computer Science Conference (ACSC), pp. 271–80, Christchurch, New Zealand, January, 1994 |
1992
|
|
|
Stephen Russell, Alan Skea, Kevin Elphinstone, Gernot Heiser, Keith Burston, Ian Gorton and Graham Hellestrand Distribution + persistence = global virtual memory Proceedings of the 2nd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992 |
Papers without TS Affiliation
2007
|
|
|
Scott Brandt and Kevin Elphinstone Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT) Pisa, Italy (July, 2007). NICTA. |
2001
|
|
|
Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller The SawMill framework for VM diversity Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001 |
2000
|
|
|
Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther The Sawmill multiserver approach Proceedings of the 9th SIGOPS European Workshop, 2000 |
1999
|
|
|
Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999 |
|
|
|
Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park Flexible access control using IPC redirection Proceedings of the 7th Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999 |
1996
|
|
|
Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996 |
Research Theses Supervised
2019
|
|
|
Qian Ge Principled elimination of microarchitectural timing channels through operating-system enforced time protection PhD Thesis, UNSW, Sydney, Australia, October, 2019 |
|
|
 |
Hira Taqdees Syeda Low-level program verification under cached address translation PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
|
|
|
Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019 |
2016
|
|
|
Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016 |
2014
|
|
|
Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014 |
2013
|
|
|
Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013 |
2010
|
|
|
Dhammika Elkaduwe A principled approach to kernel memory management PhD Thesis, UNSW, Sydney, Australia, May, 2010 |