Skip to main content
SpringerLink
Log in

Unifying Theories of Confidentiality

  • Conference paper
Unifying Theories of Programming (UTP 2010)

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

Included in the following conference series:

Abstract

This paper presents a framework for reasoning about the security of confidential data within software systems. A novelty is that we use Hoare and He’s Unifying Theories of Programming (UTP) to do so and derive advantage from this choice. We identify how information flow between users can be modelled in the UTP and devise conditions for verifying that system designs may not leak secret information to untrusted users. We also investigate how these conditions can be combined with existing notions of refinement to produce refinement relations suitable for deriving secure implementations of systems.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Denning, D.E.: Cryptography and Data Security. Addison-Wesley Longman Publishing Company, Inc., Boston (1982)

    MATH  Google Scholar 

  2. Lampson, B.W.: A note on the confinement problem. Communications of the ACM 16(10), 613–615 (1973)

    Article  Google Scholar 

  3. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the 1982 IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society, Los Alamitos (April 1982)

    Google Scholar 

  4. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science. Prentice Hall Inc., Englewood Cliffs (1998)

    MATH  Google Scholar 

  5. Mantel, H.: Possibilistic definitions of security — an assembly kit. In: 13th IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 185–199 (2000)

    Google Scholar 

  6. Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, Universität Saarbrücken (July 2003)

    Google Scholar 

  7. Banks, M.J., Jacob, J.L.: On Modelling User Observations in the UTP. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 101–119. Springer, Heidelberg (2010)

    Google Scholar 

  8. Jacob, J.L.: On the derivation of secure components. In: Proceedings of the 1989 IEEE Symposium on Security and Privacy, pp. 242–247. IEEE Computer Society, Los Alamitos (1989)

    Chapter  Google Scholar 

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

    Google Scholar 

  10. Jacob, J.L.: Security specifications. In: Proceedings of the 1988 IEEE Symposium on Security and Privacy, pp. 14–23 (1988)

    Google Scholar 

  11. Jacob, J.L.: Refinement of shared systems. In: McDermid, J.A. (ed.) The Theory and Practice of Refinement: Approaches to the Development of Large-Scale Software Systems, pp. 27–36. Butterworths, London (1989)

    Google Scholar 

  12. Focardi, R., Gorrieri, R.: A taxonomy of security properties for process algebras. Journal of Computer Security 3(1), 5–34 (1995)

    Article  Google Scholar 

  13. Seehusen, F., Stølen, K.: Maintaining information flow security under refinement and transformation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 143–157. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Seehusen, F., Stølen, K.: Information flow security, abstraction and composition. IET Information Security 3(1), 9–33 (2009)

    Article  Google Scholar 

  15. Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy, pp. 114–127. IEEE Computer Society, Los Alamitos (1995)

    Chapter  Google Scholar 

  16. Morgan, C.: The shadow knows: Refinement and security in sequential programs. Science of Computer Programming 74(8), 629–653 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  17. Morgan, C.: How to brew-up a refinement ordering. Electronic Notes in Theoretical Computer Science 259, 123–141 (2009)

    Article  MATH  Google Scholar 

  18. Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International Series in Computer Science. Prentice Hall Inc., Hertfordshire (1994)

    MATH  Google Scholar 

  19. Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Mantel, H.: On the composition of secure systems. In: Proceedings of the 2002 IEEE Symposium on Security and Privacy, pp. 88–101 (2002)

    Google Scholar 

  21. Santen, T., Heisel, M., Pfitzmann, A.: Confidentiality-preserving refinement is compositional – sometimes. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 194–211. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Smith, G.: On the foundations of quantitative information flow. In: Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Santen, T.: A formal framework for confidentiality-preserving refinement. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 225–242. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Santen, T.: Preservation of probabilistic information flow under refinement. Information and Computation 206(2-4), 213–249 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  25. Ryan, P.: Mathematical models of computer security. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 1–62. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects of Computing 21(1), 3–32 (2009)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, UK

    Michael J. Banks & Jeremy L. Jacob

Authors
  1. Michael J. Banks
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeremy L. Jacob
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Banks, M.J., Jacob, J.L. (2010). Unifying Theories of Confidentiality. In: Qin, S. (eds) Unifying Theories of Programming. UTP 2010. Lecture Notes in Computer Science, vol 6445. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16690-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16690-7_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16689-1

  • Online ISBN: 978-3-642-16690-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation