INRIA Sophia-Antipolis (FRANCE)
IIT Kharagpur (INDIA)
Esterel Technologies (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
Privacy guarantees are essential to ensure the acceptance of global
computing applications, such as electronic banking or health care
information systems. Observational determinism is a notion of security
ensuring that changes in private or secret data are not reflected in
the public data. This case study describes the application of LOTOS
and CADP so as to check if a program satisfies observational
The considered programming language is a parallel while-language, providing assignments, if-then-else statements, sequential and parallel composition, while-loops, and the statement ``wait(b)'', which blocks execution until condition ``b'' becomes true. A simulator for this language has been written in LOTOS.
To assess the privacy guarantees of a program by model checking, two different logical characterisations of observational determinism are compared. The first characterisation uses a CTL* formula, which is close to the formal definition of observational determinism. However, this first approach leads to large models, since it requires to use a memorising transition relation that, for each transition, keeps track of the source state. The second characterisation using the polyadic modal mu-calculus might seem less intuitive, but the generated models are smaller and simpler. For both characterisations, the formulas are translated into modal mu-calculus formulae and checked with EVALUATOR.
A technique to precisely verify observational determinism of parallel
while programs has been implemented using CADP. As regards the model
checking of security properties, the authors of
[Huisman-Worah-Sunesen-06] conclude that the mu-calculus is more
promising than an approach using CTL*, since the latter generates
significantly larger models.
As regards the reasons for using LOTOS and CADP, the authors of [Huisman-Worah-Sunesen-06] mention the following:
Marieke Huisman, Pratik Worah, and Kim Sunesen.
"A Temporal Logic Characterisation of Observational Determinism". In
Proceedings of the 19th IEEE Computer Security Foundations Workshop
CSFW '06 (Venice, Italy), IEEE Computer Society Press, July 2006.
Available on-line at ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf
or from our FTP site in PDF or PostScript
INRIA Sophia Antipolis
2004, route des Lucioles BP 93
06902 Sophia Antipolis
Tel: +33 (0)4 92 38 79 45
Fax: +33 (0)4 92 38 50 29
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|