Performs secure information-flow analyses on programs written in a simple imperative language to ensure that no sensitive information is inadvertently leaked. When necessary, it also produces an instrumented version of the code to do additional checks at runtime.
It uses a three-valued type system to statically check non-interference. In addition to the usual two main security levels, public (or Low) and private (or High), a third security level, Unknown, is introduced to capture the possibility that we may not know whether the information is public or private statically. Standard two-valued analysis has no choice but to be pessimistic with uncertainty and hence lead to false positives. If uncertainty arises during the analysis, the instruction in cause is tagged; in a second step, instrumentation at every such point together with dynamic analysis will result in a more precise analysis than purely static approaches. This reduces the number of false positives, and introduces a light runtime overhead by instrumenting only when there is a need for it.
The interface (interface.jar) is rather simple. There are two tabs: Channels and Code. The Channels tab is where you can define the communication channels that you want to use in your code (privateChannel and publicChannel are already defined by default). To remove one or more channels, select them and press the delete key.
The Code tab allows you to enter the code of the program that you want to analyze. To analyze the code, press the Analyze button or press Ctrl+Enter. The output of the analysis is then shown on the right side of the application. If the analyzer has detected an error, whether it is a lexical, syntactic, semantic or information flow error, a message explaining the error (when possible) will be found at the end of the analyzer's output. If the code requires an instrumentation in order to be secure, then an instrumented version of the program will be generated an displayed on the right side.
x := 0;
if highValue then
x := 1
end;
send x to publicChannel
if highValue > 42 then
c := publicChannel
else
c := privateChannel
end;
send lowValue to c
if lowValue then
c := publicChannel
else
c := privateChannel
end;
send highValue to c
i := 0;
x1 := 0;
x2 := 0;
x3 := 0;
while i < 42 do
send x3 to publicChannel;
x3 := x2;
x2 := x1;
x1 := highValue;
i := i + 1
end
This example illustrates the fact that we perform an iterative analysis when necessary. In this case, analyzing only the first iteration of the while loop would not have revealed the problem that occurs on the fourth iteration.
receiven c from publicChannel;
receivec x1 from c;
x2 := 3;
receivec x3 from c;
if x1 > 2 then
if x2 = 3 then
send x3 to publicChannel
end
end
In this example, then channel c could be either private or public. This means that the security level of x3 is U (unknown). Instead of simply rejecting this code, we instrument it so that the type of channel c is checked at runtime before sending x3 through a public channel.