Safe Client/Server Web Development with Haskell

Mark Mazumder & Timothy Braje
4 November 2016
Use Right Arrow Key or Spacebar to Advance Slides

DISTRIBUTION STATEMENT A. Approved for public release; distribution is unlimited.

This material is based upon work supported under Air Force Contract No. FA8721-05-C-0002 and/or FA8702-15-D-0001. Any opinions, findings, conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the U.S. Air Force.

© 2016 Massachusetts Institute of Technology.

Delivered to the U.S. Government with Unlimited Rights, as defined in DFARS Part 252.227-7013 or 7014 (Feb 2014). Notwithstanding any copyright notice, U.S. Government rights in this work are defined by DFARS 252.227-7013 or DFARS 252.227-7014 as detailed above. Use of this work other than as specifically authorized by the U.S. Government may violate any copyrights that exist in this work.

About us

writing Haskell for a year and a half at MIT Lincoln Laboratory

mazumder@ll.mit.edu

tbraje@ll.mit.edu

Outline

  • Haskell Crash Course

  • Phantom Types for Enforced Sanitization

  • Servant – A Web API as a Type

  • Functional Reactive Programming for the GUI

The Takeaway: Type Driven Programming

Make insecure code inexpressible

(inspired by Yaron Minsky’s “Make illegal states unrepresentable”)

Motivation

  • Types are the lightest-weight verification tool
  • Automates reasoning about your code
  • Security and correctness are tied


  • Security - properties of your code arrow_forward
  • Tests - imprecise specifications arrow_forward
  • Types - precise specifications arrow_forward
  • Difficult: code review verification arrow_forward
  • Add security properties to types
  • Tests exercise finite inputs
  • Forced to adhere to a contract
  • Easy: compiler verification

A Brief Tour of the Haskell Ecosystem

  • Types as a specification: precise properties
    • Correctness ~ Security
  • GHC: the Haskell compiler
  • GHCJS: the Haskell-to-JavaScript compiler
  • LiquidHaskell: provable properties
  • Phantom Types: lightweight enforcement against SQLi, XSS
  • Functional Reactive Programming: callback-free user interfaces
  • TypeFamilies: type-level programming
  • Software Transactional Memory: easy concurrency (no locks)

Questions for pairing up

  • Haskell experience?
  • Vim or Emacs?
  • Docker?
  • GHCJS/Reflex/Servant?


  • Has everyone run either
    • docker pull mmaz/secdev
    • docker pull mmaz/server-secdev

Docker Basics

Right now, update:

$ docker pull mmaz/secdev

Test it out:

$ docker run --rm -it mmaz/secdev /bin/intro
[0,1,2,3,4,5]
...


Behind a proxy?

$ docker run \
  -e "http_proxy=..." -e "https_proxy=..." -e "HTTP_PROXY=..." -e "HTTPS_PROXY=..."  \
  --rm -it mmaz/secdev /bin/intro

Docker stops working? In a new terminal window: docker stop $(docker ps -a -q)

Docker Run

$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/bash
$ secdev> exit # or Ctrl-d
  • -e environment variable "foo=bar"
  • -p port mapping
  • --rm stateless (don’t persist changes)
  • -i interactive (don’t background)
  • -t tag name (mmaz/secdev)
$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/ghci
GHCi, version 8.0.1
Prelude> 3 + 4
7
Prelude> :quit -- or Ctrl-D

Spacemacs: Emacs + Vim

$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> emacs AddTwoNumbers.hs
# Alternatively
#         vim  AddTwoNumbers.hs
#         nano AddTwoNumbers.hs
$ secdev> exit #or Ctrl-d
  • Default: Vim-Mode
  • Quit :q Enter (or Esc :q Enter)
  • Switch to emacs-mode: SPC t E e
  • Exit from emacs-mode: Ctrl-x Ctrl-c
  • Exit from nano: Ctrl-x

Haskell Crash Course

Intro to Haskell

Haskell:

x :: A

x = y

A -> B

Meaning:

x has type A

x defined to be y

function from A to B

theNumberFive :: Int   -- type declaration
theNumberFive = 5      -- definition

show :: Int -> String  -- function type

$ stack ghci           -- interactive repl
>>> theNumberFive
5 :: Int
>>> show theNumberFive
"5" :: String

--double dash for code comments

String literals like "5" are doublequoted

Intro to Haskell

Let’s convert this C function to Haskell

