Portability | portable |
---|---|

Stability | experimental |

Maintainer | erkokl@gmail.com |

Safe Haskell | Safe-Infered |

An implementation of AES (Advanced Encryption Standard), using SBV. For details on AES, see FIPS-197: http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf.

We do a T-box implementation, which leads to good C code as we can take advantage of look-up tables. Note that we make virtually no attempt to optimize our Haskell code. The concern here is not with getting Haskell running fast at all. The idea is to program the T-Box implementation as naturally and clearly as possible in Haskell, and have SBV's code-generator generate fast C code automatically. Therefore, we merely use ordinary Haskell lists as our data-structures, and do not bother with any unboxing or strictness annotations. Thus, we achieve the separation of concerns: Correctness via clairty and simplicity and proofs on the Haskell side, performance by relying on SBV's code generator. If necessary, the generated code can be FFI'd back into Haskell to complete the loop.

All 3 valid key sizes (128, 192, and 256) as required by the FIPS-197 standard are supported.

- type GF28 = SWord8
- gf28Mult :: GF28 -> GF28 -> GF28
- gf28Pow :: GF28 -> Int -> GF28
- gf28Inverse :: GF28 -> GF28
- type State = [SWord32]
- type Key = [SWord32]
- type KS = (Key, [Key], Key)
- toBytes :: SWord32 -> [GF28]
- fromBytes :: [GF28] -> SWord32
- rotR :: [GF28] -> Int -> [GF28]
- roundConstants :: [GF28]
- invMixColumns :: State -> State
- keyExpansion :: Int -> Key -> [Key]
- sboxTable :: [GF28]
- sbox :: GF28 -> GF28
- unSBoxTable :: [GF28]
- unSBox :: GF28 -> GF28
- sboxInverseCorrect :: GF28 -> SBool
- addRoundKey :: Key -> State -> State
- t0Func :: GF28 -> [GF28]
- t0 :: GF28 -> SWord32
- t1 :: GF28 -> SWord32
- t2 :: GF28 -> SWord32
- t3 :: GF28 -> SWord32
- u0Func :: GF28 -> [GF28]
- u0 :: GF28 -> SWord32
- u1 :: GF28 -> SWord32
- u2 :: GF28 -> SWord32
- u3 :: GF28 -> SWord32
- doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> State
- aesRound :: Bool -> State -> Key -> State
- aesInvRound :: Bool -> State -> Key -> State
- aesKeySchedule :: Key -> (KS, KS)
- aesEncrypt :: [SWord32] -> KS -> [SWord32]
- aesDecrypt :: [SWord32] -> KS -> [SWord32]
- t128Enc :: [SWord32]
- t128Dec :: [SWord32]
- t192Enc :: [SWord32]
- t192Dec :: [SWord32]
- t256Enc :: [SWord32]
- t256Dec :: [SWord32]
- aes128IsCorrect :: (SWord32, SWord32, SWord32, SWord32) -> (SWord32, SWord32, SWord32, SWord32) -> SBool
- cgAES128BlockEncrypt :: IO ()
- aes128LibComponents :: [(String, SBVCodeGen ())]
- cgAES128Library :: IO ()

# Formalizing GF(2^8)

An element of the Galois Field 2^8, which are essentially polynomials with maximum degree 7. They are conveniently represented as values between 0 and 255.

gf28Mult :: GF28 -> GF28 -> GF28Source

Multiplication in GF(2^8). This is simple polynomial multipliation, followed
by the irreducible polynomial `x^8+x^5+x^3+x^1+1`

. We simply use the `pMult`

function exported by SBV to do the operation.

gf28Pow :: GF28 -> Int -> GF28Source

Exponentiation by a constant in GF(2^8). The implementation uses the usual square-and-multiply trick to speed up the computation.

gf28Inverse :: GF28 -> GF28Source

Computing inverses in GF(2^8). By the mathematical properties of GF(2^8)
and the particular irreducible polynomial used `x^8+x^5+x^3+x^1+1`

, it
turns out that raising to the 254 power gives us the multiplicative inverse.
Of course, we can prove this using SBV:

`>>>`

Q.E.D.`prove $ \x -> x ./= 0 ==> x `gf28Mult` gf28Inverse x .== 1`

Note that we exclude `0`

