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

Copyright(c) Joel Burget
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data SQLExpr Source #

Simple expression language

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

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