Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 1998: CONCUR'98 Concurrency Theory pp 84–98Cite as

Control flow analysis for the π-calculus

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1466))

Abstract

Control Flow Analysis is a static technique for predicting safe and computable approximations to the set of values that the objects of a program may assume during its execution. We present an analysis for the π-calculus that shows how names will be bound to actual channels at run time. The formulation of the analysis requires no extensions to the π-calculus, except for assigning “channels” to the occurrences of names within restrictions, and assigning “binders” to the occurrences of names within input prefixes.

The result of our analysis establishes a super-set of the set of names to which a given name may be bound and of the set of names that may be sent along a given channel. Applications of our analysis include establishing simple security properties of processes. One example is that P has no leaks, i.e. P offers communication through public channels only, and confines its secret names within itself.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi. Secrecy by typing in security protocols. In Proceedings of Theoretical Aspects of Computer Software, Third International Symposiuoum, LNCS 1281, pages 611–638. Springer-Verlag, 1997.

    Google Scholar 

  2. R.M. Amadio. An asynchronous model of locality, failure, and process mobility. In Proceedings of COORDINATION'97, LNCS 1282. Springer-Verlag, 1997.

    Google Scholar 

  3. D.E. Bell and L.J. La Padula. Secure computer systems: Unified exposition and multics interpretation. Technical Report ESD-TR-75-306, Mitre C., 1976.

    Google Scholar 

  4. M. Dam. Proving trust in systems of second-order processes: Preliminary results. Technical Report LOMAPS-SICS 19, SICS, Sweden, 1997.

    Google Scholar 

  5. R. De Nicola, G. Ferrari, and R. Pugliese. Coordinating mobile agents via blackboards and access rights. In Proceedings of COORDINATION'97, LNCS 1282. Springer-Verlag, 1997.

    Google Scholar 

  6. R. Focardi. Comparing two information flow security properties. In Proceedings of 9th IEEE Computer Science Security Foundation W/S, pages 116–122, 1996.

    Google Scholar 

  7. R. Focardi and R. Gorrieri. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering. To appear.

    Google Scholar 

  8. C. Fournet, C. Laneve, L. Maranget, and D. Remy. Implicit typing à la ML for the join calculus. In Proceedings of CONCUR'97, LNCS. Springer-Verlag, 1997.

    Google Scholar 

  9. K.L.S. Gasser, F. Nielson, and H.R. Nielson. Systematic realisation of control flow analysis for CML. In Proceedings of ICFP'97, pages 38–51. ACM Press, 1997.

    Google Scholar 

  10. J.A. Goguen and J. Meseguer. Security policy and security models. In Proceedings of the 1982 IEEE Symposioum on Security and Privacy, pages 11–20, 1982.

    Google Scholar 

  11. T.J. Marlowe and B.J. Ryder. Properties of data flow frameworks — a unified model. Acta Informatica, 28(2):121–163, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  12. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (I and II). Information and Computation, 100(1):1–77, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. TCS, 114:149–171, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  14. J. Palsberg and M.J. Schwartzbach. Object-Oriented Type Systems. Wiley, 1994.

    Google Scholar 

  15. B.C. Pierce and D. Sangiorgi. Typing and sub-typing for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.

    MATH  MathSciNet  Google Scholar 

  16. J. Riely and M. Hennessy. A typed language for distributed mobile processes. In Proceedings of POPL'98. ACM Press, 1998.

    Google Scholar 

  17. P. Sewell. Global/local subtyping for a distributed π-calculus. Technical Report 435, Computer Laboratory, University of Cambridge, 1997.

    Google Scholar 

  18. O. Shivers. Control flow analysis in Scheme. In Proceedings of PLDI'88, volume 7(1). ACM SIGPLAN Notices, 1988.

    Google Scholar 

  19. A. Venet. Abstract interpretation of the π-calculus. In Analysis and Verification of Multiple-Agent Languages, LNCS, volume 1192. Springer-Verlag, 1997.

    Google Scholar 

  20. D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4:4–21, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100, Pisa, Italy

    Chiara Bodei, Pierpaolo Degano & Flemming Nielson

  2. Computer Science Department, Aarhus University, Ny Munkegade, DK-8000, arhus C, Denmark

    Hanne Riis Nielson

Authors
  1. Chiara Bodei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierpaolo Degano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Flemming Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hanne Riis Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Davide Sangiorgi Robert de Simone

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bodei, C., Degano, P., Nielson, F., Nielson, H.R. (1998). Control flow analysis for the π-calculus. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055617

Download citation

  • DOI: https://doi.org/10.1007/BFb0055617

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64896-3

  • Online ISBN: 978-3-540-68455-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation