Proof Engineering
- Aim: To develop knowledge, techniques and skills that facilitate practical, predictable and reliable application of large-scale formal verification to complex, real world problems.
-
Context:
Formal verification represents the next significant advancement in the
development of safety critical software: guarantees not only through design
and testing, but through proof of desireable properties for all possible
inputs.
A field in its infancy contains mostly one-off, small-scale and highly experimental developments. The field of software development has matured beyond this state largely due to its significant commercial successes. The set of knowledge, techniques and best-practice recommendations has been encompassed by the term Software Engineering.
The field of formal verification has had large-scale successes of its own. For instance, the Trustworthy Systems group is famous for its formal verification of the seL4 microkernel in the Isabelle/HOL theorem prover.
Existing proofs about the seL4 microkernel number over 700k lines. The proof engineering team updates these proofs for new kernel features, porting to new platforms, new Isabelle/HOL releases. We have clients, deadlines, time estimates, staff training, technical debt, and tool development. As Software Engineering is for software, Proof Engineering is the discipline of systematically treating large-scale formal proofs, including their development, maintenance, deployment, and project management aspects. -
Approach:
The Proof Engineering project aims to be grounded in reality.
By participating in large-scale projects such as SMACCM, we acquire knowledge about
real-world requirements. Within such projects, we maintain and verify new
features of the seL4 microkernel, such as
support for Mixed-Criticality Real-Time
Systems and Virtualisation.
To address the challenges in those verifications, we improve automation, for instance with a new proof method language (Eisbach), we significantly automate large verification steps such as abstraction from C code (AutoCorres) or completely automating entire verifications, for instance Proving Compilation Correctness. To assist our team with delivering on time and within budget, we conduct research into management aspects of large-scale proof, such as Proof Measurement and Estimation.
Present State
Our proof engineering innovation has now largely shifted to Proofcraft Pty Ltd, a company set up by former TS verification leaders Gerwin Klein, June Andronick and Rafal Kolanski. We are collaborating with Proofcraft on several projects.
Past Activities
- Platform and Product Development
- Verification
- Tool Development and Knowledge Acquisition
People
Past
|
Publications
2023
 
|
 |
Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser Formalising the prevention of microarchitectural timing channels by operating systems International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023 |
|
|
|
Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser Proving the absence of microarchitectural timing channels arXiv preprint arXiv:2310.17046, 2023 |
2022
|
|
|
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser and Gabriele Keller Property-based testing: Climbing the stairway to verification ACM SIGPLAN International Conference on Software Language Engineering, Auckland, New Zealand, December, 2022 Distinguished Artifact Award |
|
|
|
Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton Cyberassured systems engineering at scale IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022 |
2021
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell and Gabriele Keller Cogent: Uniqueness types and certifying compilation Journal of Functional Programming, Volume 31, 2021 |
2020
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein Towards provable timing-channel prevention ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020 |
|
|
 |
