sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Joel Burget
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Strings.SQLInjection

Description

Implement the symbolic evaluation of a language which operates on strings in a way similar to bash. It's possible to do different analyses, but this example finds program inputs which result in a query containing a SQL injection.

Synopsis

- data SQLExpr
  - = Query SQLExpr
  - | Const String
  - | Concat SQLExpr SQLExpr
  - | ReadVar SQLExpr
- type M = StateT (SArray String String) (WriterT [SString] Symbolic)
- eval :: SQLExpr -> M SString
- exampleProgram :: SQLExpr
- nameRe :: RegExp
- strRe :: RegExp
- selectRe :: RegExp
- dropRe :: RegExp
- statementRe :: RegExp
- exploitRe :: RegExp
- findInjection :: SQLExpr -> IO String

# Documentation

data SQLExpr Source #

Simple expression language

Constructors

Query SQLExpr |
Const String |
Concat SQLExpr SQLExpr |
ReadVar SQLExpr |

#### Instances

Instances details

IsString SQLExpr Source # | Literals strings can be lifted to be constant programs
Instance details Defined in Documentation.SBV.Examples.Strings.SQLInjection Methods fromString :: String -> SQLExpr Source #

type M = StateT (SArray String String) (WriterT [SString] Symbolic) Source #

Evaluation monad. The state argument is the environment to store variables as we evaluate.

eval :: SQLExpr -> M SString Source #

Given an expression, symbolically evaluate it

exampleProgram :: SQLExpr Source #

A simple program to query all messages with a given topic id. In SQL like notation:

      query ("SELECT msg FROM msgs where topicid='" ++ my_topicid ++ "'")

nameRe :: RegExp Source #

Limit names to be at most 7 chars long, with simple letters.

strRe :: RegExp Source #

Strings: Again, at most of length 5, surrounded by quotes.

selectRe :: RegExp Source #

A "select" command:

dropRe :: RegExp Source #

A "drop" instruction, which can be exploited!

statementRe :: RegExp Source #

We'll greatly simplify here and say a statement is either a select or a drop:

exploitRe :: RegExp Source #

The exploit: We're looking for a DROP TABLE after at least one legitimate command.

findInjection :: SQLExpr -> IO String Source #

Analyze the program for inputs which result in a SQL injection. There are other possible injections, but in this example we're only looking for a `DROP TABLE` command.

Remember that our example program (in pseudo-code) is:

      query ("SELECT msg FROM msgs WHERE topicid='" ++ my_topicid ++ "'")

Depending on your z3 version, you might see an output of the form:

      ghci> findInjection exampleProgram
      "kg'; DROP TABLE 'users"

though the topic might change obviously. Indeed, if we substitute the suggested string, we get the program:

    query ("SELECT msg FROM msgs WHERE topicid='kg'; DROP TABLE 'users'")

which would query for topic `kg` and then delete the users table!

Here, we make sure that the injection ends with the malicious string:

    >>> ("'; DROP TABLE 'users" `Data.List.isSuffixOf`) <$> findInjection exampleProgram
    True