Add DH concurrency proof

Author: amzn-jasonrk

dh/argot-proofs/dh-concurrency-proof.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+# Script to run the goroutine analysis proof on the DH implementation
+
+PWD=$(dirname "$0")
+SCRIPT_DIR=$(realpath "$PWD")
+AGENT_DIR="$SCRIPT_DIR"/../implementation
+ARGOT_BIN=argot
+
+if [ ! -e "$AGENT_DIR" ]; then
+    echo Error: "$AGENT_DIR" does not exist
+    exit 1
+fi
+cd "$AGENT_DIR" || exit
+
+echo "Running goroutine analysis on DH implementation in directory $(pwd)"
+
+"$ARGOT_BIN" goroutine -config "$SCRIPT_DIR"/argot-config-dh.yaml

dh/argot-proofs/escape-config.json

@@ -105,8 +105,9 @@
         "(*io.multiWriter).Write": "noop",
         "fmt.Errorf": "noop",
         "(*encoding/base64.Encoding).DecodeString": "summarize",
+        "(encoding/binary.bigEndian).Uint32": "summarize",
         "(*github.com/go-git/go-git/v5/plumbing/format/idxfile.Encoder).Write": "noop"
     },
-    "pkg-filter": "(dh-gobra.*)|(github.com/aws/amazon-ssm-agent.*)|(command-line-arguments)|(encoding/base64)|(sync)|(bytes)|(unicode)|(crypto/internal)|(crypto/aes)|(crypto/cipher)|(crypto/sha512)|(crypto/sha1)|(crypto/sha256)|(crypto/md5)|(crypto/subtle)|(hash/crc32)|(math/big)|(github.com/go-git/go-git/v5/plumbing.*)",
+    "pkg-filter": "(dh-gobra.*)|(command-line-arguments)|(encoding/base64)|(sync)|(bytes)|(unicode)|(crypto/internal)|(crypto/aes)|(crypto/cipher)|(crypto/sha512)|(crypto/sha1)|(crypto/sha256)|(crypto/nacl)|(crypto/ed25519)|(crypto/md5)|(crypto/chacha20)|(crypto/subtle)|(hash/crc32)|(math/big)|(github.com/go-git/go-git/v5/plumbing.*)",
     "default-summarize": false
 }

docker/dh/verify-core-assumptions.sh

@@ -15,7 +15,7 @@ SCRIPT_DIR=$(realpath "$PWD")
 /bin/bash "$SCRIPT_DIR/argot-proofs/dh-passthru-proof.sh"
 
 # TODO Verify that each core instance does not escape the goroutine in which it is created
-# /bin/bash "$SCRIPT_DIR/argot-proofs/dh-concurrency-proof.sh"
+/bin/bash "$SCRIPT_DIR/argot-proofs/dh-concurrency-proof.sh"
 
 # Verify that no arguments to core functions alias each other
 /bin/bash "$SCRIPT_DIR/argot-proofs/dh-argument-alias-proof.sh"