SACS | Imperative Process Algebra with Abstraction

Published in Volume XXXII, Issue 1, 2022, pages 137-179, doi: 10.7561/SACS.2022.1.137

Authors: C.A. Middelburg

Abstract

This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction of this kind opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established.

Full Text (PDF)

References

[1] Jos C. M. Baeten and Jan A. Bergstra. Global renaming operators in concrete process algebra. Information and Computation, 78(3):205-245, 1988. doi:10.1016/0890-5401(88)90027-2.

[2] Jos C. M. Baeten and Jan A. Bergstra. Process algebra with signals and conditions. In Manfred Broy, editor, Programming and Mathematical Method, pages 273-323, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. doi:10.1007/978-3-642-77572-7_13.

[3] Jos C. M. Baeten and W. P. Weijland. Process algebra, volume 18 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1990. doi:10.1017/CBO9780511624193.

[4] Twan Basten. Branching bisimilarity is an equivalence indeed! Information Processing Letters, 58(3):141-147, 1996. doi:10.1016/0020-0190(96)00034-8.

[5] D. E. Bell and Leonard J. LaPadula. Secure computer systems: Mathematical foundations and model. Technical Report M74-244, MITRE Corporation, 1973.

[6] Jan A. Bergstra and Jan Willem Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, 1984. doi:10.1016/S0019-9958(84)80025-X.

[7] Jan A. Bergstra and Cornelis A. Middelburg. Splitting bisimulations and retrospective conditions. Information and Computation, 204(7):1083-1138, 2006. doi:10.1016/j.ic.2006.03.003.

[8] Jan A. Bergstra and Cornelis A. Middelburg. A process calculus with finitary comprehended terms. Theory of Computing Systems, 53(4):645-668, 2013. doi:10.1007/s00224-013-9468-x.

[9] Jan A. Bergstra and Cornelis A. Middelburg. Using Hoare logic in a process algebra setting. Fundamenta Informaticae, 179(4):321-344, 2021. doi:10.3233/FI-2021-2026.

[10] Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjoberg, Stephanie Weirich, and Steve Zdancewic. Reactive noninterference. In Ehab Al-Shaer, Somesh Jha, and Angelos D. Keromytis, editors, Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, pages 79-90. ACM, 2009. doi:10.1145/1653662.1653673.

[11] Annalisa Bossi, Riccardo Focardi, Carla Piazza, and Sabina Rossi. Verifying persistent security properties. Computer Languages, Systems & Structures, 30(3-4):231-258, 2004. doi:10.1016/j.cl.2004.02.005.

[12] Gerard Boudol and Ilaria Castellani. Noninterference for concurrent programs and thread systems. Theoretical Computer Science, 281(1-2):109-130, 2002. doi:10.1016/S0304-3975(02)00010-5.

[13] Mark Bouwman, Bas Luttik, Wouter Schols, and Tim A. C. Willemse. A process algebra with global variables. In Ornela Dardha and Jurriaan Rot, editors, Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, volume 322 of Electronic Proceedings in Theoretical Computer Science, pages 33-50, 2020. doi:10.4204/EPTCS.322.5.

[14] Ellis S. Cohen. Information transmission in computational systems. In Saul Rosen and Peter J. Denning, editors, Proceedings of the Sixth Symposium on Operating System Principles, SOSP 1977, pages 133-139. ACM, 1977. doi:10.1145/800214.806556.

[15] Ellis S Cohen. Information transmission in sequential programs. In Richard A. DeMillo, David P. Dobkin, Anita K. Jones, and Richard J. Lipton, editors, Foundations of secure computation, pages 297-335. Academic Press, 1978.

[16] Robert Colvin and Ian J. Hayes. CSP with hierarchical state. In Michael Leuschel and Heike Wehrheim, editors, 7th International Conference on Integrated Formal Methods, IFM 2009,, volume 5423 of Lecture Notes in Computer Science, pages 118-135. Springer, 2009. doi:10.1007/978-3-642-00255-7\_9.

[17] Dorothy E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236-243, 1976. doi:10.1145/360051.360056.

[18] Dorothy E. Denning and Peter J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504-513, 1977. doi:10.1145/359636.359712.

[19] Ansgar Fehnker, Rob J. van Glabbeek, Peter Hofner, Annabelle McIver, Marius Portmann, and Wee Lum Tan. A process algebra for wireless mesh networks. In Helmut Seidl, editor, 21st European Symposium on Programming on Programming Languages and Systems, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, volume 7211 of Lecture Notes in Computer Science, pages 295-315. Springer, 2012. doi:10.1007/978-3-642-28869-2\_15.

