Advertisement

Successes in Deployed Verified Software (and Insights on Key Social Factors)

  • June AndronickEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

In this talk, we will share our experience in the successful deployment of verified software in a wide range of application domains, and, importantly, our insights on the key factors enabling such successful deployment, in particular the importance of the social aspects of a group working effectively together.

Our formally verified microkernel, seL4, is now used across the world in a number of applications that keeps growing. Our experience is that such an uptake is enabled not only by a technical strategy, but also by a tight integration of people from multiple disciplines and with both research and engineering profiles. This requires a strong social culture, with well designed processes, for working as one unified team. We share our observations on what concrete social structures have been key for us in creating real-world impact from research breakthroughs.

Notes

Acknowledgements

The author would like to thank Gerwin Klein and Carroll Morgan for their feedback on drafts of this paper.

References

  1. 1.
    Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576–580 (1969)CrossRefGoogle Scholar
  2. 2.
    Hoare, C.A.R.: Viewpoint - retrospective: an axiomatic basis for computer programming. CACM 52(10), 30–32 (2009)CrossRefGoogle Scholar
  3. 3.
    Klein, G., et al.: seL4: Formal verification of an operating-system kernel. CACM 53(6), 107–115 (2010)CrossRefGoogle Scholar
  4. 4.
    Klein, G., Andronick, J., Kuz, I., Murray, T., Heiser, G., Fernandez, M.: Formally verified software in the real world. CACM 61, 68–77 (2018)CrossRefGoogle Scholar
  5. 5.
    Klein, G., et al.: seL4: Formal verification of an OS kernel. In: SOSP, pp. 207–220. ACM, Big Sky, October 2009Google Scholar
  6. 6.
    Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, pp. 415–429. IEEE, San Francisco, May 2013Google Scholar
  7. 7.
    Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  8. 8.
    Sewell, T., Myreen, M., Klein, G.: Translation validation for a verified OS kernel. In: PLDI, pp. 471–481. ACM, Seattle, June 2013Google Scholar
  9. 9.
    Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 325–340. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22863-6_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.CSIRO’s Data61 and UNSWSydneyAustralia

Personalised recommendations