Security correctness for secure nested transactions extended abstract

Secure nested transactions have been introduced as a synthesis of two long-standing lines of research in computer security: security correctness for multilevel databases, and language-based security. The motivation is to consider information flow control for certain classes of concurrent applications. This article describes a noninterference result for secure nested transactions, based on observational equivalence. A semantics for secure nested transactions is provided based on an extension of the pi-calculus with nested transactions, the calculus. A novelty of this semantics is a constrained labelled transition system, where local transition rules place logical constraints on the global state of the transactional context. This context is described by a notion of logs, an abstraction for factoring transactional state out of the usual description of concurrent processes. An advantage of this approach is that it allows the consideration of security properties such as noninterference independently of transactional properties such as serializability.