Hira Taqdees Syeda and Gerwin Klein Formal reasoning under cached address translation Journal of Automated Reasoning, Volume 64, Issue 6, pp. 911-945, June, 2020 |
|
|
|
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
2019
|
|
|
Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019 |
2018
|
|
|
Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart A formal approach to constructing secure air vehicle software IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018 |
|
|
|
Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller Bringing effortless refinement of data layouts to Cogent International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 134-149, Limassol, Cyprus, November, 2018 |
|
|
|
Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018 |
|
|
|
Callum Bannister, Peter Hoefner and Gerwin Klein Backwards and forwards with separation logic International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Program verification in the presence of cached address translation International Conference on Interactive Theorem Proving, pp. 542-559, Oxford, UK, July, 2018 |
|
|
|
Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, 2018 |
2017
|
|
|
Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot Heiser The Cogent case for property-based testing Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Shanghai, China, October, 2017 |
|
|
|
Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson Secure mathematically-assured composition of control models Technical Report, Data61, CSIRO, September, 2017 |
|
|
|
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor Provably trustworthy systems Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Reasoning about translation lookaside buffers Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017 |
2016
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein Refinement through restraint: Bringing down the cost of verification International Conference on Functional Programming, Nara, Japan, September, 2016 |
|
|
|
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
|
|
|
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein A framework for the automatic formal verification of refinement from Cogent to C International Conference on Interactive Theorem Proving, Nancy, France, August, 2016 |
|
|
|
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser Cogent: verifying high-assurance file system implementations International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175–188, Atlanta, GA, USA, April, 2016 |
|
|
|
Daniel Matichuk, Toby Murray and Makarius Wenzel Eisbach: A proof method language for isabelle Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016 |
2015
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015 |
|
|
|
Jasmin Blanchette, Maximilian Haslbeck, Daniel Matichuk and Tobias Nipkow Mining the archive of formal proofs Conference on Intelligent Computer Mathematics, pp. 3–17, Washington DC, USA, July, 2015 |
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of RPC stub code International Symposium on Formal Methods (FM), pp. 273–290, Oslo, Norway, June, 2015 |
|
|
|
Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples Empirical study towards a leading indicator for cost of formal software verification International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015 |
|
|
|
Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray An empirical research agenda for understanding formal methods productivity Information and Software Technology, Volume 60, pp. 102–112, January, 2015 |
2014
|
|
|
Matthias Daum, Nelson Billing and Gerwin Klein Concerned with the unprivileged: User programs in kernel refinement Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014 |
|
|
|
Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah CDSL version 1: Simplifying verification with linear types Technical Report, NICTA, October, 2014 |
|
|
|
Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski Productivity for proof engineering Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014 |
|
|
|
Daniel Matichuk, Makarius Wenzel and Toby Murray An Isabelle proof method language International Conference on Interactive Theorem Proving, pp. 390–405, Vienna, Austria, July, 2014 |
|
|
|
Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser Mathematically verified software kernels: Raising the bar for high assurance implementations Technical Report, NICTA, July, 2014 |
|
|
|
David Greenaway, Japheth Lim, June Andronick and Gerwin Klein Don't sweat the small stuff: Formal verification of C code without the pain ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014 |
|
|
|
Gerwin Klein Proof engineering challenges for large-scale verification Abstract, AI4FM/2014 Workshop. |
|
|
|
Gerwin Klein and Tobias Nipkow Applications of interactive proof to data flow analysis and security Software Systems Safety, pp. 77–134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 2014 |
|
|
|
Gerwin Klein Proof engineering considered essential International Symposium on Formal Methods (FM), pp. 16–21, Singapore, April, 2014 |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
2013
|
|
|
Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013 |
|
|
|
Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser File systems deserve verification too! Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, Pennsylvania, USA, November, 2013 A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64. |
|
|
|
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell Formally verified system initialisation Proceedings of the 15th International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013 |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass Formal specifications better than function points for code sizing International Conference on Software Engineering, pp. 1257–1260, San Francisco, USA, May, 2013 |
2012
|
|
|
Daniel Matichuk and Toby Murray Extensible specifications for automatic re-use of specifications and proofs 10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein Noninterference for operating system kernels International Conference on Certified Programs and Proofs, pp. 126–142, Kyoto, Japan, December, 2012 |
|
|
|
Daniel Matichuk Automatic function annotations for hoare logic Systems Software Verification, pp. 10, Sydney, Australia, November, 2012 |
|
|
|
June Andronick, Andrew Boyton and Gerwin Klein Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension Technical Report, NICTA, October, 2012 |
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105 Technical Report, NICTA, October, 2012 |
|
|
|
Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012 |
|
|
|
Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh AI @ NICTA AI Magazine, Volume 33, Number 3, pp. 115–127, September, 2012 |
|
|
|
June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012 |
|
|
|
David Greenaway, June Andronick and Gerwin Klein Bridging the gap: Automatic verified abstraction of C International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012 |
|
|
|
Gerwin Klein, Rafal Kolanski and Andrew Boyton Mechanised separation algebra International Conference on Interactive Theorem Proving, pp. 332–337, Princeton, USA, August, 2012 |
|
|
|
Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski Challenges and experiences in managing large-scale proofs Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32–48, Bremen, Germany, July, 2012 |
|
|
|
June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu Large-scale formal verification in practice: A process perspective International Conference on Software Engineering, pp. 1002–1011, Zurich, Switzerland, June, 2012 |
|
|
|
Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski Simulation modeling of a large scale formal verification process International Conference on Software and Systems Process, pp. 3–12, Zurich, Switzerland, June, 2012 |
|
|
|
June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 2012 |
|
|
|
Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012 |
|
|
|
Gerwin Klein Interactive proof: Applications to semantics Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012 |