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

Copyright(c) Joel Burget
Safe HaskellNone



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.



data SQLExpr Source #

Simple expression language


IsString SQLExpr Source #

Literals strings can be lifted to be constant programs


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!