School of Computer Science

Getting Started

First, download and extract the SCH-IMP release tarball for your platform (or compile SCH-IMP yourself if one isn't available).

# From a release tarball:
cd schimp

# From source:
cd schimp/dist

Example SCH-IMP programs and function models can be found in the examples/ directory in both release tarballs and the source code repository.

Running SCH-IMP

To run the SCH-IMP tool, you'll need Java 8 or newer.

SCH-IMP uses the PRISM model checker, which has its own native-code libraries that need to be loaded when it launches:

# On Windows (assuming Command Prompt):
set path=%cd%;%path%

# On Linux (assuming bash shell):

# On macOS:

The tool is now ready to run — e.g. to analyse the DC-net example:

# From a release tarball:
java -jar schimp.jar -f examples/dc-net/dc-net.prob-large-fnmodel examples/dc-net/dc-net.schimp

# From source:
java -jar schimp.jar -f ../examples/dc-net/dc-net.prob-large-fnmodel ../examples/dc-net/dc-net.schimp

On macOS, replace java with the full path to the Java executable (which can usually be located with the help of /usr/libexec/java_home).

Command-line usage

The tool is invoked as follows:

java -jar schimp.jar [OPTION].. [PROGRAM_FILE]

where [PROGRAM_FILE] is a file containing a SCH-IMP program (typically with the extension .schimp).

After executing the SCH-IMP program, the tool identifies the attacker's optimal strategies for compromising the values of the initial variables based on the information available to them (including the program's outputs and its time and power consumption). Finally, it outputs the probability of the worst-case attack succeeding.

The following options are supported:

  • -I [VAR]..: only consider the subset of initial variables given by the comma-delimited list of [VAR]s to be secret; the others will be treated as if they had been declared with the new keyword.
  • -f [FNMODEL_FILE]: load the resource function from the file [FNMODEL_FILE] (typically with the extension .fnmodel); the default is not to use a resource function (i.e., the tool assumes that there is no time or power cost involved in executing any of the program's functions).
  • -g [RESOLUTION]: set the grid resolution used by PRISM's POMDP solver; the default is 8. Setting this too low may give unacceptably large bounds on SCH-IMP's final result; setting it too high may cause SCH-IMP not to terminate.
  • -d [PREFIX]: output the DTMC model of the program's execution to [PREFIX] and the POMDP model of the attacker to [PREFIX], both in DOT format; if [PREFIX] is not given, [PROGRAM_FILE] is used.
  • -a: when used with -d, show all deterministic transitions in the DTMC model of the program's execution, which may be helpful for debugging. This will significantly increase the number of states in the DTMC in most cases, and may cause SCH-IMP not to terminate.
  • -o: when used with -d, include the list of observations in each state in the generated DOT files; the default is to include an internal "observations ID" that is unique for each set of observations, which is fast to insert into the DOT file but isn't very helpful for debugging. This option will slow down generation of the DOT files.