A Type System for Observational Determinism

Zdancewic and Myers introduced observational determinism as a scheduler independent notion of security for concurrent programs. This paper proposes a type system for verifying observational determinism. The authors' type system verifies observational determinism by itself, and does not require the type checked program to be confluent. A polynomial time type inference algorithm is also presented. Non-interference is a property of a program which states that the program's publicly observable (i.e., low security) behavior is independent of its confidential (i.e., high security) inputs.