in our theorem, as it does not have a
multiplicative inverse.

# Implementing AES

## Types and basic operations

AES state. The state consists of four 32-bit words, each of which is in turn treated as four GF28's, i.e., 4 bytes. The T-Box implementation keeps the four-bytes together for efficient representation.

The key, which can be 128, 192, or 256 bits. Represented as a sequence of 32-bit words.

type KS = (Key, [Key], Key)Source

The key schedule. AES executes in rounds, and it treats first and last round keys slightly differently than the middle ones. We reflect that choice by being explicit about it in our type. The length of the middle list of keys depends on the key-size, which in turn determines the number of rounds.

fromBytes :: [GF28] -> SWord32Source

Conversion from 4 bytes, back to a 32-bit row, inverse of `toBytes`

above. We
have the following simple theorems stating this relationship formally:

`>>>`

Q.E.D.`prove $ \a b c d -> toBytes (fromBytes [a, b, c, d]) .== [a, b, c, d]`

`>>>`

Q.E.D.`prove $ \r -> fromBytes (toBytes r) .== r`

## The key schedule

roundConstants :: [GF28]Source

Definition of round-constants, as specified in Section 5.2 of the AES standard.

invMixColumns :: State -> StateSource

The `InvMixColumns`

transformation, as described in Section 5.3.3 of the standard. Note
that this transformation is only used explicitly during key-expansion in the T-Box implementation
of AES.

keyExpansion :: Int -> Key -> [Key]Source

Key expansion. Starting with the given key, returns an infinite sequence of words, as described by the AES standard, Section 5.2, Figure 11.

## The S-box transformation

The values of the AES S-box table. Note that we describe the S-box programmatically using the mathematical construction given in Section 5.1.1 of the standard. However, the code-generation will turn this into a mere look-up table, as it is just a constant table, all computation being done at "compile-time".

The sbox transformation. We simply select from the sbox table. Note that we
are obliged to give a default value (here `0`

) to be used if the index is out-of-bounds
as required by SBV's `select`

function. However, that will never happen since
the table has all 256 elements in it.

## The inverse S-box transformation

unSBoxTable :: [GF28]Source

The values of the inverse S-box table. Again, the construction is programmatic.

## AddRoundKey transformation

addRoundKey :: Key -> State -> StateSource

Adding the round-key to the current state. We simply exploit the fact that addition is just xor in implementing this transformation.

## Tables for T-Box encryption

## Tables for T-Box decryption

## AES rounds

doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> StateSource

Generic round function. Given the function to perform one round, a key-schedule, and a starting state, it performs the AES rounds.

aesRound :: Bool -> State -> Key -> StateSource

One encryption round. The first argument indicates whether this is the final round or not, in which case the construction is slightly different.

aesInvRound :: Bool -> State -> Key -> StateSource

One decryption round. Similar to the encryption round, the first argument indicates whether this is the final round or not.

# AES API

aesKeySchedule :: Key -> (KS, KS)Source

Key schedule. Given a 128, 192, or 256 bit key, expand it to get key-schedules for encryption and decryption. The key is given as a sequence of 32-bit words. (4 elements for 128-bits, 6 for 192, and 8 for 256.)

aesEncrypt :: [SWord32] -> KS -> [SWord32]Source

Block encryption. The first argument is the plain-text, which must have
precisely 4 elements, for a total of 128-bits of input. The second
argument is the key-schedule to be used, obtained by a call to `aesKeySchedule`

.
The output will always have 4 32-bit words, which is the cipher-text.

aesDecrypt :: [SWord32] -> KS -> [SWord32]Source

Block decryption. The arguments are the same as in `aesEncrypt`

, except
the first argument is the cipher-text and the output is the corresponding
plain-text.

# Test vectors

## 128-bit enc/dec test

128-bit encryption test, from Appendix C.1 of the AES standard:

`>>>`