[20] Riccardo Focardi and Roberto Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5-33, 1995. doi:10.3233/JCS-1994/1995-3103.

[21] Riccardo Focardi, Sabina Rossi, and Andrei Sabelfeld. Bridging language-based and process calculi security. In Vladimiro Sassone, editor, 8th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, volume 3441 of Lecture Notes in Computer Science, pages 299-315. Springer, 2005. doi:10.1007/978-3-540-31982-5\_19.

[22] Wan J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2000. doi:10.1007/978-3-662-04293-9.

[23] Wan J. Fokkink. Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences, 60(1):13-37, 2000. doi:10.1006/jcss.1999.1663.

[24] Joseph A. Goguen. Theorem proving and algebra. CoRR, abs/2101.02690, 2021. arXiv:2101.02690.

[25] Jan Friso Groote and Alban Ponse. Process algebra with guards: Combining Hoare logic with process algebra. Formal Aspects of Computing, 6(2):115-164, 1994. doi:10.1007/BF01221097.

[26] David Harel and Amir Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, volume F13 of NATO ASI Series, pages 477-498. Springer, 1984. doi:10.1007/978-3-642-82453-1\_17.

[27] Matthew Hennessy and Anna Ingolfsdottir. Communicating processes with value-passing and assignments. Formal Aspects of Computing, 5(5):432-466, 1993. doi:10.1007/BF01212486.

[28] Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995. doi:10.1016/0304-3975(94)00172-F.

[29] Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. ACM Transactions on Programming Languages and Systems, 29(6):31, 2007. doi:10.1145/1286821.1286822.

[30] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, 1994. doi:10.1145/177492.177726.

[31] Gavin Lowe. Semantic models for information flow. Theoretical Computer Science, 315(1):209-256, 2004. doi:10.1016/j.tcs.2003.11.019.

[32] Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote. Notions of bisimulation and congruence formats for SOS with data. Information and Computation, 200(1):107-147, 2005. doi:10.1016/j.ic.2005.03.002.

[33] Rocco De Nicola and Rosario Pugliese. Testing semantics of asynchronous distributed programs. In Mads Dam, editor, 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, Selected Papers, volume 1192 of Lecture Notes in Computer Science, pages 320-344. Springer, 1996. doi:10.1007/3-540-62503-8\_15.

[34] Kevin R. O’Neill, Michael R. Clarkson, and Stephen Chong. Information-flow security for interactive programs. In 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), pages 190-201. IEEE Computer Society, 2006. doi:10.1109/CSFW.2006.16.

[35] Don Pigozzi and Antonino Salibra. The abstract variable-binding calculus. Studia Logica, 55(1):129-179, 1995. doi:10.1007/BF01053036.

[36] Peter Y. A. Ryan and Steve A. Schneider. Process algebra and noninterference. Journal of Computer Security, 9(1/2):75-103, 2001. doi:10.3233/JCS-2001-91-204.

[37] Najah Ben Said and Ioana Cristescu. End-to-end information flow security for web services orchestration. Science of Computer Programming, 187:102376, 2020. doi:10.1016/j.scico.2019.102376.

[38] Donald Sannella and Andrzej Tarlecki. Algebraic preliminaries. In Egidio Astesiano, Hans-Jorg Kreowski, and Bernd Krieg-Bruckner, editors, Algebraic Foundations of Systems Specication, IFIP State-of-the-Art Reports, pages 13-30. Springer, 1999. doi:10.1007/978-3-642-59851-7\_2.

[39] Fred B. Schneider. On Concurrent Programming. Graduate Texts in Computer Science. Springer, 1997. doi:10.1007/978-1-4612-1830-2.

[40] Georey Smith and Dennis M. Volpano. Secure information flow in a multi-threaded imperative language. In David B. MacQueen and Luca Cardelli, editors, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’98, pages 355-364. ACM, 1998. doi:10.1145/268946.268975.

[41] Rob J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. doi:10.1145/233551.233556.

[42] Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith. A sound type system for secure flow analysis. Journal of Computer Security, 4(2/3):167-188, 1996. doi:10.3233/JCS-1996-42-304.

[43] Martin Wirsing. Algebraic specification. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 675-788. Elsevier and MIT Press, 1990. doi:10.1016/b978-0-444-88074-1.50018-4.

Bibtex

@article{sacscuza:kees22ipaa,
  title={Imperative Process Algebra with Abstraction},
  author={C.A. Middelburg},
  journal={Scientific Annals of Computer Science},
  volume={32},
  number={1},
  organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
  year={2022},
  pages={137-179},
  publisher={Alexandru Ioan Cuza University Press, Ia\c si},
  doi={10.7561/SACS.2022.1.137}
}