Advertisement

A Theory of Noninterference for the π-Calculus

  • Silvia Crafa
  • Sabina Rossi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)

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

Keywords

Type System Security Level Operational Semantic Secret Information Label Transition System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)CrossRefMathSciNetGoogle Scholar
  2. 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. 3.
    Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Verifying Persistent Security Properties. Computer Languages, Systems and Structures 30(3-4), 231–258 (2004)CrossRefzbMATHGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. 5.
    Crafa, S., Bugliesi, M., Castagna, G.: Information Flow Security for Boxed Ambients. ENTCS 66(3) (2002)Google Scholar
  6. 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. 7.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM 20, 504–513 (1977)CrossRefzbMATHGoogle Scholar
  8. 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)CrossRefGoogle Scholar
  9. 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. 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. 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)CrossRefGoogle Scholar
  12. 12.
    Hennessy, M.: The security picalculus and non-interference. Journal of Logic and Algebraic Programming 63(1), 3–34 (2004)CrossRefMathSciNetGoogle Scholar
  13. 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)CrossRefMathSciNetGoogle Scholar
  14. 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)CrossRefGoogle Scholar
  15. 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. 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)CrossRefGoogle Scholar
  17. 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. 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. 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)CrossRefGoogle Scholar
  20. 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. 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)CrossRefGoogle Scholar
  22. 22.
    Sangiorgi, D., Walker, D.: The pi calculus: A theory of mobile processes, Cambridge (2001)Google Scholar
  23. 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)CrossRefGoogle Scholar
  24. 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. 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)CrossRefGoogle Scholar
  26. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Silvia Crafa
    • 1
  • Sabina Rossi
    • 2
  1. 1.Dipartimento di MatematicaUniversità di PadovaItaly
  2. 2.Dipartimento di InformaticaUniversità Ca’ Foscari di VeneziaItaly

Personalised recommendations