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.

Static Analysis for the Pi-Calculus with Applications to Security

BODEI, CHIARA;DEGANO, PIERPAOLO;
2001

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 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.
Bodei, Chiara; Degano, Pierpaolo; Nielson, F.; RIIS NIELSON, H.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/176541
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 63
  • ???jsp.display-item.citation.isi??? 52
social impact