Security Correctness for Secure Nested Transactions

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