Compositional Security-Preserving Refinement for Concurrent Imperative Programs

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

June 28, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The paper "Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference" by Murray et. al. (CSF 2016) presents a compositional theory of refinement for a value-dependent noninterference property, defined in (Murray, PLAS 2015), for concurrent programs. This development formalises that refinement theory, and demonstrates its application on some small examples.

License

BSD License

History

September 2, 2016
TobyM extended "simple" refinement theory to be usable for all bisimulations. (revision 547f31c25f60)
August 19, 2016
Removed unused "stop" parameters from the sifum_refinement locale. (revision dbc482d36372)

Topics

Session Dependent_SIFUM_Refinement

Depends on

Cite

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

Download

× Download latest

Older releases: