Fred Tutorial

This tutorial explains how to use the Fred component within the SPaCIoS Tool. In particular, we give an example of using the Fred tool to obtain and execute a test case for the SAML SSO case-study.

Prerequisite

  • The SPaCIoS Tool is correctly installed.
  • (Optional) An ASLan (or ASLan++) specification with a goal specified in LTL.

Expected results

  • A certain number of abstract test cases.
  • Concretization and execution of test cases if a Test Execution Engine is available for the model.

Tutorial steps
The optional steps in the following tutorial can only be performed in case that an ASLan++ model is available. We strongly encourage instrumenting the model (steps 1. and 4.) and forcing translation with the -ltl option (step 2.) whenever an ASLan++ model is available.

 

    1. (Optional) Instrumenting the ASLan++ model with signals.
      The purpose of instrumentation is to achieve better model coverage. This is achieved by adding a new fact signal_ltl to the model after the statement we wish to cover. One example of such instrumentation is shown in the following figures:fred
      fred

 

    1. (Optional) Translating the ASLan++ model to ASLan.
      The default translation from ASLan++ to ASLan that is done automatically in the SPaCIoS Tool does not always produce LTL goals. To force a translation with LTL goals, we run the translation with the -ltl option as shown in the following figure:fred

 

    1. Using Fred on the target ASLan specification.
      An expert user is encouraged to examine the ASLan specification and possibly improve the goal by removing model-specific optimizations that may reduce the usefulness of the separation procedure. This in particular relates to reverting any simplifications in the goal that do not result in an equivalent formula. We illustrate by this step in the following figures:fred
      fredHere, the goal was simplified due to the fact that witness and dishonest arepersistent facts. This means that in this model witness and O(witness)are equivalent, but since this is not the case in general, we reintroduce the temporal operator O (standing for once).
      Now we run the Fred tool on the target ASLan specification. The Fred tool generates a number of new ASLan models in the folder of the target specification.

 

    1. (Optional) Modifying the goal of Fred outputs to contain the signal.
      If the user has instrumented the ASLan++ model, for this to have an effect, it is necessary to modify the goal of the models generated by Fred.
      Take any ASLan model, generated by Fred. The LTL goal of the model is invariably of the form G(formula), where formula is an LTL formula. The modification step consists of simply replacing the goal G(formula) with the goal G(or(formula, not(O(signal_ltl)))). The modification ensures that the signal will be present in the abstract test case that SATMC generates.

 

    1. Model checking using SATMC.
      Simply use SATMC on the ASLan model from the previous step. For details refer to the SATMC tutorial in this deliverable. The output of SATMC is an abstract test case for the system under test.

 

  1. Concretizing and executing the abstract test case.
    To concretize and execute the abstract test case, we use the IBT component of the SPaCIoS Tool. See here for a detailed tutorial on IBT. Below, we give a step-by-step description of IBT’s use to models generated using Fred.
    Click on “File”, “Import”, “General”, “Existing Project into Workspace” and locate the folders containing the necessary files. We copy the ASLan model from the previous step and the output of the SAMTC model checker to the appropriate folder. Be advised that copying the ASLan++ model to this folder will cause the \Tool{} to automatically translate it into ASLan and potentially overwrite your modified ASLan model (if the models share the same file name).
    Finally, select the abstract trace, click on “Run”, “Run Configurations…”, choose the appropriate IUT, specify the version of SATMC for generating the attacker rules or choose an attacker file, and click on “Run” to execute. If prompted by the \Tool{}, select the ASLan model that was used to generate the trace. This is illustrated in the figures below:

    fred

    fred