SPaCiTE Tutorial

In the following we provide a tutorial to demonstrate how to use SPaCiTE as part of the SPaCIoS Tool. To follow this tutorial, make sure that you use version 1.0 of SPaCiTE.

Prerequisite

  • The SPaCIoS Tool is correctly installed.
  • A SPaCIoS project is present in the workspace.
  • The project contains the ASLan++ specification file. How to create a specification file is described in Deliverable 4.3.

Expected results

  • Verdicts whether generated test cases could be successfully executed on the SUV.

Tutorial steps
For illustration purposes we take WebGoat lessons. The lesson implements an application called “Goat Hills Financial Human Resources” and allows to view, edit, and delete employee profiles. By meeting the prerequisites for this tutorial, a model of this application is available in the SPaCIoS project and describes at a high level which actions a web user can perform on which web page. For this tutorial we assume that the security analyst studied the modeling guidelines Deliverable 3.2 and already developed this model.

Since SPaCiTE applies semantic mutation operators to that model, the security analyst first has to annotate the model. The necessary steps are given below. The following code segment are all part of the server component.

 

    1. Naming Conventions
      • Message Handler A server component must react upon receiving a message m. The corresponding part of the model that describes the behavior of the server components is called the “message handler” for message m.
      • Executing a message handler A model checker considers paths of the models and verifies security properties. Such a path is specified by a sequence of statements in the model. Executing a message handler means that the model checker verifies the security properties for each of the statements given by the message handler.

 

    1. Annotating the secure model
      • The message handler for message login sends the messagelistStaff(Us) back to the client. The semantic of this message is that the information will be rendered in the browser at the client side. Because this is a message between the web application and the client side browser, and the browser will display the result, annotate this message using theWTsendToClient annotation:
        %@CONTEXTXSSBLOCKStart
        %@type: WTsendToClient
        %@{
        	Actor *->* Us : listStaff(Us);
        %@}
        %@CONTEXTXSSBLOCKEnd
      • The message handler for viewProfile is combined with 5 conditions that all have to be true before the server component executes the message handler. Only 2 out of these 5 conditions are security testing relevant because conditions can also be used to guide the model checker. The first security relevant condition (line 132) expresses that the client has to be authenticated. Provide this semantics to SPaCiTE by annotating line 132 with the WTpermissionCheck annotation:
        %@SEMANTICSStart
        %@type: WTpermissionCheck
        %@{
        	authenticated(Us)
        %@}
        %@SEMANTICSEn

        The second condition (line 133) expresses a permission check whether the current client is authorized to view the requested profile. We assume that his authorization check is implemented using an SQL query. Provide this knowledge to SPaCiTE by annotating line 133 withWTpermissionCheck and WTSQLConditionQuery:

        %@SEMANTICSStart
        %@type: WTpermissionCheck, WTSQLConditionQuery
        %@{
        	Us->canView(?A)
        %@}
        %@SEMANTICSEnd
      • Line 138 introduces a new fact called viewedByWith. This statement has several purposes. It is used to notify the model checker that the server executes the viewProfile message handler and that the server therefore reads the requested profile from the database. Such a SQL read query can either operate on sanitized user input or the user input is not correctly sanitized. Since the model is secure you must tell SPaCiTE how it can be specified that the SQL query is non-sanitizing. You do so by adding the following annotation:
        %@NONSANITIZINGFUNCTIONStart
        %@type: WTnonSanitizingViewingFunction
        %@{
        %@%nonSanitizingViewingAction(viewProfileAction);
        %@}
        %@NONSANITIZINGFUNCTIONEnd

        Now annotate the viewedByWith statement (line 138) as an SQL read query:

        %@SEMANTICSStart
        %@type: WTSQLReadQuery
        %@{
        	viewedByWith(profile(A), Us, viewProfileAction);
        %@}
        %@SEMANTICSEnd

        The binding of this annotation to the viewedByWith fact is established by using the same constant viewProfileAction. Finally the message handler sends back the profile and gets displayed in the browser in line 140. Annotate that line using the WTsendToClient annotation:

        %@CONTEXTXSSBLOCKStart
        %@type: WTsendToClient
        %@{
        % get the profile of A
        	Actor *->* Us : profile(A);
        %@}
        %@CONTEXTXSSBLOCKEnd
      • In line 149 we have the same authentication condition again as in line 132. Therefore annotate line 149 exactly in the same way as line 132.
      • In line 150 we have a condition that checks if the current user is authorized to edit the specified profile. In addition we assume that this authorization check is implemented as an SQL query. This semantics of the factcanEdit has to be given to SPaCiTE. Annotate line 150 in exact the same way as you did in line 133.
      • When the message handler for the message editProf is executed, the server component edits the profile by storing the values in the database. Annotate line 153 with WTSQLWriteQuery, to tell SPaCiTE that the web application writes data via an SQL query:
        %@SEMANTICSStart
        %@type: WTSQLWriteQuery
        %@{
        	editedByWith(profile(A), Data, Us, editProfileAction);
        %@}
        %@SEMANTICSEnd

        Similar to line 138 you have to tell SPaCiTE how to mark the editing action as not properly sanitizing. Therefore add the following code just before line 153:

        %@NONSANITIZINGFUNCTIONStart
        %@type: WTnonSanitizingEditingFunction
        %@{
        %@% nonSanitizingEditingAction(editProfileAction);
           if( flow_1_text(Data) ) { storedXSS_vulnerability; }
        %@}
        %@NONSANITIZINGFUNCTIONEnd
      • Finally, the server sends back the modified profile to the browser that renders the modified profile. Annotate line 155 in the same way as you did for line 140.
      • Similar things needs to be repeated for the deleteProf message handler. Annotate line 170 as you did for line 149, line 171 as you did for line 150, line 175 as you did for line 126, and finally annotate line 177:
        %@NONSANITIZINGFUNCTIONStart
        %@type: WTnonSanitizingDeletingFunction
        %@{
        %@% nonSanitizingDeletingAction(deleteProfileAction);
        %@}
        %@NONSANITIZINGFUNCTIONEnd
      • The last 2 annotations have to be done for line 197 and line 206-212. Line 197 tells the model checker how to mark a pre-existing artifact as malicious. Provide this semantics to SPaCiTE by annotating that line:
        %@MALICIOUSARTIFACTStart
        %@type: WTmaliciousArtifact
        %@{
        %@% maliciousProfile(profile(tom));
        %@}
        %@CONTEXTXSSBLOCKEnd

        Line 206-212 are used to configure the role based access control system. To allow SPaCiTE to test for different configurations, annotate line 206-212:

        %@SEMANTICSStart
        %@type: WTconfigurationPermissionCheck
        %@{
          tom->canEditExpl(tom);
          jerry->canViewExpl(tom);
          ...
          jerry->canDeleteExpl(jerry);
        %@}
        %@SEMANTICSEnd

 

    1. Configuration of SPaCiTE
      Before we can use SPaCiTE for the first time we have to configure it according to:Configure your own installation of SPaCiTE so that every field of the Preference Panel references the same object as shown in the previous figure. In particular, specify in the section Control Proxies how a simulated agent can communicate with the TEE. When you click on the button New... 4 different values have to be provided: (1) name of the configuration, (2) port of the control proxy, (3) port of the selenium server, and (4) port of WebScarab.

 

    1. Verify that the provided model is secure
      Before we can start generating mutated versions of the provided model, you have to verify whether the provided ASLan++ model is indeed secure. For this step, add the model to a SPaCIoS project either by storing the file in the project itself or by linking it to the project. To start the verification process, open the model and invoke the following command: SPaCIoS > SPaCiTE > Formal Modeling > Model Check secure Model as shown in the following figure:spacite
      Whenever a time consuming task is executed by SPaCiTE a progress monitor will be displayed as shown in the following:spacite
      For the case that the initial model is not secure, it has to be improved by the security analyst. Once the model is secure, SPaCiTE will show the following report, as shown in the following:spacite

 

    1. Inject vulnerabilities into the secure model
      The previous figure shows that the used model is indeed secure and can be used as a valid input for SPaCiTE. Therefore we can continue with injecting vulnerabilities into the secure models. We do that by applying all appropriate mutation operators. Therefore we first make sure that the secure model is opened and displayed in the active tab in SPaCiTE. Then, applying semantic mutation operators to an ASLan++ model can be performed as shown in the following:spacite
      When all semantic mutation operators were applied to the secure model, SPaCiTE will show the folder with the mutated models at the left side as part of the “Project Explorer”, as shown in the following picture:spacite
      All the mutated models are stored in the directory mutatedModels/[name of the secure model]/semantic.
      A SPaCIoS project is configured so that all .aslan++ files are automatically translated to .aslan files. After all mutated models are added to the project, this process will immediately start, indicated in the right lower corner (see below). Please be aware that this process might take a while.spacite

 

    1. Model check all mutated models
      At this stage, all mutated models are stored in the foldermutatedModels/[name of the secure model]/semantic. We don’t know yet if the injected vulnerability violates a high level security property. Therefore we will model check all mutated models. This is a fully automatic process so we just start it by invoking the command given in the following:spacite
      When this task has finished, the project is refreshed. The output of the model checker is stored in .atkpp files in the folder mutatedModels/[name of the secure model]/semantic, as shown in the following pictures:spacite
      spacite
      All the .atkpp files can be categorized into 2 categories. Some of the mutated models are still secure and the corresponding .atkpp file will report that no attack is found. For other mutated models the model checker will find a counter example.
      All those .atkpp files that contain an abstract counter example are now considered for further processing.

 

    1. Mapping to WAAL
      All attack traces are generated from mutated models that origin from a single secure model. We define a mapping from messages that appear in this secure model to browser actions that are performed in the browser. A property of this mapping is that upon performing the browser actions, the browser generates protocol level messages that are an instantiation of the abstract message in the secure model. This mapping depends on the partitioning of the SUV. An agent can either be a simulated agent or an observed agent. Messages that are sent by a simulated agent have to be generated, whereas received messages by a simulated agent have to be verified. Messages sent or received by an observed agent have to be verified. To define the mapping for our secure model, we first partition the SUV. For this tutorial both agents Tom and Jerry are simulated agents. This is based on the fact that all semantic mutation operators that are applied to the secure model affect the server component. We open the tab with the secure model and invoke the command Define WAAL Mapping:spacite

      If the WAALMapping file does not already exists, the above command creates a new template file, as shown in the following figure:spacite

 

    1. Providing configuration and helper functions
      In the mapping file generated in step 7, the security analyst first defines which agents are simulated. In addition each simulated agent needs access to a controllable browser. We define the IP address and the port for each involved agent. We specify where each agent finds a browser instantiation that he can use to perform browser actions. These browser instantiations are provided by the ControlProxy application which uses the Selenium framework as a backend. Therefore the security analyst specifies for each agent the following 3 values: (1) the IP and port of the control proxy location (ProxyLocation), (2) the IP and port of the controllable browser (BrowserLocation) and (3) username and password for basic HTTP Authentication, as shown in the following listing:

      SIMULATED_AGENTS {
      	tom,
      	jerry
      }
      
      AGENTS_CONFIGURATIONS {
      	Agent: tom 
      		httpBasicAuthentication_Username: "guest"
                      httpBasicAuthentication_Password: "guest"
      		BrowserLocation: 127.0.0.1:4444 
                      ProxyLocation:127.0.0.1:6789
      	Agent: jerry
      		httpBasicAuthentication_Username: "guest"
                      httpBasicAuthentication_Password: "guest"
      		BrowserLocation: 127.0.0.1:4443
                      ProxyLocation:127.0.0.1:6788
      }

      In addition to the configuration of the agent, the security analyst defines the following mappings:

      MAPPINGS {
      	employeeName:
      		abstract: "tom" concrete: "regexp:Tom.*"
      		abstract: "jerry" concrete: "regexp:Jerry.*"
      		
      	password:
      		abstract: "tom" concrete: "tom"
      		abstract: "jerry" concrete: "jerry"
      		
      	listStaffOfXPATH:
      		concrete: "`//span[@class='lesson_text_db' and \
                         contains (. ,'capitalize ($1)' ) ]'"
      
      	getSSN:
      		abstract: "jerry" concrete: "858-55-4452"
      		abstract: "tom" concrete: "792-14-6364"
      }

      We define how abstract objects are mapped to concrete objects (as they appear in the web applications). As an example, every agent has an assigned role. Therefore whenever WebGoat displays an agent in the context that we are interested in, the corresponding role appears next to its name. Nevertheless agents in the model are displayed without the assigned role. Therefore, for mapping abstract agent objects to concrete ones, we map each agent toAgent (role) using a regular expression (see the “employeeName” definition in the previous code). The password for each agent to login to the WebGoat lesson is provided by the “password” function: each agent uses his firstname as a password. For the verification whether the webserver sends back the correct response, we define the following helper functions: getSSN andlistStaffOfXPATH. When we want to check if the webserver replies with the profile of an agent, we check if the corresponding Social Security Number (SSN) is visible in the page. Therefore the security analyst defines a mapping from an agent to the its SSN. This mapping is named getSSN in the previous. Finally the security analyst defines a mapping called listStaffOfXPATH which maps an agent to its list of profiles he is supposed to have access to.

      The list of profiles the agent has access to is assumed to be visible in the browser, if there is a span element named lesson_text_db which contains the name of the agent.

 

    1. Mapping abstract messages to abstract browser actions
      The last part of the WAAL mapping consists of the translation of abstract messages to abstract browser actions. When such a mapping is applied, the mapping takes an element from a dedicated input set and generates a sequence of actions expressed in the WAAL language. The dedicated input set potentially contains the following elements:

      • the special tag START_AGENT
      • every defined message declaration from the secure model

      The first possibility is the tag START_AGENT. It takes as single parameter the agent that has to be initialized. Therefore this tag appears in the input set for the mapping e.g., as START_AGENT(tom), START_AGENT(jerry), if tom andjerry are valid agents. The second possibility are message declarations. They can have an arbitrary number of parameters. What they have all in common is, that the first parameter is an additional introduced parameter of type agent. It indicates, which agent is responsible of sending/verifying this message. If the message has to be generated, a second additional parameter of type agent is added. It indicates the receiver of the message. As an example, if a message to be generated has the signature viewProfile(profile), this message will appear in the input set for the mapping asviewProfile(agent,agent,profile). The agent who is responsible of sending the message can be retrieved with $1, the intended receiver can be retrieved with $2, whereas the profile parameter can be accessed with $3. If a message to be verified has the signature listStaffOf(agent), this message will appear in the input set for the mapping as listStaffOf(agent,agent). The agent who is responsible of verifying the message can be retrieved with $1, whereas the 2. agent parameter can be accessed with $2.

      Important to notice is that the page, where an action can be performed, is determined by the secure model. The Webgoat model defines a state machine where nodes represent pages and edges are the possible actions. When the security analyst defines the mapping for the actions, the corresponding page has to be taken into consideration as well. This in particular influences how the mapping of messages to actions has to be defined.

      We now write the WAALMapping file for the WebGoat lesson. The following mappings have to be places inside the object MESSAGES_TO_ACTIONS {...}. Before an agent can perform actions in a browser, it has to be initialized. Therefore SPaCiTE introduces for each agent the keyword START_AGENT. The security analyst has to provide a mapping for these START_AGENT tags. For this tutorial, the constant START_AGENT is mapped to the following 5 browser actions, as given in the following code:

      // Each simulated agent goes to the home page
      START_AGENT:
           'ga_goToURL($1, "http://webgoat:8080/WebGoat-5.4/attack")
           ga_clickButton($1, ByText("Start WebGoat"))
           ga_clickLink($1, ByText("Cross-Site Scripting (XSS)"))
           ga_clickLink($1, ByText("Stage 1: Stored XSS"))
           ga_clickLink($1, ByText("Restart this Lesson"))'

      First we go to the URL http://webgoat:8080/WebGoat-5.4/attack, click on the button Start WebGoat, and then on the links Access Control Flaws, Stage 3: Bypass Data Layer Access Control, and Restart this Lesson. After performing these browser actions the browser is in the starting state to use the corresponding WebGoat lesson. It is important here to mention that the URL must not be “127.0.0.1” since local requests are not monitored. If the SUV is nevertheless provided at “127.0.0.1”, please add an alias for “127.0.0.1” to the file /etc/hosts and use this alias in the WAALMapping file. The abstract action login has the signaturelogin(agent,symmetric_key): message and has therefore 4 parameters when it is in the input set. The first parameter $1 is the agent that performs the login, $2 is the receiver of the message, $3 is the abstract username, and $4 is the password for the login. Since an agent can have an arbitrary username, we apply the function employeeName to the agent to retrieve the desired username. The following mapping:

      // login
      GENERATE_login:
           'ga_selectItems($1, ByName("employee_id"), {employeeName($3)})
           ga_inputText($1, ByName("pass`\'word"), $4)
           ga_clickButton($1, ByText("Login"))'

      defines how an agent performs a login. In the browser, the agent first has to select his name from the dropdown element, where the dropdown element is identified with the name “employee_id”. After that, the agent types his password into the field identified by the name “password”. Finally the agent has to click on the button “login”.

      After an agent is logged in, he can view a profile. The message in the secure model has the signature viewProf(agent): message. When this message is in the input set for the mapping, it consumes 3 parameters. The first parameter ($1) is the agent who sends this message, $2 is the receiver of the message, and the third parameter ($3) is the agent whose profile is viewed. Viewing a profile can be done with the following actions in the browser. The agent first selects the corresponding profile from the displayed list and clicks on the buttonViewProfile. This sequence of browser actions is given in:

      //viewProfileOf
      GENERATE_viewProf:
           'ga_selectItems($1, ByName("employee_id"), {employeeName($3)})
           ga_clickButton($1, ByText("ViewProfile"))'

      Instead of viewing a profile, an agent can also decide to edit a profile. In the secure model, the message to edit a profile has the signatureeditProf(agent, text): message. When this message is in the input set for the mapping, the first parameter ($1) is the agent who has to send this message. The second parameter ($2) is the receiver of the message, and the third parameter ($3) corresponds to the agent whose profile has to be updated. Finally the fourth parameter ($4) is the updated text of the profile. The corresponding browser actions are given in:

      //editProfileOf
      GENERATE_editProf:
           'ga_clickButton($1, ByText("EditProfile"))
           ga_inputText($1, ByName("address1"), $4)
           ga_clickButton($1, ByText("UpdateProfile"))'

      The mapping expresses that an abstract editProf message can be generated by clicking on the button EditProfile, then typing the new content into the address field given by the name “address1″. For simplicity reasons, only the address field is used in this mapping. In a more complex example, other fields can be considered as well. After all values are typed into the corresponding input fields, the button with the label UpdateProfile has to be clicked. The signature of the delete message is deleteProf(agent): message. When thedeleteProf message is in the input set, the first parameter ($1) is the agent that generates this message and $2 is the receiver of the message. The agent whose profile has to be deleted is given as a third parameter ($3) when the message is in the input set. To delete a profile, the agent has to select the corresponding profile, given by the employeeName in the list identified by the name “employee_id” and clicking on the button with the label “DeleteProfile”. This mapping is given in the following snippet:

      //deleteProfileOf
      GENERATE_deleteProf:
           'ga_selectItems($1, ByName("employee_id"), {employeeName($3)})
           ga_clickButton($1, ByText("DeleteProfile"))'

      The signature of the retE2L message is retE2L: message. This message is used to return to the main page after a profile has been edited. When theretE2L message is in the input set, the first parameter ($1) is the agent that generates this message and $2 is the receiver of the message. To perform the retE2L message the agent has to click on the button with the label “ListStaff”. This mapping is given in the following snippet:

      //retE2L
      GENERATE_retE2L:
           'ga_clickButton($1, ByText("ListStaff"))'

      The two actions that are verified in this example are the message listStaffand profile. listStaff has the signature listStaff(agent): message. When this message is in the input set, it has as the first parameter ($1) the agent that is verifying this message. As the second parameter ($2) it contains the agent whose list is returned for. Whether the web server indeed sends back the abstract message listStaff is verified by checking if the list of profiles for the corresponding user is displayed in the browser. This is expressed by the WAAL action va_HTMLPage. It verifies if the span element, that is returned by the helper function listStaffOfXPATH is contained in the current HTML page. This mapping is given in the following code:

      //listStaffOf
      VERIFY_listStaff:
           'va_HTMLPage($1, ByXPath("listStaffOfXPATH($2)"))'

      The second message that is verified in this example is the profile message with the signature profile(agent): message. When this message is in the input set for the mapping, it contains as the first parameter ($1) the agent who performs the verification. As the second parameter ($2) it contains the agent whose profile the message represents. For verifying this, SPaCiTE checks if the Social Security Number of the corresponding person is contained in the current webpage. This check is defined as:

      //profileOf
      VERIFY_profile:
           'va_HTMLPage($1, ByText("getSSN($2)"))'

 

    1. Applying the mapping
      After the security analyst has defined the WAALMapping file, all attack traces can be translated to executable test cases. For starting this translation, make sure that the current open tab is the secure model. Then click the command “Instantiate All Abstract Attack Traces”, as shown in the following figure:spacite

 

  1. Executing concrete attack traces
    In the same directory as the abstract attack traces, we find now a set of instantiated attack traces in the form of *.java and *.class files. These attack traces can now be executed with the help of the TEE. Before we start the TEE we start the control proxy that configures and provides the necessary background services for the TEE. We execute the command Start Control Proxy as shown in the following figure:spacite
    Finally we start the TEE by executing the command Execute TEE as shown in the following figure:spacite
    The TEE application is very simplistic and shows 3 areas for the 3 abstraction layers, (1) the abstract attack trace, (2) WAAL actions, and (3) protocol level information. To execute an attack trace, the security analyst clicks on the Startbutton. The displayed popup window shows all generated test cases that are executable. The security analyst selects the desired test case and clicks on theOK button:spacite
    For this tutorial we execute an attack trace for a stored XSS attack. Therefore we select the test casewebgoat_annotated_XSSSanitisationCommentOut_1mutatedatkppfilteredfrom the list. The execution is fully automatic and no security analyst interaction is needed. At the end of the execution the TEE confirms the vulnerability by a popup window:spacite