|
A
Dependent
Security
Type
System
for
Concurrent
Imperative
Programs
Title: |
A Dependent Security Type System for Concurrent Imperative Programs |
Authors:
|
Toby Murray,
Robert Sison,
Edward Pierzchalski and
Christine Rizkallah
|
Submission date: |
2016-06-25 |
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. |
Change history: |
[2016-08-19]:
Removed unused "stop" parameter and "stop_no_eval" assumption from the sifum_security locale.
(revision dbc482d36372)
[2016-09-27]:
Added security locale support for the imposition of requirements on the initial memory.
(revision cce4ceb74ddb) |
BibTeX: |
@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 = jun,
year = 2016,
note = {\url{http://isa-afp.org/entries/Dependent_SIFUM_Type_Systems.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
Dependent_SIFUM_Refinement |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|