### Abstract

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

This Isabelle/HOL formalization uses theories from the entry Strong Security.

### License

BSD License

### Topics

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

### Session WHATandWHERE_Security

- WHATWHERE_Security
- Up_To_Technique
- MWLs
- Parallel_Composition
- WHATWHERE_Secure_Skip_Assign
- Language_Composition
- Type_System
- Type_System_example

### Depends on

- A Formalization of Strong Security

### Auto-related entries

- A Formalization of Assumptions and Guarantees for Compositional Noninterference

## Cite

×

WHATandWHERE_Security-AFP

    @article{WHATandWHERE_Security-AFP,
      author  = {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens Sauer},
      title   = {A Formalization of Declassification with WHAT-and-WHERE-Security},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/WHATandWHERE_Security.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 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Apr 24, 2014 : Isabelle2013-2