PicNIc - Pi-calculus non-interference checker

8 years 9 months ago
PicNIc - Pi-calculus non-interference checker
PICNIC is a tool for verifying security properties of systems, namely non-interference properties of processes expressed 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.
Silvia Crafa, Matteo Mio, Marino Miculan, Carla Pi
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2008
Where ACSD
Authors Silvia Crafa, Matteo Mio, Marino Miculan, Carla Piazza, Sabina Rossi
Comments (0)