A Temporal Logic Characterisation of Observational Determinism

Marieke Huisman, Pratik Worah, Kim Sunesen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

47 Citations (Scopus)

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 languageEnglish
Title of host publication19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy
PublisherIEEE Computer Society Press
Number of pages1
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event19th IEEE Computer Security Foundations Workshop, CSFW 2006 - Venice, Italy
Duration: 5 Jul 20067 Jul 2006
Conference number: 19

Conference

Conference19th IEEE Computer Security Foundations Workshop, CSFW 2006
Abbreviated titleCSFW 2006
CountryItaly
CityVenice
Period5/07/067/07/06

Fingerprint

Dive into the research topics of 'A Temporal Logic Characterisation of Observational Determinism'. Together they form a unique fingerprint.

Cite this