Compositional Security-Preserving Refinement for Concurrent Imperative Programs

Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

28 June 2016

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.
BSD License

Change history

[2016-08-19] Removed unused "stop" parameters from the sifum_refinement locale. (revision dbc482d36372) [2016-09-02] TobyM extended "simple" refinement theory to be usable for all bisimulations. (revision 547f31c25f60)

Depends On

Topics

Related Entries

Theories

Cite

×
@article{Dependent_SIFUM_Refinement-AFP,
  author  = {Toby Murray, Robert Sison, 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{http://isa-afp.org/entries/Dependent_SIFUM_Refinement.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download