How to use UL-SIFA?

Start the application by opening interface.jar.


Interface

The interface of UL-SIFA is rather simple. There are two tabs : Channels and Code. The Channels tab is where you can define the channels that you’ll use in the code (privateChannel and publicChannel are already defined by default). To remove one or more of the channels, select them and press the delete key.

 

 

 

Then in the Code tab, enter the code that you want to analyze on the left side and then press the button Analyze (or simply press Ctrl+Enter). The output of the analyzer 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, UL-SIFA will also generate and display the instrumented code on the right side.

 

 

 

Examples

Please note that the following examples can also be found in the folder examples of UL-SIFA.

 

Example 1 (rejected1.ulsifa)

x := 0;
if highValue then
   x := 1
end;
send x to publicChannel

This program won’t be accepted by UL-SIFA. The security level of x is High because of p (which is also High because it came from a private channel). 

 

Example 2 (rejected2.ulsifa)

if highValue > 5
   then c := publicChannel
   else c := privateChannel
end;
send lowValue to c

This program is rejected by UL-SIFA because there is a risk of implicit information flow. The final type of the variable c depends on the value of x (which is a High variable). For this reason, the channel c will be blocked if it is assigned the type public inside the if. This means that the program will be accepted only if nothing is sent on the channel c later on.

 

Example 3 (instrumented1.ulsifa)

if lowValue
   then c := publicChannel
   else c := privateChannel
end;
send highValue to c

This example is similar to the previous example except that the context in which c is defined is now Low instead of High. For this reason, it is not necessary to block the channel c. Also, because the channel c can either be a public or private channel (depending on the value of lowValue), it is marked as an unknown channel. This code will need to be instrumented to ensure that highValue is only sent to a private channel.

 

Example 4 (rejected3.ulsifa)

i := 0;
x1 := 0;
x2 := 0;
x3 := 0;
while i < 5 do
   send
x3 to publicChannel;
   x3 := x2;
   x2 := x1;
   x1 := highValue;
   i := i+1
end

This example illustrates the fact that UL-SIFA performs iterative analyses when necessary. In this case, only one iteration of the analysis on the while loop would not have detected the problem that occurs on the fourth iteration.

 

Example 5 (instrumented2.ulsifa)

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, the channel c could either be 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 the channel c is checked at runtime before sending x3 through a public channel.

 

The two following examples are also instrumented for similar reasons.

 

Example 6 (instrumented3.ulsifa)

receivec x from publicChannel;
if x > 0 then
   receiven c from publicChannel;
   send highValue to c
end

 

Example 7 (instrumented4.ulsifa)

receiven c from publicChannel;
receivec x from c;
i := 0;
while i < 50 do
   send x to publicChannel;
   receivec x from publicChannel;
   i := i + 2
end
 
  Recherche :
Imprimer cette page |  English