Email Gateway (Aug 22 2022 at 13:28): Email Gateway (Aug 22 2022 at 13:28):From: Tobias Nipkow <nipkow@in.tum.de>
A Dependent Security Type System for Concurrent Imperative Programs
Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
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.
https://www.isa-afp.org/entries/Dependent_SIFUM_Type_Systems.shtml
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC