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. Our 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.

• Type: Conference
• Year: 2008
• Where: CSFW
• Authors: Tachio Terauchi
• Keywords: CSFW 2008, Observational Determinism, Security Privacy, Type Checked Program, Verifies Observational Determinism