1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Strings.SQLInjection
-- Copyright : (c) Joel Burget
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Strings.SQLInjection where
import Control.Monad.State
import Control.Monad.Writer
import Data.String
import Data.SBV
import Data.SBV.Control
import Prelude hiding ((++))
import Data.SBV.String ((++))
import qualified Data.SBV.RegExp as R
-- | Simple expression language
data SQLExpr = Query SQLExpr
| Const String
| Concat SQLExpr SQLExpr
| ReadVar SQLExpr
-- | Literals strings can be lifted to be constant programs
instance IsString SQLExpr where
fromString = Const
-- | Evaluation monad. The state argument is the environment to store
-- variables as we evaluate.
type M = StateT (SArray String String) (WriterT [SString] Symbolic)
-- | Given an expression, symbolically evaluate it
eval :: SQLExpr -> M SString
eval (Query q) = do q' <- eval q
tell [q']
lift $ lift free_
eval (Const str) = return $ literal str
eval (Concat e1 e2) = (++) <$> eval e1 <*> eval e2
eval (ReadVar nm) = do n <- eval nm
arr <- get
return $ readArray arr n
-- | 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 ++ "'")
-- @
exampleProgram :: SQLExpr
exampleProgram = Query $ foldr1 Concat [ "SELECT msg FROM msgs WHERE topicid='"
, ReadVar "my_topicid"
, "'"
]
-- | Limit names to be at most 7 chars long, with simple letters.
nameRe :: R.RegExp
nameRe = R.Loop 1 7 (R.Range 'a' 'z')
-- | Strings: Again, at most of length 5, surrounded by quotes.
strRe :: R.RegExp
strRe = "'" * R.Loop 1 5 (R.Range 'a' 'z' + " ") * "'"
-- | A "select" command:
selectRe :: R.RegExp
selectRe = "SELECT "
* (nameRe + "*")
* " FROM "
* nameRe
* R.Opt ( " WHERE "
* nameRe
* "="
* (nameRe + strRe)
)
-- | A "drop" instruction, which can be exploited!
dropRe :: R.RegExp
dropRe = "DROP TABLE " * (nameRe + strRe)
-- | We'll greatly simplify here and say a statement is either a select or a drop:
statementRe :: R.RegExp
statementRe = selectRe + dropRe
-- | The exploit: We're looking for a DROP TABLE after at least one legitimate command.
exploitRe :: R.RegExp
exploitRe = R.KPlus (statementRe * "; ")
* "DROP TABLE 'users'"
-- | 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
findInjection :: SQLExpr -> IO String
findInjection expr = runSMT $ do
-- This example generates different outputs on different platforms (Mac vs Linux).
-- So, we explicitly set the random-seed to get a consistent doctest output
-- Otherwise the following line isn't needed.
setOption $ OptionKeyword ":smt.random_seed" ["1"]
badTopic <- sString "badTopic"
-- Create an initial environment that returns the symbolic
-- value my_topicid only, and unspecified for all other variables
emptyEnv :: SArray String String <- newArray "emptyEnv" Nothing
let env = writeArray emptyEnv "my_topicid" badTopic
(_, queries) <- runWriterT (evalStateT (eval expr) env)
-- For all the queries thus generated, ask that one of them be "exploitable"
constrain $ sAny (`R.match` exploitRe) queries
query $ do cs <- checkSat
case cs of
Unk -> error "Solver returned unknown!"
DSat{} -> error "Solver returned delta-satisfiable!"
Unsat -> error "No exploits are found"
Sat -> getValue badTopic
|
