Design and verification of information flows

Abstract

The ever-increasing systems’ interconnectivity with the amount of information made available lead to a growing demand for responsible handling of sensitive and critical data. Data use and protection policies can be specified as information-flow policies that state how information can flow and be observed through systems or computations. Enforcing information-flow policies is notoriously a challenging problem because information can be inferred by analyzing multiple executions of a system. To enforce such policies, verifying each system execution separately (as it is done for trace properties) is not enough. From a formal standpoint, information-flow policies are specified by hyperproperties. In this work, we dive into the mathematical foundations for designing and verifying secure systems.Many challenges must be addressed to design frameworks that help build secure systems. Due to the complexity of the systems’ development cycle, security requirements should be laid down as soon as possible. This approach, called security by design, is difficult to achieve in practice because hyperproperties are not closed under refinement. Moreover, it is usually unclear how to interpret security policies in terms of hyperproperties at the early stages of a system design. We address this in the first part of the thesis by separating the structural view of information flow (where information flows) from its semantic view (what is a flow of information). We then introduce an interface theory to support contract-based design for the structural perspective.Observations of different systems’ executions are often not aligned temporally, with information-flow specification often defining asynchronous hyperproperties. In the second part of the thesis, we focus on the specification of information-flow and prove that the most successful logic for hyperproperties, HyperLTL, cannot express asynchronous hyperproperties. Asynchronous hyperproperties received much attention recently, with many logics proposed to specify them. They all have, however, undecidable model-checking problems, with decidability achieved only for restricted fragments. In the last contribution of this thesis, we approach this difficulty by combining automata and logic in a new formalism called hypernode automata. The logic handles asynchronicity within specification states, while automata transitions enable synchronization points between those states.We finish by introducing a novel decidable model-checking algorithm for asynchronous hyperproperties specified with hypernode automata.