A BRICS Mini-Course
February 16 and 18, 1999
Lectures by
Pierpaolo Degano, degano@di.unipi.it
Department of Computer Science, Università di Pisa, Italy
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 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. Besides a set of rules that permit to validate a given solution, we also offer a constructive procedure that builds solutions in low polynomial time.
Applications of our analysis include establishing two simple security properties of processes. One example is that P has no leaks: P offers communication to the external environment through public channels only, and confines its secret names within itself. The other example is connected to the no read-up/no write-down property of Bell and LaPadula: once processes are given levels of security clearance, we check that a process at a high level never sends names to processes at a lower level.
Pierpaolo Degano is Professor of Computer Science since 1990, first at the University of Parma and from 1993 at the Department of Computer Science, Università di Pisa, of which he has been director for three years.
The main areas of interest of Pierpaolo Degano have been or are