We introduce a notion of controlled information release for a typed version of the pi-calculus extended with declassification primitives; this property scales to noninterference when downgrading is not allowed. We provide various characterizations of controlled release, based on a typed behavioural equivalence relative to a security level s, which captures the idea of externalbobservers of level s. First, we define our security property through a universal quantification over all the possible active attackers, i.e., malicious processes which interact with the system possibly leaking secret information. Then we characterize the controlled release property in terms of an unwinding condition, which deals with so-called passive attackers trying to infer confidential information just by observing the behaviour of the system. Furthermore, we express controlled information release in terms of partial equivalence relations (per models, for short) in the style of a stream of similar studies for imperative and multi-threaded languages. We show that the controlled release property is compositional with respect to most operators of the language leading to efficient proof techniques for the verification and the construction of (compositional) secure systems.

Controlling Information Release in the pi-calculus

ROSSI, Sabina
2007-01-01

Abstract

We introduce a notion of controlled information release for a typed version of the pi-calculus extended with declassification primitives; this property scales to noninterference when downgrading is not allowed. We provide various characterizations of controlled release, based on a typed behavioural equivalence relative to a security level s, which captures the idea of externalbobservers of level s. First, we define our security property through a universal quantification over all the possible active attackers, i.e., malicious processes which interact with the system possibly leaking secret information. Then we characterize the controlled release property in terms of an unwinding condition, which deals with so-called passive attackers trying to infer confidential information just by observing the behaviour of the system. Furthermore, we express controlled information release in terms of partial equivalence relations (per models, for short) in the style of a stream of similar studies for imperative and multi-threaded languages. We show that the controlled release property is compositional with respect to most operators of the language leading to efficient proof techniques for the verification and the construction of (compositional) secure systems.
2007
285
File in questo prodotto:
File Dimensione Formato  
Inf&Comp07.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 599.12 kB
Formato Adobe PDF
599.12 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA 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: https://hdl.handle.net/10278/29431
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? ND
social impact