Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: A Dependent Security Type Sys...


view this post on Zulip 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: Mar 29 2024 at 12:28 UTC