Saturday, December 29, 2012

Phantom types for crypto keys

Phantom types and GADTs are well-known techniques in Haskell for helping build programs that enforce certain kinds of type refinement: they essentially are used to help serve witness to some type equality. This type equality generally enforces constraints on the nature of your code. In the case of GADTs, your witnesses are the data type constructors (which actually carry around an equality constraint,) and with phantom types, you typically build valid terms from an encapsulated data type, using provided APIs.

While working on salt I recently found the types I used for various key types to be a bit inexpressive. I want the library to be type safe in a way that avoids common misusage, and helps the user write correct code: the API should be explanatory and simple.

My old API looked like this:

newtype PublicKey = PublicKey { unPublicKey :: ByteString } deriving ...
newtype SecretKey = SecretKey { unSecretKey :: ByteString } deriving ...

type KeyPair = (PublicKey, SecretKey)

And then you had things like the public-key encryption API, which looked like:

createKeypair :: IO KeyPair
encrypt :: Nonce       -- Nonce
        -> ByteString  -- Plaintext
        -> PublicKey   -- Receiver public key
        -> SecretKey   -- Sender secret key
        -> ByteString  -- Ciphertext

I thought for a little bit and eventually came up with a key API that is shared for all interfaces, very minimal and a bit more explanatory. I took the idea from repa: to tag the type constructor with type variables, and use them for distinguishing the kind of data.

So the new API looks like this:

newtype Key s i = Key { unKey :: ByteString }

data Public
data Secret

type KeyPair i = (Key Public i, Key Secret i)

And now encryption looks like this:

data PublicEncryptionKey
createKeypair :: IO (KeyPair PublicEncryptionKey)
encrypt :: Nonce
        -> ByteString
        -> Key Public PublicEncryptionKey
        -> Key Secret PublicEncryptionKey
        -> ByteString

The API is a bit wordier, but for the most part, keys will be either parametric in the key types or the key type is fixed for an API, so there’s not too much need to be so specific I imagine.

I actually like this new API quite a bit because it’s easy to see at a glance what a key is for, and type-checking makes sure you won’t make simple mistakes. It’s also quite self-explanatory, I think.

I’m working on reducing the wordiness of imports and the APIs further, so hopefully this can be improved on.

Sunday, December 16, 2012

Math test

This is a test of MathJax. $$ \newcommand{\zero}{\mathsf{z}} \newcommand{\succ}[1]{\mathsf{s}({#1})} \newcommand{\iter}[4]{\mathsf{iter}({#1}, \zero \to {#2}, \succ{#3} \to {#4})} \begin{array}{lcl} A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \bnfalt \N \\ e & ::= & () \bnfalt (e, e) \bnfalt \fst{e} \bnfalt \snd{e} \bnfalt \fun{x}{e} \bnfalt e \; e' \\ & | & \zero \bnfalt \succ{e} \bnfalt \iter{e}{e_z}{x}{e_s} \bnfalt x \bnfalt e : A \\ \Gamma & ::= & \cdot \bnfalt \Gamma, x:A \end{array} $$ $$ \begin{array}{cc} \frac{ x:A \in \Gamma } { \judge{\Gamma}{x}{A} } & \frac{ } {\judge{\Gamma}{()}{1}} \\[1em] \frac{\judge{\Gamma}{e_1}{A_1} \qquad \judge{\Gamma}{e_2}{A_2}} {\judge{\Gamma}{(e_1, e_2)}{A_1 \times A_2}} & \frac{\judge{\Gamma}{e}{A_1 \times A_2}} {\judge{\Gamma}{\pi_i(e)}{A_i}} \\[1em] \frac{\judge{\Gamma, x:A}{e}{B}} {\judge{\Gamma}{\fun{x}{e}}{A \to B}} & \frac{\judge{\Gamma}{e}{A \to B} \qquad \judge{\Gamma}{e'}{A}} {\judge{\Gamma}{e\;e'}{B}} \\[1em] \frac{ } {\judge{\Gamma}{\zero}{\N}} & \frac{\judge{\Gamma}{e}{\N} } {\judge{\Gamma}{\succ{e}}{\N}} \\[1em] \frac{\begin{array}{l} \judge{\Gamma}{e}{\N} \\ \judge{\Gamma}{e_z}{A} \\ \judge{\Gamma, x:A}{e_s}{A} \end{array}} {\judge{\Gamma}{\iter{e}{e_z}{x}{e_s}}{A}} & \frac{\judge{\Gamma}{e}{A}} {\judge{\Gamma}{(e:A)}{A}} \end{array} $$ ​It seems to work!

Tuesday, April 17, 2012

Random updates

It's been a while since I've posted and hopefully I will begin changing that, as I think I'll have more stuff to actively write about.

I've gotten a new job. I'm now a Security Researcher at Rapid7, the home of Metasploit/Nexpose. Most of my job is finding ways of detecting remote vulnerabilities in software (think MS12-020 or the recent Samba bug - CVE-2012-1182 - for examples.)

I've begun a few new pages on my website. Appropriately, one of them is a security section where I hope to write down notes about vulnerabilities in my spare time. My main personal security focus is Kernel exploits and that's what's currently up there, but I'll probably keep writing up anything interesting over there. It's separate from this blog, mostly because I feel this place is dedicated more to talking about my personal endeavours in general as opposed to any one specific thing. If anything, I'll just link to anything I write there from right here and give a short blurb.

Hopefully dust won't gather quite as quickly here as it has in the past. But I've said that before.