Trustworthy Systems

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://systems.ethz.ch/people/profile.MjEzNDEz.TGlzdC8zODkxLDEyOTU2NDI2OTI=.html

More contact information is available at the Contact page.

Photo of David Cock

Publication List

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

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
Best Paper Award
Hall of Fame Award


Trustworthy Systems Group Papers

2014

Abstract PDF 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
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014

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
Best Paper Award
Hall of Fame Award
Abstract PDF 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

Abstract PDF David Cock
Bitfields and tagged unions in C — verification through automatic generation
International Verification Workshop, pp. 44–55, Sydney, August, 2008
Abstract PDF 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

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