["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]`map hex t128Enc`

128-bit decryption test, from Appendix C.1 of the AES standard:

`>>>`

["00112233","44556677","8899aabb","ccddeeff"]`map hex t128Dec`

## 192-bit enc/dec test

192-bit encryption test, from Appendix C.2 of the AES standard:

`>>>`

["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]`map hex t192Enc`

192-bit decryption test, from Appendix C.2 of the AES standard:

`>>>`

["00112233","44556677","8899aabb","ccddeeff"]`map hex t192Dec`

## 256-bit enc/dec test

256-bit encryption, from Appendix C.3 of the AES standard:

`>>>`

["8ea2b7ca","516745bf","eafc4990","4b496089"]`map hex t256Enc`

256-bit decryption, from Appendix C.3 of the AES standard:

`>>>`

["00112233","44556677","8899aabb","ccddeeff"]`map hex t256Dec`

# Verification

While SMT based technologies can prove correct many small properties fairly quickly, it would be naive for them to automatically verify that our AES implementation is correct. (By correct, we mean decryption follewed by encryption yielding the same result.) However, we can state this property precisely using SBV, and use quick-check to gain some confidence.

:: (SWord32, SWord32, SWord32, SWord32) | plain-text words |

-> (SWord32, SWord32, SWord32, SWord32) | key-words |

-> SBool | True if round-trip gives us plain-text back |

Correctness theorem for 128-bit AES. Ideally, we would run:

prove aes128IsCorrect

to get a proof automatically. Unfortunately, while SBV will successfully generate the proof obligation for this theorem and ship it to the SMT solver, it would be naive to expect the SMT-solver to finish that proof in any reasonable time with the currently available SMT solving technologies. Instead, we can issue:

quickCheck aes128IsCorrect

and get some degree of confidence in our code. Similar predicates can be easily constructed for 192, and 256 bit cases as well.

# Code generation

We have emphasized that our T-Box implementation in Haskell was guided by clarity and correctness, not performance. Indeed, our implementation is hardly the fastest AES implementation in Haskell. However, we can use it to automatically generate straight-line C-code that can run fairly fast.

For the purposes of illustration, we only show here how to generate code for a 128-bit AES block-encrypt
function, that takes 8 32-bit words as an argument. The first 4 are the 128-bit input, and the final
four are the 128-bit key. The impact of this is that the generated function would expand the key for
each block of encryption, a needless task unless we change the key in every block. In a more serios application,
we would instead generate code for both the `aesKeySchedule`

and the `aesEncrypt`

functions, thus reusing the
key-schedule over many applications of the encryption call. (Unfortunately doing this is rather cumbersome right
now, since Haskell does not support fixed-size lists.)

cgAES128BlockEncrypt :: IO ()Source

Code generation for 128-bit AES encryption.

The following sample from the generated code-lines show how T-Boxes are rendered as C arrays:

static const SWord32 table1[] = { 0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL, 0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL, 0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL, 0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL, ... }

The generated program has 5 tables (one sbox table, and 4-Tboxes), all converted to fast C arrays. Here is a sample of the generated straightline C-code:

const SWord8 s1915 = (SWord8) s1912; const SWord8 s1916 = table0[s1915]; const SWord16 s1917 = (((SWord16) s1914) << 8) | ((SWord16) s1916); const SWord32 s1918 = (((SWord32) s1911) << 16) | ((SWord32) s1917); const SWord32 s1919 = s1844 ^ s1918; const SWord32 s1920 = s1903 ^ s1919;

The GNU C-compiler does a fine job of optimizing this straightline code to generate a fairly efficient C implementation.

# C-library generation

The `cgAES128BlockEncrypt`

example shows how to generate code for 128-bit AES encryption. As the generated
function performs encryption on a given block, it performs key expansion as necessary. However, this is
not quite practical: We would like to expand the key only once, and encrypt the stream of plain-text blocks using
the same expanded key (potentially using some crypto-mode), until we decide to change the key. In this
section, we show how to use SBV to instead generate a library of functions that can be used in such a scenario.
The generated library is a typical `.a`

archive, that can be linked using the C-compiler as usual.

aes128LibComponents :: [(String, SBVCodeGen ())]Source

Components of the AES-128 implementation that the library is generated from

cgAES128Library :: IO ()Source

Generate a C library, containing functions for performing 128-bit enc*dec*key-expansion.
A note on performance: In a very rough speed test, the generated code was able to do
6.3 million block encryptions per second on a decent MacBook Pro. On the same machine, OpenSSL
reports 8.2 million block encryptions per second. So, the generated code is about 25% slower
as compared to the highly optimized OpenSSL implementation. (Note that the speed test was done
somewhat simplistically, so these numbers should be considered very rough estimates.)