Verification of information flow properties

Abstract

Information flow properties are a way of specifying security properties of systems, that dates back to the work of Goguen and Meseguer [7] in the eighties. A system is viewed as generating traces containing “confidential” and “visible” events (only the latter being observable by a “low-level” user) and the information flow properties specify restrictions on the kind of traces the system may generate, so as to restrict the amount of information a low-level user can infer about confidential events having taken place (or not) in the system. Mantel [14, 12] identifies a set of basic information flow properties which he calls “basic security predicates” or BSP’s and shows them to be the building blocks of most of the known trace-based properties in the literature. Traditionally BSP’s have been reasoned about via unwinding conditions that capture whether a system satisfies a particular BSP. This method is not complete in general, in that a system could satisfy the information flow property but fail the unwinding condition. In this thesis, we present three results. First, we consider the problem of checking the unwinding conditions for BSP’s for finite-state systems. We show that the checking of unwinding conditions can be simplified to checking conditions on a maximal simulation relation. Second, we present a model checking technique to verify information flow properties for finite-state systems. We show that the BSP’s can be characterised in terms of regularity-preserving language-theoretic operations. This leads to a decision procedure for checking whether a finite-state system satisfies a given BSP. In contrast to unwinding, model-checking approach is language-based and complete for all information flow properties that can be expressed in terms of BSP’s. Third, we prove that the problem of verifying BSP’s for pushdown systems is undecidable.