Value-Dependent Information Flow Security

People

Supervisor

Description

Summary:
In this project, we will be looking at language-based analysis of information flow within a program. The end goal is to establish that certain sensitive information is not leaked to unauthorised parties as a result of running the program. Information flow security can be established through reasoning about potential flow between variables (or more generally, states) of a program. The idea is that some variables may contain sensitive information (let’s call them `high’ variables), while others (`low’ variables) may not. A direct information flow is possible if there is an assignment from a high variable to a low variable. A more interesting case is when the flow is implicit. A typical example is the following (in C/Java syntax):

if(secret) then {x:= 0;} else {x := 1;}

Here we assume ‘secret’ is a secret (high) boolean variable, and ‘x’ is a public (low) integer, which is accessible to the attacker. Even though there is no direct assignment from ‘secret’ to ‘x’, the value of ‘x’ is influenced by ‘secret’, and by observing the value of ‘x’, the attacker can determine the value of ‘secret’. An approach to checking potential information flow in a program is using a type system, i.e., by assigning certain labels (types) to variables, and an inference system to determine potential flows induced by statements of the program. Such an analysis is in general an approximation, in the sense that it may conclude wrongly that an information flow is possible, when it is not the case, as the next example shows:

if(y*y < 0) { x := 0; } else {x := 1;}

Here we assume that y is a secret integer variable and x is a public integer variable. The (crude) type-based analysis would typically conclude that there is a potential flow from y to x. However, since the square of an integer is always a positive number (let us assume for now that there is no integer overflow), only the else-branch will be taken when the program is executed, so an attacker observing the state of variable x will not be able to infer anything about the value of y.

Another interesting example is checking information flow when some form of access control is imposed on the caller of the program. This is common in mobile app setting (eg Android’s permission checking mechanism), e.g., consider the following (hypothetical) example

if(check(caller_id, READ_SECRET)) { send(caller_id, secret); } else { send(caller_id, NULL); }

In this case we assume that the function `check’ checks whether the user who calls the program has permission to read the secret (READ_SECRET), and if so, the secret is sent to the caller; otherwise, NULL answer is returned. In this case, there is no possible information leakage, since if the caller does not have the permission to read the secret, nothing is leaked.

In this project, we will investigate the design and implementation of type systems to enforce information flow security, covering all cases described above, but especially the last case, where information flow may be constrained by a pre-defined security policy. We will build on an existing type system for a simple imperative language described in [1]. Several problems to investigate include:

- Designs of type systems: proving soundness of the type systems; investigating information flow under various access control structures/domains
- Type inference problem: how to automate the process of inferring the security types of a program
- Implementation: efficient data structures, dealing with real language features
- Low-level language: information flow techniques for bytecode or machine code; security-preserving compilation of programs.

Reference:
[1] Hongxu Chen, Alwen Tiu, Zhiwu Xu, Yang Liu: A Permission-Dependent Type System for Secure Information Flow Analysis. In Proceedings of the 31st IEEE Symposium on Computer Security Foundations 2018: 218-232.
https://doi.org/10.1109/CSF.2018.00023

Requirements

Good programming skills, good knowledge of programming foundations, especially type systems. 

Background Literature

* Benjamin Pierce: Types and Programming Languages. MIT Press. 2002.

* Andrei Sabelfeld, Andrew C. Myers: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1): 5-19 (2003). https://doi.org/10.1109/JSAC.2002.806121

* Hongxu Chen, Alwen Tiu, Zhiwu Xu, Yang Liu: A Permission-Dependent Type System for Secure Information Flow Analysis. In Proceedings of the 31st IEEE Symposium on Computer Security Foundations 2018: 218-232. https://doi.org/10.1109/CSF.2018.00023

 
 

Keywords

cybersecurity, information flow security, programming languages, type systems, logic

 

 

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing