Skip to main content
SpringerLink
Log in

Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods

  • Conference paper
  • First Online:
Book cover Integrated Formal Methods (IFM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11918))

Included in the following conference series:

Abstract

Assurance cases (ACs) are often required to certify critical systems. The use of integrated formal methods (FMs) in assurance can improve automation, increase confidence, and overcome errant reasoning. However, ACs can rarely be fully formalised, as the use of FMs 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 for the computer-assisted construction of ACs called Isabelle/SACM. The framework guarantees well-formedness, consistency, and traceability of ACs, and allows a tight integration of formal and informal evidence of various provenance. To validate Isabelle/SACM, we present a novel formalisation of the Tokeneer benchmark, verify its security requirements, and form a mechanised AC that combines the resulting formal and informal artifacts.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    OMG Structured Assurance Case Metamodel: http://www.omg.org/spec/SACM/.

  2. 2.

    Supporting materials, including Isabelle theories, can be found on our website.

  3. 3.

    Project website: https://www.adacore.com/tokeneer.

  4. 4.

    We model all parts of SACM in DOF, but omit details for sake of brevity.

  5. 5.

    The administrator (role “guard”) part is verified but omitted for space reasons.

  6. 6.

    Most TIS operations have been mechanised, using the same names as in [6].

  7. 7.

    There seems to be no invariant that ensures the presence of a valid fingerprint in [6]. We also believe that a necessary invariant regarding admin roles is missing.

  8. 8.

    CyPhyAssure Project: https://www.cs.york.ac.uk/circus/CyPhyAssure/.

References

  1. Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: Proceedings of IEEE International Symposium on Secure Software Engineering (ISSSE) (2006)

    Google Scholar 

  2. Bishop, P.G., Bloomfield, R.E.: A methodology for safety case development. In: Redmill, F., Anderson, T. (eds.) Industrial Perspectives of Safety-Critical Systems, pp. 194–204. Springer, London (1998). https://doi.org/10.1007/978-1-4471-1534-2_14

    Chapter  Google Scholar 

  3. Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2

    Chapter  Google Scholar 

  4. Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the isabelle ontology framework. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 23–38. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96812-4_3

    Chapter  Google Scholar 

  5. Common Criteria Consortium: Common criteria for information technology security evaluation - part 1: introduction and general model. Technical report CCMB-2017-04-001 (2017). https://www.commoncriteriaportal.org

  6. Cooper, D., et al.: Tokeneer ID station: formal specification. Technical report, Praxis High Integrity Systems, August 2008. https://www.adacore.com/tokeneer

  7. Cooper, D., et al.: Tokeneer ID station: security properties. Technical report, Praxis High Integrity Systems, August 2008. https://www.adacore.com/tokeneer

  8. Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 275–294. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_18

    Chapter  Google Scholar 

  9. Denney, E., Pai, G.: Tool support for assurance case development. Autom. Softw. Eng. 25, 435–499 (2018)

    Article  Google Scholar 

  10. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  Google Scholar 

  11. Diskin, Z., Maibaum, T., Wassyng, A., Wynn-Williams, S., Lawford, M.: Assurance via model transformations and their hierarchical refinement. In: MODELS. IEEE (2018)

    Google Scholar 

  12. Foster, S., Baxter, J., Cavalcanti, A., Miyazawa, A., Woodcock, J.: Automating verification of state machines with reactive designs and Isabelle/UTP. In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 137–155. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_7

    Chapter  Google Scholar 

  13. Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. Theoretical Computer Science, September 2019

    Google Scholar 

  14. Foster, S., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying theories of time with generalised reactive processes. Inf. Process. Lett. 135, 47–52 (2018)

    Article  MathSciNet  Google Scholar 

  15. Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for modelica. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 44–64. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52228-9_3

    Chapter  Google Scholar 

  16. Foster, S., Zeyda, F., Nemouchi, Y., Ribeiro, P., Wolff, B.: Isabelle/UTP: mechanised theory engineering for unifying theories of programming. Archive of Formal Proofs (2019). https://www.isa-afp.org/entries/UTP.html

  17. Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295–314. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_17

    Chapter  Google Scholar 

  18. Gleirscher, M., Foster, S., Nemouchi, Y.: Evolution of formal model-based assurance cases for autonomous robots. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 87–104. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_5

    Chapter  Google Scholar 

  19. Gleirscher, M., Foster, S., Woodcock, J.: New opportunities for integrated formal methods. ACM Comput. Surv. (2019, in Press). Preprint: https://arxiv.org/abs/1812.10103

  20. Greenwell, W., Knight, J., Holloway, C.M., Pease, J.: A taxonomy of fallacies in system safety arguments. In: Proceedings of the 24th International System Safety Conference, July 2006

    Google Scholar 

  21. Habli, I., Kelly, T.: Balancing the formal and informal in safety case arguments. In: VeriSure Workshop, colocated with CAV, July 2014

    Google Scholar 

  22. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)

    MATH  Google Scholar 

  23. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2000)

    Article  Google Scholar 

  24. Kelly, T.: Arguing safety - a systematic approach to safety case management. Ph.D. thesis, University of York (1998)

    Google Scholar 

  25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  26. Paige, R.F.: A meta-method for formal method integration. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 473–494. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63533-5_25

    Chapter  Google Scholar 

  27. Rivera, V., Bhattacharya, S., Cataño, N.: Undertaking the tokeneer challenge in event-B. In: FormaliSE 2016. ACM Press (2016)

    Google Scholar 

  28. Rushby, J.: Logic and epistemology in safety cases. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 1–7. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40793-2_1

    Chapter  Google Scholar 

  29. Rushby, J.: Mechanized support for assurance case argumentation. In: Nakano, Y., Satoh, K., Bekki, D. (eds.) JSAI-isAI 2013. LNCS (LNAI), vol. 8417, pp. 304–318. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10061-6_20

    Chapter  Google Scholar 

  30. Wei, R., Kelly, T., Dai, X., Zhao, S., Hawkins, R.: Model based system assurance using the structured assurance case metamodel. Syst. Softw. 154, 211–233 (2019)

    Article  Google Scholar 

  31. Wenzel, M., Wolff, B.: Building formal method tools in the Isabelle/Isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 352–367. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_26

    Chapter  MATH  Google Scholar 

  32. Wenzel, M.: Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In: Proceedings of the 4th Workshop on Formal Integrated Development Environment (F-IDE), pp. 71–84 (2018). https://doi.org/10.4204/EPTCS.284.6

    Article  Google Scholar 

  33. Woodcock, J.: First steps in the verified software grand challenge. IEEE Comput. 39(10), 57–64 (2006)

    Article  Google Scholar 

  34. Woodcock, J., Aydal, E.G., Chapman, R.: The tokeneer experiments. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 405–430. Springer, London (2010). https://doi.org/10.1007/978-1-84882-912-1_17

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

This work is funded by EPSRC projects CyPhyAssureFootnote 8, (grant reference EP/S001190/1), and RoboCalc (grant reference EP/M025756/1), and additionally German Science Foundation (DFG) grant 381212925.

Author information

Authors and Affiliations

  1. University of York, York, UK

    Yakoub Nemouchi, Simon Foster, Mario Gleirscher & Tim Kelly

Authors
  1. Yakoub Nemouchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mario Gleirscher
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tim Kelly
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Foster .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T. (2019). Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34968-4_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34967-7

  • Online ISBN: 978-3-030-34968-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation