Position paper: Security correctness for secure nested transactions

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

Abstract

This article considers the synthesis of two long-standing lines of research in computer security: security correctness for multilevel databases, and language-based security. The motivation is an approach to supporting end-to-end security for a wide class of enterprise applications, those of concurrent transactional applications. The approach extends nested transactions with retroactive abort, a new form of semantics for transactional execution, motivated by security concerns. A semantics is given in terms of a local constrained labelled transition system, the Tau One calculus. This allows a noninterference result to be verified based on adapting results on observational equivalence from concurrency theory.

Original languageEnglish
Title of host publicationPLAS'12 - Proceedings of Programming Languages and Analysis for Security
DOIs
StatePublished - 2012
EventACM SIGPLAN 7th Workshop on Programming Languages and Analysis for Security, PLAS'12 - Beijing, China
Duration: 15 Jun 201215 Jun 2012

Publication series

NamePLAS'12 - Proceedings of Programming Languages and Analysis for Security

Conference

ConferenceACM SIGPLAN 7th Workshop on Programming Languages and Analysis for Security, PLAS'12
Country/TerritoryChina
CityBeijing
Period15/06/1215/06/12

Keywords

  • D.2.0 [Software Engineering]: Protection Mechanisms
  • Languages
  • Security
  • Transactions

Fingerprint

Dive into the research topics of 'Position paper: Security correctness for secure nested transactions'. Together they form a unique fingerprint.

Cite this