Skip to main content

Kevin Elphinstone

Kevin Elphinstone
Principal Researcher; Associate Professor, UNSW

Research Interests

Small operating system kernels 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:Kevin.Elphinstone@data61.csiro.au

More contact information is available at the Contact page.

Photo of Kevin Elphinstone

Publication List


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

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

Best Papers

Abstract PDF 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
Abstract PDF 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
Abstract
Slides
PDF
Presentation Video
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


NICTA Papers

2016

Abstract PDF 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

Abstract PDF Yanyan Shen and Kevin Elphinstone
Microkernel mechanisms for improving the trustworthiness of commodity hardware
European Dependable Computing Conference, pp. 12, Paris, France, September, 2015
Abstract
Slides
PDF 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

Abstract PDF 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

Abstract
Slides
PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF 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

Abstract PDF Stefan M Petters, Kevin Elphinstone and Gernot Heiser
Trustworthy real-time systems
Advances in Real-Time Systems, pp. 191-206, Springer, 2012

2010

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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

Abstract
Slides
PDF
Presentation Video
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
Abstract PDF
Presentation Video
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
Abstract PDF 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

Abstract PDF Stefan 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
Abstract PDF 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
Abstract PDF 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, Glasgow, UK, April, 2008

2007

Abstract PDF 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
Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3-11, December, 2007
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
Abstract PDF 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.
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF 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
Abstract PDF Timothy Roscoe, Kevin Elphinstone and Gernot Heiser
Hype and virtue
Workshop on Hot Topics in Operating Systems, pp. 19-24, San Diego, USA, May, 2007
Abstract PDF 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

Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF Kevin Elphinstone and Scott Brandt
Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications
Technical Report, NICTA, July, 2006
Abstract PDF 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

Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
Abstract PDF 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
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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

Abstract PDF 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

Non-NICTA Papers

2001

Abstract PS 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

Abstract PDF 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, pp. 109–114, Kolding, Denmark, 2000

1999

Abstract PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PS Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999
Abstract PDF 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, Rio Rico, AZ, USA, March, 1999
Abstract PS 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

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998
Abstract PS 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

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual – MIPS R4x00 — Version 1.0
Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997
Abstract PDF Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
Implementation and performance of the Mungi single-address-space operating system
Technical Report UNSW-CSE-TR-9704, UNSW, June, 1997
Abstract PDF 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, pp. 28–31, Cape Cod, MA, USA, May, 1997
Abstract PDF Gernot Heiser, Jerry Vochteloo, Kevin Elphinstone and Stephen Russell
The Mungi kernel API/Release 1.0
Technical Report UNSW-CSE-TR-9701, School of Computer Science and Engineering, March, 1997

1996

Abstract PS 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
Abstract PS 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
Abstract PDF Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke
Supporting persistent object systems in a single address space
Technical Report UNSW-CSE-TR-9601, UNSW, February, 1996
Abstract PDF 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

1995

Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995

1994

Abstract PDF Kevin Elphinstone, Stephen Russell and Gernot Heiser
Issues in implementing virtual memory
Technical Report UNSW-CSE-TR-9411, School of Computer Science and Engineering, September, 1994
Abstract PS 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

1993

Abstract PDF Kevin Elphinstone
Address space management issues in the Mungi operating system
Technical Report UNSW-CSE-TR-9312, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo
Mungi: A distributed single address-space operating system
Technical Report UNSW-CSE-TR-9314, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand
A distributed single address space system supporting persistence
Technical Report UNSW-CSE-TR-9302, UNSW, March, 1993

1992

Abstract PS 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

Research Theses Supervised

2016

Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, UNSW Computer Science & Engineering, Sydney, Australia, July, 2016

2014

Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014

2013

Abstract PDF 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

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.