Intro to Haskell

don’t need a type signature: still valid Haskell

Intro to Haskell

the function name

Intro to Haskell

a return value C is a definition in Haskell

Intro to Haskell

how do we read a type signature?

Intro to Haskell

still have the function name (like a header file in C)

Intro to Haskell

this is the type of the argument to plusfive

Intro to Haskell

Types read left-to-right. argument type to (“->”) return type

Intro to Haskell

name the argument value “x” in the lexical scope

Intro to Haskell

use “x” in the function definition

Intro to Haskell

all together: the input type, the output type, and the name-binding

Intro to Haskell

what about multiple arguments?

Intro to Haskell

the return type is still rightmost in Haskell

Intro to Haskell

here is the type of the first argument

Intro to Haskell

here is the type of the second argument

Intro to Haskell

so plus takes two ints and returns an int

Intro to Haskell

spaces separate name bindings instead of commas

Type Errors

1
2
3
4
5
6
7
8
plusfive :: Int -> Int
plusfive x = x + 5

>>> plusfive 4
9

>>> plusfive 4.0
 error: "not an Int"
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
andfive :: String -> String
andfive x = x <> "andfive" --concatenates strings

>>> andfive "4"           -- strings are doublequoted
"4andfive"

>>> andfive 4             -- inferred type
 error: "not a String"

>>> andfive (4 :: Int)    -- explicit type annotation
 error: "not a String"

>>> andfive (4 :: String) -- no casting allowed
 error: "No instance for (Num String)
         arising from the literal 4"

Networks, Databases, Stdout

  • a pure function like this can’t perform IO
plus :: Int -> Int -> Int
  • Wrap pure computations inside an IO action context
plusAndPrint :: Int -> Int -> IO Int
1
2
3
4
5
6
7
8
plus :: Int -> Int -> Int
plus x y = x + y

plusAndPrint :: Int -> Int -> IO Int
plusAndPrint x y = do
  let result = plus x y
  print result
  return result

Calling Functions in Haskell

Filtering a list

removeBigNumbers :: Int -> Bool
removeBigNumbers x = x < 6
>>> filter removeBigNumbers [0,1,2,3,4,5,6,7,8,9,10]
[0,1,2,3,4,5]
staticTypes :: String -> Bool
staticTypes lang
  | lang == "javascript" = False
  | lang == "ruby"       = False
  | lang == "haskell"    = True
  | lang == "scala"      = True
  | otherwise            = True --oops
>>> filter staticTypes ["javascript", "python", "haskell"]
["python","haskell"]
  ^ oops

Program against types instead of strings

Exercise 1 – Haskell 101

-- an enum
data Languages = JavaScript
               | Ruby
               | Haskell
               | Scala
               | Python
betterStaticTypes :: Languages -> Bool
betterStaticTypes lang = case lang of
  JavaScript  -> False
  Ruby        -> False
  Haskell     -> True
  Scala       -> True
  Python      -> False

If you forget a case:

  ...
  Scala       -> True
  --Python      -> False
warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Python

If you mix strings in:

>>> filter betterStaticTypes [Haskell, Python]
[Haskell]
>>> filter betterStaticTypes [Haskell, "bash"]
Couldn't match expected type ‘Languages’
                  with actual type ‘String’
    > In the expression: "bash"
    > In the second argument of ‘filter’,
      namely ‘[Haskell, "bash"]’

Exercise 1 - Try it out

data Languages = JavaScript | Haskell | ... (your fav language) | Python deriving (Eq, Show)

betterStaticTypes :: Languages -> Bool
betterStaticTypes lang = case lang of
  JavaScript  -> False
  Ruby        -> False
  Haskell     -> True
  Scala       -> True
  Python      -> False
  -- add a case here

print $ filter betterStaticTypes [Haskell, ..., (add your language)]
$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> emacs Intro.hs  #switch to pure emacs: SPC t E e
$ secdev> ghc -Wall -fforce-recomp Intro.hs

  Intro.hs:17:26: warning: [-Wincomplete-patterns]
      Pattern match(es) are non-exhaustive
      In a case alternative: Patterns not matched: YourLanguage

$ secdev> runghc Intro.hs

  ...
  [Haskell,...your language]

$ secdev> exit #or Ctrl-D

(continuous typechecking: stack build --file-watch --fast)

Exercise 1: The Takeaway

Your (deeply nested) data model grows as you refactor


You add more cases, you remove old cases


