### 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.

### License

BSD License

### History

September 27, 2016
  Added security locale support for the imposition of requirements on the initial memory. (revision cce4ceb74ddb)
August 19, 2016
  Removed unused "stop" parameter and "stop_no_eval" assumption from the sifum_security locale. (revision dbc482d36372)

### Topics

- Computer science/Security
- Computer science/Programming languages/Type systems

### Session Dependent_SIFUM_Type_Systems

- Preliminaries
- Security
- Compositionality
- Language
- TypeSystem
- LocallySoundModeUse
- Example
- TypeSystemTactics
- Example_TypeSystem
- Example_Swap_Add

### Used by

- Compositional Security-Preserving Refinement for Concurrent Imperative Programs

## Cite

×

Dependent_SIFUM_Type_Systems-AFP

    @article{Dependent_SIFUM_Type_Systems-AFP,
      author  = {Toby Murray and Robert Sison and 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

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Jun 25, 2016 : Isabelle2016