Copyright	(c) Joel Burget
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
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 (SFunArray 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

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 #

type M = StateT (SFunArray 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 lenght 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 ++ "'")

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!