adds artifact Docker image

.github/workflows/artifact.yml

@@ -0,0 +1,64 @@
+name: Creation of Artifact Docker Image
+
+on:
+  push:
+
+jobs:
+  build-verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    env:
+      IMAGE_NAME: securityprotocolimplementations-artifact
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Create Image ID
+        run: |
+          REPO_OWNER=$(echo "${{ github.repository_owner }}" | tr '[:upper:]' '[:lower:]')
+          echo "IMAGE_ID=ghcr.io/$REPO_OWNER/${{ env.IMAGE_NAME }}" >>$GITHUB_ENV
+
+      - name: Image version
+        run: |
+          VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,')
+          [ "$VERSION" == "main" ] && VERSION=latest
+          echo "IMAGE_TAG=${{ env.IMAGE_ID }}:$VERSION" >> $GITHUB_ENV
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v2
+
+      - name: Build image
+        uses: docker/build-push-action@v4
+        with:
+          context: .
+          load: true
+          file: casestudies/docker/Dockerfile
+          tags: ${{ env.IMAGE_TAG }}
+          labels: "runnumber=${{ github.run_id }}"
+          push: false
+          cache-from: type=gha, scope=${{ github.workflow }}
+          cache-to: type=gha, scope=${{ github.workflow }}
+
+      # TODO
+      # - name: Execute initiator & responder
+      #   run: docker run ${{ env.IMAGE_TAG }} ./test.sh
+
+      # - name: Verify initiator & responder
+      #   run: docker run ${{ env.IMAGE_TAG }} ./verify.sh
+
+      - name: Login to Github Packages
+        uses: docker/login-action@v2
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Push image
+        uses: docker/build-push-action@v4
+        with:
+          context: .
+          file: casestudies/wireguard/docker/Dockerfile
+          tags: ${{ env.IMAGE_TAG }}
+          labels: "runnumber=${{ github.run_id }}"
+          push: true
+          cache-from: type=gha, scope=${{ github.workflow }}
+          cache-to: type=gha, scope=${{ github.workflow }}

ReusableVerificationLibrary/verify.sh

@@ -11,12 +11,16 @@ isCi=$CI
 mkdir -p $scriptDir/.gobra
 
 gobraJar="/gobra/gobra.jar"
-additionalGobraArgs="--module github.com/viperproject/ReusableProtocolVerificationLibrary --include .verification --gobraDirectory $scriptDir/.gobra --parallelizeBranches"
+additionalGobraArgs="-I $scriptDir -I $scriptDir/.verification --module github.com/viperproject/ReusableProtocolVerificationLibrary  --parallelizeBranches"
 
 if [ $isCi ]; then
     echo -e "\033[0Ksection_start:`date +%s`:verify[collapsed=true]\r\033[0KVerifying packages"
 fi
-java -Xss128m -jar $gobraJar --recursive -I $scriptDir $additionalGobraArgs
+java -Xss128m -jar $gobraJar \
+    --projectRoot $scriptDir \
+    --gobraDirectory "$scriptDir/.gobra" \
+    --recursive \
+    $additionalGobraArgs
 exitCode=$?
 if [ $isCi ]; then
     echo -e "\033[0Ksection_end:`date +%s`:verify\r\033[0K"

VeriFastPrototype/nsl/compile.sh

