diff --git a/Dockerfile.nsym b/Dockerfile.nsym index 03d5a08d..173b0a95 100644 --- a/Dockerfile.nsym +++ b/Dockerfile.nsym @@ -9,15 +9,12 @@ ARG GO_VERSION=1.20.1 ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz" RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections RUN apt-get update -RUN apt-get install -y wget unzip git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install -RUN apt-get install -y g++-aarch64-linux-gnu lld +RUN apt-get install -y wget unzip git cmake clang llvm g++-aarch64-linux-gnu lld RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ mkdir $GOROOT && mv go/* $GOROOT && rm $GO_ARCHIVE -RUN pip3 install wllvm -RUN pip3 install psutil -ADD ./SAW/scripts /lc/scripts +ADD ./NSym/scripts /lc/scripts RUN /lc/scripts/docker_install.sh ENV CRYPTOLPATH="../../../cryptol-specs:../../spec" diff --git a/NSym/scripts/docker_install.sh b/NSym/scripts/docker_install.sh new file mode 100755 index 00000000..f6451800 --- /dev/null +++ b/NSym/scripts/docker_install.sh @@ -0,0 +1,30 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip' +YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz' + +mkdir -p /bin /deps + +# fetch Z3 +if [ ! -f /bin/z3 ] +then + mkdir -p /deps/z3 + wget $Z3_URL -O /deps/z3.zip + unzip /deps/z3.zip -d /deps/z3 + cp /deps/z3/*/bin/z3 /bin/z3 +fi + +# # fetch Yices +# if [ ! -f /bin/yices ] +# then +# mkdir -p /deps/yices +# wget $YICES_URL -O /deps/yices.tar.gz +# tar -x -f /deps/yices.tar.gz --one-top-level=/deps/yices +# cp /deps/yices/*/bin/yices /bin/yices +# cp /deps/yices/*/bin/yices-smt2 /bin/yices-smt2 +# fi diff --git a/NSym/scripts/install.sh b/NSym/scripts/install.sh new file mode 100755 index 00000000..36cf74ba --- /dev/null +++ b/NSym/scripts/install.sh @@ -0,0 +1,19 @@ +#!/bin/sh + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +set -ex + +SAW_URL='https://saw-builds.s3.us-west-2.amazonaws.com/saw-0.9.0.99-2023-06-08-ab46c76e0-Linux-x86_64.tar.gz' + +mkdir -p /bin /deps + +# fetch SAW +# This will override the current SAW in the docker in AWS-LC's CI +rm -rf /deps/saw +mkdir -p /deps/saw +wget $SAW_URL -O /deps/saw.tar.gz +tar -x -f /deps/saw.tar.gz --one-top-level=/deps/saw +cp /deps/saw/*/bin/saw /bin/saw +cp /deps/saw/*/bin/cryptol /bin/cryptol diff --git a/NSym/spec/SHA384rec.cry b/NSym/spec/SHA384rec.cry new file mode 100644 index 00000000..3bd25b9a --- /dev/null +++ b/NSym/spec/SHA384rec.cry @@ -0,0 +1,146 @@ +module SHA384rec where + +import Array +type WordArray = Array[64][64] + +type w = 64 +type j = 80 +type wd = w/8 + +H0 = [ 0xcbbb9d5dc1059ed8, 0x629a292a367cd507, 0x9159015a3070dd17, 0x152fecd8f70e5939, + 0x67332667ffc00b31, 0x8eb44a8768581511, 0xdb0c2e0d64f98fa7, 0x47b5481dbefa4fa4] + +K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, + 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, + 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, + 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, + 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, + 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, + 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, + 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, + 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, + 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, + 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, + 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, + 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, + 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, + 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, + 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, + 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, + 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, + 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, + 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] + +S0 : [w] -> [w] +S0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) + +S1 : [w] -> [w] +S1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) + +s0 : [w] -> [w] +s0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) + +s1 : [w] -> [w] +s1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) + +Ch : [w] -> [w] -> [w] -> [w] +Ch x y z = (x && y) ^ (~x && z) + +Maj : [w] -> [w] -> [w] -> [w] +Maj x y z = (x && y) ^ (x && z) ^ (y && z) + +messageSchedule_Common_rec : [16][w] -> [j][w] +messageSchedule_Common_rec Mi = messageSchedule_Common_helper Mi 0 zero + +messageSchedule_Common_helper : [16][w] -> Integer -> [j][w] -> [j][w] +messageSchedule_Common_helper Mi ind acc = + if ind >= `j then acc + else if ind < 16 then messageSchedule_Common_helper Mi (ind + 1) (update acc ind (Mi @ ind)) + // The where clause need to be wrapped in parentheses. + // Cryptol is lazy -- it can evaluate the term correctly without the parentheses. + // However, when translating to Ocaml, we lose laziness. + else (messageSchedule_Common_helper Mi (ind + 1) (update acc ind (messageSchedule_Word w1 w2 w3 w4)) + where w1 = acc @ (ind-16) + w2 = acc @ (ind-15) + w3 = acc @ (ind-7) + w4 = acc @ (ind-2)) + +messageSchedule_Word : [w] -> [w] -> [w] -> [w] -> [w] +messageSchedule_Word w1 w2 w3 w4 = w1 + s0 w2 + w3 + s1 w4 + +compress_Common_rec : [8][w] -> [j][w] -> [8][w] +compress_Common_rec H W = compress_Common_helper H W 0 H + +compress_Common_helper : [8][w] -> [j][w] -> Integer -> [8][w] -> [8][w] +compress_Common_helper H W ind acc = + if ind >= `j + then acc + H + else (compress_Common_helper H W (ind+1) [a', b', c', d', e', f', g', h'] + where a = acc @ 0 + b = acc @ 1 + c = acc @ 2 + d = acc @ 3 + e = acc @ 4 + f = acc @ 5 + g = acc @ 6 + h = acc @ 7 + T1 = compress_Common_t1 e f g h (K@ind) (W@ind) + T2 = compress_Common_t2 a b c + h' = g + g' = f + f' = e + e' = compress_Common_e d T1 + d' = c + c' = b + b' = a + a' = compress_Common_a T1 T2) + +compress_Common_t1 : [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] +compress_Common_t1 e f g h kt wt = h + S1 e + Ch e f g + kt + wt + +compress_Common_t2 : [w] -> [w] -> [w] -> [w] +compress_Common_t2 a b c = S0 a + Maj a b c + +compress_Common_e : [w] -> [w] -> [w] +compress_Common_e d T1 = d + T1 + +compress_Common_a : [w] -> [w] -> [w] +compress_Common_a T1 T2 = T1 + T2 + +// processBlock_Common_rec : [8][w] -> [16][w] -> [8][w] +// processBlock_Common_rec H Mi = compress_Common_rec H (messageSchedule_Common_rec Mi) + +processBlock_Common_rec : [8*w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [8*w] +processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 = + join (compress_Common_rec (split H) (messageSchedule_Common_rec Mi)) + where + Mi = [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] + +// processBlock_rec : [8][w] -> ByteArray -> [64] -> [8][w] +// processBlock_rec h block index = +// processBlock_Common_rec h (split (join (arrayRangeLookup block index))) + +// processBlocks_rec : [8][w] -> ByteArray -> [64] -> [64] -> [8][w] +// processBlocks_rec [a, b, c, d, e, f, g, h] data index n = processBlock_rec [a', b', c', d', e', f', g', h'] data index' +// where +// (a', b', c', d', e', f', g', h', index') = processBlocksLoop_rec n data a b c d e f g h index + +// processBlocksLoop_rec : [64] -> ByteArray -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [64] -> ([w], [w], [w], [w], [w], [w], [w], [w], [64]) +// processBlocksLoop_rec num data a b c d e f g h index = if (index + 2 * `w) < (num * 2 * `w) +// then processBlocksLoop_rec num data a' b' c' d' e' f' g' h' (index + 2 * `w) +// else (a, b, c, d, e, f, g, h, index) +// where +// [a', b', c', d', e', f', g', h'] = (processBlock_rec [a, b, c, d, e, f, g, h] data index) + +processBlocks_rec : [64] -> WordArray -> [8*w] +processBlocks_rec num data = + if num == 0 + then join H0 + // The where clause need to be wrapped in parentheses. + // Cryptol is lazy -- it can evaluate the term correctly without the parentheses. + // However, when translating to Ocaml, we lose laziness. + else (processBlock_Common_rec prev_H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where + last_Block = arrayRangeLookup data ((num-1) * 2 * `wd) + prev_H = processBlocks_rec (num - 1) data + [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = last_Block) \ No newline at end of file diff --git a/NSym/spec/SHA384rec.icry b/NSym/spec/SHA384rec.icry new file mode 100644 index 00000000..c17bd786 --- /dev/null +++ b/NSym/spec/SHA384rec.icry @@ -0,0 +1,14 @@ +:l SHA384recEquiv.cry +:prove H0_equiv +:prove K_equiv +:prove S0_equiv +:prove S1_equiv +:prove s0_equiv +:prove s1_equiv +:prove Ch_equiv +:prove Maj_equiv +:prove messageSchedule_Common_equiv +:prove compress_Common_equiv +:prove processBlock_Common_equiv + +:l SHA384rec.cry \ No newline at end of file diff --git a/NSym/spec/SHA384recEquiv.cry b/NSym/spec/SHA384recEquiv.cry new file mode 100644 index 00000000..f7053564 --- /dev/null +++ b/NSym/spec/SHA384recEquiv.cry @@ -0,0 +1,122 @@ +module SHA384recEquiv where + +import Primitive::Keyless::Hash::SHA384 as SHA384 +import SHA384rec as SHA384rec +import Array +import Common::ByteArray + +type WordArray = Array[64][64] +type w = SHA384rec::w +type j = SHA384rec::j + +// The folloing definition is the version copied from SHA384.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, + 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, + 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, + 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, + 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, + 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, + 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, + 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, + 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, + 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, + 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, + 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, + 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, + 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, + 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, + 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, + 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, + 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, + 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, + 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] + +// The folloing definition is the recursive comprehension version copied from SHA384.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +messageSchedule_Common : [16][w] -> [j][w] +messageSchedule_Common Mi = take W + where + W : [inf][_] + W = Mi # [ w1 + SHA384::s0 w2 + w3 + SHA384::s1 w4 + | w1 <- W + | w2 <- drop`{1} W + | w3 <- drop`{9} W + | w4 <- drop`{14} W + ] + +// The folloing definition is the recursive comprehension version copied from SHA384.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +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 + SHA384::S1 e + SHA384::Ch e f g + k_t + w_t + | h <- hs | e <- es | f <- fs | g <- gs | k_t <- SHA384rec::K | w_t <- W] + T2 = [ SHA384::S0 a + SHA384::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]) + +// define equiv properties +property H0_equiv = + SHA384::SHAH0 == SHA384rec::H0 + +property K_equiv = + K == SHA384rec::K + +property S0_equiv (x : [w]) = + SHA384::S0 x == SHA384rec::S0 x + +property S1_equiv (x : [w]) = + SHA384::S1 x == SHA384rec::S1 x + +property s0_equiv (x : [w]) = + SHA384::s0 x == SHA384rec::s0 x + +property s1_equiv (x : [w]) = + SHA384::s1 x == SHA384rec::s1 x + +property Ch_equiv (x : [w]) (y : [w]) (z : [w])= + SHA384::Ch x y z == SHA384rec::Ch x y z + +property Maj_equiv (x : [w]) (y : [w]) (z : [w])= + SHA384::Maj x y z == SHA384rec::Maj x y z + +property messageSchedule_Common_equiv (Mi : [16][w]) = + messageSchedule_Common Mi == SHA384rec::messageSchedule_Common_rec Mi + +property compress_Common_equiv (H : [8][w]) (W : [j][w]) = + compress_Common H W == SHA384rec::compress_Common_rec H W + +property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = + join (SHA384::processBlock_Common (split H) Mi) == SHA384rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi + +// // This property could not be proved nor checked due to Cryptol's lack of support for Arrays +// // Manual inspection is required +// property processBlock_equiv (h : [8][w]) (block : ByteArray) (index : [64]) = +// SHA384::processBlock h block index == SHA384rec::processBlock_rec h block index + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +// Manual inspection is required +property processBlocks_equiv (data : ByteArray) (data2 : WordArray) (index : [64]) (n : [64]) = + // TODO: state relationship between data and data2 + join (SHA384::processBlocks SHA384rec::H0 data 0 n) == SHA384rec::processBlocks_rec n data2 diff --git a/NSym/spec/SHA512rec.cry b/NSym/spec/SHA512rec.cry new file mode 100644 index 00000000..3b76044e --- /dev/null +++ b/NSym/spec/SHA512rec.cry @@ -0,0 +1,142 @@ +module SHA512rec where + +import Array +type WordArray = Array[64][64] + +type w = 64 +type j = 80 +type wd = w/8 + +H0 = [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1, + 0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179] + +K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, + 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, + 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, + 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, + 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, + 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, + 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, + 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, + 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, + 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, + 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, + 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, + 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, + 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, + 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, + 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, + 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, + 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, + 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, + 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] + +S0 : [w] -> [w] +S0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) + +S1 : [w] -> [w] +S1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) + +s0 : [w] -> [w] +s0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) + +s1 : [w] -> [w] +s1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) + +Ch : [w] -> [w] -> [w] -> [w] +Ch x y z = (x && y) ^ (~x && z) + +Maj : [w] -> [w] -> [w] -> [w] +Maj x y z = (x && y) ^ (x && z) ^ (y && z) + +messageSchedule_Common_rec : [16][w] -> [j][w] +messageSchedule_Common_rec Mi = messageSchedule_Common_helper Mi 0 zero + +messageSchedule_Common_helper : [16][w] -> Integer -> [j][w] -> [j][w] +messageSchedule_Common_helper Mi ind acc = + if ind >= `j then acc + else if ind < 16 then messageSchedule_Common_helper Mi (ind + 1) (update acc ind (Mi @ ind)) + // The where clause need to be wrapped in parentheses. + // Cryptol is lazy -- it can evaluate the term correctly without the parentheses. + // However, when translating to Ocaml, we lose laziness. + else (messageSchedule_Common_helper Mi (ind + 1) (update acc ind (messageSchedule_Word w1 w2 w3 w4)) + where w1 = acc @ (ind-16) + w2 = acc @ (ind-15) + w3 = acc @ (ind-7) + w4 = acc @ (ind-2)) + +messageSchedule_Word : [w] -> [w] -> [w] -> [w] -> [w] +messageSchedule_Word w1 w2 w3 w4 = w1 + s0 w2 + w3 + s1 w4 + +compress_Common_rec : [8][w] -> [j][w] -> [8][w] +compress_Common_rec H W = compress_Common_helper H W 0 H + +compress_Common_helper : [8][w] -> [j][w] -> Integer -> [8][w] -> [8][w] +compress_Common_helper H W ind acc = + if ind >= `j + then acc + H + else (compress_Common_helper H W (ind+1) [a', b', c', d', e', f', g', h'] + where a = acc @ 0 + b = acc @ 1 + c = acc @ 2 + d = acc @ 3 + e = acc @ 4 + f = acc @ 5 + g = acc @ 6 + h = acc @ 7 + T1 = compress_Common_t1 e f g h (K@ind) (W@ind) + T2 = compress_Common_t2 a b c + h' = g + g' = f + f' = e + e' = compress_Common_e d T1 + d' = c + c' = b + b' = a + a' = compress_Common_a T1 T2) + +compress_Common_t1 : [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] +compress_Common_t1 e f g h kt wt = h + S1 e + Ch e f g + kt + wt + +compress_Common_t2 : [w] -> [w] -> [w] -> [w] +compress_Common_t2 a b c = S0 a + Maj a b c + +compress_Common_e : [w] -> [w] -> [w] +compress_Common_e d T1 = d + T1 + +compress_Common_a : [w] -> [w] -> [w] +compress_Common_a T1 T2 = T1 + T2 + +processBlock_Common_rec : [8*w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [8*w] +processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 = join (compress_Common_rec (split H) (messageSchedule_Common_rec Mi)) + where + Mi = [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] + +// processBlock_rec : [8][w] -> ByteArray -> [64] -> [8][w] +// processBlock_rec h block index = +// processBlock_Common_rec h (split (join (arrayRangeLookup block index))) + +// processBlocks_rec : [8][w] -> ByteArray -> [64] -> [64] -> [8][w] +// processBlocks_rec [a, b, c, d, e, f, g, h] data index n = processBlock_rec [a', b', c', d', e', f', g', h'] data index' +// where +// (a', b', c', d', e', f', g', h', index') = processBlocksLoop_rec n data a b c d e f g h index + +// processBlocksLoop_rec : [64] -> ByteArray -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [64] -> ([w], [w], [w], [w], [w], [w], [w], [w], [64]) +// processBlocksLoop_rec num data a b c d e f g h index = if (index + 2 * `w) < (num * 2 * `w) +// then processBlocksLoop_rec num data a' b' c' d' e' f' g' h' (index + 2 * `w) +// else (a, b, c, d, e, f, g, h, index) +// where +// [a', b', c', d', e', f', g', h'] = (processBlock_rec [a, b, c, d, e, f, g, h] data index) + +processBlocks_rec : [64] -> WordArray -> [8*w] +processBlocks_rec num data = + if num == 0 + then join H0 + // The where clause need to be wrapped in parentheses. + // Cryptol is lazy -- it can evaluate the term correctly without the parentheses. + // However, when translating to Ocaml, we lose laziness. + else (processBlock_Common_rec prev_H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where + last_Block = arrayRangeLookup data ((num-1) * 2 * `wd) + prev_H = processBlocks_rec (num - 1) data + [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = last_Block) diff --git a/NSym/spec/SHA512rec.icry b/NSym/spec/SHA512rec.icry new file mode 100644 index 00000000..2aab3d01 --- /dev/null +++ b/NSym/spec/SHA512rec.icry @@ -0,0 +1,14 @@ +:l SHA512recEquiv.cry +:prove H0_equiv +:prove K_equiv +:prove S0_equiv +:prove S1_equiv +:prove s0_equiv +:prove s1_equiv +:prove Ch_equiv +:prove Maj_equiv +:prove messageSchedule_Common_equiv +:prove compress_Common_equiv +:prove processBlock_Common_equiv + +:l SHA512rec.cry \ No newline at end of file diff --git a/NSym/spec/SHA512recEquiv.cry b/NSym/spec/SHA512recEquiv.cry new file mode 100644 index 00000000..45f3881b --- /dev/null +++ b/NSym/spec/SHA512recEquiv.cry @@ -0,0 +1,122 @@ +module SHA512recEquiv where + +import Primitive::Keyless::Hash::SHA512 as SHA512 +import SHA512rec as SHA512rec +import Array +import Common::ByteArray +type WordArray = Array[64][64] + +type w = SHA512rec::w +type j = SHA512rec::j + +// The following definition is the version copied from SHA512.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, + 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, + 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, + 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, + 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, + 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, + 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, + 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, + 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, + 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, + 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, + 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, + 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, + 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, + 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, + 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, + 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, + 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, + 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, + 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] + +// The following definition is the recursive comprehension version copied from SHA512.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +messageSchedule_Common : [16][w] -> [j][w] +messageSchedule_Common Mi = take W + where + W : [inf][_] + W = Mi # [ w1 + SHA512::s0 w2 + w3 + SHA512::s1 w4 + | w1 <- W + | w2 <- drop`{1} W + | w3 <- drop`{9} W + | w4 <- drop`{14} W + ] + +// The following definition is the recursive comprehension version copied from SHA512.cry. +// We have to do this because this definition is not exported. +// Manual inspection is required +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 + SHA512::S1 e + SHA512::Ch e f g + k_t + w_t + | h <- hs | e <- es | f <- fs | g <- gs | k_t <- SHA512rec::K | w_t <- W] + T2 = [ SHA512::S0 a + SHA512::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]) + +// define equiv properties +property H0_equiv = + SHA512::SHAH0 == SHA512rec::H0 + +property K_equiv = + K == SHA512rec::K + +property S0_equiv (x : [w]) = + SHA512::S0 x == SHA512rec::S0 x + +property S1_equiv (x : [w]) = + SHA512::S1 x == SHA512rec::S1 x + +property s0_equiv (x : [w]) = + SHA512::s0 x == SHA512rec::s0 x + +property s1_equiv (x : [w]) = + SHA512::s1 x == SHA512rec::s1 x + +property Ch_equiv (x : [w]) (y : [w]) (z : [w])= + SHA512::Ch x y z == SHA512rec::Ch x y z + +property Maj_equiv (x : [w]) (y : [w]) (z : [w])= + SHA512::Maj x y z == SHA512rec::Maj x y z + +property messageSchedule_Common_equiv (Mi : [16][w]) = + messageSchedule_Common Mi == SHA512rec::messageSchedule_Common_rec Mi + +property compress_Common_equiv (H : [8][w]) (W : [j][w]) = + compress_Common H W == SHA512rec::compress_Common_rec H W + +property processBlock_Common_equiv (H : [8*w]) (Mi : [16][w]) = + join (SHA512::processBlock_Common (split H) Mi) == SHA512rec::processBlock_Common_rec H w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 + where [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15] = Mi + +// // This property could not be proved nor checked due to Cryptol's lack of support for Arrays +// // Manual inspection is required +// property processBlock_equiv (h : [8][w]) (block : ByteArray) (index : [64]) = +// SHA512::processBlock h block index == SHA512rec::processBlock_rec h block index + +// This property could not be proved nor checked due to Cryptol's lack of support for loops and Arrays +// Manual inspection is required +property processBlocks_equiv (data : ByteArray) (data2 : WordArray) (index : [64]) (n : [64]) = + // TODO: state relationship between data and data2 + join (SHA512::processBlocks SHA512rec::H0 data 0 n) == SHA512rec::processBlocks_rec n data2 \ No newline at end of file