Philip Derrin - Research Engineer
Trustworthy Embedded Systems Project
Research Interests
Philip is a research engineer working on the seL4 project, which aims to develop a specification for a new secure microkernel as a successor to L4. His research interests include the construction of secure systems, and rapid prototyping and formalisation of microkernels in functional languages.
NICTA Projects
Philip is currently working on the design and specification of the seL4 microkernel API.
Qualifications
Philip was awarded a Bachelor of Science in Computer Science, with first class Honours, by the University of New South Wales in 2005. He was also awarded the Aurema Operating Systems prize in 2003.
Contact Details
| Phone: | +61 2 8306 0564 |
|---|
| Email: | philip.derrin@nicta.com.au |
|---|
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
|
|
|
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 |
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
