WebGoat Tutorial

This tutorial shows how to produce a test for the {\em Role Based Access Control} Lesson of the WebGoat case study.

Involved Components

  • jModex For model inference.
  • SPaCiTE For test execution.
  • SIMPA For model inference (optional).


  • The SPaCIoS Tool is correctly installed.
  • Eclipse Juno – Java EE IDE for Web Developers.
  • WebGoat up and running (for optional steps).

Expected results

  • Executing a test that exhibits the vulnerability

Tutorial Steps

    1. Get WebGoat sources Download the file WebGoat.zip. It contains the WebGoat system as an Eclipse project with some modifications.
    1. Import WebGoat in the workspace Open the File -> Import menu. Then choose the Existing Project Into Workspace alternative and Select Archive File(see the figure below) Note: Make sure that the project is configured to be compiled using a Java 1.6 compiler (project properties).spacitejmodex
    1. Configure jModex Right-click on the freshly imported project, select the Properties menu, and go to the SPaCIoS -> jModex page:spacitejmodex
      Here i) Select Use Predefined Webgoat Specifier and the Predefined Java SQL Specifier and ii) set the path to the file containing the structure of the required part of the WebGoat database (the file can be downloaded from this link).
    1. Invoke jModex Right-click on the WebGoat project and select the SPaCIoS -> jModex -> Infer Aslan++ Model menu. After the initiated job is done, the extracted Aslan++ model should be found in a file having the same name as the project and that is located in the root of the analyzed project (these are the default location and name of the output file).
    2. Initialize the model Next, we must initialize the model (e.g., specify the database content). Consequently, you must manually add the lines 22-24, 86-89 and 190-194 from the following model into the generated model:
      Additionally, you must perform the changes from line 80 as mentioned in Section 7.2.2 of Deliverable 5.5.
    1. (Optional step – Available component) Using SIMPA to infer a WebGoat model. An alternative way to obtain a suitable model for the WebGoat case study is to infer it from the running system. Then, follow the procedure described inSIMPA Tutorial to apply the SIMPA inference tool.
    1. Open the model in the editor area. In order to model check the generated model, open the model in a new editor tab as shown in:spacitejmodex
    1. Setting the model checker options. Model checking is performed with Cl-Atse. To set the proper options click on SPaCIoS -> SPaCiTE -> Show the Preferences Page and set the Cl-Atse Option field to --short, as shown in:spacitejmodex
    1. Invoking the model checker. After setting the options we call Cl-Atse to model check the generated model. We execute SPaCIoS -> SPaCiTE -> Formal Modeling -> Model Check Secure Model as in:spacitejmodex
      and select Cl-Atse as in:spacitejmodex
      After a couple of seconds, Cl-Atse reports a vulnerability in the model:spacitejmodex
    1. Abstract attack trace final editing. Opens the generated abstract attack tracespacitejmodex
      and add the following line:

      Actor(66) *->*   : confirmation

      at the end of the Messages block. Rename the agent i to intruder in all messages.

    1. Define the WAAL mapping. Click on the menu Define WAAL Mapping, as shown in the following:spacitejmodex
      Then, input the following mapping:

      	Agent: intruder 
      		httpBasicAuthentication_Username: "guest"
                      httpBasicAuthentication_Password: "guest"
      MAPPINGS {
      		abstract: "rint2string(i105)" concrete: "\"regexp:Tom.*\""
        // Each simulated agent goes to the home page
           'ga_goToURL($1, "http://webgoat:8080/WebGoat-5.4/attack")
           ga_clickButton($1, ByText("Start WebGoat"))
           ga_clickLink($1, ByText("Access Control Flaws"))
           ga_clickLink($1, ByText("Stage 1: Bypass Business Layer Access Control"))
           a_clickLink($1, ByText("Restart this Lesson"))'
        // login
           'ga_selectItems($1, ByName("employee_id"), {employeeName($3)})
            ga_inputText($1, ByName("pass\`\'word"), $4)
            ga_clickButton($1, ByText("Login"))'
          'ga_selectItems($1, ByName("employee_id"), {employeeName($3)})
           ga_clickButton($1, ByText("DeleteProfile"))'
        // confirmation
           'va_HTMLPage($1, ByText("You have completed Stage 1"))'
    1. Instantiate the AAT. Click now on Instantiate Single Abstract Attack Trace so that the executable test case is generated:spacitejmodex
      SPaCiTE will ask now which WAALMapping file to use for the mapping:
      Select the file created in the previous step. The result of this step is a compiled Java file that is the executable test case, as shown in:
    1. Start the execution environment. Click on Start controlproxies to set up the execution environment.
    1. Launch the TEE. Click on Execute TEE to launch SPaCiTE test execution engine:
    2. Run the test case. Click on the Start button and select the generated test case, as shown in:
    1. Provide user input. After the correct profile is selected, SPaCiTE will need the help of the security analyst because the DeleteProfile button is not present in the browser. SPaCiTE asks the security analyst to provide either a value or an HTTP message. Click on the latter one:
    1. Select the next step. In a popup window SPaCiTE informs the security analyst about the next steps. Click on the option Intercept Requests in WebScarab, as shown in the following:
      Then, move back to SPaCiTE and click Ok on the popup window:
    1. Set the DeleteProfile action. The following figure shows a list of sample requests that SPaCiTE could generate:
      We see that in order to logout, the action is called Logout, to search staff, the action is called SearchStaff, and to view a profile, the action is calledViewProfile, (blue rectangle in the figure).
      From that we assume that in order to delete a profile, the action is calledDeleteProfile. We set the action DeleteProfile as shown in the above figure, click on the button Accept Changes and finally click on the buttonContinue as shown in the following figure:
  1. Successful termination. SPaCiTE now confirms that the profile was successfully deleted as in: /jmodexspacite/verdict.png This means that the attack trace found by model checking the extracted model has been successfully replicated on the real system.