Abstract
This paper studies observational determinism, a generalisation of non-interference for multi-threaded programs. Standard notions of non-interference only consider input and output of programs, but to ensure the security of multithreaded programs, one has to consider execution traces. In earlier work, Zdancewic and Myers propose to consider a multi-threaded program secure when it behaves deterministic w.r.t. its public (or low) variables, i.e. traces of public variables should not depend on private (or high) variables. This property is called observational determinism. The original definition of observational determinism still allows to reveal private data; this paper corrects this. The main contribution of this paper is a rephrasing of the definition of observational determinism in terms of a temporal logic. This allows to use standard model checking techniques to verify observational determinism, which has the advantage that the verification is automatic and precise. Moreover in case the verification fails, model checking can produce a counterexample. We characterise observational determinism in CTL* and in the polyadic modal mu-calculus. For both logics, model checking algorithms exist
| Original language | English |
|---|---|
| Title of host publication | 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy |
| Publisher | IEEE |
| Number of pages | 1 |
| DOIs | |
| Publication status | Published - 2006 |
| Externally published | Yes |
| Event | 19th IEEE Computer Security Foundations Workshop, CSFW 2006 - Venice, Italy Duration: 5 Jul 2006 → 7 Jul 2006 Conference number: 19 |
Conference
| Conference | 19th IEEE Computer Security Foundations Workshop, CSFW 2006 |
|---|---|
| Abbreviated title | CSFW 2006 |
| Country/Territory | Italy |
| City | Venice |
| Period | 5/07/06 → 7/07/06 |