Skip to main content
SpringerLink
Log in
Book cover

Nordic Conference on Secure IT Systems

NordSec 2013: Secure IT Systems pp 84–99Cite as

A Logic for Information Flow Analysis of Distributed Programs

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 8208))

Abstract

Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an online auction system we may want to ensure that no bidder knows the bids of any other bidder before the auction is closed. Such systems are typically interactive/reactive and communication is mostly asynchronous, lossy or unordered. Language-based security provides language mechanisms for enforcing end-to-end security. However, with few exceptions, previous research has mainly focused on relational or synchronous models, which are generally not suitable for distributed systems.

This paper proposes a general knowledge-based account of possibilistic security from a language perspective and shows how existing trace-based conditions fit in. A syntactic characterization of these conditions, given by an epistemic temporal logic, shows that existing model checking tools can be used to enforce security.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11–20. IEEE Comp. Soc. Press, Los Alamitos (1982)

    Google Scholar 

  2. Denning, D.E., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)

    Article  MATH  Google Scholar 

  3. Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE J. on Selected Ares in Communications 21(1), 5–19 (2003)

    Article  Google Scholar 

  4. O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: CSFW, pp. 190–201 (2006)

    Google Scholar 

  5. Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2,3), 167–187 (1996)

    Google Scholar 

  6. Balliu, M., Dam, M., Le Guernic, G.: Epistemic Temporal Logic for Information Flow Security. In: PLAS (2011)

    Google Scholar 

  7. Balliu, M., Dam, M., Guernic, G.L.: Encover: Symbolic exploration for information flow security. In: CSF, pp. 30–44 (2012)

    Google Scholar 

  8. Halpern, J.Y., O’Neill, K.R.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur. 12(1) (2008)

    Google Scholar 

  9. Askarov, A., Sabelfeld, A.: Gradual release: Unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy, pp. 207–221 (2007)

    Google Scholar 

  10. Askarov, A., Chong, S.: Learning is change in knowledge: Knowledge-based security for dynamic policies. In: CSF, pp. 308–322 (2012)

    Google Scholar 

  11. Guttman, J.D., Nadel, M.E.: What needs securing. In: CSFW, pp. 34–57 (1988)

    Google Scholar 

  12. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4) (2009)

    Google Scholar 

  13. Balliu, M., Le Guernic, G.: Encover (June 2012), Software release

    Google Scholar 

  14. Balliu, M.: A logic for information flow analysis of distributed programs (extended abstract). Technical report, KTH Royal Institute of Technology

    Google Scholar 

  15. Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. J. of Computer Security (2007)

    Google Scholar 

  16. Mclean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symposium on Security and Privacy, pp. 79–93 (1994)

    Google Scholar 

  17. Sutherland, D.: A model of information. In: 9th National Computer Security Conference (1986)

    Google Scholar 

  18. Wittbold, J.T., Johnson, D.M.: Information flow in nondeterministic systems. In: IEEE Symposium on Security and Privacy, pp. 144–161 (1990)

    Google Scholar 

  19. McLean, J.: Security models and information flow. In: Proc. IEEE Symposium on Security and Privacy, pp. 180–187. IEEE Computer Society Press (1990)

    Google Scholar 

  20. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  21. Askarov, A., Myers, A.C.: Attacker control and impact for confidentiality and integrity. Logical Methods in Computer Science 7(3) (2011)

    Google Scholar 

  22. Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF, pp. 43–59 (2009)

    Google Scholar 

  23. Sabelfeld, A., Mantel, H.: Securing communication in a concurrent language. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 376–394. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169–185. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Communication, KTH Royal Institute of Technology, Stockholm, Sweden

    Musard Balliu

Authors
  1. Musard Balliu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Mathematics and Computer Science, DTU Compute, Technical University of Denmark, Richard Petersens Plades, Building 322, 2800, Lyngby, Denmark

    Hanne Riis Nielson

  2. Institut für Sicherheit in verteilten Anwendungen, Technische Universität Hamburg-Harburg, E-15, Harburger Schloßstraße 20, 21079, Hamburg, Germany

    Dieter Gollmann

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Balliu, M. (2013). A Logic for Information Flow Analysis of Distributed Programs. In: Riis Nielson, H., Gollmann, D. (eds) Secure IT Systems. NordSec 2013. Lecture Notes in Computer Science, vol 8208. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41488-6_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41488-6_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41487-9

  • Online ISBN: 978-3-642-41488-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation