adds papaer artifact

viperproject · Sep 10, 2023 · bae637c · bae637c
commit bae637c
Show file tree

Hide file tree

Showing 277 changed files with 41,748 additions and 0 deletions.
diff --git a/.github/workflows/dh.yml b/.github/workflows/dh.yml
@@ -0,0 +1,74 @@
+name: Verification of DH Case Study
+
+on:
+  push:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    container:
+      image: ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29 # Gobra commit f21fe70
+    steps:
+      - name: Install prerequisites
+        run: apt-get update && apt-get install -y git wget jq
+
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Install Go
+        run: |
+          mkdir tmp
+          cd tmp
+          wget --quiet 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
+          echo "/usr/local/go/bin" >> $GITHUB_PATH
+
+      - name: Point Go to repo copy
+        run: go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$GITHUB_WORKSPACE/ReusableVerificationLibrary
+        working-directory: casestudies/dh
+
+      - name: Compile DH initiator & responder
+        run: ./compile.sh
+        working-directory: casestudies/dh
+
+      - name: Execute DH initiator & responder
+        run: ./dh
+        working-directory: casestudies/dh
+
+      - name: Setup verification of DH
+        run: |
+          ./load-modules.sh "$GITHUB_WORKSPACE/.modules"
+          mkdir -p $GITHUB_WORKSPACE/.modules/github.com/viperproject
+        working-directory: casestudies/dh
+
+      - name: Link Reusable Verification Library
+        run: ln -s $GITHUB_WORKSPACE/ReusableVerificationLibrary .modules/github.com/viperproject/ReusableProtocolVerificationLibrary
+
+      - name: Verify DH initiator
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/dh/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/dh --parallelizeBranches"
+          java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages initiator
+        working-directory: casestudies/dh
+
+      - name: Verify DH responder role
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/dh/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/dh --parallelizeBranches"
+          java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages responder
+        working-directory: casestudies/dh
+
+      - name: Verify DH trace invariants & main package
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/dh/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/dh --parallelizeBranches"
+          # verify packages located in the current directory and in `common`:
+          java -Xss128m -jar $gobraJar --directory ./ common -I ./ $additionalGobraArgs
+        working-directory: casestudies/dh
diff --git a/.github/workflows/library.yml b/.github/workflows/library.yml
@@ -0,0 +1,21 @@
+name: Verification of Reusable Verification Library for Gobra
+
+on:
+  push:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    container:
+      image: ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29 # Gobra commit f21fe70
+    steps:
+      - name: Install git
+        run: apt-get update && apt-get install -y git
+
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Verify the entire Reusable Verification Library
+        run: ./verify.sh
+        working-directory: ReusableVerificationLibrary
diff --git a/.github/workflows/nsl.yml b/.github/workflows/nsl.yml
@@ -0,0 +1,82 @@
+name: Verification of NSL Case Study
+
+on:
+  push:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    container:
+      image: ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29 # Gobra commit f21fe70
+    steps:
+      - name: Install prerequisites
+        run: apt-get update && apt-get install -y git wget jq
+
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Install Go
+        run: |
+          mkdir tmp
+          cd tmp
+          wget --quiet 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
+          echo "/usr/local/go/bin" >> $GITHUB_PATH
+
+      - name: Point Go to repo copy
+        run: go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$GITHUB_WORKSPACE/ReusableVerificationLibrary
+        working-directory: casestudies/nsl
+
+      - name: Compile NSL initiator & responder
+        run: ./compile.sh
+        working-directory: casestudies/nsl
+
+      - name: Execute NSL initiator & responder
+        run: ./nsl
+        working-directory: casestudies/nsl
+
+      - name: Setup verification of NSL
+        run: |
+          ./load-modules.sh "$GITHUB_WORKSPACE/.modules"
+          mkdir -p $GITHUB_WORKSPACE/.modules/github.com/viperproject
+        working-directory: casestudies/nsl
+
+      - name: Link Reusable Verification Library
+        run: ln -s $GITHUB_WORKSPACE/ReusableVerificationLibrary .modules/github.com/viperproject/ReusableProtocolVerificationLibrary
+
+      - name: Verify NSL initiator role 1
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
+          java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages initiator
+        working-directory: casestudies/nsl
+
+      - name: Verify NSL initiator role 2
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
+          java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages initiator2
+        working-directory: casestudies/nsl
+
+      - name: Verify NSL responder role
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
+          java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages responder
+        working-directory: casestudies/nsl
+
+      - name: Verify NSL trace invariants & main package
+        run: |
+          mkdir -p .gobra
+          gobraJar="/gobra/gobra.jar"
+          additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
+          # verify packages located in the current directory and in `common`:
+          java -Xss128m -jar $gobraJar --directory ./ common -I ./ $additionalGobraArgs
+        working-directory: casestudies/nsl
diff --git a/.github/workflows/verifast-library.yml b/.github/workflows/verifast-library.yml
@@ -0,0 +1,29 @@
+name: Verification of Reusable Verification Library in C
+
+on:
+  push:
+
+jobs:
+  build-verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    env:
+      VERIFAST_VERSION: 21.04
+    steps:
+      - name: Install prerequisites
+        run: sudo apt-get update && sudo apt-get install -y git curl tar libgomp1
+
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Download and Setup VeriFast
+        run: |
+          curl -q -s -S -L --create-dirs -o VeriFast.zip https://github.com/verifast/verifast/releases/download/${{ env.VERIFAST_VERSION }}/verifast-${{ env.VERIFAST_VERSION }}-linux.tar.gz
+          tar xzf VeriFast.zip
+          # this creates a folder called 'verifast-${{ env.VERIFAST_VERSION }}'
+          VERIFAST_BIN="$PWD/verifast-${{ env.VERIFAST_VERSION }}/bin"
+          echo "$VERIFAST_BIN" >> $GITHUB_PATH
+
+      - name: Verify Reusable Verification Library in VeriFast
+        run: ./verify.sh
+        working-directory: VeriFastPrototype/reusable_verification_library
diff --git a/.github/workflows/verifast-nsl.yml b/.github/workflows/verifast-nsl.yml
@@ -0,0 +1,33 @@
+name: Verification of the NSL case study in C
+
+on:
+  push:
+
+jobs:
+  build-verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    env:
+      VERIFAST_VERSION: 21.04
+    steps:
+      - name: Install prerequisites
+        run: sudo apt-get update && sudo apt-get install -y git curl tar libgomp1
+
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: Download and Setup VeriFast
+        run: |
+          curl -q -s -S -L --create-dirs -o VeriFast.zip https://github.com/verifast/verifast/releases/download/${{ env.VERIFAST_VERSION }}/verifast-${{ env.VERIFAST_VERSION }}-linux.tar.gz
+          tar xzf VeriFast.zip
+          # this creates a folder called 'verifast-${{ env.VERIFAST_VERSION }}'
+          VERIFAST_BIN="$PWD/verifast-${{ env.VERIFAST_VERSION }}/bin"
+          echo "$VERIFAST_BIN" >> $GITHUB_PATH
+
+      - name: Compile and execute NSL initiator & responder
+        run: ./execute.sh
+        working-directory: VeriFastPrototype/nsl
+
+      - name: Verify NSL initiator & responder using VeriFast
+        run: ./verify.sh
+        working-directory: VeriFastPrototype/nsl
diff --git a/.github/workflows/wireguard.yml b/.github/workflows/wireguard.yml
@@ -0,0 +1,63 @@
+name: Verification of WireGuard Case Study
+
+on:
+  push:
+
+jobs:
+  build-verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    env:
+      IMAGE_NAME: securityprotocolimplementations-wireguard
+    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/wireguard/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 }}
+
+      - 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 }}