Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

Published in: Journal of Automated Reasoning 8/2021

07-09-2021

An Automatically Verified Prototype of the Tokeneer ID Station Specification

Authors: Maximiliano Cristiá, Gianfranco Rossi

Published in: Journal of Automated Reasoning | Issue 8/2021

Login to get access
share
SHARE

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.
Appendix
Available only for authorised users
Footnotes
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\}\).
 
Literature
2.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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)
Metadata
Title
An Automatically Verified Prototype of the Tokeneer ID Station Specification
Authors
Maximiliano Cristiá
Gianfranco Rossi
Publication date
07-09-2021
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 8/2021
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-021-09602-2

Other articles of this Issue 8/2021

Journal of Automated Reasoning 8/2021 Go to the issue

Premium Partner