GHC checks exhaustiveness at all use-sites

Ex 2: LiquidHaskell

Verify absolutevalue always returns a positive number:

Change x < 0 to x > 0 in this example:

{-@ absolutevalue :: Int -> { n : Int | 0 <= n }    @-}
    absolutevalue :: Int -> Int
    absolutevalue x = if x < 0 then negate x else x

{ n : Int | 0 <= n } returns n :: Int such that 0 is less than or equal to n

$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> emacs HelloLiquid.hs  #switch to pure emacs: SPC t E e
$ secdev> liquid HelloLiquid.hs

  **** RESULT: SAFE ****
   or
  **** RESULT: UNSAFE ****

$ secdev> exit #or Ctrl-D

LiquidHaskell Proofs

  • Binary serialization lib fpco/store
  • Fast as memcpy
  • Safe: no access violations outside bytebuffer
  • After adding constraints, fails to compile until negative numbers are handled:

LiquidHaskell can enforce many security properties - see HeartBleed example:

ucsd-progsys.github.io/liquidhaskell-tutorial/11-case-study-pointers

Gaussian Blobs

$f(x,y) = \alpha \cdot \exp(- (\frac{(x - x_0)^2}{2\sigma^2_x} + \frac{(y - y_0)^2}{2\sigma^2_y}))$

gaussian ::
GaussianParameters Float -> Float -> Float -> Float
^ (sigmas, x0, y0...)       ^ x      ^ y      ^ f(x,y)
data GaussianParameters a = GaussianParameters {
  sigmaX :: a
, sigmaY :: a
, x0     :: a
, y0     :: a
, alpha  :: a }
  • a is a type parameter
  • Substitute Float, Double, Int
  • constrain a with “=>
gaussian :: (Fractional a) =>
            GaussianParameters a -> a -> a -> a
gaussian GaussianParameters{..} x y =
  alpha * exp ( negate (  xnumerator / xdenominator
                        + ynumerator / ydenominator) )
  where
    xnumerator   = (x - x0) ** 2
    xdenominator = 2 * (sigmaX ** 2)
    ynumerator   = (y - y0) ** 2
    ydenominator = 2 * (sigmaY ** 2)

GHCJS Demo: Click to try it!

Phantom Types for Enforced Sanitization

Injection Attacks, Simplified

  • Executing user input as code is dangerous!

  • For example, assume you assemble an insert statement by concatenating some strings:

    "INSERT INTO person (name) VALUES ('" + name + "')"
  • Substitute, for name:

    name = Robert'); drop table person; --
  • And you get:

    INSERT INTO person (name) VALUES ('Robert'); drop table person; --')

Let’s Get Some Setup Out of the Way

1
2
3
4
5
6
7
8
9
10
11
12
13
14
initDB :: IO Database
initDB = do
  conn <- open ":memory:"                                             -- create in memory database
  exec conn "CREATE TABLE person (id INTEGER PRIMARY KEY, name TEXT)" -- initialize table
  exec conn "INSERT INTO person (name) VALUES ('Tim')"
  exec conn "INSERT INTO person (name) VALUES ('Mark')"               -- insert some data
  exec conn "INSERT INTO person (name) VALUES ('Sarah')"
  return conn                                                         -- return connection for future access to DB

readDB :: Database -> IO ()
readDB = flip execPrint "select * from person"                        -- print database contents to stdout

closeDB :: Database -> IO ()
closeDB =  close                                                      -- cleanup database

(raw SQL statements are in green doublequotes)

Remember to Sanitize User Input

1
2
3
4
5
6
7
8
insertDB :: Database -> Text -> IO ()                               -- make the horrible mistake of
insertDB conn name =                                                -- building up an insert statement by
  exec conn $ "INSERT INTO person (name) VALUES ('" <> name <> "')" -- string concatenation

