Logics for Information Flow Security: From Specification to Verification

Abstract

Software is becoming increasingly ubiquitous and today we find software running everywhere. There is software driving our favorite game application or inside the web portal we use to read the morning news, and when we book a vacation. Being so commonplace, software has become an easy target to compromise maliciously or at best to get it wrong. In fact, recent trends and highly-publicized attacks suggest that vulnerable software is at the root of many security attacks. Information flow security is the research field that studies methods and techniques to provide strong security guarantees against software security attacks and vulnerabilities. The goal of an information flow analysis is to rigorously check how sensitive information is used by the software application and ensure that this information does not escape the boundaries of the application, unless it is properly granted permission to do so by the security policy at hand. This process can be challenging as it first requires to determine what the applications security policy is and then to provide a mechanism to enforce that policy against the software application. In this thesis we address the problem of (information flow) policy specification and policy enforcement by leveraging formal methods, in particular logics and language-based analysis and verification techniques.

The thesis contributes to the state of the art of information flow security in several directions, both theoretical and practical. On the policy specification side, we provide a framework to reason about information flow security conditions using the notion of knowledge. This is accompanied by logics that can be used to express the security policies precisely in a syntactical manner. Also, we study the interplay between confidentiality and integrity to enforce security in presence of active attacks. On the verification side, we provide several symbolic algorithms to effectively check whether an application adheres to the associated security policy. To achieve this, we propose techniques based on symbolic execution and first-order reasoning (SMT solving) to first extract a model of the target application and then verify it against the policy. On the practical side, we provide tool support by automating our techniques and thereby making it possible to verify programs written in Java or ARM machine code. Besides the expected limitations, our case studies show that the tools can be used to verify the security of several realistic scenarios. More specifically, the thesis consists of two parts and six chapters. We start with an introduction giving an overview of the research problems and the results of the thesis. Then we move to the specification part which relies on knowledge-based reasoning and epistemic logics to specify state-based and trace-based information flow conditions and on the weakest precondition calculus to certify security in presence of active attacks. The second part of the thesis addresses the problem of verification of the security policies introduced in the first part. We use symbolic execution and SMT solving techniques to enable model checking of the security properties. In particular, we implement a tool that verifies noninterference and declassification policies for Java programs. Finally, we conclude with relational verification of low level code, which is also supported by a tool.