Document Open Access Logo

Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency

Authors Farzaneh Derakhshan , Stephanie Balzer , Yue Yao

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.11.pdf
  • Filesize: 1.34 MB
  • 29 pages

Document Identifiers

Author Details

Farzaneh Derakhshan
  • Illinois Institute of Technology, Chicago, IL, USA
Stephanie Balzer
  • Carnegie Mellon University, Pittsburgh, PA, USA
Yue Yao
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • 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

Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 11:1-11:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.11

Abstract

Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. Information flow control (IFC) type systems assert noninterference by tracking the level of information learned (pc) and disallowing communication to entities of lesser or unrelated level than the pc. Control flow constructs such as loops are at odds with this pattern because they necessitate downgrading the pc upon recursion to be practical. In a concurrent setting, however, downgrading is not generally safe. This paper utilizes session types to track the flow of information and contributes an IFC type system for message-passing concurrent processes that allows downgrading the pc upon recursion. To make downgrading safe, the paper introduces regrading policies. Regrading policies are expressed in terms of integrity labels, which are also key to safe composition of entities with different regrading policies. The paper develops the type system and proves progress-sensitive noninterference for well-typed processes, ruling out timing attacks that exploit the relative order of messages. The type system has been implemented in a type checker, which supports security-polymorphic processes.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Security and privacy → Logic and verification
  • Theory of computation → Process calculi
Keywords
  • Regrading policies
  • session types
  • progress-sensitive noninterference

Metrics

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

Related Versions

Supplementary Materials

