Abstract
Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abdelhalim I, Sharp J, Schneider S, Treharne H (2010) Formal verification of Tokeneer behaviours modelled in fUML using CSP. In: Formal methods and software engineering, volume 6447 of LNCS. Springer, pp 371–387
Brucker AD, Aït-Sadoune I, Crisafulli P, Wolff B (2018) Using the Isabelle Ontology Framework—linking the formal with the informal. In: Proceedings of the 11th international conference on intelligent computer mathematics (CICM), volume 11006 of LNCS. Springer, pp 23–38
Banham D (2020) Formalising the language of risk. Saf Syst 28(1), February 2020
Bishop PG, Bloomfield RE (1998) A methodology for safety case development. In: Redmill F, Anderson T (eds) Industrial perspectives of safety-critical systems: proceedings of 6th safety-critical systems symposium. Springer, pp 194–204
Blanchette JC, Bulwahn L, Nipkow T (2011) Automatic proof and disproof in Isabelle/HOL. In: Proceedings of 8th international symposium on frontiers of combining systems (FroCoS), volume 6989 of LNCS. Springer, pp 12–27
Barnes J, Chapman R, Johnson R, Widmaier J, Cooper D, Everett B (2006) Engineering the Tokeneer enclave protection software. In: Proceedings of IEEE international symposium on secure software engineering (ISSSE)
Bettini L (2016) Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd
Barmpis K, Kolovos D (2019) Hawk: towards a scalable model indexing architecture. In: Proceedings of the workshop on scalability inmodel driven engineering, pp 1–9
Brucker A, Wolff B (2019) Isabelle/DOF: Design and implementation. In: Proceedings of 17th international conference on software engineering and formal methods (SEFM), LNCS 11724. Springer, pp 279–292
Brucker A, Wolff B (2019) Using ontologies in formal developments targeting certification. In: Integrated formal methods (iFM), volume 11918 of LNCS. Springer, pp 65–82
Cooper D et al Tokeneer ID station: formal specification. Technical report, Praxis High Integrity Systems, August 2008. https://www.adacore.com/tokeneer
Cooper D et al Tokeneer ID station: security properties. Technical report, Praxis high integrity systems, August 2008. https://www.adacore.com/tokeneer
Cooper D et al Tokeneer ID station: summary report. Technical report S.P1229.81.1, Praxis High integrity systems, August 2008. https://www.adacore.com/tokeneer
Cruanes S, Hamon G, Owre S, Shankar N (2013) Tool integration with the evidential tool bus. In: Proceedings of 14th interantional conference on verification, model checking, and abstract interpretation (VMCAI), volume 7737 of LNCS. Springer
Common Criteria Consortium (2017). Common criteria for information technology security evaluation—part 1: Introduction and general model. Technical report CCMB-2017-04-001, Common Criteria Consortium, 2017
Cavalcanti A, Woodcock J (2006) A tutorial introduction to CSP in unifying theories of programming. In: Refinement techniques in software engineering, volume 3167 of LNCS. Springer, pp 220–268
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8), 453–457 (1975)
Diskin Z, Maibaum T, Wassyng A, Wynn-Williams S, Lawford M (2018) Assurance via model transformations and their hierarchical refinement. In: MODELS. IEEE
Denney E, Pai G (2013) A formal basis for safety case patterns. In: Proceedings of 32nd international conference on computer safety, reliability, and security (SAFECOMP), volume 8153 of LNCS. Springer, pp 21–32
Denney E, Pai G (2015) Towards a formal basis for modular safety cases. In: 34th inteenational confernece on computer safety, reliability, and security (SAFECOMP), volume 9337 of LNCS. Springer, pp 328–343
Denney, E., Pai, G.: Tool support for assurance case development. Autom Softw Eng 25, 435–499 (2018)
Foster S, Baxter J (2020) Automated algebraic reasoning for collections and local variables with lenses. In: Winter M (ed) Proceedings of 18th international conference on relational and algebraic methods in computer science (RAMiCS), volume 12062 of LNCS. Springer, April 2020
Foster S, Baxter J, Cavalcanti A, Miyazawa A, Woodcock J (2018) Automating verification of state machines with reactive designs and Isabelle/UTP. In 15th Intl. Conf. on Formal Aspects of Component Software (FACS), volume 11222 of LNCS, pages 137–155. Springer, October 2018
Foster S, Baxter J, Cavalcanti A, Woodcock J, Zeyda F (2020) Unifying semantic foundations for automated verification tools in Isabelle/UTP. Sci Comput Program 197, October 2020
Foster S, Cavalcanti A, Canham S, Woodcock J, Zeyda F (2019) Unifying theories of reactive design contracts. Theor Comput Sci 802, September 2019
Foster, S., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying theories of time with generalised reactive processes. Inf Process Lett 135, 47–52 (2018)
Foster S, Gleirscher M, Calinescu R (2020) Towards deductive verification of control algorithms for autonomous marine vehicles. In: 25th proceedings of international conference on engineering of complex computer systems (ICECCS). IEEE, October 2020
Foster, J., Greenwald, M., Moore, J., Pierce, B.: Schmitt A (2007) Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans Program Lang Syst 29(3), (May 2007)
Foster S, Nemouchi Y, Gleirscher M, Kelly T (2019) Isabelle/SACM: Computer-assisted assurance cases with integrated formal methods. In: Proceedings of 15th international conference on integrated formal methods (iFM), volume 11918 of LNCS. Springer, pp 379–398, December 2019
Foster S, Nemouchi Y, O'Halloran C, Tudor N, Stephenson K (2020) Formal model-based assurance cases in Isabelle/SACM: an autonomous underwater vehicle case study. In: Formal methods in software engineering (FormaliSE 2020): proceedings of the 8th international conference. ACM, 2020
Foster S (2019) Hybrid relations in Isabelle/UTP. In: UTP, volume 11885 of LNCS. Springer, pp 130–153
Foster S, Thiele B, Cavalcanti A, Woodcock J (2016) Towards a UTP semantics for Modelica. In: UTP, LNCS 10134. Springer, pp 44–64
Foster S, Zeyda F, Nemouchi Y, Ribeiro P, Wolff B (2019) Isabelle/UTP: mechanised theory engineering for unifying theories of programming. Archive of Formal Proofs, https://www.isa-afp.org/entries/UTP.html
Foster S, Zeyda F, Woodcock J (2016) Unifying heterogeneous state-spaces with lenses. In: Proceedings of 13th international colloquium on theoretical aspects of computing (ICTAC), LNCS 9965. Springer
Gleirscher M, Carlan C (2017) Arguing from hazard analysis in safety cases: a modular argument pattern. In High assurance systems engineering (HASE), 18th international symposium, pp 53–60
Gleirscher M, Foster S, Nemouchi Y (2019) Evolution of formal model-based assurance cases for autonomous robots. In Proceedings 17th International Conference on Software Engineering and Formal Methods (SEFM), LNCS 11724. Springer
Gleirscher M, Foster S, Woodcock J (2019) New opportunities for integrated formal methods. ACM Comput. Surv 52(6). https://dl.acm.org/doi/10.1145/3357231
Greenwell W, Knight J, Holloway CM, Pease J (2006) A taxonomy of fallacies in system safety arguments. In: Proceedings of 24th international system safety conference, pp 430–439, July 2006
Gleirscher, M., Marmsoler, D.: Formal methods in dependable systems engineering: a survey of professionals from Europe and North America. Empir Softw Eng 25(6), (2020)
Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice-Hall (1998)
Hawkins R, Habli I, Kolovos D, Paige R, Kelly T (2015) Weaving and assurance case from design: A model-based approach. In Proceedings 16th international symposium on high assurance systems engineering. IEEE, pp 110–117
Habli I, Kelly T (2014) Balancing the formal and informal in safety case arguments. In: VeriSure workshop, colocated with CAV, July 2014
Krodel J et al (2011) Formal methods supplement to DO-178C and DO-278A. RTCA, Inc
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans Softw Eng Methodol 11(2), 256–290 (2000)
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings 22nd symposium on operating systems principles (SOSP), ACM, pp 207–220
Kelly T (1998) Arguing safety—a systematic approach to safety case management. Ph.D. thesis, University of York
Kolovos D, Paige R, Polack F (2006) Eclipse development tools for Epsilon. In: Eclipse summit Europe, eclipse modeling symposium, vol 20062, p 200
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2), 125–43 (1977)
Lammich, P.: Refinement to imperative HOL. J Autom Reason 62(4), 481–503 (2017)
Miyazawa A, Ribeiro P, Li W, Cavalcanti A, Timmis J, Woodcock J (2019) Robochart: modelling and verification of the functional behaviour of robotic applications. Softw Syst Modell 18, January 2019
Munive JHY, Struth G, Foster S (2020) Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. In: 18th international conference on relational and algebraic methods in computer science (RAMiCS), volume 12062 of LNCS. Springer, pp 169–186, April 2020
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic, volume 2283 of LNCS. Springer
Safety of Autonomous Systems Working Group (2020) Safety assurance objectives for autonomous systems (version 2.0), volume SCS-153A. Safety Critical Systems Club, February 2020
Object Management Group (2020) Structured assurance case metamodel specification. https://www.omg.org/spec/SACM/, April 2020
Paige RF (1997) A meta-method for formal method integration. In: Formal methods Europe (FME), volume 1313 of LNCS. Springer, pp 473–494
Rivera V, Bhattacharya S, Cataño N (2016) Undertaking the Tokeneer challenge in Event-B. In: Proceedings of 4th international conference on formal methods in software engineering (FormaliSE). ACM Press
Rushby J (2013) Logic and epistemology in safety cases. In: Proceeidngs of 32nd international conference on computer safety, reliability, and security (SAFECOMP), volume 8153 of LNCS. Springer, pp 1–7
Rushby J (2014) Mechanized support for assurance case argumentation. In: New frontiers in artificial intelligence, volume 8417 of LNCS. Springer
Spivey, M.: The Z-notation–a reference manual. Prentice Hall, Englewood Cliffs, N. J. (1989)
Verbeek F, Havle O, Schmaltz J, Tverdyshev S, Blasum H, Langenstein W, Stephan B, Wolff B, Nemouchi Y (2015) Formal API specification of the PikeOS separation kernel. In: Proceedings of 7th NASA formal methods symposium (NFM 2015), volume 9058 of LNCS. Springer, pp 375–389
Woodcock J, Aydal EA, Chapman R (2010) The Tokeneer experiments. In: Reflections on the work of C.A.R. Hoare. Springer, pp 405–430
Wenzel M (2018) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In: Proceedings of 4th workshop on formal integrated development environment (F-IDE), pp 71–84
Wenzel M (2019) Interaction with formal mathematical documents in Isabelle/PIDE. In Proceedings of 12th international confrence on intelligent computer mathematics (CICM), volume 11617 of LNCS. Springer, pp 1–15
Wei R, Kelly T, Dai X, Zhao S, Hawkins R (2019) Model based system assurance using the structured assurance case metamodel. Syst Softw 154
Woodcock, J.: First steps in the verified software grand challenge. IEEE Comput 39(10), (2006)
Wenzel M, Wolff B (2007) Building formal method tools in the Isabelle/Isar framework. In Proceedings of the 20th international conference on theorem proving in higher order logics (TPHOLs), volume 4732 of LNCS. Springer, pp 352–367
Acknowledgements
This work is funded by EPSRC projects CyPhyAssure (CyPhyAssure Project: https://www.cs.york.ac.uk/circus/CyPhyAssure/) (grant reference EP/S001190/1) and RoboCalc (grant reference EP/M025756/1), the German Science Foundation (DFG; grant 381212925), and the Assuring Autonomy International Programme (AAIP; grant CSI:Cobot).
Author information
Authors and Affiliations
Corresponding author
Additional information
Lizeth Tarifa, Wolfgang Ahrendt and Heike Warheim
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Foster, S., Nemouchi, Y., Gleirscher, M. et al. Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM. Form Asp Comp 33, 855–884 (2021). https://doi.org/10.1007/s00165-021-00537-4
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00537-4