Documentation

Simple expression language

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

Given an expression, symbolically evaluate it

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

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

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

A "select" command:

A "drop" instruction, which can be exploited!

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

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

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