Offline Team2 Benchmark3

SQL Injection. An abstract property capturing the requirement that SQL query strings passed to a server, and any derived stings, should be sanitised before use.

Benchmark Data

The Trace Part

<< Will appear shortly>

The Property Part

Informal Description

This specification is from the setting of SQL queries being taken as input to a server and then used on a database. To prevent malicious behaviour such as a query string ’; DROP TABLE table; it is necessary to sanitise these query strings before use. It is also necessary to ensure that no query strings derived from the original query string are used before sanitisation.

The property we want to monitor is that every string s2 derived from an input string s1 is sanitised before use. Note that once a string has been sanitised then all strings derived from it are safe to use.

We abstractly capture the input of a string as input(string), the derivation of a string as derive(string,string), the use of a string as use(string) and the sanitisation of a string as sanitise(string).

Demonstration Traces

The following traces should be accepted

   input(A).sanitise(A).use(A)
   input(A).derive(A,B).derive(A,C).sanitise(C).use(C)
   input(A).derive(A,B).derive(A,C).derive(C,D).derive(D,E)

The following traces should be rejected

   input(C).use(C)
   input(A).derive(A,B).derive(B,C).sanitise(B).use(C)
   input(A).derive(A,B).derive(B,C).sanitise(C).input(C).use(C)

The first two traces traces use C without sanitising it first. In the last case the use of C is invalid even though C was sanitised before it was input.

Formal Specification

A QEA following the original semantics can be given as

  qea(SQLInjection){
    Negated
    skip(start){ 
      input(s1) -> start
      input(s1) -> dirty 
    }
    skip(dirty){
      derive(s2,s3) if [ s1=s2 ] do[ s1:=s3 ]  -> dirty
      derive(s2,s3) if [ s1=s2 ] -> dirty
      sanitise(s2) if [ s1=s2 ] -> failure
      use(s2) if [ s1=s2 ] -> success
    }
  }

This uses a some-path non-determinism with negation. This variant of determinism is what requires the negative form.

We now believe that a more useful semantics is an all-path non-determinism and this property can be formulated using this approach as follows

  qea(SQLInjection){
    accept skip(start){ 
      input(s1) -> start
      input(s1) -> dirty 
    }
    accept skip(dirty){
      derive(s2,s3) if [ s1=s2 ] do[ s1:=s3 ]  -> dirty
      derive(s2,s3) if [ s1=s2 ] -> dirty
      sanitise(s2) if [ s1=s2 ] -> Success
      use(s2) if [ s1=s2 ] -> Failure
    }
  }

This looks similar but the Success and the Failure states make more sense.

Clarification Requests

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.