Control Flow Analysis for the Pi-calculus

C. Bodei, P. Degano, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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 pi-calculus that shows how names will be bound to actual channels at run time. The formulation of the analysis requires no extensions to the pi-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.
    Original languageEnglish
    Title of host publicationProc. CONCUR'98
    PublisherSpringer Verlag
    Publication date1998
    Pages84-98
    Publication statusPublished - 1998
    EventProc. CONCUR'98 -
    Duration: 1 Jan 1998 → …

    Conference

    ConferenceProc. CONCUR'98
    Period01/01/1998 → …

    Cite this

    Bodei, C., Degano, P., Nielson, F., & Nielson, H. R. (1998). Control Flow Analysis for the Pi-calculus. In Proc. CONCUR'98 (pp. 84-98). Springer Verlag.