International Conference (Noordwijk, the Netherlands,
May 12–14). Curran, Red Hook, N Y, 2008.
9. Davis, J. and Myreen, M.O. The reflective Milawa
theorem prover is sound (down to the machine code
that runs it). Journal of Automated Reasoning 55, 2
(Aug. 2015), 117–183.
10. Dennis, J. B. and Van Horn, E. C. Programming
semantics for multi-programmed computations.
Commun. ACM 9, 3 (Mar. 1966), 143–155.
11. Elliott, T., Pike, L., Winwood, S., Hickey, P., Bielman,
J., Sharp, J., Seidel, E., and Launchbury, J. Guilt-free
Ivory. In Proceedings of the ACM SIGPLAN Haskell
Symposium (Vancouver, Canada, Sept. 3–4). ACM
Press, New York, 189–200.
12. Fernandez, M. Formal Verification of a Component
Platform. Ph.D. thesis. School of Computer Science &
Engineering, University of New South Wales, Sydney,
Australia, July 2016.
13. Fernandez, M., Andronick, J., Klein, G., and Kuz,
I. Automated verification of RPC stub code. In
Proceedings of the 20th International Symposium on
Formal Methods (Oslo, Norway, June 22–26). Springer,
Heidelberg, Germany, 2015, 273–290.
14. Floyd, R. W. Assigning meanings to programs.
Mathematical Aspects of Computer Science 19,
15. Gonthier, G. A Computer-Checked Proof of the Four-Colour Theorem. Microsoft Research, Cambridge, U.K,
16. Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen,
C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor,
R., Biha S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi,
E., and Théry, L. A machine-checked proof of the
Odd Order Theorem. In Proceedings of the Fourth
International Conference on Interactive Theorem
Proving, Volume 7998 of LNCS (Rennes, France, July
22–26). Springer, Heidelberg, Germany, 2013, 163–179.
17. Gu, R., Shao, Z., Chen, H., Wu, X. (N.)., Kim, J., Sjöberg, V.,
and Costanzo, C. CertiKOS: An extensible architecture
for building certified concurrent OS kernels. In
Proceedings of the 12th USENIX Symposium on
Operating Systems Design and Implementation
(Savannah, GA, Nov. 2–4). ACM Press, New York, 2016.
18. Hales, T.C., Adams, M., Bauer, G., Dang, D. T., Harrison,
J., Le Hoang, T., Kaliszyk, C., Magron, V., McLaughlin, S.,
Nguyen, T. T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso,
J., Rute, J., Solovyev, A., Ta, A. H. T., Tran, T.N., Trieu, T. T.,
Urban, J., Vu, K.K., and Zumkeller, R. A formal proof
of the Kepler Conjecture. Forum of Mathematics, Pi,
Volume 5. Cambridge University Press, 2017.
19. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R.,
Parno, B., Roberts, M.L., Setty, S. T.V., and Zill, B.
IronFleet: Proving practical distributed systems
correct. In Proceedings of the 25th ACM Symposium on
Operating Systems Principles (Monterey, CA, Oct. 5–7).
ACM Press, New York, 2015, 1–17.
20. Heiser, G. and Elphinstone, K. L4 microkernels: The
lessons from 20 years of research and deployment.
ACM Transactions on Computer Systems 34, 1 (Apr.
2016), 1:1–1: 29.
21. Kanav, S., Lammich, P., and Popescu, A. A
conference management system with verified
document confidentiality. In Proceedings of the
26th International Conference on Computer Aided
Verification (Vienna, Austria, July 18–22). ACM Press,
New York, 2014, 167–183.
22. Klein, G., Andronick, J., Elphinstone, K., Murray, T.,
Sewell, T., Kolanski, R., and Heiser, G. Comprehensive
formal verification of an OS microkernel. ACM
Transactions on Computer Systems 32, 1 (Feb. 2014),
23. Klein, G., Elphinstone, K., Heiser, G., Andronick, J.,
Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K.,
Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and
Winwood, S. seL4: Formal verification of an OS kernel.
In Proceedings of the 22nd ACM Symposium on
Operating Systems Principles (Big Sky, MT, Oct. 11–14).
ACM Press, New York, 2009, 207–220.
24. Kumar, R., Arthan, R., Myreen, M.O., and Owens, S.
Self-formalisation of higher-order logic: Semantics,
soundness, and a verified implementation. Journal of
Automated Reasoning 56, 3 (Apr. 2016), 221–259.
25. Kumar, R., Myreen, M., Norrish, M., and Owens,
S. CakeML: A verified implementation of ML. In
Proceedings of the 41st ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages
(San Diego, CA, Jan. 22–24). ACM Press, New York,
26. Kuz, I., Klein, G., Lewis, C., and Walker, A. capDL: A
language for describing capability-based systems. In
Proceedings of the First ACM Asia-Pacific Workshop
on Systems (New Delhi, India, Aug. 30–Sept. 3). ACM
Press, New York, 2010, 31–35.
27. Kuz, I., Liu, Y., Gorton, I., and Heiser, G. CAmkES:
A component model for secure microkernel-based
embedded systems. Journal of Systems and Software
(Special Edition on Component-Based Software
Engineering of Trustworthy Embedded Systems) 80, 5
(May 2007), 687–699.
28. Leroy, X. Formal verification of a realistic compiler.
Commun. ACM 52, 7 (July 2009), 107–115.
29. Murray, T., Matichuk, D., Brassil, M., Gammie, P.,
Bourke, T., Seefried, S., Lewis, C., Gao, X., and Klein, G.
seL4: From general-purpose to a proof of information
flow enforcement. In Proceedings of the 2013 IEEE
Symposium on Security and Privacy (San Francisco,
CA, May 19–22). IEEE Press, Los Alamitos, CA, 2013,
30. Pnueli, A., Siegel, M., and Singerman, E. Translation
validation. In Proceedings of the Fourth International
Conference on Tools and Algorithms for Construction
and Analysis of Systems (Lisbon, Portugal, Mar. 28–
Apr. 4). Springer, Berlin, Germany, 1998, 151–166.
31. Rushby, J. Design and verification of secure systems.
In Proceedings of the Eighth Symposium on Operating
System Principles (Pacific Grove, CA, Dec. 14–16).
ACM Press, New York, 1981, 12–21.
32. Ryzhyk, L., Chubb, P., Kuz, I., Le Sueur, E., and Heiser,
G. Automatic device driver synthesis with Termite. In
Proceedings of the 22nd ACM Symposium on Operating
Systems Principles (Big Sky, M T, Oct. 11–14). ACM
Press, New York, 2009, 73–86.
33. seL4 microkernel code and proofs; https://github.
34. Sewell, T., Kam, F., and Heiser, G. Complete, high-assurance determination of loop bounds and infeasible
paths for WCET analysis. In Proceedings of the 22nd
IEEE Real Time and Embedded Technology and
Applications Symposium (Vienna, Austria, Apr. 11–14).
IEEE Press, 2016.
35. Sewell, T., Myreen, M., and Klein, G. Translation
validation for a verified OS kernel. In Proceedings
of the 34th Annual ACM SIGPLAN Conference on
Programming Language Design and Implementation
(Seattle, WA, June 16–22). ACM Press, New York,
36. Sewell, T., Winwood, S., Gammie, P., Murray, T.,
Andronick, J., and Klein, G. seL4 enforces integrity.
In Proceedings of the International Conference
on Interactive Theorem Proving (Nijmegen, the
Netherlands, Aug. 22–25). Springer, Heidelberg,
Germany, 2011, 325–340.
Gerwin Klein ( firstname.lastname@example.org) is a Chief
Research Scientist at Data61, CSIRO, and Conjoint
Professor at UNSW, Sydney, Australia.
June Andronick ( email@example.com) is a
Principal Research Scientist at Data61, CSIRO, Conjoint
Associate Professor at UNSW, Sydney, Australia, and
the leader of the Trustworthy Systems group at Data61,
known for the formal verification of the seL4 operating
Matthew Fernandez ( firstname.lastname@example.org)
participated in this project while he was a Ph.D. student
at UNSW, Sydney, Australia, and is today a researcher at
Intel Labs, USA.
Ihor Kuz ( email@example.com) is a Principal
Research Engineer at Data61, CSIRO , and also a Conjoint
Associate Professor at UNSW, Sydney, Australia.
Toby Murray ( firstname.lastname@example.org) is a lecturer
at the University of Melbourne, Australia, and a Senior
Research Scientist at Data61, CSIRO.
Gernot Heiser ( email@example.com) is a Scientia
Professor and John Lions Chair of Computer Science at
UNSW, Sydney, Australia, a Chief Research Scientist at
Data61, CSIRO, and a fellow of the ACM, the IEEE, and
the Australian Academy of Technology and Engineering.
Copyright held by authors.
Publication rights licensed to ACM. $15.00
Fisher for having the vision to start the
program. John Launchbury coined
the term “seismic security retrofit.”
We thank Lee Pike for feedback on an
earlier draft. We would also like to acknowledge our HACMS project partners from Rockwell Collins, the University of Minnesota, Galois, and Boeing.
While we concentrated on the operating system aspects of the HACMS
project here, the rapid construction
of high-assurance systems includes
many further components, including
a trusted build, as well as architecture
and security-analysis tools. This material is based on research sponsored by
the U.S. Air Force Research Laboratory
and the Defense Advanced Research
Projects Agency under agreement
number FA8750-12-9-0179. The U.S.
government is authorized to reproduce and distribute reprints for governmental purposes notwithstanding
any copyright notation thereon. The
views and conclusions contained herein are those of the authors and should
not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied,
of the Air Force Research Laboratory,
Defense Advanced Research Projects
Agency, or U.S. government.
1. Alves-Foss, J., Oman, P. W., Taylor, C., and Harrison, S.
The MILS architecture for high-assurance embedded
systems. International Journal of Embedded Systems
2, 3-4 (2006), 239–247.
2. Blackham, B., Shi, Y., Chattopadhyay, S.,
Roychoudhury, A., and Heiser, G. Timing analysis of a
protected operating system kernel. In Proceedings of
the 32nd IEEE Real-Time Systems Symposium (Vienna,
Austria, Nov. 29–Dec. 2). IEEE Computer Society
Press, 2011, 339–348.
3. Boeing. Unmanned Little Bird H-6U; http://www.
4. Boyton, A., Andronick, J., Bannister, C., Fernandez,
M., Gao, X., Greenaway, D., Klein, G., Lewis, C., and
Sewell, T. Formally verified system initialisation. In
Proceedings of the 15th International Conference
on Formal Engineering Methods (Queenstown, New
Zealand, Oct. 29–Nov. 1). Springer, Heidelberg,
Germany, 2013 70–85.
5. Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Frans
Kaashoek, M., and Zeldovich, N. Using Crash
Hoare logic for certifying the FSCQ file system. In
Proceedings of the 25th ACM Symposium on Operating
Systems Principles (Monterey, CA, Oct. 5–7). ACM
Press, New York, 2015, 18–37.
6. Cock, D., Ge, Q., Murray, T., and Heiser, G. The last mile:
An empirical study of some timing channels on seL4.
In Proceedings of the ACM SIGSAC Conference on
Computer and Communications Security (Scottsdale,
AZ, Nov. 3–7). ACM Press, New York, 2014, 570–581.
7. Cock, D., Klein, G., and Sewell, T. Secure microkernels,
state monads and scalable refinement. In
Proceedings of the 21st International Conference on
Theorem Proving in Higher Order Logics (Montreal,
Canada, Aug. 18–21). Springer, Heidelberg, Germany,
8. Colbert, E. and Boehm, B. Cost estimation for
secure software & systems. In Proceedings of
the International Society of Parametric Analysts /
Society of Cost Estimating and Analysis 2008 Joint