Skip to main content
SpringerLink
Log in

Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10695))

Included in the following conference series:

Abstract

We propose a solution for verifying the information-flow security of distributed programs in a compositional manner. Our focus is on the treatment of message passing in such a verification, and our goal is to boost the precision of modular reasoning using rely-guarantee-style reasoning. Enabling a more precise treatment of message passing required the identification of novel concepts that capture assumptions about how a process’s environment interacts. Our technical contributions include a process-local security condition that allows one to exploit such assumptions when analyzing individual processes, a security type system that is sensitive in the content as well as in the availability of messages, and a soundness proof for our security type system. Our results complement existing solutions for rely-guarantee-style reasoning about information-flow security that focused on multi-threading and shared memory.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The addendum can be found at http://www.mais.informatik.tu-darmstadt.de/WebBibPHP/papers/2017/LiMantelTasch-addendum-APLAS2017.pdf.

References

  1. Alpízar, R., Smith, G.: Secure information flow for distributed systems. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 126–140. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12459-4_10

    Chapter  Google Scholar 

  2. Amtoft, T., Hatcliff, J., Rodríguez, E., Robby, H.J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 229–245. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0

    Chapter  Google Scholar 

  3. Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: CSF 2015, pp. 137–151 (2015)

    Google Scholar 

  4. Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: S&P 2007, pp. 207–221 (2007)

    Google Scholar 

  5. Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T.: Session types for access and information flow control. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 237–252. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_17

    Chapter  Google Scholar 

  6. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)

    Article  Google Scholar 

  7. Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: PLAS 2008, pp. 113–124 (2008)

    Google Scholar 

  8. Focardi, R., Gorrieri, R.: Classification of security properties (part I: information flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45608-2_6

    Chapter  Google Scholar 

  9. Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P 1982. IEEE Computer Society (1982)

    Google Scholar 

  10. Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF 2016, pp. 253–267 (2016)

    Google Scholar 

  11. Honda, K., Vasconcelos, V., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 180–199. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46425-5_12

    Chapter  Google Scholar 

  12. Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79–90 (2006)

    Google Scholar 

  13. Jones, C.B.: Development methods for computer programs including a notion of interference. Oxford University Computing Laboratory (1981)

    Google Scholar 

  14. Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4–5), 291–347 (2005)

    Article  MATH  Google Scholar 

  15. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  16. Li, X., Nielson, F., Nielson, H.R., Feng, X.: Disjunctive information flow for communicating processes. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 95–111. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28766-9_7

    Chapter  Google Scholar 

  17. Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605–607. Springer, New York (2011)

    Google Scholar 

  18. Mantel, H., Müller-Olm, M., Perner, M., Wenner, A.: Using dynamic pushdown networks to automate a modular information-flow analysis. In: LOPSTR 2015 (2015)

    Google Scholar 

  19. Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218–232 (2011)

    Google Scholar 

  20. Martel, M., Gengler, M.: Communication topology analysis for concurrent programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 265–286. Springer, Heidelberg (2000). https://doi.org/10.1007/10722468_16

    Chapter  Google Scholar 

  21. McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. 16(6), 563–568 (1990)

    Article  Google Scholar 

  22. Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF 2016 (2016)

    Google Scholar 

  23. Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP 1997, pp. 129–142 (1997)

    Google Scholar 

  24. Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF 2012, pp. 293–307 (2012)

    Google Scholar 

  25. Sabelfeld, A., Mantel, H.: Securing communication in a concurrent language. In: SAS 2002, pp. 376–394 (2002)

    Google Scholar 

  26. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)

    Article  Google Scholar 

  27. Tanenbaum, A.S., van Steen, M.: Distributed Systems - Principles and Paradigms, 2nd edn. Prentice-Hall Inc., Upper Saddle River (2007)

    MATH  Google Scholar 

  28. Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)

    Article  Google Scholar 

  29. Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW 2003, pp. 29–43 (2003)

    Google Scholar 

  30. Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2–3), 67–84 (2007)

    Article  Google Scholar 

Download references

Acknowledgments

The authors thank the anonymous reviewers for their helpful comments. This work was supported partially by the DFG under project RSCP (MA 3326/4-2/3) in the priority program RS3 (SPP 1496), and partially by the German Federal Ministry of Education and Research (BMBF) as well as by the Hessen State Ministry for Higher Education, Research and the Arts (HMWK) within CRISP.

Author information

Authors and Affiliations

  1. Department of Computer Science, TU-Darmstadt, Darmstadt, Germany

    Ximeng Li, Heiko Mantel & Markus Tasch

Authors
  1. Ximeng Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heiko Mantel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Markus Tasch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Ximeng Li , Heiko Mantel or Markus Tasch .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, X., Mantel, H., Tasch, M. (2017). Taming Message-Passing Communication in Compositional Reasoning About Confidentiality. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

  • Online ISBN: 978-3-319-71237-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation