diff options
Diffstat (limited to 'security/nss/automation')
24 files changed, 1300 insertions, 45 deletions
diff --git a/security/nss/automation/abi-check/expected-report-libnspr4.so.txt b/security/nss/automation/abi-check/expected-report-libnspr4.so.txt index 44f52325f..e69de29bb 100644 --- a/security/nss/automation/abi-check/expected-report-libnspr4.so.txt +++ b/security/nss/automation/abi-check/expected-report-libnspr4.so.txt @@ -1,8 +0,0 @@ -Functions changes summary: 1 Removed, 0 Changed, 0 Added function -Variables changes summary: 0 Removed, 0 Changed, 0 Added variable - -1 Removed function: - - 'function void PR_EXPERIMENTAL_ONLY_IN_4_17_GetOverlappedIOHandle(void**)' {PR_EXPERIMENTAL_ONLY_IN_4_17_GetOverlappedIOHandle} - - diff --git a/security/nss/automation/abi-check/expected-report-libssl3.so.txt b/security/nss/automation/abi-check/expected-report-libssl3.so.txt index 2a093094f..ad818d0aa 100644 --- a/security/nss/automation/abi-check/expected-report-libssl3.so.txt +++ b/security/nss/automation/abi-check/expected-report-libssl3.so.txt @@ -1,3 +1,28 @@ -Functions changes summary: 0 Removed, 0 Changed (5 filtered out), 0 Added function -Variables changes summary: 0 Removed, 0 Changed, 0 Added variable + +1 function with some indirect sub-type change: + + [C]'function SECStatus SSL_GetChannelInfo(PRFileDesc*, SSLChannelInfo*, PRUintn)' at sslinfo.c:12:1 has some indirect sub-type changes: + parameter 2 of type 'SSLChannelInfo*' has sub-type changes: + in pointed to type 'typedef SSLChannelInfo' at sslt.h:318:1: + underlying type 'struct SSLChannelInfoStr' at sslt.h:251:1 changed: + type size hasn't changed + 1 data member change: + type of 'SSLSignatureScheme SSLChannelInfoStr::signatureScheme' changed: + underlying type 'enum __anonymous_enum__' at sslt.h:115:1 changed: + type size hasn't changed + 3 enumerator deletions: + '__anonymous_enum__::ssl_sig_rsa_pss_sha256' value '2052' + '__anonymous_enum__::ssl_sig_rsa_pss_sha384' value '2053' + '__anonymous_enum__::ssl_sig_rsa_pss_sha512' value '2054' + + 6 enumerator insertions: + '__anonymous_enum__::ssl_sig_rsa_pss_rsae_sha256' value '2052' + '__anonymous_enum__::ssl_sig_rsa_pss_rsae_sha384' value '2053' + '__anonymous_enum__::ssl_sig_rsa_pss_rsae_sha512' value '2054' + '__anonymous_enum__::ssl_sig_rsa_pss_pss_sha256' value '2057' + '__anonymous_enum__::ssl_sig_rsa_pss_pss_sha384' value '2058' + '__anonymous_enum__::ssl_sig_rsa_pss_pss_sha512' value '2059' + + + diff --git a/security/nss/automation/abi-check/previous-nss-release b/security/nss/automation/abi-check/previous-nss-release index a91a569f5..c213ca3f8 100644 --- a/security/nss/automation/abi-check/previous-nss-release +++ b/security/nss/automation/abi-check/previous-nss-release @@ -1 +1 @@ -NSS_3_34_BRANCH +NSS_3_35_BRANCH diff --git a/security/nss/automation/buildbot-slave/build.sh b/security/nss/automation/buildbot-slave/build.sh index 844254dae..00e749672 100755 --- a/security/nss/automation/buildbot-slave/build.sh +++ b/security/nss/automation/buildbot-slave/build.sh @@ -212,7 +212,7 @@ test_nss() RET=$? print_log "######## details of detected failures (if any) ########" - grep -B50 FAILED ${OUTPUTFILE} + grep -B50 -w FAILED ${OUTPUTFILE} [ $? -eq 1 ] || RET=1 print_result "NSS - tests - ${BITS} bits - ${OPT}" ${RET} 0 @@ -268,10 +268,49 @@ check_abi() fi abidiff --hd1 $PREVDIST/public/ --hd2 $NEWDIST/public \ $PREVDIST/*/lib/$SO $NEWDIST/*/lib/$SO \ + > ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt + RET=$? + cat ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt \ + | grep -v "^Functions changes summary:" \ + | grep -v "^Variables changes summary:" \ > ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt - if [ $? -ne 0 ]; then + rm -f ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt + ABIDIFF_ERROR=$((($RET & 0x01) != 0)) + ABIDIFF_USAGE_ERROR=$((($RET & 0x02) != 0)) + ABIDIFF_ABI_CHANGE=$((($RET & 0x04) != 0)) + ABIDIFF_ABI_INCOMPATIBLE_CHANGE=$((($RET & 0x08) != 0)) + ABIDIFF_UNKNOWN_BIT_SET=$((($RET & 0xf0) != 0)) + + # If abidiff reports an error, or a usage error, or if it sets a result + # bit value this script doesn't know yet about, we'll report failure. + # For ABI changes, we don't yet report an error. We'll compare the + # result report with our whitelist. This allows us to silence changes + # that we're already aware of and have been declared acceptable. + + REPORT_RET_AS_FAILURE=0 + if [ $ABIDIFF_ERROR -ne 0 ]; then + print_log "abidiff reported ABIDIFF_ERROR." + REPORT_RET_AS_FAILURE=1 + fi + if [ $ABIDIFF_USAGE_ERROR -ne 0 ]; then + print_log "abidiff reported ABIDIFF_USAGE_ERROR." + REPORT_RET_AS_FAILURE=1 + fi + if [ $ABIDIFF_UNKNOWN_BIT_SET -ne 0 ]; then + print_log "abidiff reported ABIDIFF_UNKNOWN_BIT_SET." + REPORT_RET_AS_FAILURE=1 + fi + + if [ $ABIDIFF_ABI_CHANGE -ne 0 ]; then + print_log "Ignoring abidiff result ABI_CHANGE, instead we'll check for non-whitelisted differences." + fi + if [ $ABIDIFF_ABI_INCOMPATIBLE_CHANGE -ne 0 ]; then + print_log "Ignoring abidiff result ABIDIFF_ABI_INCOMPATIBLE_CHANGE, instead we'll check for non-whitelisted differences." + fi + + if [ $REPORT_RET_AS_FAILURE -ne 0 ]; then ABI_PROBLEM_FOUND=1 - print_log "FAILED to run abidiff {$PREVDIST , $NEWDIST} for $SO, or failed writing to ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt" + print_log "abidiff {$PREVDIST , $NEWDIST} for $SO FAILED with result $RET, or failed writing to ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt" fi if [ ! -f ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt ]; then ABI_PROBLEM_FOUND=1 diff --git a/security/nss/automation/release/nspr-version.txt b/security/nss/automation/release/nspr-version.txt index 01eeb3615..701680d2c 100644 --- a/security/nss/automation/release/nspr-version.txt +++ b/security/nss/automation/release/nspr-version.txt @@ -1,4 +1,4 @@ -4.18 +4.19 # The first line of this file must contain the human readable NSPR # version number, which is the minimum required version of NSPR diff --git a/security/nss/automation/saw/bmul.cry b/security/nss/automation/saw/bmul.cry new file mode 100644 index 000000000..87303dad6 --- /dev/null +++ b/security/nss/automation/saw/bmul.cry @@ -0,0 +1,8 @@ +/* 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/security/nss/automation/saw/bmul.saw b/security/nss/automation/saw/bmul.saw new file mode 100644 index 000000000..22cd2757b --- /dev/null +++ b/security/nss/automation/saw/bmul.saw @@ -0,0 +1,26 @@ +// 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/security/nss/automation/saw/chacha20.cry b/security/nss/automation/saw/chacha20.cry new file mode 100644 index 000000000..0b52d51ad --- /dev/null +++ b/security/nss/automation/saw/chacha20.cry @@ -0,0 +1,357 @@ +/* +** ChaCha20 specification +** Author: Austin Seipp <aseipp@pobox.com>. 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/security/nss/automation/saw/chacha20.saw b/security/nss/automation/saw/chacha20.saw new file mode 100644 index 000000000..92145ab74 --- /dev/null +++ b/security/nss/automation/saw/chacha20.saw @@ -0,0 +1,40 @@ +// 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" [] (SpecChaCha20 64)); + +print "Proving equality for multiple blocks..."; +time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 256)); diff --git a/security/nss/automation/saw/poly1305-hacl.saw b/security/nss/automation/saw/poly1305-hacl.saw new file mode 100644 index 000000000..a4dfff6d9 --- /dev/null +++ b/security/nss/automation/saw/poly1305-hacl.saw @@ -0,0 +1,38 @@ +// 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/security/nss/automation/saw/poly1305.cry b/security/nss/automation/saw/poly1305.cry new file mode 100644 index 000000000..6321a4f19 --- /dev/null +++ b/security/nss/automation/saw/poly1305.cry @@ -0,0 +1,336 @@ +/* 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 <https://tools.ietf.org/html/rfc7539> 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/security/nss/automation/saw/poly1305.saw b/security/nss/automation/saw/poly1305.saw new file mode 100644 index 000000000..44be1e3e0 --- /dev/null +++ b/security/nss/automation/saw/poly1305.saw @@ -0,0 +1,47 @@ +// 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/security/nss/automation/taskcluster/docker-hacl/Dockerfile b/security/nss/automation/taskcluster/docker-hacl/Dockerfile index e8a88f06c..63f9a24e2 100644 --- a/security/nss/automation/taskcluster/docker-hacl/Dockerfile +++ b/security/nss/automation/taskcluster/docker-hacl/Dockerfile @@ -5,11 +5,11 @@ MAINTAINER Franziskus Kiefer <franziskuskiefer@gmail.com> # the original F* formula with Daniel Fabian # Pinned versions of HACL* (F* and KreMLin are pinned as submodules) -ENV haclrepo https://github.com/mitls/hacl-star.git +ENV haclrepo https://github.com/franziskuskiefer/hacl-star.git # Define versions of dependencies ENV opamv 4.04.2 -ENV haclversion dcd48329d535727dbde93877b124c5ec4a7a2b20 +ENV haclversion 668d6cf274c33bbe2e951e3a84b73f2b6442a51f # Install required packages and set versions ADD setup.sh /tmp/setup.sh diff --git a/security/nss/automation/taskcluster/docker-saw/Dockerfile b/security/nss/automation/taskcluster/docker-saw/Dockerfile new file mode 100644 index 000000000..a481ba048 --- /dev/null +++ b/security/nss/automation/taskcluster/docker-saw/Dockerfile @@ -0,0 +1,46 @@ +FROM ubuntu:latest +MAINTAINER Tim Taubert <ttaubert@mozilla.com> + +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/security/nss/automation/taskcluster/docker-saw/LLVMgold.so.zip b/security/nss/automation/taskcluster/docker-saw/LLVMgold.so.zip Binary files differnew file mode 100644 index 000000000..b5e5a593d --- /dev/null +++ b/security/nss/automation/taskcluster/docker-saw/LLVMgold.so.zip diff --git a/security/nss/automation/taskcluster/docker-saw/bin/checkout.sh b/security/nss/automation/taskcluster/docker-saw/bin/checkout.sh new file mode 100644 index 000000000..0cdd2ac40 --- /dev/null +++ b/security/nss/automation/taskcluster/docker-saw/bin/checkout.sh @@ -0,0 +1,15 @@ +#!/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/security/nss/automation/taskcluster/docker/setup.sh b/security/nss/automation/taskcluster/docker/setup.sh index 01f9c413a..7b90b2e69 100644 --- a/security/nss/automation/taskcluster/docker/setup.sh +++ b/security/nss/automation/taskcluster/docker/setup.sh @@ -12,6 +12,7 @@ apt-get install -y --no-install-recommends apt-utils apt_packages=() apt_packages+=('build-essential') apt_packages+=('ca-certificates') +apt_packages+=('clang-5.0') apt_packages+=('curl') apt_packages+=('npm') apt_packages+=('git') @@ -47,16 +48,17 @@ echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu xenial main" > apt-get -y update apt-get install -y --no-install-recommends ${apt_packages[@]} -# Download clang. -curl -LO https://releases.llvm.org/4.0.0/clang+llvm-4.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz -curl -LO https://releases.llvm.org/4.0.0/clang+llvm-4.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig -# Verify the signature. -gpg --keyserver pool.sks-keyservers.net --recv-keys B6C8F98282B944E3B0D5C2530FC3042E345AD05D -gpg --verify *.tar.xz.sig -# Install into /usr/local/. -tar xJvf *.tar.xz -C /usr/local --strip-components=1 -# Cleanup. -rm *.tar.xz* +# Latest version of abigail-tools +apt-get install -y libxml2-dev autoconf libelf-dev libdw-dev libtool +git clone git://sourceware.org/git/libabigail.git +cd ./libabigail +autoreconf -fi +./configure --prefix=/usr --disable-static --disable-apidoc --disable-manual +make +make install +cd .. +apt-get remove -y libxml2-dev autoconf libtool +rm -rf libabigail # Install latest Rust (stable). su worker -c "curl https://sh.rustup.rs -sSf | sh -s -- -y" diff --git a/security/nss/automation/taskcluster/graph/src/extend.js b/security/nss/automation/taskcluster/graph/src/extend.js index 90e23ae60..ee9ac9b74 100644 --- a/security/nss/automation/taskcluster/graph/src/extend.js +++ b/security/nss/automation/taskcluster/graph/src/extend.js @@ -30,6 +30,11 @@ const HACL_GEN_IMAGE = { path: "automation/taskcluster/docker-hacl" }; +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) || " + @@ -72,7 +77,8 @@ queue.filter(task => { } } - if (task.tests == "fips" && task.platform == "mac") { + if (task.tests == "fips" && + (task.platform == "mac" || task.platform == "aarch64")) { return false; } @@ -88,7 +94,7 @@ queue.filter(task => { } } - // Don't run additional hardware tests on ARM (we don't have anything there). + // Don't run all additional hardware tests on ARM. if (task.group == "Cipher" && task.platform == "aarch64" && task.env && (task.env.NSS_DISABLE_PCLMUL == "1" || task.env.NSS_DISABLE_HW_AES == "1" || task.env.NSS_DISABLE_AVX == "1")) { @@ -187,8 +193,8 @@ export default async function main() { UBSAN_OPTIONS: "print_stacktrace=1", NSS_DISABLE_ARENA_FREE_LIST: "1", NSS_DISABLE_UNLOAD: "1", - CC: "clang", - CCC: "clang++", + CC: "clang-5.0", + CCC: "clang++-5.0", }, platform: "linux64", collection: "asan", @@ -266,6 +272,18 @@ export default async function main() { }, aarch64_base) ); + await scheduleLinux("Linux AArch64 (debug, make)", + merge({ + env: {USE_64: "1"}, + command: [ + "/bin/bash", + "-c", + "bin/checkout.sh && nss/automation/taskcluster/scripts/build.sh" + ], + collection: "make", + }, aarch64_base) + ); + await scheduleMac("Mac (opt)", {collection: "opt"}, "--opt"); await scheduleMac("Mac (debug)", {collection: "debug"}); } @@ -418,12 +436,12 @@ async function scheduleLinux(name, base, args = "") { // Extra builds. let extra_base = merge({group: "Builds"}, build_base); queue.scheduleTask(merge(extra_base, { - name: `${name} w/ clang-4.0`, + name: `${name} w/ clang-5.0`, env: { - CC: "clang", - CCC: "clang++", + CC: "clang-5.0", + CCC: "clang++-5.0", }, - symbol: "clang-4.0" + symbol: "clang-5.0" })); queue.scheduleTask(merge(extra_base, { @@ -895,6 +913,13 @@ function scheduleTests(task_build, task_cert, test_base) { env: {NSS_DISABLE_AVX: "1"}, group: "Cipher" })); queue.scheduleTask(merge(no_cert_base, { + name: "Cipher tests", symbol: "NoSSSE3|NEON", tests: "cipher", + env: { + NSS_DISABLE_ARM_NEON: "1", + NSS_DISABLE_SSSE3: "1" + }, group: "Cipher" + })); + queue.scheduleTask(merge(no_cert_base, { name: "EC tests", symbol: "EC", tests: "ec" })); queue.scheduleTask(merge(no_cert_base, { @@ -946,6 +971,18 @@ async function scheduleTools() { kind: "test" }; + //ABI check task + queue.scheduleTask(merge(base, { + symbol: "abi", + name: "abi", + image: LINUX_IMAGE, + command: [ + "/bin/bash", + "-c", + "bin/checkout.sh && nss/automation/taskcluster/scripts/check_abi.sh" + ], + })); + queue.scheduleTask(merge(base, { symbol: "clang-format-3.9", name: "clang-format-3.9", @@ -958,13 +995,13 @@ async function scheduleTools() { })); queue.scheduleTask(merge(base, { - symbol: "scan-build-4.0", - name: "scan-build-4.0", + symbol: "scan-build-5.0", + name: "scan-build-5.0", image: LINUX_IMAGE, env: { USE_64: "1", - CC: "clang", - CCC: "clang++", + CC: "clang-5.0", + CCC: "clang++-5.0", }, artifacts: { public: { @@ -991,5 +1028,69 @@ 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 -m32" + ] + })); + + 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" + ] + })); + + 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" + ] + })); + return queue.submit(); } diff --git a/security/nss/automation/taskcluster/graph/src/image_builder.js b/security/nss/automation/taskcluster/graph/src/image_builder.js index b89b6980c..d9d7755dc 100644 --- a/security/nss/automation/taskcluster/graph/src/image_builder.js +++ b/security/nss/automation/taskcluster/graph/src/image_builder.js @@ -30,7 +30,7 @@ export async function buildTask({name, path}) { let ns = `docker.images.v1.${process.env.TC_PROJECT}.${name}.hash.${hash}`; return { - name: "Image Builder", + name: `Image Builder (${name})`, image: "nssdev/image_builder:0.1.5", routes: ["index." + ns], env: { diff --git a/security/nss/automation/taskcluster/graph/src/queue.js b/security/nss/automation/taskcluster/graph/src/queue.js index 29b570729..809a17bf1 100644 --- a/security/nss/automation/taskcluster/graph/src/queue.js +++ b/security/nss/automation/taskcluster/graph/src/queue.js @@ -31,10 +31,11 @@ function parseRoutes(routes) { ]; // Notify about failures (except on try). - if (process.env.TC_PROJECT != "nss-try") { + // Turned off, too noisy. + /*if (process.env.TC_PROJECT != "nss-try") { rv.push(`notify.email.${process.env.TC_OWNER}.on-failed`, `notify.email.${process.env.TC_OWNER}.on-exception`); - } + }*/ return rv; } diff --git a/security/nss/automation/taskcluster/graph/src/try_syntax.js b/security/nss/automation/taskcluster/graph/src/try_syntax.js index 1f4e12eee..1c06dde13 100644 --- a/security/nss/automation/taskcluster/graph/src/try_syntax.js +++ b/security/nss/automation/taskcluster/graph/src/try_syntax.js @@ -51,7 +51,7 @@ function parseOptions(opts) { } // Parse tools. - let allTools = ["clang-format", "scan-build", "hacl"]; + let allTools = ["clang-format", "scan-build", "hacl", "saw", "abi"]; let tools = intersect(opts.tools.split(/\s*,\s*/), allTools); // If the given value is "all" run all tools. @@ -77,7 +77,8 @@ function filter(opts) { // are not affected by platform or build type selectors. if (task.platform == "nss-tools") { return opts.tools.some(tool => { - return task.symbol.toLowerCase().startsWith(tool); + return task.symbol.toLowerCase().startsWith(tool) || + (task.group && task.group.toLowerCase().startsWith(tool)); }); } diff --git a/security/nss/automation/taskcluster/scripts/check_abi.sh b/security/nss/automation/taskcluster/scripts/check_abi.sh new file mode 100644 index 000000000..dbc1a476f --- /dev/null +++ b/security/nss/automation/taskcluster/scripts/check_abi.sh @@ -0,0 +1,172 @@ +#! /bin/bash + +set_env() +{ + cd /home/worker + HGDIR=/home/worker + OUTPUTDIR=$(pwd)$(echo "/output") + DATE=$(date "+TB [%Y-%m-%d %H:%M:%S]") + + if [ ! -d "${OUTPUTDIR}" ]; then + echo "Creating output dir" + mkdir "${OUTPUTDIR}" + fi + + if [ ! -d "nspr" ]; then + for i in 0 2 5; do + sleep $i + hg clone -r "default" "https://hg.mozilla.org/projects/nspr" "${HGDIR}/nspr" && break + rm -rf nspr + done + fi + + cd nss + ./build.sh -v -c + cd .. +} + +check_abi() +{ + set_env + set +e #reverses set -e from build.sh to allow possible hg clone failures + if [[ "$1" != --nobuild ]]; then # Start nobuild block + + echo "######## NSS ABI CHECK ########" + echo "######## creating temporary HG clones ########" + + rm -rf ${HGDIR}/baseline + mkdir ${HGDIR}/baseline + BASE_NSS=`cat ${HGDIR}/nss/automation/abi-check/previous-nss-release` #Reads the version number of the last release from the respective file + NSS_CLONE_RESULT=0 + for i in 0 2 5; do + sleep $i + hg clone -u "${BASE_NSS}" "https://hg.mozilla.org/projects/nss" "${HGDIR}/baseline/nss" + if [ $? -eq 0 ]; then + NSS_CLONE_RESULT=0 + break + fi + rm -rf "${HGDIR}/baseline/nss" + NSS_CLONE_RESULT=1 + done + if [ ${NSS_CLONE_RESULT} -ne 0 ]; then + echo "invalid tag in automation/abi-check/previous-nss-release" + return 1 + fi + + BASE_NSPR=NSPR_$(head -1 ${HGDIR}/baseline/nss/automation/release/nspr-version.txt | cut -d . -f 1-2 | tr . _)_BRANCH + hg clone -u "${BASE_NSPR}" "https://hg.mozilla.org/projects/nspr" "${HGDIR}/baseline/nspr" + NSPR_CLONE_RESULT=$? + + if [ ${NSPR_CLONE_RESULT} -ne 0 ]; then + rm -rf "${HGDIR}/baseline/nspr" + for i in 0 2 5; do + sleep $i + hg clone -u "default" "https://hg.mozilla.org/projects/nspr" "${HGDIR}/baseline/nspr" && break + rm -rf "${HGDIR}/baseline/nspr" + done + echo "Nonexisting tag ${BASE_NSPR} derived from ${BASE_NSS} automation/release/nspr-version.txt" + echo "Using default branch instead." + fi + + echo "######## building baseline NSPR/NSS ########" + echo "${HGDIR}/baseline/nss/build.sh" + cd ${HGDIR}/baseline/nss + ./build.sh -v -c + cd ${HGDIR} + else # Else nobuild block + echo "######## using existing baseline NSPR/NSS build ########" + fi # End nobuild block + + set +e #reverses set -e from build.sh to allow abidiff failures + + echo "######## Starting abidiff procedure ########" + abi_diff +} + +#Slightly modified from builbot-slave/build.sh +abi_diff() +{ + ABI_PROBLEM_FOUND=0 + ABI_REPORT=${OUTPUTDIR}/abi-diff.txt + rm -f ${ABI_REPORT} + PREVDIST=${HGDIR}/baseline/dist + NEWDIST=${HGDIR}/dist + ALL_SOs="libfreebl3.so libfreeblpriv3.so libnspr4.so libnss3.so libnssckbi.so libnssdbm3.so libnsssysinit.so libnssutil3.so libplc4.so libplds4.so libsmime3.so libsoftokn3.so libssl3.so" + for SO in ${ALL_SOs}; do + if [ ! -f ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt ]; then + touch ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt + fi + abidiff --hd1 $PREVDIST/public/ --hd2 $NEWDIST/public \ + $PREVDIST/*/lib/$SO $NEWDIST/*/lib/$SO \ + > ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt + RET=$? + cat ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt \ + | grep -v "^Functions changes summary:" \ + | grep -v "^Variables changes summary:" \ + > ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt + rm -f ${HGDIR}/nss/automation/abi-check/new-report-temp$SO.txt + + ABIDIFF_ERROR=$((($RET & 0x01) != 0)) + ABIDIFF_USAGE_ERROR=$((($RET & 0x02) != 0)) + ABIDIFF_ABI_CHANGE=$((($RET & 0x04) != 0)) + ABIDIFF_ABI_INCOMPATIBLE_CHANGE=$((($RET & 0x08) != 0)) + ABIDIFF_UNKNOWN_BIT_SET=$((($RET & 0xf0) != 0)) + + # If abidiff reports an error, or a usage error, or if it sets a result + # bit value this script doesn't know yet about, we'll report failure. + # For ABI changes, we don't yet report an error. We'll compare the + # result report with our whitelist. This allows us to silence changes + # that we're already aware of and have been declared acceptable. + + REPORT_RET_AS_FAILURE=0 + if [ $ABIDIFF_ERROR -ne 0 ]; then + echo "abidiff reported ABIDIFF_ERROR." + REPORT_RET_AS_FAILURE=1 + fi + if [ $ABIDIFF_USAGE_ERROR -ne 0 ]; then + echo "abidiff reported ABIDIFF_USAGE_ERROR." + REPORT_RET_AS_FAILURE=1 + fi + if [ $ABIDIFF_UNKNOWN_BIT_SET -ne 0 ]; then + echo "abidiff reported ABIDIFF_UNKNOWN_BIT_SET." + REPORT_RET_AS_FAILURE=1 + fi + + if [ $ABIDIFF_ABI_CHANGE -ne 0 ]; then + echo "Ignoring abidiff result ABI_CHANGE, instead we'll check for non-whitelisted differences." + fi + if [ $ABIDIFF_ABI_INCOMPATIBLE_CHANGE -ne 0 ]; then + echo "Ignoring abidiff result ABIDIFF_ABI_INCOMPATIBLE_CHANGE, instead we'll check for non-whitelisted differences." + fi + + if [ $REPORT_RET_AS_FAILURE -ne 0 ]; then + ABI_PROBLEM_FOUND=1 + echo "abidiff {$PREVDIST , $NEWDIST} for $SO FAILED with result $RET, or failed writing to ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt" + fi + if [ ! -f ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt ]; then + ABI_PROBLEM_FOUND=1 + echo "FAILED to access report file: ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt" + fi + + diff -wB -u ${HGDIR}/nss/automation/abi-check/expected-report-$SO.txt \ + ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt >> ${ABI_REPORT} + if [ ! -f ${ABI_REPORT} ]; then + ABI_PROBLEM_FOUND=1 + echo "FAILED to compare exepcted and new report: ${HGDIR}/nss/automation/abi-check/new-report-$SO.txt" + fi + done + + if [ -s ${ABI_REPORT} ]; then + echo "FAILED: there are new unexpected ABI changes" + cat ${ABI_REPORT} + return 1 + elif [ $ABI_PROBLEM_FOUND -ne 0 ]; then + echo "FAILED: failure executing the ABI checks" + cat ${ABI_REPORT} + return 1 + fi + + return 0 +} + +check_abi $1 diff --git a/security/nss/automation/taskcluster/scripts/run_saw.sh b/security/nss/automation/taskcluster/scripts/run_saw.sh new file mode 100644 index 000000000..0e9a8224a --- /dev/null +++ b/security/nss/automation/taskcluster/scripts/run_saw.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +source $(dirname "$0")/tools.sh + +# Fetch artifact if needed. +fetch_dist + +# Run SAW. +saw "nss/automation/saw/$1.saw" diff --git a/security/nss/automation/taskcluster/scripts/run_scan_build.sh b/security/nss/automation/taskcluster/scripts/run_scan_build.sh index 4024c226e..014530b42 100755 --- a/security/nss/automation/taskcluster/scripts/run_scan_build.sh +++ b/security/nss/automation/taskcluster/scripts/run_scan_build.sh @@ -34,7 +34,7 @@ for i in "${!scan[@]}"; do done # run scan-build (only building affected directories) -scan-build -o /home/worker/artifacts --use-cc=$CC --use-c++=$CCC make nss_build_all && cd .. +scan-build-5.0 -o /home/worker/artifacts --use-cc=$CC --use-c++=$CCC make nss_build_all && cd .. # print errors we found set +v +x |