Secure information flow: analysis and enforcement

Adetoye, Adedayo Oyelakin (2009). Secure information flow: analysis and enforcement. University of Birmingham. Ph.D.

Preview

adetoye09PhD.pdf
PDF
Download (1MB)

Abstract

When a computer program requires legitimate access to confidential data, the question arises whether such a program may reveal sensitive information to an unauthorised observer. There is therefore a need to ensure that a program, which processes confidential data, is free of unwanted information flow. This thesis presents a formal framework for the analysis and enforcement of secure information flow in computational systems such as computer programs. An important aspect of the problem of secure information flow is the development of policies by which we can express intended information release. For this reason information lattices and maps on these lattices are presented as models, which capture intuitive notions about information and information flow. A definition of security is given, based on the lattice formalisation of information and information flow, that exploits the partial order of the information lattice. The lattice formalisation gives us a uniform way to enforce information security policies under various qualitative and quantitative representations of information. An input-output relational model, which describes how a system transforms its input to publicly observable outputs with respect to a given attacker model, is presented as a primitive for the study of secure information flow. By using the relational model, various representations of information, which are shown to fit into the lattice model of information, are derived for the analysis of information flow under deterministic and nondeterministic system models. A systematic technique to derive the relational model of a system, under a given attacker model, from the operational semantics in a language-based setting, is also presented. This allows the development of information flow analyses parametrised by chosen attacker models. A flow-sensitive and termination-sensitive static analysis calculus is presented for the analysis of information flow in programs written in a deterministic While language with outputs. The analysis is shown to be correct with respect to an attacker model that is able to observe all program outputs and which can determine the termination or nontermination of program execution. The static analysis also detects certain disjunctive information release. A termination-sensitive dependency analysis is developed which demonstrates how, by employing abstract interpretation techniques, other less precise but possibly more efficient information flow analysis may be obtained. The thesis concludes with further examples to highlight various aspects of the information flow analysis and enforcement framework developed.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):