Accountable Noninterference

In the context of preventing information leaks in programs, we may agree that the following code is "bad:"

{H}int x;
{L}int y;
if (x) y = 0; else y = 1;

We may reject this code because to do otherwise would allow a "covert channel" in the control flow. We may take a less doctronaire approach and say that fundamentally we are primarily concerned with preventing data flows that violate security restrictions. We wish to propagate such restrictions through sequential transformations on data, such as marshalling and unmarshalling. Therefore we want to disallow code such as the above that violates this checking of confidentiality levels on data flows, propagated through sequential transformations. "Noninterference" is the classic result that assures us that there are no such indirect information flow leaks.

What about the following code:

{H}int x;
{L}int y;
if (x) send(c1); else send(c2);		/* T1 */
receive(c1) -> y = 0;				/* T2 */
receive(c2) -> y = 1;				/* T3 */

The idea here is that we have three threads. The thread T1 executes at a "high" level, and sends a message on either channel c1 or c2, depending on the level of the high variable x. The "low" threads T2 and T3 block, and one is unblocked by T1 and sets the low variable y to the value of the high variable x. Should we try to prevent this form of information leak?

While the language theorist will say, Of course, the system builder may be more skeptical. In a local area network, there is some hope that we can prevent T1 sending messages to public channels read by T2 and T3. However it is not clear how we can prevent these kinds of information leaks over the Internet, where in general we cannot prevent attacks such as traffic analysis (or at least, not without unacceptable cost). The point of this example is that security is fundamentally about economics: what compromise are we willing to make, between the level of security we desire and the price we are willing to pay for that security?

The idea of accountable noninterference is to specify the information flows that we are willing to regulate, and verify noninterference for just those information flows. These information flows are specified as part of an operational semantics. We then have two flow relations:

The information flows that exist in the system.
The information flows that are regulated by the security system.

Accountable noninterference then verifies that there is no accountable information flow from high to low.

More formally, we focus on the observable events or actions in the operational description of a concurrent or distributed system. We assume that the system semantics is expressed as a labeled transition system (LTS)

K1 ->Aa K2

where K1 and K2 are the semantic contexts before and after the computation step, respectively. The label a is the event or action offered to the environment, and the annotation A is further information about the observation that may be used for example for dependency checking.

Causality A1 =>caus A2 must be a relation that satisfies:

Suppose K1 ->A1a1 K2 and K2 ->A2a2 K3 and it is not the cause that A1 =>caus A2 or A2 =>caus A1, so (the events are concurrent). Then there is some K2’ such that K1 ->A1'a1 K2' and K2' ->A2'a2 K3. In other words, the aspect of causality that we are principally interested in is that we can permute the observations of concurrent events.

Accountability A1 =>acc A2 can be any relation that is a subset of causality.

For example, we can define an operational semantics for a concurrent system where causality and accountability are identified, and we choose to enforce all information flows:

Global Causality

As another example, we can define a system where only sequential flows are considered accountable. This corresponds to the motivation we described at the beginning: rather than trying to prevent covert channels through indirect effects in language semantics, we focus on enforcing constraints on data flows, and this extends to indirect effects through sequential control flow because we wish to propagate these restrictions through data transformations, for example, in marshalling and unmarshalling.

Local Causality

The final example is a hybrid system, where we assume that there are parts of the network where we can enforce information flow restrictions, including indirect control flows. But over the internet, we do not have resources to enforce these restrictions, so in this hybrid system we only track accountable information flows through local communication.

Hybrid accountability

Accountable noninterference offers a framework for considering both policy and mechanism. Policy refers to the end-to-end security properties of shared data, while mechanism refers to how these security properties are enforced. Decoupling policy and mechanism allows us to reason explicitly about the trade-offs that have to be made in enforcing security in network and distributed applications.