COAL Project: Tutorial

The COAL language enables specification of composite constant propagation problems. This tutorial shows how to use it in combination with the COAL solver to obtain the values of objects at interesting program points.

Before you get started, make sure that you download the COAL solver. See the installation page for instructions. Version 7 of a Java Runtime Environment is also needed. Finally, you need the COAL tutorial files. You can download a zip, tar.gz, or tar.bz2 archive. After extracting the archive, make coal-tutorial-0.1.7 your current directory.

In this tutorial, we will get the COAL solver to automatically determine the possibles values of object variables. More specifically, we will study how to write COAL specifications that allow the COAL solver to infer these values.

Running Example

Consider the following code:

public void sendMessage(boolean b) {
  Message message = new Message();
  Data data = new Data();
  if (b) {
    message.setTarget("Adversary");
    data.addString("Secret");
    message.setDataAndType(data, "Secret Type");
  } else {
    message.setTarget("Trusted Target");
    data.addInt(123);
    message.setData(data);
  }
  Messaging.send(message);
  Messaging.send(message, "Other Secret");
}

In this tutorial, we will be interested in inferring the possible values of the message variable. The Message and Data classes are defined as follows:

class Message {
  private String target;
  private Data data;
  private String dataType;

  public void setTarget(String target) {
    this.target = target;
  }

  public void setDataAndType(Data data, String type) {
    this.data = data;
    this.dataType = type;
  }

  public void setType(String type) {
    this.dataType = type;
    this.data = null;
  }

  public void setData(Data data) {
    this.data = data;
    this.dataType = null;
  }

  public String getTarget() {
    return this.target;
  }

  public Data getData() {
    return this.data;
  }
}

class Data {
  private Set<String> strings = new HashSet<>();
  private Set<Integer> integers = new HashSet<>();

  public void addString(String value) {
    string.add(value);
  }

  public void addInt(int value) {
    integers.add(value);
  }

  public Set<String> getStrings() {
    return this.strings;
  }

  public Set<Integer> getInts() {
    return this.integers;
  }
}

You can execute the program:

% java -cp coal-tutorial-main-0.1.7.jar:coal-tutorial-classpath-0.1.7.jar \
edu.psu.cse.siis.coal.tuto.TutorialMain
Sending Message:
  - target: Trusted Target
  - data type: null
  - data: strings: [] - integers: [123]
Sending Message:
  - target: Trusted Target
  - data type: null
  - data: strings: [] - integers: [123]
with parameter: Other Secret

As expected, two messages are sent, one with an accompanying parameter. Adding a command line argument causes Boolean b to be set to true in the code above. This cause a different set of messages to be sent:

% java -cp coal-tutorial-main-0.1.7.jar:coal-tutorial-classpath-0.1.7.jar \
edu.psu.cse.siis.coal.tuto.TutorialMain 3
Sending Message:
  - target: Adversary
  - data type: Secret Type
  - data: strings: [Secret] - integers: []
Sending Message:
  - target: Adversary
  - data type: Secret Type
  - data: strings: [Secret] - integers: []
with parameter: Other Secret

Our goal in this tutorial is to accurately infer all these possible message values using static analysis.

A First Attempt

We first create a COAL specification that takes into account the setTarget() method and only infers the value of the target field. Using your favorite text editor, create a file called message.model and add the following content.

class edu.psu.cse.siis.coal.tuto.Message {
  String target;

  mod <edu.psu.cse.siis.coal.tuto.Message: void setTarget(java.lang.String)> {
    0: replace target;
  }

  query <edu.psu.cse.siis.coal.tuto.Messaging: void 
         send(edu.psu.cse.siis.coal.tuto.Message)> {
    0: type edu.psu.cse.siis.coal.tuto.Message;
  }
}

Next, you will run the COAL solver with the following command in your terminal:

% java -jar coal-all-0.1.7.jar -model message.model -input \
coal-tutorial-main-0.1.7.jar -classpath coal-tutorial-classpath-0.1.7.jar
...
*****Result*****
edu.psu.cse.siis.coal.tuto.TutorialMain/void sendMessage(boolean) : staticinvoke 
<edu.psu.cse.siis.tuto.Messaging: void send(edu.psu.cse.siis.coal.tuto.Message)>(r1)
    0: Value: 2 path values
  target=[Adversary, ],
  target=[Trusted Target, ],

The result lists the two possible values of the target field.

Adding Support for Data Objects

In the result above, the data field is missing. To add support for it, create a new file data.model and add the following:

class edu.psu.cse.siis.coal.tuto.Data {
  Set<String> strings;
  Set<int> integers;

  mod <edu.psu.cse.siis.coal.tuto.Data: void addString(java.lang.String)> {
    0: add strings;
  }

  mod <edu.psu.cse.siis.coal.tuto.Data: void addInt(int)> {
    0: add integers;
  }
}

This specification models the Data class. In order to model the setDataAndType and setData methods, update the message.model with the following:

class edu.psu.cse.siis.coal.tuto.Message {
  String target;
  Set<String> strings;
  Set<int> integers;
  String dataType;

  mod <edu.psu.cse.siis.coal.tuto.Message: void setTarget(java.lang.String)> {
    0: replace target;
  }

