A Dependent Security Type System for Concurrent Imperative Programs

Toby Murray 🌐, Robert Sison, Edward Pierzchalski and Christine Rizkallah 🌐

June 25, 2016

Abstract

The paper "Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference" by Murray et. al. (CSF 2016) presents a dependent security type system for compositionally verifying a value-dependent noninterference property, defined in (Murray, PLAS 2015), for concurrent programs. This development formalises that security definition, the type system and its soundness proof, and demonstrates its application on some small examples. It was derived from the SIFUM_Type_Systems AFP entry, by Sylvia Grewe, Heiko Mantel and Daniel Schoepe, and whose structure it inherits.
BSD License

Topics

Theories of Dependent_SIFUM_Type_Systems

Used by

Cite

× 
@article{Dependent_SIFUM_Type_Systems-AFP,
  author  = {Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah},
  title   = {A Dependent Security Type System for Concurrent Imperative Programs},
  journal = {Archive of Formal Proofs},
  month   = June,
  year    = 2016,
  note    = {\url{https://isa-afp.org/entries/Dependent_SIFUM_Type_Systems.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest