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 language | English |
|---|---|
| Title of host publication | Proc. CONCUR'98 |
| Publisher | Springer Verlag |
| Publication date | 1998 |
| Pages | 84-98 |
| Publication status | Published - 1998 |
| Event | Proc. CONCUR'98 - Duration: 1 Jan 1998 → … |
Conference
| Conference | Proc. CONCUR'98 |
|---|---|
| Period | 01/01/1998 → … |