Security Properties through the Lens of Modal Logic

Abstract

Computer security research is on a long-running quest for a universal framework to reason about security properties. Such a framework ought to be expressive enough to capture any security policy conceived of, while also being independent of syntactic details and enforcement mechanisms, applicable to any system on which we may wish to impose security, and intuitive enough that humans can grasp the meaning of any given property (and not experience surprises due to a false sense of grasping).

In this talk, I will present a framework based on modal logic which we have recently introduced in pursuit of these goals. In our approach, we combine established techniques for modal reasoning about knowledge with modalities of time and possible actions, and carefully distinguish between agents' capabilities and the effects we wish to permit them to achieve.

As we show, our formalism can be used to represent various progress- and termination-(in)sensitive variants of confidentiality, integrity, robust declassification and transparent endorsement, for each of which we have proven 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.

This project is joint work with Musard Balliu and Roberto Guanciale at KTH.