Security Properties through the Lens of Modal Logic

TL;DR

This paper presents a modal logic-based framework for reasoning about various security properties of computer systems, offering a unified, expressive, and intuitive approach that clarifies assumptions and enables the formulation of new security concepts.

Contribution

It introduces a novel modal logic framework that captures diverse security properties, clarifies underlying assumptions, and facilitates the development of new security definitions.

Findings

Framework effectively represents confidentiality, integrity, and related properties

Proves equivalence to standard security definitions

Highlights assumptions and potential issues in existing security models

Abstract

We introduce a framework for reasoning about the security of computer systems using modal logic. This framework is sufficiently expressive to capture a variety of known security properties, while also being intuitive and independent of syntactic details and enforcement mechanisms. We show how to use our formalism to represent various progress- and termination-(in)sensitive variants of confidentiality, integrity, robust declassification and transparent endorsement, and prove equivalence to standard definitions. The intuitive nature and closeness to semantic reality of our approach allows us to make explicit several hidden assumptions of these definitions, and identify potential issues and subtleties with them, while also holding the promise of formulating cleaner versions and future extension to entirely novel properties.