TLSAT

TOC

TL SAT is a static analysis tool based on ideas from dataflow analysis and abstract interpretation which allows for checking various security properties related to the use of critical APIs, resource use etc. In the scope of Mobius, the tool has been extended to manage simple information flow policies. In the following, we describe this last feature.

Explanation

The tool guarantees the absence of explicite information flow, in other words information flow resulting from conditional branching is not considered. In particular, invocation of critical API methods which may potentially reveal sensible data and which access explicitely such data are detected. This is based on a dataflow analysis which infers an overapproximation for the local variables, the heap and the method arguments and return values. This overapproximation is then interpreted by the information flow checker.

Milestones and Tickets

Source Code

Example

WikiInclude(TypecheckerNameExample)

Example 1. Suppose that we have an API for mobile phone applications which contains the following API methods:

getPhoneBook, which returns a data structure representing a mapping of the names to the respective phone numbers
sendToNet(String s) which sends to the network its string argument.

A mobile phone application which contains for instance the following fragment will be rejected:

... PhoneBook phoneBook = getPhoneAddressBook();//get the phone book data

String strPhoneBook = phoneBook.toString();//convert the phone book data structure to String

sendToNet(strPhoneBook);//send the information on the network ...

Example 2.

The following example illustrates the limitations of the tool related to the fact that implicite information flow are not taken into account. If we keep the same API as in the previous example the following code which potentially reveals sensitive information to an attacker will not be rejected:

...

PhoneBook phoneBook = getPhoneAddressBook();//get the phone book data

int i = 0;

while(i < phoneBook.length) {

if (phoneBook.element(i).getPhoneNumber.getFirstDigit() == 0) {
  send("0"); 
} else if (phoneBook.element(i).getPhoneNumber.getFirstDigit() == 1) {
  send("1"); 
} ...  else (phoneBook.element(i).getPhoneNumber.getFirstDigit() == 9) {
  send("9"); 
}    

...

if (phoneBook.element(i).getPhoneNumber.getTenthDigit() == 0) {
  send("0"); 
} else if (phoneBook.element(i).getPhoneNumber.getTenthDigit() == 1) {
  send("1"); 
} ... else (phoneBook.element(i).getPhoneNumber.getTenthDigit() == 9) {
  send("9"); 
}

} ...

Taking into account such implicite information leaks should be implemented in the future versions of the tool.