SHA.cry

/*
   Copyright (c) 2018, Galois Inc.
   www.cryptol.net
   You can freely use this source code for educational purposes.
*/

module SHA where

sha : {L} (2 * w >= width L) => [L] -> [digest_size]
sha M = take (join (SHA_2_Common' [ split x | x <- parse`{num_blocks L} (pad`{L} M) ]))

parameter

  /** Word size
    Specifications are based on word size w, rather than digest size (8 * w)
    or block size (m == 16 * w), in order to avoid confusing Cryptol's type
    constraint verifier with integer division.
  */

  type w : #
  type constraint (fin w, w >= 2, 32 >= width w)

  type digest_size : #
  type constraint (fin digest_size, 8*w >= digest_size)

  /** The number of iterations in the hash computation
  (i.e. the number of words in K) */

  type j : #
  type constraint (fin j, j >= 17)

  H0 : [8][w]
  K  : [j][w]

  /* FIPS 180-4 defines lowercase and uppercase
      (respective to the Greek alphabet) sigma functions for SHA-256 and SHA-512.
      (4.4)-(4.7) SHA-224, SHA-256 (w==32)
      (4.10)-(4.13) SHA-384, SHA-512, SHA-512/224, SHA-512/256 (w==64) */

  SIGMA_0 : [w] -> [w]
  SIGMA_1 : [w] -> [w]
  sigma_0 : [w] -> [w]
  sigma_1 : [w] -> [w]

// Export some of the parameters
SHAH0 = H0
S0 = SIGMA_0
S1 = SIGMA_1
s0 = sigma_0
s1 = sigma_1

// Export Ch, Maj and the block function to be used in SAW proofs
/** (4.1) (w==32), (4.2) (w==32), (4.8) (w==64) */
Ch : [w] -> [w] -> [w] -> [w]
Ch x y z = (x && y) ^ (~x && z)


/** (4.1) (w==32), (4.3) (w==32), (4.9) (w==64) */
Maj : [w] -> [w] -> [w] -> [w]
Maj x y z = (x && y) ^ (x && z) ^ (y && z)

processBlock_Common : [8][w] -> [16][w] -> [8][w]
processBlock_Common H Mi = compress_Common H (messageSchedule_Common Mi)


private

  /** block size corresponding to word size for all SHA algorithms in
      FIPS 180-4 */
  type block_size = 16 * w

  type num_blocks L     = (L+1+2*w) /^ block_size
  type padded_size L    = num_blocks L * block_size


  /**
    5.1 Padding the Message
    5.1.1 SHA-1, SHA-224 and SHA-256 (w==32)
    5.1.2 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 (w==64)

  The constraint ensure that the message size, `L`, fits within a
  (2 * w)-bit word (consistent w/ Figure 1)
  */
  pad : {L} (2 * w >= width L) => [L] -> [padded_size L]
  pad M = M # 0b1 # zero # (`L : [2*w])

  /**
    5.2 Parsing the Message
    5.2.1 SHA-1, SHA-224 and SHA-256 (w==32)
    5.2.2 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 (w==64)
  */
  parse : {m} [m * block_size] -> [m][block_size]
  parse = split

  /**
  SHA-256 and SHA-512 (and their respective derivatives) use a similar
  message schedule that can be expressed in the same way relative to their
  respective sigma functions.

    6.2.2 SHA-256 Hash Computation (w==32, j=64)
    6.4.2 SHA-512 Hash Computation (w==64, j=80)
  */
  messageSchedule_Common : [16][w] -> [j][w]
  messageSchedule_Common Mi = take W
    where
    W : [inf][_]
    W = Mi # [ w1 + s0 w2 + w3 + s1 w4
             | w1 <- W
             | w2 <- drop`{1} W
             | w3 <- drop`{9} W
             | w4 <- drop`{14} W
             ]


  /**
  Amazon S2N's SHA-256 specification includes a compression routine intended
  to reflect typical implementations.  This same compression routine applies
  to SHA-512, modulo respective constants, sigma functions,
  and message schedules.
  */

  compress_Common : [8][w] -> [j][w] -> [8][w]
  compress_Common H W =
    // XXX: This whole definitions looks like it might be simplifiable.
    [ (as ! 0) + (H @ 0),
      (bs ! 0) + (H @ 1),
      (cs ! 0) + (H @ 2),
      (ds ! 0) + (H @ 3),
      (es ! 0) + (H @ 4),
      (fs ! 0) + (H @ 5),
      (gs ! 0) + (H @ 6),
      (hs ! 0) + (H @ 7)
    ]
    where
      T1 = [h + S1 e + Ch e f g + k_t + w_t
                | h <- hs | e <- es | f <- fs | g <- gs | k_t <- K | w_t <- W]
      T2 = [ S0 a + Maj a b c | a <- as | b <- bs | c <- cs]
      hs = take`{j + 1}([H @ 7] # gs)
      gs = take`{j + 1}([H @ 6] # fs)
      fs = take`{j + 1}([H @ 5] # es)
      es = take`{j + 1}([H @ 4] # [d + t1 | d <- ds | t1 <- T1])
      ds = take`{j + 1}([H @ 3] # cs)
      cs = take`{j + 1}([H @ 2] # bs)
      bs = take`{j + 1}([H @ 1] # as)
      as = take`{j + 1}([H @ 0] # [t1 + t2 | t1 <- T1 | t2 <- T2])


  SHA_2_Common' : {L} (fin L) => [L][16][w] -> [8][w]
  SHA_2_Common' blocks = hash ! 0
    where
    hash = [H0] # [ processBlock_Common h b | h <- hash | b <- blocks]


///////////////////////////////////////////////////////////////////////////////
// SHA imperative specification
///////////////////////////////////////////////////////////////////////////////

/*
 * This section contains an SHA specification that more closely matches the
 * BoringSSL C implementation to simplify SAW correctness proofs of the
 * implementation.
 */

//////// Imperative top level ////////

type SHAState = { h : [8][w]
                , block : [w * 2][8]
                , n : [32]
                , sz : [w * 2]
                }

// Initial state for SHA
SHAInit : SHAState
SHAInit = { h = H0
          , block = zero
          , n = 0
          , sz = 0
          }

// Process message being hashed, iteratively updating the SHA state with the
// input message.
SHAUpdate : {n} (fin n) => SHAState -> [n][8] -> SHAState
SHAUpdate sinit bs = ss!0
  where ss = [sinit] # [ SHAUpdate1 s b | s <- ss | b <- bs ]

// Add padding and size and process the final block.
SHAFinal : SHAState -> [digest_size]
SHAFinal s = take (join (processBlock_Common h b'))
  // Because the message is always made up of bytes, and the size is a
  // fixed number of bytes, the 1 pad will always be at least a byte.
  where s' = SHAUpdate1 s 0x80
        // Don't need to add zeros. They're already there. Just update
        // the count of bytes in this block. After adding the 1 pad, there
        // are two possible cases: the size will fit in the current block,
        // or it won't.
        (h, b) = if s'.n <= (`w*2 - (`w/4)) then (s'.h, s'.block)
                 else (processBlock_Common s'.h (split (join s'.block)), zero)
        b' = split (join b || (zero # s.sz))

// Imperative SHA implementation
SHAImp : {n} (fin n) => [n][8] -> [digest_size]
SHAImp msg = SHAFinal (SHAUpdate SHAInit msg)


private

  // SHAUpdate1 updates a single byte at position s.n in s.block and return a
  // new state to pass to subsequent updates.  If s.n is 128, updates position 0
  // to b and zeros the remainder of the block, setting s.n to 1 for the next
  // update.
  SHAUpdate1 : SHAState -> [8] -> SHAState
  SHAUpdate1 s b =
    if s.n == (2 * `w - 1)
      then { h = processBlock_Common s.h (split (join (update s.block s.n b)))
           , block = zero
           , n = 0
           , sz = s.sz + 8
           }
      else { h = s.h
           , block = update s.block s.n b
           , n = s.n + 1
           , sz = s.sz + 8
           }