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.
Index Terms:
Security, Programming Language, Type System, Linear Programming
Citation:
Tachio Terauchi, "A Type System for Observational Determinism," csf, pp.287-300, 2008 21st IEEE Computer Security Foundations Symposium, 2008