Article Preview
Top1. Introduction
Data integrity is an important issue for programs, but this does not mean that programs must guarantee that all good data is perfectly preserved, or that no bad data can affect a program’s output in any way. It is often the case that a good service can be provided with a small but acceptable loss in the the integrity of data. Therefore, there is a need for a framework in which the level of integrity a system provides can be accurately measured.
Qualitative integrity has been well-studied (see e.g. the work of Birgisson et al. (Birgisson, Russo, & Sabelfeld, 2010), who provide a unified framework for qualitative integrity policies), but quantitative integrity measures have received far less attention. An exception to this is the work of Clarkson and Schneider, which defines the data integrity measures of “contamination” and “suppression” (Clarkson & Schneider, 2010, 2014). In this paper, we extend these measures to a small imperative language, give this language a Markov chain semantics, and show how these measures of integrity can be calculated for programs with multiple trusted and untrusted inputs and outputs. We extend an existing quantitative information flow (QIF) tool, CH-IMP (Chothia, Kawamoto, Novakovic, & Parker, 2013), to use this semantics to automatically calculate these measures.
Clarkson and Schneider’s definitions are based on conditional mutual information and entropy. Existing QIF tools can calculate the mutual information between a system’s secret values and observable outputs; we investigate whether mutual information can be used to calculate conditional mutual information. We find that for secrecy, in which the public inputs of a system must be unrelated to the secret inputs, conditional mutual information can be calculated using mutual information (and therefore that existing QIF tools can calculate conditional mutual information-based definitions of secrecy by simply appending a program’s public inputs to its public outputs). However, for integrity, the trusted data is considered to be public, and so the untrusted data sent to a system may depend on it, so conditional mutual information must be calculated explicitly.
The semantics we present makes it possible to calculate the integrity between multiple trusted and untrusted inputs and outputs. In doing so, we pay particular attention to what data is recorded by the semantics, and thus the probability distributions used to calculate the integrity measures. These decisions define the attacker model: CH-IMP models an attacker that wishes to learn anything they can about the secret values (including, e.g., the order in which they occur) and can only observe certain outputs from the system. For integrity, we consider a model in which we are only concerned that data is correctly preserved as it flows between variables. Thus, because of the different attacker models, the calculation of quantitative integrity is not the dual of the calculation of quantitative secrecy.
We combine the integrity model with our previous work on secrecy (Chothia et al., 2013) to make a single framework in which both integrity and secrecy can be measured, and therefore their trade off analysed. We have implemented a tool in OCaml to carry out this analysis and illustrate it with a number of examples, including examples based on error correcting codes, the Dining Cryptographers protocol and the attempts by a number of banks to influence the Libor rate (BBC, 2012). Our tool takes in a program written in our language CH-IMP-IQ, builds the state space, and from this calculates the probability distribution over trusted, untrusted, secrecy and public variables, from which it calculates the measures of integrity and secrecy described below. We have used our tool to analyse programs with a state space as large as 222, which takes a few hours on a standard desktop machine.