NAME

soter - Safety checker fOr The ERlang language!

SYNOPSIS

soter [OPTIONS]... FILE

soter --stats module.erl
soter --dump --quiet module.erl

DESCRIPTION

Soter is a program analyser for Erlang modules. It extracts an abstract (approximate sound) model from the source-code of the Erlang module and tries to verify safety properties of it using a powerful model checking back-end (BFC).

The name Soter derives from the Ancient Greek name of the spirit of safety, preservation and deliverance from harm.

Please Note: in order for Soter to work properly you need to have BFC installed in you system and the bfc executable must be in your PATH.

Output meaning:

Soter normally goes through three phases:

Parsing of input Erlang module;
Extraction of the abstract model;
Verification of the properties (using BFC).

If phase 1 or 2 encounter errors, error messages get written to stderr and Soter terminates with exit code 1.

In phase 3, Soter will attempt to verify each of the specified properties in turn. The outcome of such attempts can be one of:

Safe. The program fulfills the property just checked. The exit code is 0.
Unsafe. The program could be safe but Soter could not come up with a proof. The exit code is 10.
Error. The call to BFC failed; this could be because of a bug, an unexpected output from BFC (must be version 1.0) or BFC aborted, maybe for lack of resources or by manual intervention. The exit code is 1.
Timeout. If timeouts are set and the analysis does not terminate within the time-limit then Soter will terminate with exit code 12; if one of the calls to BFC does not terminate within the time-limit then Soter will terminate with exit code 13.

OPTIONS

Input:

-f --fromcore: input is assumed to be in CoreErlang
--no-simpl: do not apply simplification of ACS
--peano: use a Peano encoding of positive integers (use with care)
-m --main=FUN-NAME: the name of the function representing the entry point of the program; it must be of arity 0. The default is `main'

Output:

-d --dump -odir=[DIR]: dump all intermediate results to the specified directory; if no directory is specified, soter will use (and create if non existing) a directory with the name of the module in the directory of the module. The dumped files are described in the Output files section.
-s --stats: show statistics
-v --verbose: Loud verbosity
-q --quiet: Quiet verbosity
--json: Reserved for future use

Verification:

-A --prove-all: attempt to prove absence of any error
-a --prove-assertions: attempt to prove absence of assertion violations
-e --prove-no-error: attempt to prove absence of `error' exceptions
-u --prove --uncoverable=PROP: tells Soter to prove the specified property. See soter(7) for syntax.
--prop[=FILE] --prove-file: tells Soter to prove every property specified in the .prop file. If no file is specified Soter will attempt to read a .prop file with the same basename of the input Erlang module. See soter(7) for syntax.
-D --val-depth=INT: specifies a depth for the data abstraction
-M --msg-depth=INT: specifies a depth for the message abstraction
--ct --cfa-timeout=INT: timeout for the CFA in seconds (no timeout if <= 0)
--bt --bfc-timeout=INT: timeout for the BFC verification in seconds (no timeout if <= 0)

Help:

-? --help: Display help message
-V --version: Print version information

ERLANG INPUT MODULE

The Erlang module supplied as input should follow these guidelines:

the filename should match the name of the module in -module(modname).
always write a main() function which acts as entry point. Entry points with free variables are not supported but can be simulated via non-deterministic choice (see soter(7))
do not use functions from other modules, nor import modules: the module system is not currently supported by Soter.

Refer to soter(7) for a detailed description of the current restriction on the Erlang programs accepted by Soter.

A tipical Erlang module that can be analysed by Soter looks like the following:

-module(example).
-compile(export_all).

-include_lib("soter.hrl").
-include_lib("grammars.hrl").

-uncoverable("wrong_incipit > 0").

main() ->
    N = ?any_nat(),
    P = spawn(fun()-> f(N) end),
    P ! {hi, self()} ,
    receive
        X -> X
    end.

f(N) ->
    receive
        {hi, P} ->
            P ! {hey, N}
            start_protocol(N, P);
        bla ->
            ?label(wrong_incipit),
            complain(N)
    end.

...

See soter(7) for the full details.

OUTPUT FILES

Suppose FILE = examples/myfile.erl then after running soter on it you will find a new subdirectory of examples/ called myfile containing the following files:

myfile.core: This is the Core Erlang version of myfile.erl myfile.ir; This is the Intermediate Representation of the program myfile.cfa; This is the full content of the output of the CFA myfile.dot; This file (meant to be used with acsview.py) is a Graphviz file showing the generated ACS in graphical form myfile.bfc; The ACS model translated into the BFC input format. The ids of the local states coincide with the ones displayed in the nodes of the ACS in the dot file myfile.simpl.*; These files correspond to translations of the ACS after simplification myfile.stats; This contains a summary of the performance myfile.results; This contains the results of the verification of each property.

BUGS

Limitations

Soter deals with a `pure' core fragment of the Erlang language. See soter(7) for details.

Reporting Bugs

Email bug reports to

Emanuele D'Osualdo emanuele.dosualdo@gmail.com

Known Bugs

Soter can be very slow for big inputs. Use with care.

SOTER 0.1 | Command-line tool

Emanuele D'Osualdo

Jonathan Kochems

Luke Ong