-- Please don't use this sanitization function in real life!
sanitize :: Text -> Text                                            -- hokey sanitization function that strips
sanitize =                                                          -- off the rest of the sql statement once
  takeWhile (`notElem` [';','\'','"'])                              -- it encounters one of [; ' "]

Sanitization will only work if the developer remembers to call sanitize before every call to insertDB

Let’s Get Some Help From the Type System

Phantom Types

Lame types

Fancy types

types narrowed from any Text

UserInput

types differentiate safe and unsafe

UserInput Clean, UserInput Dirty

augment with cleanliness flag

data UserInput = UserInput {
    input   :: Text
  , isClean :: Boolean
}

cleanliness maintained in the type

data Clean
data Dirty

newtype UserInput a = UserInput { input :: Text }

runtime validation, error handling

compile time verification

carry additional boolean etc. at runtime

no runtime cost

A Phantom User Input

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
module MySafeStore                    -- carefully control what is visible outside of module
  (
    ...

  , UserInput                         -- only export the type of UserInput, not its constructor
  , readInput                         -- export readInput so we can convert Text to UserInput

  ) where

data Clean                            -- create types Clean and Dirty, with no values
data Dirty

newtype UserInput a = UserInput {     -- put phantom type parameter a in UserInput
  input :: Text
}

readInput :: Text -> UserInput Dirty  -- force bare Text values to begin life Dirty
readInput = UserInput

Phantoms Can Force Cleanliness

1
2
3
4
5
6
7
8
insertDB :: DataStore -> UserInput Clean -> IO ()                         -- we still concatenate strings to
insertDB DataStore{..} UserInput{..} =                                    -- build up sql statements, but we
  exec conn $ "INSERT INTO person (name) VALUES ('" <> input <> "')"      -- only accept sanitized input

-- Please don't use this sanitization function in real life!
sanitize :: UserInput Dirty -> UserInput Clean                            -- the only public way to
sanitize =                                                                -- sanitize a UserInput Dirty
  UserInput . takeWhile (`notElem` [';','\'','"']) . input
  • Only way to convert a UserInput Dirty into a UserInput Clean is sanitize

Exercise 3 – SQL Injection

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
main :: IO ()
main = main1 -- unsanitized version

main1 = do
  conn <- initDB
  print "Contents of initial database:"
  readDB conn

  insertDB conn "Haskell Curry"
  print "Contents after insert of our saint"
  readDB conn

  insertDB conn (sanitize "Evil'); drop table person; --")
  print "Contents after allowing my sadistic co-worker to use my library"
  readDB conn

  insertDB conn "Evil'); drop table person; --"
  print "Contents after allowing my sadistic co-worker to use my library a second time"
  readDB conn
{-
main2 :: IO ()
main2 = ...
-}
$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> stack runghc PhantomTypes.hs
  • Play with the unsafe version, making edits
  • Uncomment main2, import safe module, update main, and discover that you can no longer inject

Exercise 3 – The Takeaway

  • GHC won’t compile unsanitized user input
    • Insecure code is unrepresentable

Servant – A Web API as a Type

Crash Course on JSON

data HelloWorld = HelloWorld          -- create a new type called HelloWorld

instance ToJSON HelloWorld where      -- manual JSON definition
  toJSON =
    const $ object [ "hello" .= ("world" :: Text) ]
>>> encode HelloWorld
{"hello":"world"}
data Car = Car {
  make  :: String
, model :: String
, year  :: Int
} deriving (Generic)
instance ToJSON Car
--Generic: figure out how to JSON for me!
>>> mycar = Car "Toyota" "Prius" 2013
         -- Car("Toyota", "Prius", 2013)

>>> encode mycar
{"year":2013,"model":"Prius","make":"Toyota"}

DataKinds: Values to Types

  • 3 is a Value

  • Int is a Type

  • DataKinds promotes Values to Types

  • URL path components foo and bar
    • without DataKinds, they’re String values
  • Type-level strings promote a route /foo/bar to a type

Blogpost with details: arow.info/blog/posts/2015-07-10-servant-intro

Web Services with Servant

--  represent 'GET /sayhello/' as a type:

type API = "sayhello" :> Get '[JSON] HelloWorld

helloHandler = return HelloWorld                           -- {"hello":"world"}

main = run 8080 $ serve (Proxy :: Proxy API) helloHandler  -- serve on port 8080

In one terminal window:

$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/hello-servant

In another terminal window:

$ curl localhost:8080/sayhello
{"hello":"world"}

Web Services with Servant

-- the type of 'GET /tesla/Int'
type API = "tesla" :> Capture "year" Int  :> Get '[JSON] Car

carHandler :: Int -> Handler Car
carHandler inputyear
  | inputyear < 2012 =  throwError $ err501 { errBody = "too old!"}
  | otherwise        =  return $ Car "Tesla" "Model S" inputyear


main = run 8080 $ serve (Proxy :: Proxy API) carHandler
$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/hello-servant
$ curl localhost:8080/tesla/2011
"too old!"
$ curl localhost:8080/tesla/2016
{"year":2016,"model":"Model S","make":"Tesla"}

Types as a Lightweight Specification

1
2
3
4
5
6
7
8
data Status = OK | Fail
  deriving (Generic, Show, Read, Ord, Eq)

data Log = Log {
  ident :: Int
, timestamp :: Int
, message :: Text
} deriving (Generic, Show, Typeable)
type LogApi = "logs" :> Get '[JSON] [Log]
         :<|> "log"  :> ReqBody '[JSON] Log :> Post '[PlainText] Status
         :<|> "log"  :> Capture "id" Int :> Get '[JSON] Log
GET /logs
POST {JSON content} /log
GET /log/1

The API type specifies the http method, argument types, and return types

Exercise 4 – Match Servant API To Handlers

1
2
3
4
5
6
7
8
9
10
11
12
13
14
server :: Server LogApi
server = undefined :<|> undefined :<|> undefined -- line 68

foo :: Log -> Handler Status
foo _ = return OK

bar :: Handler [Log]
bar = return [
    Log {ident = 1, timestamp = 101, message = "msg1"}
  , Log {ident = 2, timestamp = 201, message = "msg2"}
  ]

baz :: Int -> Handler Log
baz n = return Log {ident = n, timestamp = 102, message = "message"}
  • Compiler checked server implementation
  • Server is combination of handlers
  • Task: fill in server implementation
$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/bash
$ secdev> emacs LogApi.hs #edit line 68
$ secdev> stack runghc LogApi.hs

Leveraging the Specification

-- Generate clients for our api
(getLogs :<|> postLog :<|> getLogById) = client logApi

-- Generate Swagger specification of api
swaggerDocs :: Swagger
swaggerDocs = toSwagger logApi
  • Types specific enough to generate clients and Swagger API specification
  • Swagger specification can generate clients in many languages
  • Type-checked documentation, never out of sync!

Swagger Docs Generated for LogApi

Swagger Docs Generated for LogApi

Swagger Docs Generated for LogApi

Functional Reactive Programming

Reflex – a FRP Library for Haskell

  • Web bindings through reflex-dom
    • Haskell code compiled to Javascript via GHCJS
  • FRP abstractions from Reflex:
    • Behavior - value as a function of time
    • Event - stream of discrete values
    • Dynamic - some combination of the above

Point of Order

Many of the following slides will have the format: code snippet followed by the rendered results of executing that code in the DOM.

-- haskell code snippet that executes
-- changes to the DOM, results of which
-- would be rendered below

divs like this are results of executing code snippets

Reflex Example (1)

1
2
3
start :: MonadWidget t m => m ()
start = do
  el "div" (text "hello")

Maps and Folds

Some useful functions:

1
2
3
4
5
6
7
8
fmap :: (a -> b) -> [a] -> [b]
fmap = ...

fold :: (a -> b -> b) -> b -> [a] -> b
fold = ...

const :: a -> b -> a
const = ...
>>> fmap (plus 5) [0,3]
[5,8]

>>> fold plus 0 [1,2,3,4]
10 -- == 0 + 1 + 2 + 3 + 4

>>> const "foo" "bar"
"foo"

Reflex Example (2)

1
2
3
4
5
6
7
8
start :: MonadWidget t m => m ()
start = mdo
  inp <- mdlInput ""                  -- create input element
  let inpEv   = _textInput_input inp  -- grab the keypress events

  inpValDyn <- foldDyn const "" inpEv -- build dynamic from input events

  el "div" (display inpValDyn)        -- render contents of above dynamic

Reflex Example (3)

1
2
3
4
5
6
7
8
9
10
11
12
start :: MonadWidget t m => m ()
start = mdo
  inp <- mdlInput' "" clickEv                      -- create input element
  b   <- btn "clear"                               -- create button

  let inpEv   = _textInput_input inp               -- grab input events
      clickEv = fmap (const "") (domEvent Click b) -- grab button click events
      combEv  = appendEvents clickEv inpEv         -- merge input and click events

  inpValDyn <- foldDyn const "" combEv             -- create dynamic over combined events

  el "div" (display inpValDyn)                     -- render contents of dynammic

XSS – Executing User Code Within the Browser

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
start :: MonadWidget t m => m ()
start = grid $ do
  cell2 blank
  cell8 $ do
    let defInp  = "<span>spooky user input</span>"

    inp <- mdlInput defInp                                 -- create input element
    let inpEv   = _textInput_input inp                     -- grab input events

    safeDyn   <- foldDyn (\n _ -> sanitize n) defInp inpEv -- dynamic with sanitized input
    unsafeDyn <- foldDyn const defInp inpEv                -- dynamic with raw input

    grid $ do
      cell5 $ mdlTitleCard "Sanitized"    "clsf"   $ elDynHtml' "span" safeDyn
      cell2 blank
      cell5 $ mdlTitleCard "Un-Sanitized" "clunsf" $ elDynHtml' "span" unsafeDyn
    blank
  cell2 blank

XSS – Wrapping a Library for Safety

1
2
3
4
5
6
7
-- unsafe function which is hidden from library users
elDynHtmlUnsafe :: MonadWidget t m => Text -> Dynamic t Text -> m (El t)
elDynHtmlUnsafe e = ...

-- safe version of elDynHtmlUnsafe (only this function is exposed to users)
elDynHtml :: MonadWidget t m => Text -> Dynamic t (UserInput Clean) -> m (El t)
elDynHtml e = elDynHtmlUnsafe e . fmap getInput

Same idea as database example – potentially unsafe functions now only accept properly sanitized input

Complete XSS Example – Server

1
2
3
4
5
6
7
8
9
10
11
12
type SanitizeApi =
       "sanitize" :> ReqBody '[PlainText] Text :> Post '[PlainText] Text -- POST for sanitization
  :<|> Raw                                                               -- serve static content

sanitizer :: Text -> Handler Text                                        -- Servant handler that
sanitizer = return . sanitize                                            -- wrap our friend sanitize

endpoints :: Server SanitizeApi
endpoints = sanitizer :<|> serveDirectory "static"                       -- the server

main :: IO ()
main = run 8080 $ serve (Proxy :: Proxy SanitizeApi) endpoints           -- run the thing

Simple server serves some static content (index.html, css, js) and provides a post function to sanitize content

Complete XSS Example – Sanitize Request

1
2
3
4
5
6
7
8
9
10
11
12
sanitize :: MonadWidget t m => Event t (UserInput Dirty) -> m (Event t (UserInput Clean))
sanitize inp = do
  evResp <- performRequestAsync $ fmap makeReq inp        -- build a XhrRequest and send it

  let evInp = _xhrResponse_responseText <$> evResp        -- when the XhrResponse Event fires, wrap
  return $ fmap (maybe (UserInput "") UserInput) evInp    -- up in the correct UserInput type

makeReq :: UserInput Dirty -> XhrRequest Text             -- plumbing for building up the XhrRequest
makeReq inp =
  xhrRequest
    "POST" "/sanitize"
    (def {_xhrRequestConfig_sendData = (getInput inp)} )

Upon every key press, we send the input back to the server to sanitize it.

Complete XSS Example – Demo

docker run -p 8080:8080 --rm -it mmaz/secdev /bin/bash -c "cd /root/examples/reflex-ghcjs-server; stack exec server"

Ex 5: Type-Level Functions

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
data Democrat   = Obama   | LBJ                     -- create some enums
data Republican = Lincoln | Eisenhower

class (Policy p) => Politician p where              -- define Policy, scoped to specific party
  data Policy p :: *
  govern :: p -> Policy p

instance Politician Democrat where                  -- define Democrats, with their policies
  data Policy Democrat = Obamacare | CivilRights
  govern Obama = Obamacare
  govern LBJ   = CivilRights

instance Politician Republican where                -- define Republicans, with their policies
  data Policy Republican = EstablishNASA | ThirteenthAmendment
  govern Lincoln    = ThirteenthAmendment
  govern Eisenhower = EstablishNASA

data Strategy = Subsidize | Amend | Legislate       -- one more enum

class (Politician p) => Enact p where               -- politicians are only allowed to enact
  enact :: p -> Strategy                            -- their own policies

instance Enact Democrat where
  enact p = case govern p of                        -- type level determination of allowed
    Obamacare   -> Subsidize                        -- policies for Democrats
    CivilRights -> Legislate

instance Enact Republican where                     -- type level determination of allowed
  enact p = case govern p of                        -- policies for Republicans
    ThirteenthAmendment -> Amend
    EstablishNASA       -> Subsidize

Type-Level Functions

TypeFamilies and Proxy let Servant compute Authentication types

type AuthAPI = "private" :> AuthProtect "cookie-auth" :> PrivateAPI
          :<|> "public"  :> PublicApi

-- Type Function to compute the type of data returned after authentication
type instance AuthServerData (AuthProtect "cookie-auth") = Account

TypeFamilies allow Servant to have multiple authentication schemes protecting an API

Resources

Supplementary Topics

Don’t Mix IO

This is not the Haskell way:

insertDB(Row, "foo");
result = Network.request("bar");
tryLock { myCriticalVar = result; }
catch {blah}

Simple Example: Shared State

  • increment the number of us in yuuuuge
$ curl localhost:8080/yuge/1
"not yuge enough!"
$ curl localhost:8080/yuge/2
"yuuge"
$ curl localhost:8080/yuge/7
"yuuuuuuuge"
$ curl localhost:8080/yuge/5
"not yuuuuuuuge enough!"

What did we last set yuge to?

$ curl localhost:8080/yuge
{"pronunciation":"yuuuuuuuge","howyuge":7}

Make a variable in Haskell

data Yuge = Yuge {
  howyuge :: Int
, pronunciation :: Text
} deriving (Generic)
instance ToJSON Yuge

type MyStore = TVar Yuge
Yuge {
   howyuge = 3
   pronunciation = "yuuuge"
}                    ^^^


MyStore = STM container for Yuge
  • MyStore is like a variable, except better
  • howyuge and pronunciation will never have a race condition
  • STM: “just-works” concurrency
    • no event loop spaghetti
    • no locking orders

How do we incorporate this in Servant?

makeYuge :: Int -> Yuge
makeYuge numUs = Yuge numUs ("y" <> uuu <> "ge")
  where uuu = T.pack $ replicate numUs 'u'

tryIncreasingYuge :: Int
                  -> MyStore
                  -> ExceptT ServantErr STM Yuge
tryIncreasingYuge requestedUs yugeStore = do
  currentYuge <- read yugeStore
  if requestedUs <= howyuge currentYuge
    then throwError
      err501 { "not " <> currentYuge <>  " enough!"}
    else do
      let newyuge = makeYuge requestedUs
      write yugeStore newyuge
      return newyuge
makeYuge(numUs) {
  Yuge(numUs, ("y" + 'u' * numUs + "ge"))
} -- returns a Yuge(int, text)

tryIncreasingYuge :: number of Us
                  -> global variable
                  -> ExceptT ServantErr STM Yuge
tryIncreasingYuge(requestedUs, yugeStore) {
  try to increase yugeStore:
  if requestedYuge < yugeStore
      then error msg
      else (1) perform the update
           (2) return the new Yuge
}

Let us first understand this return type

tryIncreasingYuge :: Int -> MyStore -> ExceptT ServantErr STM Yuge
tryIncreasingYuge requestedYuge yugeStore = ???

Understanding Big Types

Understanding Big Types

Understanding Big Types

Understanding Big Types

Understanding Big Types

How do we incorporate this in Servant?

makeYuge :: Int -> Yuge
makeYuge numUs = Yuge numUs ("y" <> uuu <> "ge")
  where uuu = T.pack $ replicate numUs 'u'

tryIncreasingYuge :: Int
                  -> MyStore
                  -> ExceptT ServantErr STM Yuge
tryIncreasingYuge requestedUs yugeStore = do
  currentYuge <- read yugeStore
  if requestedUs <= howyuge currentYuge
    then throwError
      err501 { "not " <> currentYuge <>  " enough!"}
    else do
      let newyuge = makeYuge requestedUs
      write yugeStore newyuge
      return newyuge
makeYuge(numUs) {
  Yuge(numUs, ("y" + 'u' * numUs + "ge"))
} -- returns a Yuge(int, text)

tryIncreasingYuge :: number of Us
                  -> global variable
                  -> ExceptT ServantErr STM Yuge
tryIncreasingYuge(requestedUs, yugeStore) {
  currentYuge <- read yugeStore
  if requestedUs <= currentYuge
    then throwError
      err = current # of 'U's too small
    else do
      let newyuge = makeYuge requestedUs
      store and return the update
}

The benefit

  • Types determine what operations are permitted
    • In the STM monad you can’t do network or database IO
  • Composable “separation of concerns”

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

How do we call this from a Servant handler?

setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
  yugeStore <- ask
  pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
  • Servant handlers are in IO. This means we have to hoist our monad stack.

These are generic functions!