-----------------------------------------------------------------------------
-- |
-- 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 :: String -> SQLExpr
fromString = String -> SQLExpr
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 :: SQLExpr -> M SString
eval (Query SQLExpr
q)         = do SString
q' <- SQLExpr -> M SString
eval SQLExpr
q
                            forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [SString
q']
                            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a. SymVal a => Symbolic (SBV a)
sbvExists_
eval (Const String
str)       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => a -> SBV a
literal String
str
eval (Concat SQLExpr
e1 SQLExpr
e2)    = SString -> SString -> SString
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SQLExpr -> M SString
eval SQLExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SQLExpr -> M SString
eval SQLExpr
e2
eval (ReadVar SQLExpr
nm)      = do SString
n   <- SQLExpr -> M SString
eval SQLExpr
nm
                            SArray String String
arr <- forall s (m :: * -> *). MonadState s m => m s
get
                            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray String String
arr SString
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 :: SQLExpr
exampleProgram = SQLExpr -> SQLExpr
Query forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SQLExpr -> SQLExpr -> SQLExpr
Concat [ SQLExpr
"SELECT msg FROM msgs WHERE topicid='"
                                       , SQLExpr -> SQLExpr
ReadVar SQLExpr
"my_topicid"
                                       , SQLExpr
"'"
                                       ]

-- | Limit names to be at most 7 chars long, with simple letters.
nameRe :: R.RegExp
nameRe :: RegExp
nameRe = Int -> Int -> RegExp -> RegExp
R.Loop Int
1 Int
7 (Char -> Char -> RegExp
R.Range Char
'a' Char
'z')

-- | Strings: Again, at most of length 5, surrounded by quotes.
strRe :: R.RegExp
strRe :: RegExp
strRe = RegExp
"'" forall a. Num a => a -> a -> a
* Int -> Int -> RegExp -> RegExp
R.Loop Int
1 Int
5 (Char -> Char -> RegExp
R.Range Char
'a' Char
'z' forall a. Num a => a -> a -> a
+ RegExp
" ") forall a. Num a => a -> a -> a
* RegExp
"'"

-- | A "select" command:
selectRe :: R.RegExp
selectRe :: RegExp
selectRe = RegExp
"SELECT "
         forall a. Num a => a -> a -> a
* (RegExp
nameRe forall a. Num a => a -> a -> a
+ RegExp
"*")
         forall a. Num a => a -> a -> a
* RegExp
" FROM "
         forall a. Num a => a -> a -> a
* RegExp
nameRe
         forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.Opt (  RegExp
" WHERE "
                  forall a. Num a => a -> a -> a
* RegExp
nameRe
                  forall a. Num a => a -> a -> a
* RegExp
"="
                  forall a. Num a => a -> a -> a
* (RegExp
nameRe forall a. Num a => a -> a -> a
+ RegExp
strRe)
                  )

-- | A "drop" instruction, which can be exploited!
dropRe :: R.RegExp
dropRe :: RegExp
dropRe = RegExp
"DROP TABLE " forall a. Num a => a -> a -> a
* (RegExp
nameRe forall a. Num a => a -> a -> a
+ RegExp
strRe)

-- | We'll greatly simplify here and say a statement is either a select or a drop:
statementRe :: R.RegExp
statementRe :: RegExp
statementRe = RegExp
selectRe forall a. Num a => a -> a -> a
+ RegExp
dropRe

-- | The exploit: We're looking for a DROP TABLE after at least one legitimate command.
exploitRe :: R.RegExp
exploitRe :: RegExp
exploitRe = RegExp -> RegExp
R.KPlus (RegExp
statementRe forall a. Num a => a -> a -> a
* RegExp
"; ")
          forall a. Num a => a -> a -> a
* RegExp
"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 :: SQLExpr -> IO String
findInjection SQLExpr
expr = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ 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.
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption forall a b. (a -> b) -> a -> b
$ String -> [String] -> SMTOption
OptionKeyword String
":smt.random_seed" [String
"1"]

    SString
badTopic <- String -> Symbolic SString
sString String
"badTopic"

    -- Create an initial environment that returns the symbolic
    -- value my_topicid only, and unspecified for all other variables
    SArray String String
emptyEnv :: SArray String String <- forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"emptyEnv" forall a. Maybe a
Nothing

    let env :: SArray String String
env = forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray SArray String String
emptyEnv SString
"my_topicid" SString
badTopic

    (SString
_, [SString]
queries) <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (SQLExpr -> M SString
eval SQLExpr
expr) SArray String String
env)

    -- For all the queries thus generated, ask that one of them be "exploitable"
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a. (a -> SBool) -> [a] -> SBool
sAny (forall a. RegExpMatchable a => a -> RegExp -> SBool
`R.match` RegExp
exploitRe) [SString]
queries

    forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
               case CheckSatResult
cs of
                 CheckSatResult
Unk    -> forall a. HasCallStack => String -> a
error String
"Solver returned unknown!"
                 DSat{} -> forall a. HasCallStack => String -> a
error String
"Solver returned delta-satisfiable!"
                 CheckSatResult
Unsat  -> forall a. HasCallStack => String -> a
error String
"No exploits are found"
                 CheckSatResult
Sat    -> forall a. SymVal a => SBV a -> Query a
getValue SString
badTopic