Skip to main content
SpringerLink
Log in

Conditional Information Flow Policies and Unwinding Relations

  • Conference paper
Trustworthy Global Computing (TGC 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7173))

Included in the following conference series:

Abstract

Noninterference provides a control over information flow in systems for ensuring confidentiality and integrity security properties. In general, user A is not allowed to interfere with user B if A’s behaviour cannot cause any difference in B’s observation. Unwinding relations are useful verification techniques for noninterference-based properties. This paper defines a framework for the notion of conditional noninterference, which allows to specify information flow policies based on the semantics of action channels. To verify the properties, we present unwinding relations that are both sound and complete for the new policies.

A major part of the work was done when the author was a postdoc researcher in the SaToSS group, University of Luxembourg.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Backes, M., Pfitzmann, B.: Intransitive non-interference for cryptographic purpose. In: Proc. S&P, pp. 140–152 (2003)

    Google Scholar 

  2. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proc. CSFW, pp. 100–114 (2004)

    Google Scholar 

  3. Bell, D.E., LaPadula, L.J.: Secure Computer System: Vol.I—mathematical foundations, Vol.II—a mathematical model, Vol.III—a refinement of the mathematical model. Technical report MTR-2547 (three volumes), The MITRE Corporation (March-December 1973)

    Google Scholar 

  4. Bell, D.E., LaPadula, L.J.: Secure computer system: unified exposition and MULTICS interpretation. Technical report MTR-2997 Rev. 1, The MITRE Corporation (March 1976)

    Google Scholar 

  5. Bevier, W.R., Young, W.D.: A state-based approach to noninterference. In: Proc. CSFW, pp. 11–21 (1994)

    Google Scholar 

  6. Bossi, A., Piazza, C., Rossi, S.: Modelling downgrading in information flow security. In: Proc. CSFW, pp. 187–201 (2004)

    Google Scholar 

  7. Brewer, D.F.C., Nash, M.J.: The Chinese Wall security policy. In: Proc. S&P, pp. 206–214 (1989)

    Google Scholar 

  8. Clark, D., Wilson, D.: A comparison of commercial and military computer security policies. In: Proc. S&P, pp. 184–193 (1987)

    Google Scholar 

  9. Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Proc. Workshop on Industrial-Strength Formal Specification Techniques (1996)

    Google Scholar 

  10. Darvas, Á., Hähnle, R., Sands, D.: A Theorem Proving Approach to Analysis of Secure Information Flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. D’Souza, D., Holla, R., Kulkarni, J., Ramesh, R.K., Sprick, B.: On the Decidability of Model-Checking Information Flow Properties. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 26–40. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Eggert, S., van der Meyden, R., Schnoor, H., Wilke, T.: The complexity of intransitive noninterference. In: Proc. S&P, pp. 196–211 (2011)

    Google Scholar 

  13. Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security 3(1), 5–33 (1995)

    Google Scholar 

  14. Focardi, R., Rossi, S.: Information flow security in dynamic contexts. In: Proc. CSFW, pp. 307–319 (2002)

    Google Scholar 

  15. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. S&P, pp. 11–20 (1982)

    Google Scholar 

  16. Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proc. S&P, p. 75 (1984)

    Google Scholar 

  17. Ben Hadj-Alouane, N., Lafrance, S., Lin, F., Mullins, J., Yeddes, M.: On the verification of intransitive noninterference in mulitlevel security. IEEE Transactions on Systems, Man and Cybernetics 35(5), 948–958 (2005)

    Article  Google Scholar 

  18. Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Transactions on Software Engineering 13(2), 141–150 (1987)

    Article  Google Scholar 

  19. Mantel, H.: Possiblistic definitions of security – an assembly kit. In: Proc. CSFW, pp. 185–199 (2000)

    Google Scholar 

  20. Mantel, H.: Unwinding Security Properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 238–254. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  21. Mantel, H., Reinhard, A.: Controlling the What and Where of Declassification in Language-Based Security. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 141–156. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Mantel, H., Sands, D.: Controlled Declassification Based on Intransitive Noninterference. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 129–145. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  23. Milner, R.: Communication and concurrency. Prentice-Hall (1989)

    Google Scholar 

  24. Roscoe, A.W.: CSP and determinism in security modelling. In: Proc. S&P, pp. 114–221 (1995)

    Google Scholar 

  25. Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference ? In: Proc. CSFW, pp. 228–238 (1999)

    Google Scholar 

  26. Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, SRI international (December 1992)

    Google Scholar 

  27. Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. CSFW, pp. 255–269 (2005)

    Google Scholar 

  28. Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  29. van der Meyden, R.: What, Indeed, Is Intransitive Noninterference (Extended Abstract). In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 235–250. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. van der Meyden, R., Zhang, C.: Algorithmic verification on noninterference properties. ENTCS 168, 61–75 (2007)

    Google Scholar 

  31. van der Meyden, R., Zhang, C.: A comparison of semantic models for noninterference. Theoretical Computer Science 411(7), 4123–4147 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  32. von Oheimb, D.: Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225–243. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, The University of New South Wales, Australia

    Chenyi Zhang

Authors
  1. Chenyi Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Pisa, Largo Bruno Pontecorvo 3, 56127, Pisa, Italy

    Roberto Bruni

  2. ECS, University of Southampton, University Road, SO17 1BJ, Southampton, UK

    Vladimiro Sassone

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, C. (2012). Conditional Information Flow Policies and Unwinding Relations. In: Bruni, R., Sassone, V. (eds) Trustworthy Global Computing. TGC 2011. Lecture Notes in Computer Science, vol 7173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30065-3_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30065-3_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-30064-6

  • Online ISBN: 978-3-642-30065-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation