Software Systems Research
Telephone: (+61) 2 8306 0486
NICTA personnel page
It has become apparent that producing systems software to the highest degree of assurance is possible, without sacrificing performance, and at lower cost than has historically been assumed. With careful design and effective use of automation, it should be possible to reduce the cost to the point that such an approach is commonplace for critical systems, and tackle currently unsolved issues, including concurrency. A strong familiarity with the discipline of low-level systems programming, and an understanding of the application domain will remain essential to ensure that performance is not sacrificed. Likewise, a clear understanding of the state of the art in formal verification is essential to ensure that systems are designed such that verification remains tractable.
- Ph.D., UNSW, "Leakage in Trustworthy Systems", adviser Gernot Heiser.
- Research Engineer, L4.verified.
- B.Sc. (hons), UNSW
I worked as a research engineer (or research assistant), under the supervision of Dr. Gerwin Klein, on the L4.verified project, which ran from 2005 until 2009, and produced the world's first formally verified general-purpose operating-system kernel.
I was responsible for the high-performance C and assembly implementation of the verified ARM kernel, which achieved the highest published IPC performance of any microkernel on this architecture.
I was also heavily involved in producing our underlying reasoning framework, in particular our monadic Hoare calculus.
Verified Bitfield Generation
We were able to automatically generate a substantial fraction of the code in seL4, and its associated proof of correctness, namely the low-level manipulation of packed structures (or bitfields). A description of this work has been published, and the tool itself is publically available
pGCL in Isabelle
To support my PhD work, I developed a formalisation of the probabilistic programming logic/refinement calculus pGCL, of McIver and Morgan. This package is available under an open source license. For details see here.
Covert Channel Analysis Suite
Also as part of my PhD work, I conducted a systematic large-scale empirical study of side-channel bandwidth on seL4. The toolkit that I built up in the course of this work, in order to efficiently process and analyse large sparse channel matrices, has also now been released.
|[Coc14a]||David Cock. From probabilistic operational semantics to information theory - side channels with pGCL in isabelle. In Proceedings of the 5th International Conference on Interactive Theorem Proving, pages 1-15, Vienna, Austria, July 2014. Springer. [ .pdf ]|
|[Coc14b]||David Cock. Leakage in Trustworthy Systems. PhD thesis, University of New South Wales, 2014. (under examination).|
|[Coc13]||David Cock. Practical probability: Applying pGCL to lattice scheduling. In Proceedings of the 4th International Conference on Interactive Theorem Proving, pages 1-16, Rennes, France, July 2013. [ DOI | .pdf ]|
|[Coc12]||David Cock. Verifying probabilistic correctness in Isabelle with pGCL. In Proceedings of the 7th Systems Software Verification, pages 1-10, Sydney, Australia, November 2012. [ DOI | .pdf ]|
|[Coc11]||David Cock. Exploitation as an inference problem. In Proceedings of the 4th ACM Workshop on Artificial Intelligence and Security, pages 105-106, Chicago, IL, USA, October 2011. [ DOI | .pdf ]|
|[Coc10]||David Cock. Lyrebird - assigning meanings to machines. In Gerwin Klein, Ralf Huuck, and Bastian Schlich, editors, Proceedings of the 5th Systems Software Verification, pages 1-9, Vancouver, Canada, October 2010. USENIX. [ .pdf ]|
|[KAE+10]||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, June 2010. [ DOI | .pdf ]|
|[KEH+09]||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, October 2009. ACM. [ DOI | .pdf ]|
|[WKS+09]||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, August 2009. Springer-Verlag. [ DOI | .pdf ]|
|[Coc08]||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, August 2008. [ .pdf ]|
|[CKS08]||David Cock, Gerwin Klein, and Thomas Sewell. Secure microkernels, state monads and scalable refinement. In Otmane Ait Mohamed, César Muñoz, Soﬁène Tahar, editor, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pages 167-182, Montreal, Canada, August 2008. Springer. [ DOI | .pdf ]|
|[DEK+06]||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, September 2006. [ DOI | .pdf ]|
|[Coc04]||David Cock. The weyl algebras, 2004. [ .pdf ]|
This file was generated by bibtex2html 1.97.