Skip to main content

David Cock

David Cock
Research Engineer

Research Interests

My current research area is metrics and countermeasures for side-channel leaks in componentized secure systems.

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
Web:http://www.inf.ethz.ch/people/person-detail.html?persid=213413

More contact information is available at the Contact page.

Photo of David Cock

Projects

Past

L4.verified

Collaborations

seL4

Career Summary

Research Engineer (L4.verified)

Qualifications

BSc.(Hons), Mathematics and Computer Science, UNSW, 2004

Affiliations

NICTA, UNSW

NICTA 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
Abstract
Slides
PDF David Cock
From probabilistic operational semantics to information theory - side channels with pGCL in isabelle
Proceedings of the 5th International Conference on Interactive Theorem Proving, pp. 1–15, Vienna, Austria, July, 2014

2013

Abstract
Slides
PDF David Cock
Practical probability: Applying pGCL to lattice scheduling
Proceedings of the 4th International Conference on Interactive Theorem Proving, pp. 1–16, Rennes, France, July, 2013

2012

Abstract
Slides
PDF David Cock
Verifying probabilistic correctness in Isabelle with pGCL
Proceedings of the 7th Systems Software Verification, pp. 1–10, Sydney, Australia, November, 2012

2011

Abstract
Slides
PDF David Cock
Exploitation as an inference problem
4th Workshop on Artificial Intelligence and Security, pp. 105–106, Chicago, IL, USA, October, 2011

2010

Abstract
Slides
PDF David Cock
Lyrebird - assigning meanings to machines
Systems Software Verification, pp. 1–9, Vancouver, BC, Canada , October, 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
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
VERIFY08, pp. 44-55, Sydney, August, 2008
Abstract PDF David Cock, Gerwin Klein and Thomas Sewell
Secure microkernels, state monads and scalable refinement
Proceedings of the 21st 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