Model checking the observational determinism security property using PROMELA and SPIN

Observational determinism is a property that ensures the confidentiality in concurrent programs. It conveys that public variables are independent of private variables during the execution of programs, and the scheduling policy of threads. Different definitions for observational determinism have been proposed. On the other hand, observational determinism is not a standard property and it should be checked over two or more executions of a program. The self-composition approach allows comparing two different copies of a program using a single formula. In this paper, we propose a new specification for the observational determinism security property in linear temporal logic. We also present a general method to create the appropriate program model using the self-composition approach. Both the program model and the observational determinism property are encoded in embedded C codes in PROMELA using the SPIN model checker. The paper also discusses a method for the instrumentation of PROMELA code in order to encode the program model for specifying the observational determinism security property.