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
| Phone: | +61 2 8306 0573 |
|---|---|
| Email: | kevin.elphinstone@nicta.com.au |
| Web: | http://www.cse.unsw.edu.au/~kevine/ |
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
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 |