David Cock
PhD Student
Research Interests
David's research area was metrics and countermeasures for side-channel leaks in componentized secure systems. He is now a researcher at ETH Zurich.
My previous research areas include: High-performance architectural simulation, Domain-specific languages, Theorem Prover performance and automation, Kernel development, Verified software
I am currently a Post-Doc at ETH Zurich.
Contact Details
| Phone: | +61 2 8306 0486 |
|---|---|
| Email: | david.cock@inf.ethz.ch |
| Web: | https:/ |
More contact information is available at the Contact page.
Projects
Past |
L4.verified
Collaborations
seL4
Career Summary
Research Engineer (L4.verified)
Qualifications
BSc.(Hons), Mathematics and Computer Science, UNSW, 2004
Affiliations
NICTA, UNSW
Publications
Best Papers
 
|
  |
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
2014
|
|
|
David Cock, Qian Ge, Toby Murray and Gernot Heiser The last mile: An empirical study of some timing channels on seL4 ACM Conference on Computer and Communications Security, pp. 570–581, Scottsdale, AZ, USA, November, 2014 |
|
|
|
David Cock Leakage in trustworthy systems PhD Thesis, UNSW, Sydney, Australia, August, 2014 |
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 |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009 |
2008
|
|
|
David Cock Bitfields and tagged unions in C — verification through automatic generation International Verification Workshop, pp. 44–55, Sydney, August, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement International Conference on Theorem Proving in Higher Order Logics, pp. 167–182, Montreal, Canada, August, 2008 |
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 |