The tool uses a responsive design and can be used on any device with a modern browser. The tool has been developed and tested in Google Chrome v60. The online version of the tool has also been tested in Firefox v49, Opera v46, Safari v10, and Internet Explorer v11.
The core functionality is written in F# and then converted to JavaScript using Fable.
Developed by Kasper Laursen and Hanne Riis Nielson, based on the specification developed by Hanne Riis Nielson and Flemming Nielson.
This software is protected under the Simplified BSD License and the Intellectual Property Rights of the Technical University of Denmark.
Please report all bugs and suggestions to post@formalmethods.dk.
Explore how the memory changes, upon execution of the actions. Recall that if more guards are satisfied then it is non-deterministic which action to take.
When using the Show Trace feature, non-deterministic choices will be shown in the first column as , and if clicked the trace will be "reset" from that configuration.
When using the Show Resulting Configurations feature, all non-deterministic choices will be explored, until it reaches the number of steps, gets stuck or terminates. A short summary of the final configurations is found at the end. Warning If the input code is highly non-deterministic, and the number of steps is high, the tree of possible end-configurations will grow big (and therefore cause long execution).
For both outputs, all non-terminated and non-stuck configurations can be extended with 1-1000 steps.
Determine the shortest path fragments, and the proof obligations by providing a partial predicate assigment for the covering nodes of the graph.
It is then left to the user to verify that the partial assigment is correct.
Determine the sign of the variables and arrays in the specified program at each node in the generated program graph.
The analysis requires you to specify abstract values for all the variables and arrays in the program before it is possible to get a result.
Recall that an analysis function takes a set of abstract memories as input, it is therefore possible to initialize multiple different abstract memories for the variables and arrays (and remove them again if nessesary).
Explore the information flows in the specified program, according to a user defined security lattice and classification of variables and arrays.
Recall that the security analysis only works on a deterministic program graph, it is therefore nessesary that the Deterministic model is selected.
There are templates for the lattices known from the book, but it is also possible to specify a custom security lattice. The lattice must be a partialy ordered set shown in the right as , otherwise there will be shown an error as . When a correct lattice is specified, it is illustrated below as a Hasse diagram.
The analysis requires you to classify all the variables and arrays in the program before it is possible to get a result.
The result shows the difference between the set of actual information flows in the program and which information flows that are allowed by the specified security classification.