Difference between revisions of "Offline Team2 Benchmark3"

Latest revision as of 16:04, 7 June 2016

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

There are two traces in marq/offline/bench3

• sql_trace_valid
• sql_trace_invalid

The first trace consists of 9,447,753 events of which 1,909,800 are input events, 2,478,902 are derive events, 3,149,251 are sanitise events and 1,909,800 are use events. This trace satisfies the property. The second trace is the same as the first but with two sanitise events missing, causing it to fail after 9,438,748 events.

The trace sql_trace_invalid should be used for the competition, the other is for testing.

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.

A FO-LTL Specification

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.