  mod <edu.psu.cse.siis.coal.tuto.Message: void 
       setDataAndType(edu.psu.cse.siis.coal.tuto.Data,java.lang.String)> {
    0: replaceAll strings, type edu.psu.cse.siis.coal.tuto.Data:strings;
    0: replaceAll integers, type edu.psu.cse.siis.coal.tuto.Data:integers;
    1: replace dataType;
  }

  mod <edu.psu.cse.siis.coal.tuto.Message: void 
       setData(edu.psu.cse.siis.coal.tuto.Data)> {
    0: replaceAll strings, type edu.psu.cse.siis.coal.tuto.Data:strings;
    0: replaceAll integers, type edu.psu.cse.siis.coal.tuto.Data:integers;
    0: null dataType;
  }

  query <edu.psu.cse.siis.coal.tuto.Messaging: void 
         send(edu.psu.cse.siis.coal.tuto.Message)> {
    0: type edu.psu.cse.siis.coal.tuto.Message;
  }
}

Notice that we have added support for the dataType field in addition to the data fields. For the strings and integers fields, note the type annotation, which indicates which fields of the Data object should be copied to the fields of the Message object. Running the COAL solver with this new specification yields the following result:

% java -jar coal-all-0.1.7.jar -model message.model:data.model -input 
coal-tutorial-main-0.1.7.jar -classpath coal-tutorial-classpath-0.1.7.jar
...
*****Result*****
edu.psu.cse.siis.coal.tuto.TutorialMain/void sendMessage(boolean) : staticinvoke 
<edu.psu.cse.siis.tuto.Messaging: void send(edu.psu.cse.siis.coal.tuto.Message)>(r1)
    0: Value: 2 path values
  dataType=[Secret Type, ],strings=[Secret, ],target=[Adversary, ],
  integers=[123, ],target=[Trusted Target, ],

These are the two expected values of the message variable. Finally, we would like to infer the values of the last call to the send method. In order to do so, we must add a query to the message specification. This is shown below. Note that as part of the query, we specify the second argument to the method, which is a string of characters.

class edu.psu.cse.siis.coal.tuto.Message {
  String target;
  Set<String> strings;
  Set<int> integers;
  String dataType;

  mod <edu.psu.cse.siis.coal.tuto.Message: void setTarget(java.lang.String)> {
    0: replace target;
  }

  mod <edu.psu.cse.siis.coal.tuto.Message: void 
       setDataAndType(edu.psu.cse.siis.coal.tuto.Data,java.lang.String)> {
    0: replaceAll strings, type edu.psu.cse.siis.coal.tuto.Data:strings;
    0: replaceAll integers, type edu.psu.cse.siis.coal.tuto.Data:integers;
    1: replace dataType;
  }

  mod <edu.psu.cse.siis.coal.tuto.Message: void 
       setData(edu.psu.cse.siis.coal.tuto.Data)> {
    0: replaceAll strings, type edu.psu.cse.siis.coal.tuto.Data:strings;
    0: replaceAll integers, type edu.psu.cse.siis.coal.tuto.Data:integers;
    0: null dataType;
  }

  query <edu.psu.cse.siis.coal.tuto.Messaging: void 
         send(edu.psu.cse.siis.coal.tuto.Message)> {
    0: type edu.psu.cse.siis.coal.tuto.Message;
  }

  query <edu.psu.cse.siis.coal.tuto.Messaging: void 
         send(edu.psu.cse.siis.coal.tuto.Message,java.lang.String)> {
    0: type edu.psu.cse.siis.coal.tuto.Message;
    1: type String;
  }
}

You should now see the the following results:

% java -jar coal-all-0.1.7.jar -model message.model:data.model -input \
coal-tutorial-main-0.1.7.jar -classpath coal-tutorial-classpath-0.1.7.jar
...
*****Result*****
edu.psu.cse.siis.coal.tuto.TutorialMain/void sendMessage(boolean) : staticinvoke 
<edu.psu.cse.siis.tuto.Messaging: void send(edu.psu.cse.siis.coal.tuto.Message)>(r1)
    0: Value: 2 path values
  dataType=[Secret Type, ],strings=[Secret, ],target=[Adversary, ],
  integers=[123, ],target=[Trusted Target, ],

edu.psu.cse.siis.coal.tuto.TutorialMain/void sendMessage(boolean) : staticinvoke 
<edu.psu.cse.siis.tuto.Messaging: void send 
(edu.psu.cse.siis.coal.tuto.Message,java.lang.String)>(r1, "Other Secret")
    0: Value: 2 path values
  dataType=[Secret Type, ],strings=[Secret, ],target=[Adversary, ],
  integers=[123, ],target=[Trusted Target, ],
    1: [Other Secret]

Advanced Usage

This tutorial has shown the basic usage of the COAL language and solver. It is possible to implement more advanced analyses by supporting additional argument analyses (for example, beyond strings and integers). It is also possible to add support for different field operations. In order to do so, please refer to the Javadoc. Maven users can find COAL on the Central Repository with groupId edu.psu.cse.siis and artifactId coal.

Source Code

Instructions to download the source code for the tutorial are available on the source page.