References

  1. Martín Abadi. Secrecy by typing in security protocols. In TACS, volume 1281 of LNCS, pages 611-638. Springer, 1997. Google Scholar
  2. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In POPL, pages 147-160. ACM, 1999. Google Scholar
  3. Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, volume 3924 of LNCS, pages 69-83. Springer, 2006. Google Scholar
  4. Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, and Keith Winstein. Secure serverless computing using dynamic information flow control. Proc. ACM Program. Lang., 2(OOPSLA):118:1-118:26, 2018. Google Scholar
  5. Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657-683, 2001. Google Scholar
  6. Aslan Askarov and Andrew C. Myers. Attacker control and impact for confidentiality and integrity. Log. Methods Comput. Sci., 7(3), 2011. Google Scholar
  7. Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. CoRR, abs/2309.00192, 2023. URL: https://arxiv.org/abs/2309.00192.
  8. Kenneth J. Biba. Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, Electronic Systems Division, Air Force Systems Command, United States Air Force, 1977. Google Scholar
  9. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222-236. Springer, 2010. Google Scholar
  10. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Typing access control and secure information flow in sessions. Inf. Comput., 238:68-105, 2014. Google Scholar
  11. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Information flow safety in multiparty sessions. Mathematical Structures in Computer Science, 26(8):1352-1394, 2016. URL: https://doi.org/10.1017/S0960129514000619.
  12. Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk. Session types for access and information flow control. In CONCUR, pages 237-252, 2010. Google Scholar
  13. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Aspects Comput., 28(4):669-696, 2016. Google Scholar
  14. Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Inf. Comput., 207(10):1044-1077, 2009. Google Scholar
  15. Stephen Chong and Andrew C. Myers. Decentralized robustness. In CSFW, pages 242-256. IEEE, 2006. Google Scholar
  16. Silvia Crafa, Michele Bugliesi, and Giuseppe Castagna. Information flow security for boxed ambients. Electronic Notes in Theoretical Computer Science, 66(3):76-97, 2002. Google Scholar
  17. Silvia Crafa and Sabina Rossi. A theory of noninterference for the π-calculus. In TGC, volume 3705 of LNCS, pages 2-18. Springer, 2005. Google Scholar
  18. Silvia Crafa and Sabina Rossi. Controlling information release in the pi-calculus. Inf. Comput., 205(8):1235-1273, 2007. Google Scholar
  19. Karl Crary, Robert Harper, and Sidd Puri. What is a recursive module? In PLDI, pages 50-63. ACM, 1999. Google Scholar
  20. Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In LICS, pages 1-14. IEEE, 2021. Google Scholar
  21. Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading policies for flexible information flow control in session-typed concurrency. CoRR, 2024. Google Scholar
  22. Elena Ferrari, Pierangela Samarati, Elisa Bertino, and Sushil Jajodia. Providing flexibility in information flow control for object-oriented systems. In IEEE Symposium on Security and Privacy, pages 130-140. IEEE, 1997. Google Scholar
  23. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. Google Scholar
  24. Daniel Heidin and Andrei Sabelfeld. A perspective on information flow control. Technical report, Marktoberdorf, 2011. Google Scholar
  25. Matthew Hennessy. The security pi-calculus and non-interference. J. Log. Algebraic Methods Program., 63(1):3-34, 2005. Google Scholar
  26. Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of LNCS, pages 509-523. Springer, 1993. Google Scholar
  27. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of LNCS, pages 122-138. Springer, 1998. Google Scholar
  28. Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In ESOP, volume 1782 of LNCS, pages 180-199. Springer, 2000. Google Scholar
  29. Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. In POPL, pages 81-92. ACM, 2002. Google Scholar
  30. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. Google Scholar
  31. Naoki Kobayashi. Type-based information flow analysis for the pi-calculus. Acta Inf., 42(4):291-347, December 2005. Google Scholar
  32. Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. TOSEM, 9(4):410-442, 2000. Google Scholar
  33. Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing robust declassification and qualified robustness. J. Comput. Secur., 14(2):157-196, 2006. Google Scholar
  34. François Pottier. A simple view of type-secure information flow in the π-calculus. In CSFW-15, pages 320-330. IEEE, 2002. Google Scholar
  35. Andrei Sabelfeld and Heiko Mantel. Static confidentiality enforcement for distributed programs. In SAS, volume 2477 of LNCS, pages 376-394. Springer, 2002. Google Scholar
  36. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE J. Sel. Areas Commun., 21(1):5-19, 2003. Google Scholar
  37. Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In CSFW, pages 200-214. IEEE, 2000. Google Scholar
  38. Davide Sangiorgi and David Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  39. Geoffrey Smith and Dennis M. Volpano. Secure information flow in a multi-threaded imperative language. In POPL, pages 355-364. ACM, 1998. Google Scholar
  40. Deian Stefan, Alejandro Russo, Pablo Buiras, Amit Levy, John C. Mitchell, and David Mazières. Addressing covert termination and timing channels in concurrent information flow systems. In ICFP, pages 201-214. ACM, 2012. Google Scholar
  41. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In ESOP, volume 7792 of LNCS, pages 350-369. Springer, 2013. Google Scholar
  42. Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith. A sound type system for secure flow analysis. J. Comput. Secur., 4(2/3):167-188, 1996. Google Scholar
  43. Philip Wadler. Propositions as sessions. In ICFP, pages 273-286. ACM, 2012. Google Scholar
  44. Steve Zdancewic. A type system for robust declassification. In MFPS, volume 83 of Electronic Notes in Theoretical Computer Science, pages 263-277. Elsevier, 2003. Google Scholar
  45. Steve Zdancewic and Andrew C. Myers. Robust declassification. In CSFW, pages 15-23. IEEE, 2001. Google Scholar
  46. Steve Zdancewic and Andrew C. Myers. Secure information flow and CPS. In ESOP, volume 2028 of LNCS, pages 46-61. Springer, 2001. Google Scholar
  47. Steve Zdancewic and Andrew C. Myers. Secure information flow via linear continuations. High. Order Symb. Comput., 15(2-3):209-234, 2002. Google Scholar
  48. Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In CSFW, pages 1-15. IEEE, 2003. Google Scholar
  49. Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure program partitioning. TOCS, 20(3):283-328, 2002. Google Scholar
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