PICNIC is a tool for verifying security properties of systems, namely non-interference properties of processes ex- pressed as terms of the π-calculus with two security levels and declassification primitives. More precisely, it checks whether inserting a process into two different high contexts no information leakage to the low level observers occurs. These properties are decidable over finite control processes, but decidability can be extended by compositionality also to some infinite state processes. Notably, PICNIC has been developed in Fresh O’CaML, a dialect of CaML with native support for binders and fresh/local names; thus, this work can be seen also as a non-trivial case study about the applicability of these new programming languages.

PicNic - pi-calculus non-interference checker. (Tool paper)

CRAFA, SILVIA;
2008

Abstract

PICNIC is a tool for verifying security properties of systems, namely non-interference properties of processes ex- pressed as terms of the π-calculus with two security levels and declassification primitives. More precisely, it checks whether inserting a process into two different high contexts no information leakage to the low level observers occurs. These properties are decidable over finite control processes, but decidability can be extended by compositionality also to some infinite state processes. Notably, PICNIC has been developed in Fresh O’CaML, a dialect of CaML with native support for binders and fresh/local names; thus, this work can be seen also as a non-trivial case study about the applicability of these new programming languages.
Proc. of the 8th International Conference on Application of Concurrency to System Design (ACSD'08)
9781424418381
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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: https://hdl.handle.net/11577/2272457
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact