Skip to main content
SpringerLink
Log in

Stepwise Development of Secure Systems

  • Conference paper
Computer Safety, Reliability, and Security (SAFECOMP 2006)

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

Included in the following conference series:

Abstract

System development by stepwise refinement is a well-established method in classical software engineering. We discuss how this method can be adapted to systematically incorporate security issues, in particular, confidentiality into the software construction process. Starting with an abstract system model that precisely captures the relevant confidentiality requirements, subsequent refinements produce models which introduce more detail or relax assumptions on the environment. For each refinement, changing adversary capabilities must be captured and their compatibility with the given confidentiality requirements must be established. In this context, security, and dependability in general, are existential properties: The existence of a secure implementation must be kept invariant during the development process. This considerably adds to the complexity of a development.

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. Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Chaum, D.L.: Untraceable electronic mail, return addresses, and digital pseudonyms. Communications of the ACM 24(2), 84–88 (1981)

    Article  Google Scholar 

  4. Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Derrick, J., Boiten, E.: Refinement in Z and Object-Z. Springer, London (2001)

    MATH  Google Scholar 

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

    Google Scholar 

  7. Gray III., J.W.: Toward a mathematical foundation for information flow security. Journal of Computer Security, 255–294 (1992)

    Google Scholar 

  8. Heisel, M., Pfitzmann, A., Santen, T.: Confidentiality-preserving refinement. In: 14th IEEE Computer Security Foundations Workshop, pp. 295–305. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  9. Hutter, D.: Possibilistic information flow control in MAKS and action refinement. In: Müller, G. (ed.) ETRICS 2006. LNCS, vol. 3995, pp. 268–281. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Jackson, M.: Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley, Reading (2000)

    Google Scholar 

  11. Jacob, J.: On the derivation of secure components. In: IEEE Symposium on Security and Privacy, pp. 242–247. IEEE Press, Los Alamitos (1989)

    Chapter  Google Scholar 

  12. Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  13. Jürjens, J.: Secrecy-preserving refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 135–152. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Jürjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  15. Mantel, H.: Preserving information flow properties under refinement. In: IEEE Symposium on Security and Privacy, pp. 78–91. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  16. Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. Ph.D thesis, Universität des Saarlandes (2003)

    Google Scholar 

  17. McLean, J.: A general theory of composition for a class of “possibilistic” properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996)

    Article  Google Scholar 

  18. Meyer, B.: Applying “design by contract”. IEEE Computer, 40–51 (October 1992)

    Google Scholar 

  19. Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)

    Article  MATH  Google Scholar 

  20. Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: IEEE Symposium on Security and Privacy, pp. 184–201. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

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

    Google Scholar 

  22. Santen, T.: Probabilistic confidentiality properties based on indistinguishability. In: Federrath, H. (ed.) Proc. Sicherheit 2005 – Schutz und Zuverlässigkeit. Lecture Notes in Informatics, pp. 113–124. Gesellschaft für Informatik (2005)

    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. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  25. Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Proc. IEEE Symposium on Security and Privacy, pp. 94–102 (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, Germany

    Thomas Santen

Authors
  1. Thomas Santen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software Engineering, Gdańsk University of Technology,, Narutowicza 11/12, 80-952, Gdańsk, Poland

    Janusz Górski

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Santen, T. (2006). Stepwise Development of Secure Systems. In: Górski, J. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2006. Lecture Notes in Computer Science, vol 4166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11875567_11

Download citation

  • DOI: https://doi.org/10.1007/11875567_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-45762-6

  • Online ISBN: 978-3-540-45763-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation