Skip to main content
SpringerLink
Log in

A Theory of Noninterference for the π-Calculus

  • Conference paper
Trustworthy Global Computing (TGC 2005)

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

Included in the following conference series:

Abstract

We develop a theory of noninterference for a typed version of the π-calculus where types are used to assign secrecy levels to channels. We provide two equivalent characterizations of noninterference based on a typed behavioural equivalence relative to a security level σ, which captures the idea of external observers of level σ. The first characterization involves a universal quantification over all the possible active attacks, i.e., malicious processes which interact with the system possibly leaking secret information. The second definition of noninterference is expressed in terms of an unwinding condition, which deals with so-called passive attacks trying to infer confidential information just by observing the behaviour of the system. This unwinding-based characterization naturally leads to efficient methods for the verification and construction of (compositional) secure systems. Furthermore, we characterize noninterference in terms of bisimulation-like (partial) equivalence relations in the style of a stream of similar studies for other process calculi (e.g., CCS and CryptoSPA) and languages (e.g., imperative and multi-threaded languages).

Supported by the EU-FET project IST-2001-32617 and the FIRB project RBAU018RCZ.

An erratum to this chapter can be found at http://dx.doi.org/10.1007/11580850_20 .

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. Bodei, C., Degano, P., Nielson, F., Nielson, H.R.: Static analysis for the pi-calculus with applications to security. Information and Computation 168, 69–92 (2001)

    Article  MathSciNet  Google Scholar 

  2. Boreale, M., Sangiorgi, D.: Bisimulation in Name-Passing Calculi without Matching. In: Proc. of 13th IEEE Symposium on Logic in Computer Science (LICS 1998), pp. 165–175. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  3. Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Verifying Persistent Security Properties. Computer Languages, Systems and Structures 30(3-4), 231–258 (2004)

    Article  MATH  Google Scholar 

  4. Bossi, A., Piazza, C., Rossi, S.: Modelling Downgrading in Information Flow Security. In: Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 187–201. IEEE Computer Society Press, Los Alamitos (2004)

    Chapter  Google Scholar 

  5. Crafa, S., Bugliesi, M., Castagna, G.: Information Flow Security for Boxed Ambients. ENTCS 66(3) (2002)

    Google Scholar 

  6. Crafa, S., Rossi, S.: A Theory of Noninterference for the π-calculus. Technical Report CS-2004-8, Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Italy (2004), http://www.dsi.unive.it/~silvia/CS-2004-8.ps.gz

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

    Article  MATH  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)

    Chapter  Google Scholar 

  9. Focardi, R., Rossi, S.: Information Flow Security in Dynamic Contexts. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 2002), pp. 307–319. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  10. Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. of the IEEE Symposium on Security and Privacy (SSP 1982), pp. 11–20. IEEE Computer Society Press, Los Alamitos (1982)

    Google Scholar 

  11. Heintze, N., Riecke, J.G.: The SLam Calculus: Programming with Secrecy and Integrity. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1998), pp. 365–377. ACM Press, New York (1998)

    Chapter  Google Scholar 

  12. Hennessy, M.: The security picalculus and non-interference. Journal of Logic and Algebraic Programming 63(1), 3–34 (2004)

    Article  MathSciNet  Google Scholar 

  13. Hennessy, M., Rathke, J.: Typed Behavioural Equivalences for Processes in the Presence of Subtyping. Mathematical Structures in Computer Science 14(5), 651–684 (2004)

    Article  MathSciNet  Google Scholar 

  14. Hennessy, M., Riely, J.: Information Flow vs. Resource Access in the Asynchronous Pi-calculus. ACM Transactions on Programming Languages and Systems (TOPLAS) 24(5), 566–591 (2002)

    Article  Google Scholar 

  15. Honda, K., Vasconcelos, V.T., Yoshida, N.: Secure Information Flow as Typed Process Behaviour. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 180–199. Springer, Heidelberg (2000)

    Google Scholar 

  16. Honda, K., Yoshida, N.: A Uniform Type Structure for Secure Information Flow. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 81–92. ACM Press, New York (2002)

    Chapter  Google Scholar 

  17. Kobayashi, N.: Type-Based Information Flow Analysis for the Pi-Calculus. Technical Report TR03-0007, Dept. of Computer Science, Tokyo Institute of Technology (2003)

    Google Scholar 

  18. Pottier, F.: A simple view of type-secure information flow in the π-calculus. In: Proc. of the 15th IEEE Computer Security Foundations Work shop, pp. 320–330 (2002)

    Google Scholar 

  19. Pottier, F., Simonet, V.: Information Flow Inference for ML. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 319–330. ACM Press, New York (2002)

    Chapter  Google Scholar 

  20. Sabelfeld, A., Mantel, H.: Static Confidentiality Enforcement for Distributed Programs. In: Proc. of Int. Static Analysis Symposium (SAS 2002). LNCS, vol. 2477, pp. 376–394. Springer, Heidelberg (2002)

    Google Scholar 

  21. Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 200–215. IEEE Computer Society Press, Los Alamitos (2000)

    Chapter  Google Scholar 

  22. Sangiorgi, D., Walker, D.: The pi calculus: A theory of mobile processes, Cambridge (2001)

    Google Scholar 

  23. Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1998), pp. 355–364. ACM Press, New York (1998)

    Chapter  Google Scholar 

  24. Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(3), 167–187 (1996)

    Google Scholar 

  25. Yoshida, N., Honda, K., Berger, M.: Linearity and Bisimulation. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 417–434. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Zdancewic, S., Myers, A.C.: Observational Determinism for Concurrent Program Security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop, pp. 29–45 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Matematica, Università di Padova, Italy

    Silvia Crafa

  2. Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Italy

    Sabina Rossi

Authors
  1. Silvia Crafa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sabina Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Sistemi e Informatica, Università di Firenze, Italy

    Rocco De Nicola

  2. Università di Bologna, Italy

    Davide Sangiorgi

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Crafa, S., Rossi, S. (2005). A Theory of Noninterference for the π-Calculus. In: De Nicola, R., Sangiorgi, D. (eds) Trustworthy Global Computing. TGC 2005. Lecture Notes in Computer Science, vol 3705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11580850_2

Download citation

  • DOI: https://doi.org/10.1007/11580850_2

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-31483-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation