Documentation.SBV.Examples.Strings.SQLInjection

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.

Documentation

data SQLExpr

Simple expression language

Constructors

Query SQLExpr

Const String

Concat SQLExpr SQLExpr

ReadVar SQLExpr

Instances

IsString SQLExpr

Literals strings can be lifted to be constant programs

Methods

fromString :: String -> SQLExpr

type M = StateT (SFunArray String String) (WriterT [SString] Symbolic)

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

eval :: SQLExpr -> M SString

Given an expression, symbolically evaluate it

exampleProgram :: SQLExpr

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

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

strRe :: RegExp

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

selectRe :: RegExp

A "select" command:

dropRe :: RegExp

A "drop" instruction, which can be exploited!

statementRe :: RegExp

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

exploitRe :: RegExp

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

findInjection :: SQLExpr -> IO String

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 ++ "'")

We have:

>>> findInjection exampleProgram
"h'; DROP TABLE 'users"

Indeed, if we substitute the suggested string, we get the program:

  query ("SELECT msg FROM msgs where topicid=h; DROP TABLE users")

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