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 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, which is now available as open source!
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
Timing Channels in seL4
Since the noninterference proof for seL4 showed that storage channels could be provable eliminated in a kernel such as seL4, my Ph.D. work was on tackling timing channels, which are invisible to the type of formal specification used for seL4. For more detail on this project, see here.
The figure on the right shows the effectiveness of one of our mitigation strategies, scheduled delivery, used here to mitigate the Lucky 13 attack against OpenSSL. This can be implemented without kernel modification, and achieves higher performance and better security than a constant-time implementation. For more information, see our CCS paper.
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, and is now in the archive of formal proofs. For recent versions, 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.
The figure on the right shows the residual channel on and Exynos4412, after using instruction-based scheduling to mitigate the cache-contention channel. For more details, see the paper, or my Ph.D. thesis, available below.
- The Last Mile—An empirical study of timing channels on seL4 (CCS 2014) slides
- Measuring and Mitigating Side Channels (ETH, EPFL, LIP6 2013; SSRG Summer School 2014) slides
- Lyrebird (SSV 2010; Cambridge 2013), slides
- Verifying Probabilistic Correctness in Isabelle with pGCL (SSV 2012), slides
- Practical Probability—Applying pGCL to Lattice Scheduling (ITP 2013), slides
- From Probabilistic Operational Semantics to Information Theory—Side Channels with pGCL in Isabelle (ITP 2014), slides
- Ten Years of Trustworthy Systems (ETH, EPFL 2014), slides
- Navigating the Literature (SSRG Student Bootcamp 2014), slides
|[CGMH14]||David Cock, Qian Ge, Toby Murray, and Gernot Heiser. The last mile: An empirical study of timing channels on seL4. In Proceedings of the 21st ACM Conference on Computer and Communications Security, Scottsdale, Arizona, USA, November 2014. [ .pdf ]|
|[Coc14b]||David Cock. Leakage in Trustworthy Systems. Phd thesis, Computer Science and Engineering, Sydney, Australia, August 2014. [ .pdf ]|
|[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 ]|
|[Coc14c]||David Cock. pGCL for Isabelle. Archive of Formal Proofs, July 2014. http://afp.sf.net/entries/pGCL.shtml, Formal proof development.|
|[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 ]|
This file was generated by bibtex2html 1.98.