writing Haskell for a year and a half at MIT Lincoln Laboratory
mazumder@ll.mit.edu
tbraje@ll.mit.edu
Haskell Crash Course
Phantom Types for Enforced Sanitization
Servant – A Web API as a Type
Functional Reactive Programming for the GUI
Make insecure code inexpressible
(inspired by Yaron Minsky’s “Make illegal states unrepresentable”)
GHC
: the Haskell compilerGHCJS
: the Haskell-to-JavaScript compilerLiquidHaskell
: provable propertiesPhantom Types
: lightweight enforcement against SQLi, XSSFunctional Reactive Programming
: callback-free user interfacesTypeFamilies
: type-level programmingSoftware Transactional Memory
: easy concurrency (no locks)docker pull mmaz/secdev
docker pull mmaz/server-secdev
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 -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
$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> emacs AddTwoNumbers.hs
# Alternatively
# vim AddTwoNumbers.hs
# nano AddTwoNumbers.hs
$ secdev> exit #or Ctrl-d
:q Enter
(or Esc :q Enter
)SPC t E e
Ctrl-x Ctrl-c
Ctrl-x
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
Let’s convert this C function to Haskell
don’t need a type signature: still valid Haskell
the function name
a return value C is a definition in Haskell
how do we read a type signature?
still have the function name (like a header file in C)
this is the type
of the argument
to plusfive
Types read left-to-right. argument
type to (“->
”) return
type
name the argument value “x
” in the lexical scope
use “x
” in the function definition
all together: the input type
,
the output type
,
and the name-binding
what about multiple arguments?
the return type
is still rightmost in Haskell
here is the type of the first argument
here is the type of the second argument
so plus
takes two int
s and returns an int
spaces separate name bindings
instead of commas
1 2 3 4 5 6 7 8 |
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
|
plus :: Int -> Int -> Int
IO
action contextplusAndPrint :: Int -> Int -> IO Int
1 2 3 4 5 6 7 8 |
|
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
-- 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"]’
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
)
Your (deeply nested) data model grows as you refactor
You add more cases, you remove old cases
GHC checks exhaustiveness at all use-sites
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
Proofsfpco/store
memcpy
LiquidHaskell
can enforce many security properties - see HeartBleed example:
ucsd-progsys.github.io/liquidhaskell-tutorial/11-case-study-pointers
$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 parameterFloat
, Double
, Int
…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)
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; --')
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
|
(raw SQL statements are in green doublequotes)
1 2 3 4 5 6 7 8 |
|
Sanitization will only work if the developer remembers to call sanitize before every call to insertDB
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
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
|
1 2 3 4 5 6 7 8 |
|
UserInput Dirty
into a UserInput Clean
is sanitize
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 |
|
$ docker run --rm -it mmaz/secdev /bin/bash
$ secdev> stack runghc PhantomTypes.hs
main2
, import safe module, update main
, and discover that you can no longer injectdata 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 Types3
is a Value
Int
is a Type
DataKinds
promotes Value
s to Type
s
foo
and bar
DataKinds
, they’re String
valuesType-level strings promote a route /foo/bar
to a type
Blogpost with details: arow.info/blog/posts/2015-07-10-servant-intro
-- 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"}
-- 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"}
1 2 3 4 5 6 7 8 |
|
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
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
|
$ docker run -p 8080:8080 --rm -it mmaz/secdev /bin/bash
$ secdev> emacs LogApi.hs #edit line 68
$ secdev> stack runghc LogApi.hs
-- Generate clients for our api
(getLogs :<|> postLog :<|> getLogById) = client logApi
-- Generate Swagger specification of api
swaggerDocs :: Swagger
swaggerDocs = toSwagger logApi
reflex-dom
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
1 2 3 |
|
Some useful functions:
1 2 3 4 5 6 7 8 |
|
>>> fmap (plus 5) [0,3]
[5,8]
>>> fold plus 0 [1,2,3,4]
10 -- == 0 + 1 + 2 + 3 + 4
>>> const "foo" "bar"
"foo"
1 2 3 4 5 6 7 8 |
|
1 2 3 4 5 6 7 8 9 10 11 12 |
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
|
1 2 3 4 5 6 7 |
|
Same idea as database example – potentially unsafe functions now only accept properly sanitized input
1 2 3 4 5 6 7 8 9 10 11 12 |
|
Simple server serves some static content (index.html, css, js) and provides a post function to sanitize content
1 2 3 4 5 6 7 8 9 10 11 12 |
|
Upon every key press, we send the input back to the server to sanitize it.
docker run -p 8080:8080 --rm -it mmaz/secdev /bin/bash -c "cd /root/examples/reflex-ghcjs-server; stack exec server"
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 |
|
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
This is not the Haskell way:
insertDB(Row, "foo");
result = Network.request("bar");
tryLock { myCriticalVar = result; }
catch {blah}
u
s 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}
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 betterhowyuge
and pronunciation
will never have a race conditionmakeYuge :: 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 = ???
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
}
setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.setYuge :: Int -> ReaderT MyStore (ExceptT ServantErr IO) Text
setYuge requestedUs = do
yugeStore <- ask
pronunciation <$> lift (hoist atomically (tryIncreasingYuge requestedUs yugeStore))
hoist
our monad stack.