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 result of our analysis establishes a super-set of the set of channels to which a given name may be bound and of the set of channels that may be sent along a given channel. Besides a set of rules that permits one 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 channels 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 channels to processes at a lower level.
|Autori:||BODEI C.; DEGANO P; NIELSON F.; RIIS NIELSON H.|
|Titolo:||Static Analysis for the Pi-Calculus with Applications to Security|
|Anno del prodotto:||2001|
|Digital Object Identifier (DOI):||10.1006/inco.2000.3020|
|Appare nelle tipologie:||1.1 Articolo in rivista|