Dave@Work

Contact

CSE email
NICTA email
Work phone
(02) 8306 0486
Mobile
0407 487 919

Research

I am working towards a Ph.D. at CSE/NICTA (in the ERTOS group) under the supervision of Dr. Gernot Heiser.

pGCL for Isabelle

The pGCL for Isabelle package is available here.

L4.verified

My previous project was as a research assistant on the l4.verified project at NICTA. We produced the world's first formally verified operating system kernel. For details go to l4.verified.

Publications

[1]
David Cock. Exploitation as an inference problem. In Proceedings of the 4th ACM workshop on Security and artificial intelligence, AISec '11, pages 105-106, New York, NY, USA, 2011. ACM. [ bib | DOI | .pdf ]
Keywords: bayesian networks, side channels
[2]
David Cock. Lyrebird - assigning meanings to machines. In Gerwin Klein, Ralf Huuck, and Bastian Schlich, editors, Proceedings of the 5th Workshop on Systems Software Verification, pages 1-9, Vancouver, Canada, Oct 2010. USENIX. [ bib | .pdf ]
[3]
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, 53(6):107-115, Jun 2010. [ bib | .pdf ]
[4]
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. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pages 207-220, Big Sky, MT, USA, Oct 2009. ACM. [ bib | .pdf ]
[5]
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. Mind the gap: A verification framework for low-level C. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 500-515, Munich, Germany, Aug 2009. Springer-Verlag. [ bib | .pdf ]
[6]
David Cock. Bitfields and tagged unions in C: Verification through automatic generation. In Bernhard Beckert and Gerwin Klein, editors, Proceedings of the 5th International Verification Workshop, volume 372 of CEUR Workshop Proceedings, pages 44-55, Sydney, Australia, Aug 2008. [ bib | .pdf ]
[7]
David Cock, Gerwin Klein, and Thomas Sewell. Secure microkernels, state monads and scalable refinement. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science, pages 167-182, Montreal, Canada, Aug 2008. Springer-Verlag. [ bib | .pdf ]
[8]
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, Sep 2006. [ bib | .pdf ]
[9]
David Cock. The weyl algebras, 2004. [ bib | .pdf ]