SHA1 SAW Example

broken_sha1.c

#include <stdint.h>
#include <string.h>
#include <stdlib.h>
#include <stdio.h>

uint32_t ROL(uint32_t val, uint32_t shift) {
  shift &= 0x1f;
  val = (val >> (0x20 - shift)) | (val << shift);
  return val;
}

void sha1_calcHashBuf(const char *input, size_t length, uint32_t *result) {
  void *dataptr = malloc(1024);
  memset(dataptr, 0, 1024);
  uint32_t *data = (uint32_t *) dataptr;
  memcpy(data, input, length);

  for (int i = 16; i < 80; i++) {
    data[i] = ROL(1, (int) (data[i-16] ^ data[i-8] ^ data[i-14] ^ data[i-3]) % 32);
  }

  uint32_t A = 0x67452301;
  uint32_t B = 0xefcdab89;
  uint32_t C = 0x98badcfe;
  uint32_t D = 0x10325476;
  uint32_t E = 0xc3d2e1f0;

  uint32_t temp = 0;
  for (int i = 0; i < 20; i++) {
    temp = *data++ + ROL(A, 5) + E + ((B & C) | (~B & D)) + 0x5a827999;
    E = D;
    D = C;
    C = ROL(B, 30);
    B = A;
    A = temp;
  }

  for (int i = 0; i < 20; i++) {
    temp = (D ^ C ^ B) + E + ROL(temp, 5) + *data++ + 0x6ed9eba1;
    E = D; D = C; C = ROL(B, 30); B = A; A = temp;
  }

  for (int i = 0; i < 20; i++) {
    temp = *data++ + ROL(temp, 5) + E + ((C & B) | (D & C) | (D & B)) - 0x70E44324;
    E = D; D = C; C = ROL(B, 30); B = A; A = temp;
  }

  for (int i = 0; i < 20; i++) {
    temp = (D ^ C ^ B) + E + ROL(temp, 5) + *data++ - 0x359d3e2a;
    E = D; D = C; C = ROL(B, 30); B = A; A = temp;
  }

  result[0] = A + 0x67452301;
  result[1] = B + 0xefcdab89;
  result[2] = C + 0x98badcfe;
  result[3] = D + 0x10325476;
  result[4] = E + 0xc3d2e1f0;

  free(dataptr);
}

char *sha1(char *input) {
  uint32_t result[5];
  sha1_calcHashBuf(input, strlen(input), (uint32_t *)result);
  char *output = malloc(40);
  sprintf(output, "%08x%08x%08x%08x%08x", result[0], result[1], result[2], result[3], result[4]);
  return output;
}

int main(int argc, char** argv) {
  char *input = argv[1];
  char *output = sha1(input);
  printf("SHA1 %s: %s\n", input, output);
  return 0;
}

output

$ ~/src/opensource/saw-script/build/bin/saw sha1.saw
Loading module Cryptol
Loading file "sha1.saw"
Loading module Main
[warning] at :1:1--87:48:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:86:24--86:36
  to 20
[warning] at ./sha1.cry:59:5--65:15:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:64:21--64:29
  to 7
[warning] at ./sha1.cry:49:1--52:36:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:49:26--49:33
  to 5
[warning] at ./sha1.cry:49:1--52:36:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:50:26--50:34
  to 6
[warning] at ./sha1.cry:49:1--52:36:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:51:26--51:34
  to 6
[warning] at ./sha1.cry:49:1--52:36:
  Defaulting type parameter 'bits'
             of finite enumeration
             at ./sha1.cry:52:26--52:34
  to 7
saw: user error (Only integer arguments are supported for now.)

sha1.cry

/*
 * Copyright (c) 2004, 2013-2015 Galois, Inc.
 * Distributed under the terms of the BSD3 license (see LICENSE file)
 */

// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-4.htm

sha1 msg = sha1' pmsg
    where
        pmsg = pad(join(msg))

sha1' : {chunks} (fin chunks) => [chunks][512] -> [160]
sha1' pmsg = join (Hs!0)
  where
    Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] #
         [ block(H, split(M))
         | H <- Hs
         | M <- pmsg
         ]

/*
As a summary, a "1" followed by m "0"s followed by a 64-
   bit integer are appended to the end of the message to produce a
   padded message of length 512 * n.  The 64-bit integer is the length
   of the original message.  The padded message is then processed by the
   SHA-1 as n 512-bit blocks.
*/

pad : {msgLen,contentLen,chunks,padding}
     ( fin msgLen
     , 64 >= width msgLen                             // message width fits in a word
     , contentLen == msgLen + 65                      // message + header
     , chunks     == (contentLen+511) / 512
     , padding    == (512 - contentLen % 512) % 512   // prettier if type #'s could be < 0
     , msgLen     == 512 * chunks - (65 + padding)    // redundant, but Cryptol can't yet do the math
     )
     => [msgLen] -> [chunks][512]
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))

f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
       if (0 <= t)  && (t <= 19) then (x && y) ^ (~x && z)
        | (20 <= t) && (t <= 39) then x ^ y ^ z
        | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
        | (60 <= t) && (t <= 79) then x ^ y ^ z
        else error "f: t out of range"

Ks : [80][32]
Ks = [ 0x5a827999 | t <- [0..19]  ]
   # [ 0x6ed9eba1 | t <- [20..39] ]
   # [ 0x8f1bbcdc | t <- [40..59] ]
   # [ 0xca62c1d6 | t <- [60..79] ]

block : ([5][32], [16][32]) -> [5][32]
block ([H0, H1, H2, H3, H4], M) =
 [(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)]
  where
    Ws : [80][32]
    Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1
             | W16 <- drop`{16 - 16} Ws
             | W14 <- drop`{16 - 14} Ws
             | W8  <- drop`{16 - 8}  Ws
             | W3  <- drop`{16 - 3}  Ws
             | t <- [16..79]
             ]
    As = [H0] # TEMP
    Bs = [H1] # As
    Cs = [H2] # [ B <<< 30 | B <- Bs ]
    Ds = [H3] # Cs
    Es = [H4] # Ds
    TEMP : [80][32]
    TEMP = [ (A <<< 5) + f(t, B, C, D) + E + W + K
           | A <- As | B <- Bs | C <- Cs | D <- Ds | E <- Es
           | W <- Ws | K <- Ks
           | t <- [0..79]
           ]


t0 = sha1 "" == 0xda39a3ee5e6b4b0d3255bfef95601890afd80709

// Sample messages and their digests from FIPS180-1 appendix.

t1 = sha1 "abc" == 0xA9993E364706816ABA3E25717850C26C9CD0D89D
t2 = sha1 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" ==
     0x84983E441C3BD26EBAAE4AA1F95129E5E54670F1
t3 = sha1 [ 'a' | i <- [1..1000000] ] ==
     0x34AA973CD4C4DAA4F61EEB2BDBAD27316534016F

property testsPass = [t0, t1, t2, t3] == ~zero

sha1.saw

import "sha1.cry";

l <- llvm_load_module "sha1.bc";
c_sha1_imp <- llvm_extract l "sha1" llvm_pure;

print "C imp <-> Cryptol imp";
let thm1 = {{ \x -> sha1 x == c_sha1_imp x }};
prove_print abc thm1;