Skip to main content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 8/2021

07.09.2021

An Automatically Verified Prototype of the Tokeneer ID Station Specification

verfasst von: Maximiliano Cristiá, Gianfranco Rossi

Erschienen in: Journal of Automated Reasoning | Ausgabe 8/2021

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost-effective manner. Altran UK was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be readily and naturally encoded in the \(\{log\}\) set constraint language, thereby generating a functional prototype. Furthermore, we show that \(\{log\}\) ’s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use \(\{log\}\) to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verification activities discussed in the paper.
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
We use ellipses to shorten the presentation.
 
2
These are the operation schemas whose names begin with TIS.
 
3
By explicit precondition we mean a precondition written down in the schema as opposed to the implicit preconditions ‘that arise from the interaction between the state invariant and the predicates that are explicit in the operation schema’ [31, page 54]. Implicit preconditions were made explicit and simplified as is customary when working with Z specifications. In general they are trivial; for example, asserting that an integer variable is nonnegative.
 
4
The prime symbol is not allowed as part of a variable name in Prolog+\(\{log\}\).
 
Literatur
2.
Zurück zum Zitat Abdelhalim, I., Sharp, J., Schneider, S.A., Treharne, H.: Formal verification of Tokeneer behaviours modelled in fUML using CSP. In: Dong, J.S., Zhu, H. (eds.) Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6447, pp. 371–387. Springer (2010), https://​doi.​org/​10.​1007/​978-3-642-16901-4_​25 Abdelhalim, I., Sharp, J., Schneider, S.A., Treharne, H.: Formal verification of Tokeneer behaviours modelled in fUML using CSP. In: Dong, J.S., Zhu, H. (eds.) Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6447, pp. 371–387. Springer (2010), https://​doi.​org/​10.​1007/​978-3-642-16901-4_​25
4.
Zurück zum Zitat Andréka, H., Givant, S.R., Németi, I.: Decision problems for equational theories of relation algebras, vol. 604. American Mathematical Soc. (1997) Andréka, H., Givant, S.R., Németi, I.: Decision problems for equational theories of relation algebras, vol. 604. American Mathematical Soc. (1997)
5.
Zurück zum Zitat Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: Proceedings of the IEEE International Symposium on Secure Software Engineering. IEEE (2006) Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: Proceedings of the IEEE International Symposium on Secure Software Engineering. IEEE (2006)
7.
Zurück zum Zitat Barnes, J.E.: Experiences in the industrial use of formal methods. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46,(2011) Barnes, J.E.: Experiences in the industrial use of formal methods. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46,(2011)
12.
Zurück zum Zitat Cooper, D., Everett, B., Johnson, R., Widmaier, J.: Security by construction – Engineering software to exceed EAL5. In: Proceedings of the Fourth Annual High Confidence Software and Systems Conference (2004) Cooper, D., Everett, B., Johnson, R., Widmaier, J.: Security by construction – Engineering software to exceed EAL5. In: Proceedings of the Fourth Annual High Confidence Software and Systems Conference (2004)
13.
Zurück zum Zitat Cristiá, M., Albertengo, P., Frydman, C.S., Plüss, B., Rodríguez Monetti, P.: Tool support for the test template framework. Softw. Test. Verif. Reliab. 24(1), 3–37 (2014) CrossRef Cristiá, M., Albertengo, P., Frydman, C.S., Plüss, B., Rodríguez Monetti, P.: Tool support for the test template framework. Softw. Test. Verif. Reliab. 24(1), 3–37 (2014) CrossRef
14.
Zurück zum Zitat Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185–201. Springer (2017), https://​doi.​org/​10.​1007/​978-3-319-63046-5_​12 Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185–201. Springer (2017), https://​doi.​org/​10.​1007/​978-3-319-63046-5_​12
15.
Zurück zum Zitat Cristiá, M., Rossi, G.: Programming in Java with restricted intensional sets. In: Cristiá, M., Delahaye, D., Dubois, C. (eds.) Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, SETS@ABZ 2018, Southamptom, UK, June 5, 2018. CEUR Workshop Proceedings, vol. 2199, pp. 17–31. CEUR-WS.org (2018), http://​ceur-ws.​org/​Vol-2199/​paper2.​pdf Cristiá, M., Rossi, G.: Programming in Java with restricted intensional sets. In: Cristiá, M., Delahaye, D., Dubois, C. (eds.) Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, SETS@ABZ 2018, Southamptom, UK, June 5, 2018. CEUR Workshop Proceedings, vol. 2199, pp. 17–31. CEUR-WS.org (2018), http://​ceur-ws.​org/​Vol-2199/​paper2.​pdf
16.
Zurück zum Zitat Cristiá, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333–349. Springer (2018), https://​doi.​org/​10.​1007/​978-3-030-02149-8_​20 Cristiá, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333–349. Springer (2018), https://​doi.​org/​10.​1007/​978-3-030-02149-8_​20
22.
Zurück zum Zitat Cristiá, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229–243. Springer (2013) Cristiá, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229–243. Springer (2013)
23.
Zurück zum Zitat Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000) CrossRef Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000) CrossRef
24.
25.
Zurück zum Zitat Evans, A.: An improved recipe for specifying reactive systems in Z. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM ’97: The Z Formal Specification Notation, 10th International Conference of Z Users, Reading, UK, April 3-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1212, pp. 275–294. Springer (1997), https://​doi.​org/​10.​1007/​BFb0027293 Evans, A.: An improved recipe for specifying reactive systems in Z. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM ’97: The Z Formal Specification Notation, 10th International Conference of Z Users, Reading, UK, April 3-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1212, pp. 275–294. Springer (1997), https://​doi.​org/​10.​1007/​BFb0027293
26.
Zurück zum Zitat Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12327, pp. 3–69. Springer (2020), https://​doi.​org/​10.​1007/​978-3-030-58298-2_​1 Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12327, pp. 3–69. Springer (2020), https://​doi.​org/​10.​1007/​978-3-030-58298-2_​1
28.
Zurück zum Zitat Holzbaur, C., Menezes, F., Barahona, P.: Defeasibility in CLP(Q) through generalized slack variables. In: Freuder, E.C. (ed.) Lecture notes in computer science, vol. 1118, pp. 209–223. Springer, Berlin (1996) Holzbaur, C., Menezes, F., Barahona, P.: Defeasibility in CLP(Q) through generalized slack variables. In: Freuder, E.C. (ed.) Lecture notes in computer science, vol. 1118, pp. 209–223. Springer, Berlin (1996)
31.
Zurück zum Zitat Jacky, J.: The way of Z: practical programming with formal methods. Cambridge University Press, New York, NY, USA (1996) CrossRef Jacky, J.: The way of Z: practical programming with formal methods. Cambridge University Press, New York, NY, USA (1996) CrossRef
33.
Zurück zum Zitat Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. In: Monahan, R., Prevosto, V., Proença, J. (eds.) Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019. EPTCS, vol. 310, pp. 50–62 (2019), https://​doi.​org/​10.​4204/​EPTCS.​310.​6 Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. In: Monahan, R., Prevosto, V., Proença, J. (eds.) Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019. EPTCS, vol. 310, pp. 50–62 (2019), https://​doi.​org/​10.​4204/​EPTCS.​310.​6
38.
Zurück zum Zitat Moy, Y., Wallenburg, A.: Tokeneer: Beyond formal program verification. Embed. Real Time Software Syst. 24,(2010) Moy, Y., Wallenburg, A.: Tokeneer: Beyond formal program verification. Embed. Real Time Software Syst. 24,(2010)
39.
Zurück zum Zitat Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013. pp. 415–429. IEEE Computer Society (2013), https://​doi.​org/​10.​1109/​SP.​2013.​35 Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013. pp. 415–429. IEEE Computer Society (2013), https://​doi.​org/​10.​1109/​SP.​2013.​35
40.
Zurück zum Zitat Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Isabelle/SACM: Computer-assisted assurance cases with integrated formal methods. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11918, pp. 379–398. Springer (2019), https://​doi.​org/​10.​1007/​978-3-030-34968-4_​21 Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Isabelle/SACM: Computer-assisted assurance cases with integrated formal methods. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11918, pp. 379–398. Springer (2019), https://​doi.​org/​10.​1007/​978-3-030-34968-4_​21
41.
Zurück zum Zitat Plagge, D., Leuschel, M.: Validating Z specifications using the probanimator and model checker. In: Davies, J., Gibbons, J. (eds.) Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4591, pp. 480–500. Springer (2007), https://​doi.​org/​10.​1007/​978-3-540-73210-5_​25 Plagge, D., Leuschel, M.: Validating Z specifications using the probanimator and model checker. In: Davies, J., Gibbons, J. (eds.) Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4591, pp. 480–500. Springer (2007), https://​doi.​org/​10.​1007/​978-3-540-73210-5_​25
42.
Zurück zum Zitat Potter, B., Sinclair, J., Till, D.: An introduction to formal specification and Z. Prentice Hall PTR Upper Saddle River, NJ, USA (1996) MATH Potter, B., Sinclair, J., Till, D.: An introduction to formal specification and Z. Prentice Hall PTR Upper Saddle River, NJ, USA (1996) MATH
46.
Zurück zum Zitat Schanda, F., Brain, M.: Using answer set programming in the development of verified software. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary. LIPIcs, vol. 17, pp. 72–85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012), https://​doi.​org/​10.​4230/​LIPIcs.​ICLP.​2012.​72 Schanda, F., Brain, M.: Using answer set programming in the development of verified software. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary. LIPIcs, vol. 17, pp. 72–85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012), https://​doi.​org/​10.​4230/​LIPIcs.​ICLP.​2012.​72
48.
Zurück zum Zitat Spivey, J.M.: The Z notation: a reference manual. Prentice Hall International (UK) Ltd., Hertfordshire, UK (1992) MATH Spivey, J.M.: The Z notation: a reference manual. Prentice Hall International (UK) Ltd., Hertfordshire, UK (1992) MATH
49.
Zurück zum Zitat Stocks, P., Carrington, D.: A Framework for specification-based testing. IEEE Trans. Software Eng. 22(11), 777–793 (1996) CrossRef Stocks, P., Carrington, D.: A Framework for specification-based testing. IEEE Trans. Software Eng. 22(11), 777–793 (1996) CrossRef
51.
Zurück zum Zitat Woodcock, J., Aydal, 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 (2010) Woodcock, J., Aydal, 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 (2010)
52.
Zurück zum Zitat Yin, X., Knight, J.C.: Formal verification of large software systems. In: Muñoz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings. NASA Conference Proceedings, vol. NASA/CP-2010-216215, pp. 192–201 (2010) Yin, X., Knight, J.C.: Formal verification of large software systems. In: Muñoz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings. NASA Conference Proceedings, vol. NASA/CP-2010-216215, pp. 192–201 (2010)
Metadaten
Titel
An Automatically Verified Prototype of the Tokeneer ID Station Specification
verfasst von
Maximiliano Cristiá
Gianfranco Rossi
Publikationsdatum
07.09.2021
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 8/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-021-09602-2

Weitere Artikel der Ausgabe 8/2021

Journal of Automated Reasoning 8/2021 Zur Ausgabe

Premium Partner