@@ -50,6 +50,6 @@ C_FILES=($TMP_DIR/*.c)
 C_FILES_STR=$(printf "%s " "${C_FILES[@]}")
 
 # compile initiator and responder
-gcc $C_FILES_STR -iquote $VERIFAST_BIN -lcrypto -o nsl
+gcc $C_FILES_STR -iquote $VERIFAST_BIN -lcrypto -lpthread -o $SCRIPT_DIR/nsl
 
 rm -r $TMP_DIR

casestudies/wireguard/docker/compile.sh

@@ -1,3 +1,9 @@
 #!/bin/bash
 
-go build -v -o wireguard-gobra
+# exit when any command fails
+set -e
+
+scriptDir=$(dirname "$0")
+
+# temporarily switch to `$scriptDir`:
+(cd "$scriptDir" && go build -v -o wireguard-gobra)

casestudies/wireguard/docker/test.sh

@@ -1,9 +1,14 @@
 #!/bin/bash
 
-source ./compile.sh
+# exit when any command fails
+set -e
+
+scriptDir=$(dirname "$0")
+
+source "$scriptDir/compile.sh"
 
 function initiator() {
-    echo -e "Hello\nWorld!\n" | ./wireguard-gobra \
+    echo -e "Hello\nWorld!\n" | "$scriptDir/wireguard-gobra" \
         --interfaceName utun10 \
         --privateKey YIQ1ZXYUVs6OjE2GjDhJgAqoJDaPPdReVtSQ1zOy7n8= \
         --publicKey Y1842DzWWfqP42p9SJNoX1fEJdTOkuyi/fx+1Y7aFU4= \
@@ -15,7 +20,7 @@ function initiator() {
 }
 
 function responder() {
-    echo -e "Hello back\nI'm the responder\n" | ./wireguard-gobra \
+    echo -e "Hello back\nI'm the responder\n" | "$scriptDir/wireguard-gobra" \
         --interfaceName utun8 \
         --privateKey oCxC44w/QKqastjiex7OTiKCfJphexquZ3MmJE5upU0= \
         --publicKey poKDYnMyFZWkSwGlAXXb79nh0L8rEb+S8XWAtXQxsmc= \

casestudies/wireguard/docker/verify.sh

@@ -4,27 +4,33 @@
 set -e
 
 scriptDir=$(dirname "$0")
-mkdir -p .gobra
+mkdir -p "$scriptDir/.gobra"
 
-additionalGobraArgs="-I $scriptDir/verification -I $scriptDir/.modules-precedence -I $scriptDir/.modules -I $scriptDir --module github.com/viperproject/ProtocolVerificationCaseStudies/wireguard --gobraDirectory $scriptDir/.gobra --parallelizeBranches"
+additionalGobraArgs="-I $scriptDir/verification -I $scriptDir/.modules-precedence -I $scriptDir/.modules -I $scriptDir --module github.com/viperproject/ProtocolVerificationCaseStudies/wireguard --parallelizeBranches"
 
 # verify initiator
 echo "Verifying the Initiator. This might take some time..."
-java -Xss128m -jar gobra.jar \
+java -Xss128m -jar /gobra/gobra.jar \
+    --projectRoot $scriptDir \
+    --gobraDirectory "$scriptDir/.gobra" \
     --recursive \
     --includePackages initiator \
     $additionalGobraArgs
 
 # verify responder
 echo "Verifying the Responder. This might take some time..."
-java -Xss128m -jar gobra.jar \
+java -Xss128m -jar /gobra/gobra.jar \
+    --projectRoot $scriptDir \
+    --gobraDirectory "$scriptDir/.gobra" \
     --recursive \
     --includePackages responder \
     $additionalGobraArgs
 
 echo "Verifying packages containing lemmas and trace invariants. This might take some time..."
 packages="common messageCommon messageInitiator messageResponder labelLemma labelLemmaCommon labelLemmaInitiator labelLemmaResponder"
-java -Xss128m -jar gobra.jar \
+java -Xss128m -jar /gobra/gobra.jar \
+    --projectRoot $scriptDir \
+    --gobraDirectory "$scriptDir/.gobra" \
     --recursive \
     --includePackages $packages \
     $additionalGobraArgs

docker/Dockerfile

@@ -0,0 +1,167 @@
+# Gobra commit f21fe70
+FROM ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29
+
+RUN apt-get update && \
+	apt-get install -y \
+    curl \
+    gcc \
+    wget \
+    jq \
+    build-essential \
+    checkinstall \
+    zlib1g-dev
+
+# install openssl
+RUN mkdir tmp && \
+    cd tmp && \
+    wget https://www.openssl.org/source/openssl-3.1.3.tar.gz && \
+    tar xvf openssl-3.1.3.tar.gz && \
+    cd openssl-3.1.3 && \
+    ./config && \
+    make && \
+    make install && \
+    ldconfig && \
+    cd ../../ && \
+    rm -rf tmp
+
+# install go
+RUN mkdir tmp && \
+    cd tmp && \
+    wget https://go.dev/dl/go1.17.3.linux-amd64.tar.gz && \
+    rm -rf /usr/local/go && tar -C /usr/local -xzf go1.17.3.linux-amd64.tar.gz && \
+    cd ../ && \
+    rm -rf tmp
+
+# add Go to path:
+ENV PATH="${PATH}:/usr/local/go/bin"
+
+# install VeriFast
+ARG VERIFAST_VERSION=21.04
+RUN mkdir tmp && \
+    cd tmp && \
+    curl -q -s -S -L --create-dirs -o VeriFast.zip https://github.com/verifast/verifast/releases/download/$VERIFAST_VERSION/verifast-$VERIFAST_VERSION-linux.tar.gz && \
+    tar xzf VeriFast.zip && \
+    # this creates a folder called 'verifast-$VERIFAST_VERSION'
+    mv verifast-$VERIFAST_VERSION /usr/local && \
+    cd ../ && \
+    rm -rf tmp
+
+# add VeriFast to path:
+ENV PATH="${PATH}:/usr/local/verifast-$VERIFAST_VERSION/bin"
+ENV VERIFAST_BIN="/usr/local/verifast-$VERIFAST_VERSION/bin"
+
+RUN mkdir C && mkdir Go
+
+# copy the reusable verification library
+COPY ReusableVerificationLibrary ./Go/ReusableVerificationLibrary
+
+ENV ReusableVerificationLibrary=/gobra/Go/ReusableVerificationLibrary
+
+# copy DH
+copy casestudies/dh ./Go/dh
+
+# point Go to local copy of the library:
+RUN cd ./Go/dh && \
+    go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$ReusableVerificationLibrary
+
+# load modules and manually add symlink to reusable verification library:
+RUN cd ./Go/dh && \
+    ./load-modules.sh "../.modules" && \
+    mkdir -p ../.modules/github.com/viperproject && \
+    ln -s $ReusableVerificationLibrary ../.modules/github.com/viperproject/ReusableProtocolVerificationLibrary
+
+# compile to trigger download of dependent Go packages:
+RUN cd ./Go/dh && \
+    ./compile.sh
+
+# copy NSL
+copy casestudies/nsl ./Go/nsl
+
+# point Go to local copy of the library:
+RUN cd ./Go/nsl && \
+    go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$ReusableVerificationLibrary
+
+# load modules and manually add symlink to reusable verification library:
+RUN cd ./Go/nsl && \
+    ./load-modules.sh "../.modules"
+    # mkdir -p .modules/github.com/viperproject && \
+    # ln -s $ReusableVerificationLibrary .modules/github.com/viperproject/ReusableProtocolVerificationLibrary
+
+# compile to trigger download of dependent Go packages:
+RUN cd ./Go/nsl && \
+    ./compile.sh
+
+# copy WireGuard
+copy casestudies/wireguard ./Go/wireguard
+# RUN mkdir wireguard
+# COPY casestudies/wireguard/.modules-precedence ./Go/wireguard/.modules-precedence
+# COPY casestudies/wireguard/conn ./Go/wireguard/conn
+# COPY casestudies/wireguard/device ./Go/wireguard/device
+# COPY casestudies/wireguard/endpoint ./Go/wireguard/endpoint
+# COPY casestudies/wireguard/initiator ./Go/wireguard/initiator
+# COPY casestudies/wireguard/ipc ./Go/wireguard/ipc
+# COPY casestudies/wireguard/library ./Go/wireguard/library
+# COPY casestudies/wireguard/log ./Go/wireguard/log
+# COPY casestudies/wireguard/replay ./Go/wireguard/replay
+# COPY casestudies/wireguard/responder ./Go/wireguard/responder
+# COPY casestudies/wireguard/tai64n ./Go/wireguard/tai64n
+# COPY casestudies/wireguard/tun ./Go/wireguard/tun
+# COPY casestudies/wireguard/verification ./Go/wireguard/verification
+# COPY casestudies/wireguard/go.mod ./Go/wireguard
+# COPY casestudies/wireguard/go.sum ./Go/wireguard
+# COPY casestudies/wireguard/main.go ./Go/wireguard
+# COPY casestudies/wireguard/README.md ./Go/wireguard
+# COPY casestudies/wireguard/docker/compile.sh ./Go/wireguard
+# COPY casestudies/wireguard/docker/test.sh ./Go/wireguard
+# COPY casestudies/wireguard/docker/verify.sh ./Go/wireguard
+# COPY casestudies/wireguard/load-modules.sh ./Go/wireguard
+RUN mv ./Go/wireguard/docker/compile.sh ./Go/wireguard && \
+    mv ./Go/wireguard/docker/test.sh ./Go/wireguard && \
+    mv ./Go/wireguard/docker/verify.sh ./Go/wireguard
+
+# point Go to local copy of the library:
+RUN cd ./Go/wireguard && \
+    go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$ReusableVerificationLibrary
+
+# load modules and manually add symlink to reusable verification library:
+RUN cd ./Go/wireguard && \
+    ./load-modules.sh && \
+    mkdir -p .modules/github.com/viperproject && \
+    ln -s $ReusableVerificationLibrary .modules/github.com/viperproject/ReusableProtocolVerificationLibrary
+
+# compile to trigger download of dependent Go packages:
+RUN cd ./Go/wireguard && \
+    ./compile.sh
+
+# copy the reusable verification library
+COPY VeriFastPrototype/reusable_verification_library ./C/reusable_verification_library
+
+# copy NSL
+COPY VeriFastPrototype/nsl ./C/nsl
+
+# copy shell scripts
+COPY docker/*.sh ./
+
+# set library paths correctly such that compiling and executing the C NSL implementation
+# works:
+ENV LD_LIBRARY_PATH="/usr/local/openssl/lib:${LD_LIBRARY_PATH}"
+ENV LD_LIBRARY_PATH="/usr/local/lib64:${LD_LIBRARY_PATH}"
+
+# install a code editor for convenience:
+RUN apt-get install -y vim
+
+# remove some unneeded folders that come with the base image:
+RUN rm -r evaluation
+RUN rm -r tutorial-examples
+
+RUN mv Go Go-orig && \
+    mv C C-orig
+
+RUN mkdir Go && \
+    mkdir C
+
+# disable entry point specified by the Gobra base container:
+# ENTRYPOINT []
+ENTRYPOINT cp -r Go-orig/. Go/ && \
+    cp -r C-orig/. C/ && \
+    /bin/bash

docker/test-c-nsl.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/C/nsl/execute.sh

docker/test-dh.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/Go/dh/compile.sh
+/gobra/Go/dh/dh

docker/test-nsl.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/Go/nsl/compile.sh
+/gobra/Go/nsl/nsl

docker/test-wireguard.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/Go/wireguard/test.sh

docker/verify-c-library.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/C/reusable_verification_library/verify.sh

docker/verify-c-nsl.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# exit when any command fails
+set -e
+
+/gobra/C/nsl/verify.sh