Vera Tutorial

In the following tutorial we explain how to use the Vera tool. As a running example we use a lesson of WebGoat.

Prerequisite

Expected results

  • Create a low-level attacker model for a SQL Injection and
  • tests the WebGoat’s “String SQL Injection” lesson.

Resources required

Tutorial steps

 

    1. Creating a project: The first time a user open the Vera tool Eclipse plugin, he has to create a new project and name it. The project we are crating (e.g., “siemens_test”) will contain all test to be performed on the AUT.
      vera
      In order to divide the test inside the project the security analyst can create a new folder (e.g., “SQL-Inj”) in which he can store all the file needed for the execution of the tests.
      vera
      At this point the security analyst has to create the three files needed for the execution of the Vera tool (another possibility is to copy the files from a previous test, but the very first execution of the tool require the creation of the single files):

      • “SQL_injection.scm” containing the attacker model (remember to add the extension),
      • “Configuration File” (containing the configuration values), and
      • “Instantiation Library” (containing the payloads).

 

    1. Creating the attacker model: The attacker model we use in this lesson is simple injection-model which tries to submit the given payloads in every field of the page. The model has to be created trough the graphical interface (an example of graph is shown below) according to the attacker model (see Deliverable 2.4.1 and Deliverable 3.3 for more information on the “Definition of Attacker Behavior Models”) presented in the following:vera

 

    1. Defining the configuration values: After the definition of the correct attacker model and the payloads to use, we have to define the values needed in order to perform the test on the AUT (even if the data saved in this file are intuitive, a full description can be found in Deliverable 3.3). The URL of the WebGoat lesson that we have to save in the configuration file is:
      • URL="http://127.0.0.1:8080/WebGoat/attack?Screen=36&menu=1100"

      The WebGoat’s menu “Show Cookies” displays the following:veraso we can save this information in the configuration file along with the remaining information needed for the correct execution of the test:

        • Cookie="JSESSIONID=FE57429A5098D823256B527B2A77C2E2"
        • Header={"Basic": "Z3Vlc3Q6Z3Vlc3Q="}
      • Domain="http://127.0.0.1:8080/WebGoat/"

      The Configuration File will look like this:vera

 

    1. Defining the instantiation library: The instantiation library contains the payloads to be used during the test; the one used in the tutorial has to be like this:veraThe preparation phase of the test is thus completed and we are ready to execute the test.

 

    1. Executing the test: In order to execute the test, the security analyst has to interact with the Vera tool menu:
      vera
      In the following we explain the actions (i.e., the functionalities of the menu) that the user has to perform in order to launch a test:

      • Load Model: This item loads the three configuration files saved in the state chart diagram (e.g. “SQL_injection.scm”) into the system. If the information about the model, the configuration file and the instantiation library have not been previously saved this command has to be omitted.
      • Generate XML: Generates an XML file from the state chart diagram “Injection.scd”. A file “SQL_injection”-XML is created in the folder containing “SQL_injection.scd”, and the absolute path of the file is saved in the state chart diagram “SQL_injection.scd”. The user has to generate the XML file after the creation of the low-level attacker model.
      • Read Instantiation: This item reads the instantiation library used by the VERA-tool engine.
      • Load Configuration: This item loads the Configuration file used by the VERA-tool.
      • The configuration is loaded in two steps:

        • the user chooses the file,
        • the user is asked if he wants to modify the file contents or continue without any changes in the selected file.

        We introduce the possibility to change the configuration file in the case that a user wants to use the same parameters from a previous test with some changes (e.g. with a different cookie). A file “SQL_injection-ConfigurationFile” is created in the folder containing “SQL_injection.scd”.

      • Summing up before the test, the resulting eclipse folders will look like this:
        vera
      • Execute VERA: This item performs the actual call to the VERA-tool test execution engine. The tool will automatically check how many instantiation files are passed as parameters, and will launch an execution for each file. After the execution the output of the VERA-tool test engine is saved in files named “SQL_injection-VeraOutput-0.txt”.

 

  1. Review the output: After launching the “Execute VERA” command we can open the lesson page and we can see that the it has been successfully completed:
    vera
    Also the “SQL_injection-VeraOutput-0.txt” file reports the successful attack:

    • Vulnerability found:
    • attack?Screen=36&menu=1100 - Smith' or '1'='1