Email Gateway (Aug 19 2022 at 14:11): Email Gateway (Aug 19 2022 at 14:11):From: Tobias Nipkow <nipkow@in.tum.de>
A Formalization of Assumptions and Guarantees for Compositional Noninterference
Sylvia Grewe, Heiko Mantel, Daniel Schoepe
Research in information-flow security aims at developing methods to identify
undesired information leaks within programs from private (high) sources to
public (low) sinks. For a concurrent system, it is desirable to have
compositional analysis methods that allow for analyzing each thread
independently and that nevertheless guarantee that the parallel composition of
successfully analyzed threads satisfies a global security guarantee. However,
such a compositional analysis should not be overly pessimistic about what an
environment might do with shared resources. Otherwise, the analysis will reject
many intuitively secure programs.
The paper "Assumptions and Guarantees for Compositional Noninterference" by
Mantel et. al. presents one solution for this problem: an approach for
compositionally reasoning about non-interference in concurrent programs via
rely-guarantee-style reasoning. We present an Isabelle/HOL formalization of the
concepts and proofs of this approach.
http://afp.sourceforge.net/entries/SIFUM_Type_Systems.shtml
A Formalization of Strong Security
Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
Research in information-flow security aims at developing methods to identify
undesired information leaks within programs from private sources to public
sinks. Noninterference captures this intuition. Strong security from Sabelfeld
and Sands formalizes noninterference for concurrent systems.
We present an Isabelle/HOL formalization of strong security for arbitrary
security lattices (Sabelfeld and Sands use a two-element security lattice in the
original publication). The formalization includes compositionality proofs for
strong security and a soundness proof for a security type system that checks
strong security for programs in a simple while language with dynamic thread
creation.
Our formalization of the security type system is abstract in the language for
expressions and in the semantic side conditions for expressions. It can easily
be instantiated with different syntactic approximations for these side
conditions. The soundness proof of such an instantiation boils down to showing
that these syntactic approximations imply the semantic side conditions.
http://afp.sourceforge.net/entries/Strong_Security.shtml
A Formalization of Declassification with WHAT-and-WHERE-Security
Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
AbsResearch in information-flow security aims at developing methods to identify
undesired information leaks within programs from private sources to public
sinks. Noninterference captures this intuition by requiring that no information
whatsoever flows from private sources to public sinks. However, in practice this
definition is often too strict: Depending on the intuitive desired security
policy, the controlled declassification of certain private information (WHAT) at
certain points in the program (WHERE) might not result in an undesired
information leak.
We present an Isabelle/HOL formalization of such a security property for
controlled declassification, namely WHAT&WHERE-security from
"Scheduler-Independent Declassification" by Lux, Mantel, and Perner. The
formalization includes compositionality proofs for and a soundness proof for a
security type system that checks for programs in a simple while language with
dynamic thread creation.
Our formalization of the security type system is abstract in the language for
expressions and in the semantic side conditions for expressions. It can easily
be instantiated with different syntactic approximations for these side
conditions. The soundness proof of such an instantiation boils down to showing
that these syntactic approximations imply the semantic side conditions.
http://afp.sourceforge.net/entries/WHATandWHERE_Security.shtml
Enjoy!
Last updated: Apr 16 2024 at 20:15 UTC