Document Open Access Logo

Information Flow Control in Cyclic Process Networks

Authors Bas van den Heuvel , Farzaneh Derakhshan , Stephanie Balzer

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.40.pdf
  • Filesize: 0.96 MB
  • 30 pages

Document Identifiers

Author Details

Bas van den Heuvel
  • HKA Karlsruhe, Germany
  • University of Freiburg, Germany
  • University of Groningen, The Netherlands
Farzaneh Derakhshan
  • Illinois Institutie of Technology, Chicago, IL, USA
Stephanie Balzer
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • van den Heuvel, Bas: Supported in part by the Dutch Research Council (NWO) under project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).
  • Balzer, Stephanie: Supported in part by the Air Force Office of Scientific Research under award number FA9550-21-1-0385 (Tristan Nguyen, program manager). Any opinions, findings and conclusions or recommendations expressed here are those of the author(s) and do not necessarily reflect the views of the U.S. Department of Defense.

Cite AsGet BibTex

Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information Flow Control in Cyclic Process Networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 40:1-40:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.40

Abstract

Protection of confidential data is an important security consideration of today’s applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today’s applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Security and privacy → Logic and verification
  • Theory of computation → Process calculi
  • Theory of computation → Type theory
Keywords
  • Cyclic process networks
  • linear session types
  • logical relations
  • deadlock-sensitive noninterference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In 15th European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, pages 69-83. Springer, 2006. URL: https://doi.org/10.1007/11693024_6.
  2. Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 340-353. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480925.
  3. Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(5):657-683, 2001. URL: https://doi.org/10.1145/504709.504712.
  4. Robert Atkey. Observed communication semantics for classical processes. In Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 26, pages 56-82. Springer, 2017. Google Scholar
  5. Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. CoRR, abs/2309.00192, 2023. URL: https://doi.org/10.48550/arXiv.2309.00192.
  6. Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proceedings of the ACM on Programming Languages, 1(ICFP):37:1-37:29, 2017. URL: https://doi.org/10.1145/3110281.
  7. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In 28th European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 611-639. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
  8. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In 22nd European Symposium on Programming (ESOP), pages 330-349, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_19.
  9. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In 21th International Conference onf Concurrency Theory (CONCUR), volume 6269 of Lecture Notes in Computer Science, pages 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  10. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  11. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Typing access control and secure information flow in sessions. Information and Computation, 238:68-105, 2014. URL: https://doi.org/10.1016/j.ic.2014.07.005.
  12. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Information flow safety in multiparty sessions. Mathematical Structures in Computer Science, 26(8):1352-1394, December 2016. URL: https://doi.org/10.1017/S0960129514000619.
  13. Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk. Session types for access and information flow control. In 21th International Conference on Concurrency Theory (CONCUR), pages 237-252, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_17.
  14. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Aspects of Computing, 28(4):669-696, 2016. URL: https://doi.org/10.1007/s00165-016-0381-3.
  15. Silvia Crafa, Michele Bugliesi, and Giuseppe Castagna. Information flow security for boxed ambients. Electronic Notes in Theoretical Computer Science, 66(3):76-97, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80417-1.
  16. Silvia Crafa and Sabina Rossi. A theory of noninterference for the π-calculus. In International Symposium on Trustworthy Global Computing (TGC), volume 3705 of Lecture Notes in Computer Science, pages 2-18. Springer, 2005. URL: https://doi.org/10.1007/11580850_2.
  17. Silvia Crafa and Sabina Rossi. P-congruences as non-interference for the pi-calculus. In ACM Workshop on Formal Methods in Security Engineering (FMSE), pages 13-22. ACM, 2006. URL: https://doi.org/10.1145/1180337.1180339.
  18. Silvia Crafa and Sabina Rossi. Controlling information release in the π-calculus. Information and Computation, 205(8):1235-1273, August 2007. URL: https://doi.org/10.1016/j.ic.2007.01.001.
  19. Ornela Dardha and Simon J. Gay. A New Linear Logic for Deadlock-Free Session-Typed Processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, pages 91-109. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_5.
  20. Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14. IEEE Computer Society, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470654.
  21. Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-axiomatic sequent calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD), volume 167 of LIPIcs, pages 29:1-29:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.29.
  22. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 143-156. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863566.
  23. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5):477-528, 2012. URL: https://doi.org/10.1017/S095679681200024X.
  24. Daniel Hedin and Andrei Sabelfeld. A Perspective on Information-Flow Control. In Software Safety and Security, pages 319-347. IOS Press, 2012. URL: https://doi.org/10.3233/978-1-61499-028-4-319.
  25. Matthew Hennessy. The security pi-calculus and non-interference. The Journal of Logic and Algebraic Programming, 63(1):3-34, April 2005. URL: https://doi.org/10.1016/j.jlap.2004.01.003.
  26. Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous pi-calculus. ACM Transactions on Programming Languages and Systems, 24(5):566-591, September 2002. URL: https://doi.org/10.1145/570886.570890.
  27. Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information Flow Control in Cyclic Process Networks, July 2024. URL: https://doi.org/10.48550/arXiv.2407.02304.
  28. Bas van den Heuvel, Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Typed Non-determinism in Functional and Concurrent Calculi. In Chung-Kil Hur, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 112-132, Singapore, 2023. Springer Nature. URL: https://doi.org/10.1007/978-981-99-8311-7_6.
  29. Bas van den Heuvel and Jorge A. Pérez. Deadlock freedom for asynchronous and cyclic process networks. In Julien Lange, Anastasia Mavridou, Larisa Safina, and Alceste Scalas, editors, Proceedings 14th Interaction and Concurrency Experience, Online, 18th June 2021, volume 347 of Electronic Proceedings in Theoretical Computer Science, pages 38-56. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.347.3.
  30. Bas van den Heuvel and Jorge A. Pérez. A decentralized analysis of multiparty protocols. Science of Computer Programming, page 102840, June 2022. URL: https://doi.org/10.1016/j.scico.2022.102840.
  31. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  32. Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory (CONCUR), volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  33. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In 7th European Symposium on Programming (ESOP), volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  34. Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In 9th European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 180-199. Springer, 2000. URL: https://doi.org/10.1007/3-540-46425-5_12.
  35. Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. In 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 81-92. ACM, 2002. URL: https://doi.org/10.1145/503272.503281.
  36. Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(6):31, 2007. URL: https://doi.org/10.1145/1286821.1286822.
  37. Chung-Kil Hur and Derek Dreyer. A kripke logical relation between ML and assembly. In 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 133-146. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926402.
  38. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. In 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 128-141, 2001. URL: https://doi.org/10.1145/360204.360215.
  39. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. Theoretical Computer Science, 311(1-3):121-163, 2004. URL: https://doi.org/10.1016/S0304-3975(03)00325-6.
  40. Naoki Kobayashi. A partially deadlock-free typed process calculus. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 128-139. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614941.
  41. Naoki Kobayashi. Type-based information flow analysis for the pi-calculus. Acta Informatica, 42(4-5):291-347, 2005. URL: https://doi.org/10.1007/s00236-005-0179-x.
  42. Naoki Kobayashi. A New Type System for Deadlock-Free Processes. In Christel Baier and Holger Hermanns, editors, CONCUR 2006 endash Concurrency Theory, Lecture Notes in Computer Science, pages 233-247. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11817949_16.
  43. Wen Kokke, J. Garrett Morris, and Philip Wadler. Towards races in linear logic. Logical Methods in Computer Science, 16(4), 2020. URL: https://lmcs.episciences.org/6979.
  44. Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 141-152. ACM, 2006. URL: https://doi.org/10.1145/1111037.1111050.
  45. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In 24th European Symposium on Programming (ESOP), volume 9032 of Lecture Notes in Computer Science, pages 560-584. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_23.
  46. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 434-447. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951921.
  47. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  48. Robin Milner. Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, 1989. Google Scholar
  49. Robin Milner. Communicating and Mobile Systems - the Pi-calculus. Cambridge University Press, 1999. Google Scholar
  50. Georg Neis, Derek Dreyer, and Andreas Rossberg. Non-parametric parametricity. Journal of Functional Programming, 21(4-5):497-562, 2011. URL: https://doi.org/10.1017/S0956796811000165.
  51. Luca Padovani. Deadlock and Lock Freedom in the Linear π-calculus. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pages 72:1-72:10, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2603088.2603116.
  52. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations for session-based concurrency. In 21st European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 539-558. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_27.
  53. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. URL: https://doi.org/10.1016/j.ic.2014.08.001.
  54. Andrew M. Pitts and Ian Stark. Operational reasoning for functions with local state. Higher Order Operational Techniques in Semantics (HOOTS), pages 227-273, 1998. Google Scholar
  55. F. Pottier. A simple view of type-secure information flow in the π-calculus. In Proceedings 15th IEEE Computer Security Foundations Workshop (CSFW-15), pages 320-330, 2002. URL: https://doi.org/10.1109/CSFW.2002.1021826.
  56. Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proceedings of the ACM on Programming Languages, 5(ICFP):1-31, 2021. URL: https://doi.org/10.1145/3473567.
  57. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal of Selected Areas in Communications, 21(1):5-19, 2003. URL: https://doi.org/10.1109/JSAC.2002.806121.
  58. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS), pages 293-302. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.17.
  59. Davide Sangiorgi and David Walker. The Pi-Calculus - a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  60. Geoffrey Smith and Dennis M. Volpano. Secure information flow in a multi-threaded imperative language. In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 355-364. ACM, 1998. URL: https://doi.org/10.1145/268946.268975.
  61. Kristian Støvring and Søren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 161-172. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190244.
  62. Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):26, 2007. URL: https://doi.org/10.1145/1284320.1284325.
  63. Jacob Thamsborg and Lars Birkedal. A kripke logical relation for effect-based program transformations. In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 445-456. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034831.
  64. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In 22nd European Symposium on Programming (ESOP), volume 7792 of Lecture Notes in Computer Science, pages 350-369. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_20.
  65. 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. URL: https://doi.org/10.3233/JCS-1996-42-304.
  66. Philip Wadler. Propositions as sessions. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
  67. Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384-418, May 2014. URL: https://doi.org/10.1017/S095679681400001X.
  68. Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June - 2 July 2003, Pacific Grove, CA, USA, page 29. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212703.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact