Kevin Elphinstone - Senior Researcher
Trustworthy Embedded Systems Project
Research Interests
Dr Elphinstone is a senior lecturer at the University of New South Wales. I specialise in teaching operating systems at the undergraduate and postgraduate level. My courses have a reputation for being extremely challenging and rewarding. See COMP3231 http://cgi.cse.unsw.edu.au/~cs3231/ and COMP9242 http://www.cse.unsw.edu.au/~cs9242/ for details.
I'm seconded to NICTA where I work within the ERTOS group leading and contributing to various world-class operating systems research projects.
Dr Elphinstone's main research interests lie in the area of operating systems, specifically 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 (and operating systems in general), security, real-time systems, computer architecture as it pertains to operating systems, and virtualisation.
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.
NICTA Projects
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.
Career Summary
Prior to joining NICTA, 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).
Contact Details
More contact information is available at the
ERTOS Contacts page.
Publications
Best Papers
|
 |
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 OS kernel
Communications of the ACM, 53(6), 107–115, (June, 2010) |
|
|
|
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
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper Award! |
NICTA Papers
2010
|
|
June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th Workshop on Scalable Trusted Computing, Chicago, IL, USA, October, 2010
Invited paper |
|
|
|
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 OS kernel
Communications of the ACM, 53(6), 107–115, (June, 2010) |
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
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper 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, Edinburgh, UK, August, 2009 |
|
|
|
Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone
Towards real multi-criticality scheduling
Proceedings of the 15th IEEE Conference on Embedded and Real-Time Computing and Applications, Beijing, China, August, 2009 |
2008
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Proceedings of Verified Software: Theories, Tools and Experiments 2008, 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, Glasgow, UK, April, 2008 |
2007
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco
Lazy scheduling and direct process switch — merit or myths?
Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007
Preliminary version |
|
|
|
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, 41(4), 3–11, (July, 2007) |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Proceedings of the 11th Workshop on Hot Topics in Operating Systems, 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
Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
A memory allocation model for an embedded microkernel
Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, 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
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 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 , 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, Germany, 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, 20(5), 654–664, (September, 2005)
See TR PA005043 for a preprint |
|
|
|
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 Goetz
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 |
2001
|
|
 |
Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller
The SawMill framework for VM diversity
Proceedings of the 6th Australasian Computer Systems Architecture Conference, Gold Coast, Australia, January, 2001 |
2000
|
|
|
Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin J. Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther
The Sawmill multiserver approach
Proceedings of the 9th SIGOPS European Workshop, Kolding, Denmark, 2000 |
1999
|
|
|
Kevin Elphinstone
Virtual memory in a 64-bit microkernel, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 1999
|
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Proceedings of the 4th Australasian Computer Architecture Conference, Auckland, New Zealand, January, 1999 |
1998
|
|
|
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 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
The Mungi single-address-space operating system
Software: Practice and Experience, 28(9), 901–928, (July, 1998) |
1997
|
|
|
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 |
|
|
|
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, University of NSW, June, 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, Cape Cod, MA, USA, May, 1997 |
|
|
|
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
|
|
|
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, 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, Cape May, NJ, USA, May, 1996 |
|
|
|
Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke
Supporting persistent object systems in a single address space
Technical Report UNSW-CSE-TR-9601, University of NSW, February, 1996 |
1995
|
|
|
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
|
|
|
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 |
|
|
|
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, Christchurch, New Zealand, January, 1994 |
1993
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand
A distributed single address space system supporting persistence
Technical Report UNSW-CSE-TR-9302, University of NSW, March, 1993 |
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, Dourdan, France, September, 1992 |
Research Theses Supervised
2010
|
|
|
Dhammika Elkaduwe
A principled approach to kernel memory management, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2010
|
