From d7f9dd55acd70f549c65c4d36eabc56541f07d2a Mon Sep 17 00:00:00 2001 From: Anna Weine Date: Mon, 7 Nov 2022 18:26:26 +0000 Subject: Bug 1765759 - Removing SAW docker from the NSS build system. r=nss-reviewers,jschanck Differential Revision: https://phabricator.services.mozilla.com/D160237 --- automation/saw/bmul.cry | 8 - automation/saw/bmul.saw | 26 -- automation/saw/chacha20.cry | 357 ---------------------- automation/saw/chacha20.saw | 40 --- automation/saw/poly1305-hacl.saw | 38 --- automation/saw/poly1305.cry | 336 -------------------- automation/saw/poly1305.saw | 47 --- automation/taskcluster/docker-saw/Dockerfile | 46 --- automation/taskcluster/docker-saw/LLVMgold.so.zip | Bin 13558285 -> 0 bytes automation/taskcluster/docker-saw/bin/checkout.sh | 15 - automation/taskcluster/graph/src/extend.js | 73 ----- automation/taskcluster/scripts/run_saw.sh | 9 - 12 files changed, 995 deletions(-) delete mode 100644 automation/saw/bmul.cry delete mode 100644 automation/saw/bmul.saw delete mode 100644 automation/saw/chacha20.cry delete mode 100644 automation/saw/chacha20.saw delete mode 100644 automation/saw/poly1305-hacl.saw delete mode 100644 automation/saw/poly1305.cry delete mode 100644 automation/saw/poly1305.saw delete mode 100644 automation/taskcluster/docker-saw/Dockerfile delete mode 100644 automation/taskcluster/docker-saw/LLVMgold.so.zip delete mode 100644 automation/taskcluster/docker-saw/bin/checkout.sh delete mode 100755 automation/taskcluster/scripts/run_saw.sh (limited to 'automation') diff --git a/automation/saw/bmul.cry b/automation/saw/bmul.cry deleted file mode 100644 index 87303dad6..000000000 --- a/automation/saw/bmul.cry +++ /dev/null @@ -1,8 +0,0 @@ -/* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ - -bmul : {n,m} (fin n, n >= 1, m == n*2 - 1) => [n] -> [n] -> ([n], [n]) -bmul a b = (take`{n} prod, drop`{n} prod) - where prod = pad (pmult a b : [m]) - pad x = zero # x diff --git a/automation/saw/bmul.saw b/automation/saw/bmul.saw deleted file mode 100644 index 22cd2757b..000000000 --- a/automation/saw/bmul.saw +++ /dev/null @@ -1,26 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. - -import "bmul.cry"; - -print "Loading LLVM bitcode..."; -m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc"; - -let SpecBinaryMul n = do { - x <- llvm_var "x" (llvm_int n); - y <- llvm_var "y" (llvm_int n); - llvm_ptr "r_high" (llvm_int n); - r_high <- llvm_var "*r_high" (llvm_int n); - llvm_ptr "r_low" (llvm_int n); - r_low <- llvm_var "*r_low" (llvm_int n); - - let res = {{ bmul x y }}; - llvm_ensure_eq "*r_high" {{ res.0 }}; - llvm_ensure_eq "*r_low" {{ res.1 }}; - - llvm_verify_tactic abc; -}; - -print "Proving equality for 32-bit bmul()..."; -time (llvm_verify m "bmul32" [] (SpecBinaryMul 32)); diff --git a/automation/saw/chacha20.cry b/automation/saw/chacha20.cry deleted file mode 100644 index 0b52d51ad..000000000 --- a/automation/saw/chacha20.cry +++ /dev/null @@ -1,357 +0,0 @@ -/* -** ChaCha20 specification -** Author: Austin Seipp . Released in the Public Domain. -** -** Based on RFC 7539 - "ChaCha20 and Poly1305 for IETF Protocols" -** https://tools.ietf.org/html/rfc7539 -*/ -module chacha20 where - -/* -------------------------------------------------------------------------- */ -/* -- Implementation -------------------------------------------------------- */ - -type Round = [16][32] // An input to the ChaCha20 core function -type Block = [64][8] // An output block from the ChaCha20 core function. -type Key = [32][8] // A 32-byte input key -type Nonce = [12][8] // A 12-byte nonce -type Counter = [32] // Starting block counter. Usually 1 or 0. - -/* ---------------------------------- */ -/* -- Quarter Round ----------------- */ - -// The quarter round. This takes 4 32-bit integers and diffuses them -// appropriately, and is the core of the column and diagonal round. -qround : [4][32] -> [4][32] -qround [ a0, b0, c0, d0 ] = [ a2, b4, c2, d4 ] - where - a1 = a0 + b0 /* a += b; d ^= a; d <<<= 16 */ - d1 = d0 ^ a1 - d2 = d1 <<< 16 - - c1 = c0 + d2 /* c += d; b ^= c; b <<<= 12 */ - b1 = b0 ^ c1 - b2 = b1 <<< 12 - - a2 = a1 + b2 /* a += b; d ^= a; d <<<= 8 */ - d3 = d2 ^ a2 - d4 = d3 <<< 8 - - c2 = c1 + d4 /* c += d; b ^= c; b <<<= 7 */ - b3 = b2 ^ c2 - b4 = b3 <<< 7 - - -/* ---------------------------------- */ -/* -- Column and diagonal rounds ---- */ - -// Perform the column round, followed by the diagonal round on the -// input state, which are both defined in terms of the quarter -// round. ChaCha20 requires 20 total rounds of interleaving -// column/diagonal passes on the state, and therefore `cdround` actually -// does two passes at once (mostly for simplicity). -cdround : Round -> Round -cdround [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 ] - = [ z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15 ] - where - // Column round - [ y0, y4, y8, y12 ] = qround [ x0, x4, x8, x12 ] - [ y1, y5, y9, y13 ] = qround [ x1, x5, x9, x13 ] - [ y2, y6, y10, y14 ] = qround [ x2, x6, x10, x14 ] - [ y3, y7, y11, y15 ] = qround [ x3, x7, x11, x15 ] - - // Diagonal round - [ z0, z5, z10, z15 ] = qround [ y0, y5, y10, y15 ] - [ z1, z6, z11, z12 ] = qround [ y1, y6, y11, y12 ] - [ z2, z7, z8, z13 ] = qround [ y2, y7, y8, y13 ] - [ z3, z4, z9, z14 ] = qround [ y3, y4, y9, y14 ] - - -/* ---------------------------------- */ -/* -- Block encryption -------------- */ - -// Given an input round, calculate the core ChaCha20 algorithm over -// the round and return an output block. These output blocks form the -// stream which you XOR your plaintext with, and successive iterations of -// the core algorithm result in an infinite stream you can use as a -// cipher. -core : Round -> Block -core x = block - where - rounds = iterate cdround x // Do a bunch of column/diagonal passes... - result = rounds @ 10 // And grab the 10th result (20 total passes) - block = blocked (x + result) // Add to input, convert to output block - - -/* ---------------------------------- */ -/* -- Key Expansion ----------------- */ - -// Key expansion. Given a nonce and a key, compute a round (which is -// fed to the core algorithm above) by taking the initial round state and -// mixing in the key and nonce appropriately. -kexp : Key -> Counter -> Nonce -> Round -kexp k c n = [ c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15 ] - where - // The following describes the layout of the output round, which - // is fed into the core algorithm successively. - - // Bytes 0-3: Constants - [ c0, c1, c2, c3 ] = [ 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574 ] - - // Bytes 4-11: Key - [ c4, c5, c6, c7 ] = map rjoin (groupBy`{4} kslice1 : [4][4][8]) : [4][32] - [ c8, c9, c10, c11 ] = map rjoin (groupBy`{4} kslice2 : [4][4][8]) : [4][32] - kslice1 = k @@ ([ 0 .. 15 ] : [16][32]) // Top half - kslice2 = k @@ ([ 16 .. 31 ] : [16][32]) // Bottom half - - // Bytes 12: Counter, starts off with whatever the user specified - // (usually 0 or 1) - [ c12 ] = [ c ] - - // Bytes 14-15: Nonce - [ c13, c14, c15 ] = map rjoin (groupBy`{4} n) - - -/* ---------------------------------- */ -/* -- Round increments -------------- */ - -// Take a given number of iterations and the input round (after key -// expansion!), and calculate the input round for the core algorithm -// function. This allows you to index into a particular Round which -// can be passed to the 'core' function. -iround : [64] -> Round -> Round -iround n r = (iterate once r) @ n where - // Given a round, increment the counter inside (index no 12) - once [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 ] - = [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12+1, x13, x14, x15 ] - -/* ---------------------------------- */ -/* -- ChaCha20 encryption ----------- */ - -// Produce a psuedo-random stream given a nonce and a key, which can -// be XOR'd with your data to encrypt it. -stream : {n} (fin n) => Key -> Counter -> Nonce -> [n][8] -stream k c n = take`{n} (join rounds) // Take n bytes from the final result - where - // Expand key - key = kexp k c n - - // Produce the stream by successively incrementing the input round - // by `i`, and running the core algorithm to get the resulting - // stream for the `i`th input. Once these are concatenated, you have - // an infinite list representing the ChaCha20 stream. - rounds = [ core (iround i key) | i <- [ 0, 1 ... ] ] - - -// Given an message, a nonce, and a key, produce an encrypted -// message. This is simply defined as the XOR of the message and the -// corresponding encryption stream. -encrypt : {n} (fin n) => Key -> Counter -> Nonce -> [n][8] -> [n][8] -encrypt k c n m = m ^ (stream k c n) - -/* -------------------------------------------------------------------------- */ -/* -- Theorems, tests ------------------------------------------------------- */ - -// Tests are private -private - qround01 = qround in == out - where - in = [ 0x11111111, 0x01020304, 0x9b8d6f43, 0x01234567 ] - out = [ 0xea2a92f4, 0xcb1cf8ce, 0x4581472e, 0x5881c4bb ] - - core01 = kexp k 1 n == out - where - n = [ 0x00, 0x00, 0x00, 0x09, 0x00, 0x00, 0x00, 0x4a, - 0x00, 0x00, 0x00, 0x00 ] - k = [ 0x00, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, - 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e, 0x0f, - 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, - 0x18, 0x19, 0x1a, 0x1b, 0x1c, 0x1d, 0x1e, 0x1f ] - out = [ 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574, - 0x03020100, 0x07060504, 0x0b0a0908, 0x0f0e0d0c, - 0x13121110, 0x17161514, 0x1b1a1918, 0x1f1e1d1c, - 0x00000001, 0x09000000, 0x4a000000, 0x00000000 ] - - core02 = core (kexp k 1 n) == out - where - n = [ 0x00, 0x00, 0x00, 0x09, 0x00, 0x00, 0x00, 0x4a, - 0x00, 0x00, 0x00, 0x00 ] - k = [ 0x00, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, - 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e, 0x0f, - 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, - 0x18, 0x19, 0x1a, 0x1b, 0x1c, 0x1d, 0x1e, 0x1f ] - out = [ 0x10, 0xf1, 0xe7, 0xe4, 0xd1, 0x3b, 0x59, 0x15, - 0x50, 0x0f, 0xdd, 0x1f, 0xa3, 0x20, 0x71, 0xc4, - 0xc7, 0xd1, 0xf4, 0xc7, 0x33, 0xc0, 0x68, 0x03, - 0x04, 0x22, 0xaa, 0x9a, 0xc3, 0xd4, 0x6c, 0x4e, - 0xd2, 0x82, 0x64, 0x46, 0x07, 0x9f, 0xaa, 0x09, - 0x14, 0xc2, 0xd7, 0x05, 0xd9, 0x8b, 0x02, 0xa2, - 0xb5, 0x12, 0x9c, 0xd1, 0xde, 0x16, 0x4e, 0xb9, - 0xcb, 0xd0, 0x83, 0xe8, 0xa2, 0x50, 0x3c, 0x4e ] - - rfctest01 = encrypt zero zero zero zero - == [ 0x76, 0xb8, 0xe0, 0xad, 0xa0, 0xf1, 0x3d, 0x90, 0x40, 0x5d, - 0x6a, 0xe5, 0x53, 0x86, 0xbd, 0x28, 0xbd, 0xd2, 0x19, 0xb8, - 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, - 0x0d, 0xc7, 0xda, 0x41, 0x59, 0x7c, 0x51, 0x57, 0x48, 0x8d, - 0x77, 0x24, 0xe0, 0x3f, 0xb8, 0xd8, 0x4a, 0x37, 0x6a, 0x43, - 0xb8, 0xf4, 0x15, 0x18, 0xa1, 0x1c, 0xc3, 0x87, 0xb6, 0x69, - 0xb2, 0xee, 0x65, 0x86 ] - - rfctest02 = encrypt (zero # [1]) 1 (zero # [2]) msg == out - where - out = [ 0xa3, 0xfb, 0xf0, 0x7d, 0xf3, 0xfa, 0x2f, 0xde, 0x4f, 0x37, - 0x6c, 0xa2, 0x3e, 0x82, 0x73, 0x70, 0x41, 0x60, 0x5d, 0x9f, - 0x4f, 0x4f, 0x57, 0xbd, 0x8c, 0xff, 0x2c, 0x1d, 0x4b, 0x79, - 0x55, 0xec, 0x2a, 0x97, 0x94, 0x8b, 0xd3, 0x72, 0x29, 0x15, - 0xc8, 0xf3, 0xd3, 0x37, 0xf7, 0xd3, 0x70, 0x05, 0x0e, 0x9e, - 0x96, 0xd6, 0x47, 0xb7, 0xc3, 0x9f, 0x56, 0xe0, 0x31, 0xca, - 0x5e, 0xb6, 0x25, 0x0d, 0x40, 0x42, 0xe0, 0x27, 0x85, 0xec, - 0xec, 0xfa, 0x4b, 0x4b, 0xb5, 0xe8, 0xea, 0xd0, 0x44, 0x0e, - 0x20, 0xb6, 0xe8, 0xdb, 0x09, 0xd8, 0x81, 0xa7, 0xc6, 0x13, - 0x2f, 0x42, 0x0e, 0x52, 0x79, 0x50, 0x42, 0xbd, 0xfa, 0x77, - 0x73, 0xd8, 0xa9, 0x05, 0x14, 0x47, 0xb3, 0x29, 0x1c, 0xe1, - 0x41, 0x1c, 0x68, 0x04, 0x65, 0x55, 0x2a, 0xa6, 0xc4, 0x05, - 0xb7, 0x76, 0x4d, 0x5e, 0x87, 0xbe, 0xa8, 0x5a, 0xd0, 0x0f, - 0x84, 0x49, 0xed, 0x8f, 0x72, 0xd0, 0xd6, 0x62, 0xab, 0x05, - 0x26, 0x91, 0xca, 0x66, 0x42, 0x4b, 0xc8, 0x6d, 0x2d, 0xf8, - 0x0e, 0xa4, 0x1f, 0x43, 0xab, 0xf9, 0x37, 0xd3, 0x25, 0x9d, - 0xc4, 0xb2, 0xd0, 0xdf, 0xb4, 0x8a, 0x6c, 0x91, 0x39, 0xdd, - 0xd7, 0xf7, 0x69, 0x66, 0xe9, 0x28, 0xe6, 0x35, 0x55, 0x3b, - 0xa7, 0x6c, 0x5c, 0x87, 0x9d, 0x7b, 0x35, 0xd4, 0x9e, 0xb2, - 0xe6, 0x2b, 0x08, 0x71, 0xcd, 0xac, 0x63, 0x89, 0x39, 0xe2, - 0x5e, 0x8a, 0x1e, 0x0e, 0xf9, 0xd5, 0x28, 0x0f, 0xa8, 0xca, - 0x32, 0x8b, 0x35, 0x1c, 0x3c, 0x76, 0x59, 0x89, 0xcb, 0xcf, - 0x3d, 0xaa, 0x8b, 0x6c, 0xcc, 0x3a, 0xaf, 0x9f, 0x39, 0x79, - 0xc9, 0x2b, 0x37, 0x20, 0xfc, 0x88, 0xdc, 0x95, 0xed, 0x84, - 0xa1, 0xbe, 0x05, 0x9c, 0x64, 0x99, 0xb9, 0xfd, 0xa2, 0x36, - 0xe7, 0xe8, 0x18, 0xb0, 0x4b, 0x0b, 0xc3, 0x9c, 0x1e, 0x87, - 0x6b, 0x19, 0x3b, 0xfe, 0x55, 0x69, 0x75, 0x3f, 0x88, 0x12, - 0x8c, 0xc0, 0x8a, 0xaa, 0x9b, 0x63, 0xd1, 0xa1, 0x6f, 0x80, - 0xef, 0x25, 0x54, 0xd7, 0x18, 0x9c, 0x41, 0x1f, 0x58, 0x69, - 0xca, 0x52, 0xc5, 0xb8, 0x3f, 0xa3, 0x6f, 0xf2, 0x16, 0xb9, - 0xc1, 0xd3, 0x00, 0x62, 0xbe, 0xbc, 0xfd, 0x2d, 0xc5, 0xbc, - 0xe0, 0x91, 0x19, 0x34, 0xfd, 0xa7, 0x9a, 0x86, 0xf6, 0xe6, - 0x98, 0xce, 0xd7, 0x59, 0xc3, 0xff, 0x9b, 0x64, 0x77, 0x33, - 0x8f, 0x3d, 0xa4, 0xf9, 0xcd, 0x85, 0x14, 0xea, 0x99, 0x82, - 0xcc, 0xaf, 0xb3, 0x41, 0xb2, 0x38, 0x4d, 0xd9, 0x02, 0xf3, - 0xd1, 0xab, 0x7a, 0xc6, 0x1d, 0xd2, 0x9c, 0x6f, 0x21, 0xba, - 0x5b, 0x86, 0x2f, 0x37, 0x30, 0xe3, 0x7c, 0xfd, 0xc4, 0xfd, - 0x80, 0x6c, 0x22, 0xf2, 0x21 ] - - msg = [ 0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, 0x69, 0x73, - 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x74, 0x6f, 0x20, 0x74, 0x68, - 0x65, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74, - 0x65, 0x6e, 0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, 0x69, 0x62, - 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, 0x6f, 0x72, 0x20, 0x70, - 0x75, 0x62, 0x6c, 0x69, 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, - 0x20, 0x61, 0x73, 0x20, 0x61, 0x6c, 0x6c, 0x20, 0x6f, 0x72, - 0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, 0x20, 0x61, - 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x49, 0x6e, 0x74, - 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, - 0x74, 0x20, 0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61, - 0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73, 0x74, 0x61, - 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x20, 0x6d, 0x61, 0x64, - 0x65, 0x20, 0x77, 0x69, 0x74, 0x68, 0x69, 0x6e, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74, - 0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, - 0x46, 0x20, 0x61, 0x63, 0x74, 0x69, 0x76, 0x69, 0x74, 0x79, - 0x20, 0x69, 0x73, 0x20, 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, - 0x65, 0x72, 0x65, 0x64, 0x20, 0x61, 0x6e, 0x20, 0x22, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, 0x69, - 0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, 0x22, 0x2e, 0x20, 0x53, - 0x75, 0x63, 0x68, 0x20, 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, - 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75, - 0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, 0x73, 0x74, - 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, - 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x73, 0x65, 0x73, - 0x73, 0x69, 0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x65, 0x6c, 0x6c, 0x20, 0x61, 0x73, 0x20, 0x77, 0x72, - 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, 0x61, 0x6e, 0x64, 0x20, - 0x65, 0x6c, 0x65, 0x63, 0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, - 0x20, 0x63, 0x6f, 0x6d, 0x6d, 0x75, 0x6e, 0x69, 0x63, 0x61, - 0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, 0x64, 0x65, - 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x74, 0x69, - 0x6d, 0x65, 0x20, 0x6f, 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, - 0x65, 0x2c, 0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, - 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65, 0x73, 0x73, - 0x65, 0x64, 0x20, 0x74, 0x6f ] - - rfctest03 = encrypt key 42 (zero # [2]) msg == out - where - key = [ 0x1c, 0x92, 0x40, 0xa5, 0xeb, 0x55, 0xd3, 0x8a, 0xf3, 0x33, - 0x88, 0x86, 0x04, 0xf6, 0xb5, 0xf0, 0x47, 0x39, 0x17, 0xc1, - 0x40, 0x2b, 0x80, 0x09, 0x9d, 0xca, 0x5c, 0xbc, 0x20, 0x70, - 0x75, 0xc0 ] - out = [ 0x27, 0x54, 0x77, 0x61, 0x73, 0x20, 0x62, 0x72, 0x69, 0x6c, - 0x6c, 0x69, 0x67, 0x2c, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x73, 0x6c, 0x69, 0x74, 0x68, 0x79, 0x20, - 0x74, 0x6f, 0x76, 0x65, 0x73, 0x0a, 0x44, 0x69, 0x64, 0x20, - 0x67, 0x79, 0x72, 0x65, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x67, - 0x69, 0x6d, 0x62, 0x6c, 0x65, 0x20, 0x69, 0x6e, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x77, 0x61, 0x62, 0x65, 0x3a, 0x0a, 0x41, - 0x6c, 0x6c, 0x20, 0x6d, 0x69, 0x6d, 0x73, 0x79, 0x20, 0x77, - 0x65, 0x72, 0x65, 0x20, 0x74, 0x68, 0x65, 0x20, 0x62, 0x6f, - 0x72, 0x6f, 0x67, 0x6f, 0x76, 0x65, 0x73, 0x2c, 0x0a, 0x41, - 0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x6d, 0x6f, 0x6d, - 0x65, 0x20, 0x72, 0x61, 0x74, 0x68, 0x73, 0x20, 0x6f, 0x75, - 0x74, 0x67, 0x72, 0x61, 0x62, 0x65, 0x2e ] - - msg = [ 0x62, 0xe6, 0x34, 0x7f, 0x95, 0xed, 0x87, 0xa4, 0x5f, 0xfa, - 0xe7, 0x42, 0x6f, 0x27, 0xa1, 0xdf, 0x5f, 0xb6, 0x91, 0x10, - 0x04, 0x4c, 0x0d, 0x73, 0x11, 0x8e, 0xff, 0xa9, 0x5b, 0x01, - 0xe5, 0xcf, 0x16, 0x6d, 0x3d, 0xf2, 0xd7, 0x21, 0xca, 0xf9, - 0xb2, 0x1e, 0x5f, 0xb1, 0x4c, 0x61, 0x68, 0x71, 0xfd, 0x84, - 0xc5, 0x4f, 0x9d, 0x65, 0xb2, 0x83, 0x19, 0x6c, 0x7f, 0xe4, - 0xf6, 0x05, 0x53, 0xeb, 0xf3, 0x9c, 0x64, 0x02, 0xc4, 0x22, - 0x34, 0xe3, 0x2a, 0x35, 0x6b, 0x3e, 0x76, 0x43, 0x12, 0xa6, - 0x1a, 0x55, 0x32, 0x05, 0x57, 0x16, 0xea, 0xd6, 0x96, 0x25, - 0x68, 0xf8, 0x7d, 0x3f, 0x3f, 0x77, 0x04, 0xc6, 0xa8, 0xd1, - 0xbc, 0xd1, 0xbf, 0x4d, 0x50, 0xd6, 0x15, 0x4b, 0x6d, 0xa7, - 0x31, 0xb1, 0x87, 0xb5, 0x8d, 0xfd, 0x72, 0x8a, 0xfa, 0x36, - 0x75, 0x7a, 0x79, 0x7a, 0xc1, 0x88, 0xd1 ] - -property allTestsPass = - ([ // Basic tests - qround01, core01, core02 - // Full RFC test vectors - , rfctest01, rfctest02, rfctest03 - ] : [_]Bit) == ~zero // All test bits should equal one - -/* -------------------------------------------------------------------------- */ -/* -- Private utilities ----------------------------------------------------- */ - -private - // Convert a round into a block, by splitting every 32-bit round entry - // into 4 bytes, and then serialize those values into a full block. - blocked : Round -> Block - blocked x = join (map toBytes x) - where - // This essentially splits a 32-bit number into 4-byte - // little-endian form, where 'rjoin' is the inverse and would merge - // 4 bytes as a 32-bit little endian number. - toBytes : [32] -> [4][8] - toBytes v = reverse (groupBy`{8} v) - - // Map a function over a finite list. - map : { a, b, c } - (a -> b) -> [c]a -> [c]b - map f xs = [ f x | x <- xs ] - - // Map a function iteratively over a seed value, producing an infinite - // list of successive function applications: - // - // iterate f 0 == [ 0, f 0, f (f 0), f (f (f 0)), ... ] - iterate : { a } (a -> a) -> a -> [inf]a - iterate f x = [x] # [ f v | v <- iterate f x ] - where - // NB: Needs a binded name in order to tie the recursive knot. - xs = [x] # [ f v | v <- xs ] - - // rjoin = join . reverse - // This encodes a sequence of values as a little endian number - // e.g. [ 0xaa, 0xbb, 0xcc, 0xdd ] is serialized as \xdd\xcc\xbb\xaa - rjoin : {a, b, c} - ( fin a, fin c - ) => [c][a]b -> [a * c]b - rjoin x = join (reverse x) diff --git a/automation/saw/chacha20.saw b/automation/saw/chacha20.saw deleted file mode 100644 index cf98466b2..000000000 --- a/automation/saw/chacha20.saw +++ /dev/null @@ -1,40 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. - -import "chacha20.cry" as chacha20; - -print "Proving ChaCha20 spec..."; -prove_print abc {{ chacha20::allTestsPass }}; - -print "Loading LLVM bitcode..."; -m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc"; - -let SpecChaCha20 n = do { - llvm_ptr "output" (llvm_array n (llvm_int 8)); - output <- llvm_var "*output" (llvm_array n (llvm_int 8)); - - llvm_ptr "plain" (llvm_array n (llvm_int 8)); - plain <- llvm_var "*plain" (llvm_array n (llvm_int 8)); - - len <- llvm_var "len" (llvm_int 32); - llvm_assert_eq "len" {{ `n : [32] }}; - - llvm_ptr "k" (llvm_array 32 (llvm_int 8)); - k <- llvm_var "*k" (llvm_array 32 (llvm_int 8)); - - llvm_ptr "n1" (llvm_array 12 (llvm_int 8)); - n1 <- llvm_var "*n1" (llvm_array 12 (llvm_int 8)); - - ctr <- llvm_var "ctr" (llvm_int 32); - - llvm_ensure_eq "*output" {{ chacha20::encrypt k ctr n1 plain }}; - - llvm_verify_tactic abc; -}; - -print "Proving equality for a single block..."; -time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 64)); - -print "Proving equality for multiple blocks..."; -time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 256)); diff --git a/automation/saw/poly1305-hacl.saw b/automation/saw/poly1305-hacl.saw deleted file mode 100644 index a4dfff6d9..000000000 --- a/automation/saw/poly1305-hacl.saw +++ /dev/null @@ -1,38 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. - -import "poly1305.cry" as poly1305; - -print "Proving Poly1305 spec..."; -prove_print abc {{ poly1305::allTestsPass }}; - -print "Loading LLVM bitcode..."; -m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc"; - -let SpecPoly1305 n = do { - llvm_ptr "output" (llvm_array 16 (llvm_int 8)); - output <- llvm_var "*output" (llvm_array 16 (llvm_int 8)); - - llvm_ptr "input" (llvm_array n (llvm_int 8)); - input <- llvm_var "*input" (llvm_array n (llvm_int 8)); - - llvm_var "len1" (llvm_int 64); - llvm_ptr "k1" (llvm_array 32 (llvm_int 8)); - k1 <- llvm_var "*k1" (llvm_array 32 (llvm_int 8)); - - llvm_assert_eq "*input" {{ zero : [n][8] }}; - llvm_assert_eq "len1" {{ `n : [64] }}; - - llvm_assert_eq "*k1" {{ zero : [32][8] }}; - - let res = {{ poly1305::Poly1305 input (take`{16} k1) (drop`{16} k1) }}; - llvm_ensure_eq "*output" {{ res }}; - - llvm_verify_tactic abc; -}; - -print "Proving equality for a single block..."; -// This is currently disabled as it takes way too long. We need to help Z3 -// prove this before we can enable it on Taskcluster. -//time (llvm_verify m "Hacl_Poly1305_64_crypto_onetimeauth" [] (SpecPoly1305 16)); diff --git a/automation/saw/poly1305.cry b/automation/saw/poly1305.cry deleted file mode 100644 index 6321a4f19..000000000 --- a/automation/saw/poly1305.cry +++ /dev/null @@ -1,336 +0,0 @@ -/* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ - -/* This file provides a spec of the Poly1305 one-time authenticator. - * See for details. */ - -module poly1305 where - -P : [136] -P = 2^^130 - 5 - -Poly1305 : {n} (fin n) => [n][8] -> [16][8] -> [16][8] -> [16][8] -Poly1305 msg r s = reverse (groupBy (drop ((rounds ! 0) + s'))) - where - rounds = [zero] # [ Poly1305_block acc r' b | b <- blocks | acc <- rounds ] - r' = zero # (Poly1305_clamp (join (reverse r))) - s' = zero # (join (reverse s)) - blocks = Poly1305_split msg - -private - // 0x0f - for r[3], r[7], r[11], r[15] - // 0xfc - for r[4], r[8], r[12] - Poly1305_clamp r = r && 0x0ffffffc0ffffffc0ffffffc0fffffff - - // Poly1305_block : ((acc + msg) * r) % P - Poly1305_block : [136] -> [136] -> [136] -> [136] - Poly1305_block acc r msg = drop (prod % (zero # P)) - where - acc' : [137] - // Add the current block to the accumulator. - acc' = (zero # acc) + (zero # msg) - prod : [273] - // Multiply the new accumulator value by r. - prod = ((zero : [137]) # r) * ((zero : [136]) # acc') - - Poly1305_split : {n, nb, nf} (fin n, nf == n / 16, nb == (n + 15) / 16) => [n][8] -> [nb][136] - Poly1305_split msg = take ((h1 : [nf][136]) # h2) - where - // Split all full 16-byte blocks and append 0x01, then convert to LE. - h1 = [ join (reverse (b # [0x01])) | b <- groupBy`{16} (take msg)] - // Pad the remaining bytes (if any) and convert to LE. - h2 = [join (reverse ((drop`{nf * 16} msg) # [0x01] # zero))] - -/* -------------------------------------------------------------------------- */ -/* -- Tests ----------------------------------------------------------------- */ - -private - // https://tools.ietf.org/html/rfc7539#section-2.5.2 - rval1 = [0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33, - 0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06, 0xa8] - sval1 = [0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd, - 0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49, 0xf5, 0x1b] - text1 = [0x43, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x67, 0x72, - 0x61, 0x70, 0x68, 0x69, 0x63, 0x20, 0x46, 0x6f, - 0x72, 0x75, 0x6d, 0x20, 0x52, 0x65, 0x73, 0x65, - 0x61, 0x72, 0x63, 0x68, 0x20, 0x47, 0x72, 0x6f, - 0x75, 0x70] - - rfctest01 = Poly1305 text1 rval1 sval1 - == [0xa8, 0x06, 0x1d, 0xc1, 0x30, 0x51, 0x36, 0xc6, - 0xc2, 0x2b, 0x8b, 0xaf, 0x0c, 0x01, 0x27, 0xa9] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #1 - rval2 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval2 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text2 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - rfctest02 = Poly1305 text2 rval2 sval2 - == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #2 - rval3 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval3 = [0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, - 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a, 0x86, 0x3e] - text3 = [0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, - 0x69, 0x73, 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x74, - 0x6f, 0x20, 0x74, 0x68, 0x65, 0x20, 0x49, 0x45, - 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74, 0x65, 0x6e, - 0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, - 0x69, 0x62, 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, - 0x6f, 0x72, 0x20, 0x70, 0x75, 0x62, 0x6c, 0x69, - 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, 0x20, 0x61, - 0x73, 0x20, 0x61, 0x6c, 0x6c, 0x20, 0x6f, 0x72, - 0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, - 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, - 0x20, 0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, - 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x20, - 0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61, - 0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73, - 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, - 0x20, 0x6d, 0x61, 0x64, 0x65, 0x20, 0x77, 0x69, - 0x74, 0x68, 0x69, 0x6e, 0x20, 0x74, 0x68, 0x65, - 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74, - 0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x61, 0x63, 0x74, 0x69, - 0x76, 0x69, 0x74, 0x79, 0x20, 0x69, 0x73, 0x20, - 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, 0x65, 0x72, - 0x65, 0x64, 0x20, 0x61, 0x6e, 0x20, 0x22, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74, - 0x72, 0x69, 0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, - 0x22, 0x2e, 0x20, 0x53, 0x75, 0x63, 0x68, 0x20, - 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, - 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75, - 0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, - 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, - 0x74, 0x73, 0x20, 0x69, 0x6e, 0x20, 0x49, 0x45, - 0x54, 0x46, 0x20, 0x73, 0x65, 0x73, 0x73, 0x69, - 0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x65, 0x6c, 0x6c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x72, 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, - 0x61, 0x6e, 0x64, 0x20, 0x65, 0x6c, 0x65, 0x63, - 0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, 0x20, 0x63, - 0x6f, 0x6d, 0x6d, 0x75, 0x6e, 0x69, 0x63, 0x61, - 0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, - 0x64, 0x65, 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, - 0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, - 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c, - 0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, - 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65, - 0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f] - - rfctest03 = Poly1305 text3 rval3 sval3 - == [0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, - 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a, 0x86, 0x3e] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #3 - rval4 = [0x36, 0xe5, 0xf6, 0xb5, 0xc5, 0xe0, 0x60, 0x70, - 0xf0, 0xef, 0xca, 0x96, 0x22, 0x7a, 0x86, 0x3e] - sval4 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text4 = [0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, - 0x69, 0x73, 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x74, - 0x6f, 0x20, 0x74, 0x68, 0x65, 0x20, 0x49, 0x45, - 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74, 0x65, 0x6e, - 0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, - 0x69, 0x62, 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, - 0x6f, 0x72, 0x20, 0x70, 0x75, 0x62, 0x6c, 0x69, - 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, 0x20, 0x61, - 0x73, 0x20, 0x61, 0x6c, 0x6c, 0x20, 0x6f, 0x72, - 0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, - 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, - 0x20, 0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, - 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x20, - 0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61, - 0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73, - 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, - 0x20, 0x6d, 0x61, 0x64, 0x65, 0x20, 0x77, 0x69, - 0x74, 0x68, 0x69, 0x6e, 0x20, 0x74, 0x68, 0x65, - 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74, - 0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x61, 0x63, 0x74, 0x69, - 0x76, 0x69, 0x74, 0x79, 0x20, 0x69, 0x73, 0x20, - 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, 0x65, 0x72, - 0x65, 0x64, 0x20, 0x61, 0x6e, 0x20, 0x22, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74, - 0x72, 0x69, 0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, - 0x22, 0x2e, 0x20, 0x53, 0x75, 0x63, 0x68, 0x20, - 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, - 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75, - 0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, - 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, - 0x74, 0x73, 0x20, 0x69, 0x6e, 0x20, 0x49, 0x45, - 0x54, 0x46, 0x20, 0x73, 0x65, 0x73, 0x73, 0x69, - 0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x65, 0x6c, 0x6c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x72, 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, - 0x61, 0x6e, 0x64, 0x20, 0x65, 0x6c, 0x65, 0x63, - 0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, 0x20, 0x63, - 0x6f, 0x6d, 0x6d, 0x75, 0x6e, 0x69, 0x63, 0x61, - 0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, - 0x64, 0x65, 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, - 0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, - 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c, - 0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, - 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65, - 0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f] - - rfctest04 = Poly1305 text4 rval4 sval4 - == [0xf3, 0x47, 0x7e, 0x7c, 0xd9, 0x54, 0x17, 0xaf, - 0x89, 0xa6, 0xb8, 0x79, 0x4c, 0x31, 0x0c, 0xf0] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #4 - rval5 = [0x1c, 0x92, 0x40, 0xa5, 0xeb, 0x55, 0xd3, 0x8a, - 0xf3, 0x33, 0x88, 0x86, 0x04, 0xf6, 0xb5, 0xf0] - sval5 = [0x47, 0x39, 0x17, 0xc1, 0x40, 0x2b, 0x80, 0x09, - 0x9d, 0xca, 0x5c, 0xbc, 0x20, 0x70, 0x75, 0xc0] - text5 = [0x27, 0x54, 0x77, 0x61, 0x73, 0x20, 0x62, 0x72, - 0x69, 0x6c, 0x6c, 0x69, 0x67, 0x2c, 0x20, 0x61, - 0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x73, - 0x6c, 0x69, 0x74, 0x68, 0x79, 0x20, 0x74, 0x6f, - 0x76, 0x65, 0x73, 0x0a, 0x44, 0x69, 0x64, 0x20, - 0x67, 0x79, 0x72, 0x65, 0x20, 0x61, 0x6e, 0x64, - 0x20, 0x67, 0x69, 0x6d, 0x62, 0x6c, 0x65, 0x20, - 0x69, 0x6e, 0x20, 0x74, 0x68, 0x65, 0x20, 0x77, - 0x61, 0x62, 0x65, 0x3a, 0x0a, 0x41, 0x6c, 0x6c, - 0x20, 0x6d, 0x69, 0x6d, 0x73, 0x79, 0x20, 0x77, - 0x65, 0x72, 0x65, 0x20, 0x74, 0x68, 0x65, 0x20, - 0x62, 0x6f, 0x72, 0x6f, 0x67, 0x6f, 0x76, 0x65, - 0x73, 0x2c, 0x0a, 0x41, 0x6e, 0x64, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x6d, 0x6f, 0x6d, 0x65, 0x20, - 0x72, 0x61, 0x74, 0x68, 0x73, 0x20, 0x6f, 0x75, - 0x74, 0x67, 0x72, 0x61, 0x62, 0x65, 0x2e] - - rfctest05 = Poly1305 text5 rval5 sval5 - == [0x45, 0x41, 0x66, 0x9a, 0x7e, 0xaa, 0xee, 0x61, - 0xe7, 0x08, 0xdc, 0x7c, 0xbc, 0xc5, 0xeb, 0x62] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #5 - rval6 = [0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval6 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text6 = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] - - rfctest06 = Poly1305 text6 rval6 sval6 - == [0x03, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #6 - rval7 = [0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval7 = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] - text7 = [0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - rfctest07 = Poly1305 text7 rval7 sval7 - == [0x03, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #7 - rval8 = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval8 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text8 = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xf0, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0x11, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - rfctest08 = Poly1305 text8 rval8 sval8 - == [0x05, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #8 - rval9 = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval9 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text9 = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xfb, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, - 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, 0xfe, - 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, - 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01] - - rfctest09 = Poly1305 text9 rval9 sval9 - == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #9 - rval10 = [0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval10 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text10 = [0xfd, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] - - rfctest10 = Poly1305 text10 rval10 sval10 - == [0xfa, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, - 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #10 - rval11 = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval11 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text11 = [0xe3, 0x35, 0x94, 0xd7, 0x50, 0x5e, 0x43, 0xb9, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x33, 0x94, 0xd7, 0x50, 0x5e, 0x43, 0x79, 0xcd, - 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - rfctest11 = Poly1305 text11 rval11 sval11 - == [0x14, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x55, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - // https://tools.ietf.org/html/rfc7539#appendix-A.3 - // Test Vector #11 - rval12 = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - sval12 = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - text12 = [0xe3, 0x35, 0x94, 0xd7, 0x50, 0x5e, 0x43, 0xb9, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x33, 0x94, 0xd7, 0x50, 0x5e, 0x43, 0x79, 0xcd, - 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - - rfctest12 = Poly1305 text12 rval12 sval12 - == [0x13, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - -property allTestsPass = - ([ // Full RFC test vectors - rfctest01, rfctest02, rfctest03, rfctest04, - rfctest05, rfctest06, rfctest07, rfctest08, - rfctest09, rfctest10, rfctest11, rfctest12 - ] : [_]Bit) == ~zero // All test bits should equal one diff --git a/automation/saw/poly1305.saw b/automation/saw/poly1305.saw deleted file mode 100644 index 44be1e3e0..000000000 --- a/automation/saw/poly1305.saw +++ /dev/null @@ -1,47 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. - -import "poly1305.cry" as poly1305; - -print "Proving Poly1305 spec..."; -prove_print abc {{ poly1305::allTestsPass }}; - -print "Loading LLVM bitcode..."; -m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc"; - -let SpecPoly1305 n = do { - llvm_ptr "out" (llvm_array 16 (llvm_int 8)); - out <- llvm_var "*out" (llvm_array 16 (llvm_int 8)); - - llvm_ptr "ad" (llvm_array 16 (llvm_int 8)); - ad <- llvm_var "*ad" (llvm_array 16 (llvm_int 8)); - - adLen <- llvm_var "adLen" (llvm_int 32); - - llvm_ptr "ciphertext" (llvm_array n (llvm_int 8)); - ciphertext <- llvm_var "*ciphertext" (llvm_array n (llvm_int 8)); - - ciphertextLen <- llvm_var "ciphertextLen" (llvm_int 32); - - llvm_ptr "key" (llvm_array 32 (llvm_int 8)); - key <- llvm_var "*key" (llvm_array 32 (llvm_int 8)); - - llvm_assert_eq "*ad" {{ zero : [16][8] }}; - llvm_assert_eq "adLen" {{ 16 : [32] }}; - - llvm_assert_eq "*ciphertext" {{ zero : [n][8] }}; - llvm_assert_eq "ciphertextLen" {{ `n : [32] }}; - - llvm_assert_eq "*key" {{ zero : [32][8] }}; - - let res = {{ poly1305::Poly1305 (ad # ciphertext # [16, 0, 0, 0, 0, 0, 0, 0] # [`n, 0, 0, 0, 0, 0, 0, 0]) (take`{16} key) (drop`{16} key) }}; - llvm_ensure_eq "*out" {{ res }}; - - llvm_verify_tactic abc; -}; - -print "Proving equality for a single block..."; -// This is currently disabled as it takes way too long. We need to help Z3 -// prove this before we can enable it on Taskcluster. -//time (llvm_verify m "Poly1305Do" [] (SpecPoly1305 16)); diff --git a/automation/taskcluster/docker-saw/Dockerfile b/automation/taskcluster/docker-saw/Dockerfile deleted file mode 100644 index d67787010..000000000 --- a/automation/taskcluster/docker-saw/Dockerfile +++ /dev/null @@ -1,46 +0,0 @@ -FROM ubuntu:16.04 -MAINTAINER Tim Taubert - -RUN useradd -d /home/worker -s /bin/bash -m worker -WORKDIR /home/worker - -ENV DEBIAN_FRONTEND noninteractive - -RUN apt-get update && apt-get install -y \ - binutils \ - build-essential \ - bzip2 \ - clang-3.8 \ - curl \ - gcc-multilib \ - g++-multilib \ - gyp \ - lib32z1-dev \ - mercurial \ - ninja-build \ - unzip \ - zlib1g-dev - -# Add missing LLVM plugin for gold linker. -ADD LLVMgold.so.zip /usr/lib/llvm-3.8/lib/LLVMgold.so.zip -RUN unzip /usr/lib/llvm-3.8/lib/LLVMgold.so.zip -d /usr/lib/llvm-3.8/lib/ - -# Install SAW/Cryptol. -RUN curl -LO https://saw.galois.com/builds/nightly/saw-0.2-2018-01-14-Ubuntu14.04-64.tar.gz && \ - tar xzvf saw-*.tar.gz -C /usr/local --strip-components=1 && \ - rm saw-*.tar.gz - -# Install Z3. -RUN curl -LO https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-ubuntu-16.04.zip && \ - unzip z3*.zip && \ - cp -r z3*/* /usr/local/ && \ - rm -fr z3* - -ADD bin /home/worker/bin -RUN chmod +x /home/worker/bin/* - -# Change user. -USER worker - -# Set a default command useful for debugging -CMD ["/bin/bash", "--login"] diff --git a/automation/taskcluster/docker-saw/LLVMgold.so.zip b/automation/taskcluster/docker-saw/LLVMgold.so.zip deleted file mode 100644 index b5e5a593d..000000000 Binary files a/automation/taskcluster/docker-saw/LLVMgold.so.zip and /dev/null differ diff --git a/automation/taskcluster/docker-saw/bin/checkout.sh b/automation/taskcluster/docker-saw/bin/checkout.sh deleted file mode 100644 index 0cdd2ac40..000000000 --- a/automation/taskcluster/docker-saw/bin/checkout.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/usr/bin/env bash - -set -v -e -x - -# Default values for testing. -REVISION=${NSS_HEAD_REVISION:-default} -REPOSITORY=${NSS_HEAD_REPOSITORY:-https://hg.mozilla.org/projects/nss} - -# Clone NSS. -for i in 0 2 5; do - sleep $i - hg clone -r $REVISION $REPOSITORY nss && exit 0 - rm -rf nss -done -exit 1 diff --git a/automation/taskcluster/graph/src/extend.js b/automation/taskcluster/graph/src/extend.js index 0f2498bb2..f354f7f73 100644 --- a/automation/taskcluster/graph/src/extend.js +++ b/automation/taskcluster/graph/src/extend.js @@ -41,11 +41,6 @@ const FUZZ_IMAGE_32 = { path: "automation/taskcluster/docker-fuzz32" }; -const SAW_IMAGE = { - name: "saw", - path: "automation/taskcluster/docker-saw" -}; - const WINDOWS_CHECKOUT_CMD = "bash -c \"hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss || " + "(sleep 2; hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss) || " + @@ -1189,74 +1184,6 @@ async function scheduleTools() { ] })); - let task_saw = queue.scheduleTask(merge(base, { - symbol: "B", - group: "SAW", - name: "LLVM bitcode build (32 bit)", - image: SAW_IMAGE, - kind: "build", - env: { - AR: "llvm-ar-3.8", - CC: "clang-3.8", - CCC: "clang++-3.8" - }, - artifacts: { - public: { - expires: 24 * 7, - type: "directory", - path: "/home/worker/artifacts" - } - }, - command: [ - "/bin/bash", - "-c", - "bin/checkout.sh && nss/automation/taskcluster/scripts/build_gyp.sh --disable-tests --emit-llvm -t ia32" - ] - })); - - queue.scheduleTask(merge(base, { - parent: task_saw, - symbol: "bmul", - group: "SAW", - name: "bmul.saw", - image: SAW_IMAGE, - command: [ - "/bin/bash", - "-c", - "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh bmul" - ] - })); - - // TODO: The ChaCha20 saw verification is currently disabled because the new - // HACL 32-bit code can't be verified by saw right now to the best of - // my knowledge. - // Bug 1604130 - // queue.scheduleTask(merge(base, { - // parent: task_saw, - // symbol: "ChaCha20", - // group: "SAW", - // name: "chacha20.saw", - // image: SAW_IMAGE, - // command: [ - // "/bin/bash", - // "-c", - // "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20" - // ] - // })); - - queue.scheduleTask(merge(base, { - parent: task_saw, - symbol: "Poly1305", - group: "SAW", - name: "poly1305.saw", - image: SAW_IMAGE, - command: [ - "/bin/bash", - "-c", - "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh poly1305" - ] - })); - queue.scheduleTask(merge(base, { symbol: "Coverage", name: "Coverage", diff --git a/automation/taskcluster/scripts/run_saw.sh b/automation/taskcluster/scripts/run_saw.sh deleted file mode 100755 index 0e9a8224a..000000000 --- a/automation/taskcluster/scripts/run_saw.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -source $(dirname "$0")/tools.sh - -# Fetch artifact if needed. -fetch_dist - -# Run SAW. -saw "nss/automation/saw/$1.saw" -- cgit v1.2.1