merge master

.github/dependabot.yml

@@ -0,0 +1,12 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: "/"
+    schedule:
+      interval: monthly
+      day: monday
+    groups:
+      all:
+        patterns:
+          - "*"

.github/workflows/license-check.yml

@@ -16,9 +16,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Gobra
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
       - name: Check license headers
-        uses: viperproject/check-license-header@v1
+        uses: viperproject/check-license-header@v2
         with:
           path: ./
           config: ./.github/license-check/config.json

.github/workflows/test.yml

@@ -15,7 +15,15 @@ jobs:
   build-test-deploy-container:
     runs-on: ubuntu-latest
     env:
-      IMAGE_NAME: gobra
+      IMAGE_ID: ghcr.io/${{ github.repository_owner }}/gobra
+      # image labels are new-line separated key value pairs (according to https://specs.opencontainers.org/image-spec/annotations/):
+      IMAGE_LABELS: |
+        org.opencontainers.image.authors=Viper Project <https://viper.ethz.ch>
+        org.opencontainers.image.url=https://github.com/viperproject/gobra/pkgs/container/gobra
+        org.opencontainers.image.source=${{ github.server_url }}/${{ github.repository }}
+        org.opencontainers.image.revision=${{ github.sha }}
+        org.opencontainers.image.licenses=MPL-2.0
+        org.opencontainers.image.description=Gobra image for revision ${{ github.sha }} built by workflow run ${{ github.run_id }}
       CONCLUSION_SUCCESS: "success"
       CONCLUSION_FAILURE: "failure"
       # Output levels according to severity.
@@ -25,43 +33,59 @@ jobs:
       FAILURE_LEVEL: "error"
     steps:
       - name: Checkout Gobra
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           submodules: 'recursive'
       - name: Check that silicon & carbon reference same silver commit
         run: |
           SILICON_SILVER_REF=$(git -C viperserver/silicon/silver rev-parse HEAD) && \
           CARBON_SILVER_REF=$(git -C viperserver/carbon/silver rev-parse HEAD) && \
           if [ "$SILICON_SILVER_REF" != "$CARBON_SILVER_REF" ]; then echo "Silicon and Carbon reference different Silver commits ($SILICON_SILVER_REF and $CARBON_SILVER_REF)" && exit 1 ; fi
-      - name: Create image tag
-        run: |
-          IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME
-
-          # Change all uppercase to lowercase
-          IMAGE_ID=$(echo $IMAGE_ID | tr '[A-Z]' '[a-z]')
-          # Strip git ref prefix from version
-          VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,')
-          # Strip "v" prefix from tag name
-          [[ "${{ github.ref }}" == "refs/tags/"* ]] && VERSION=$(echo $VERSION | sed -e 's/^v\.?//')
-          # Use Docker `latest` tag convention
-          [ "$VERSION" == "master" ] && VERSION=latest
-          echo "IMAGE_TAG=$IMAGE_ID:$VERSION" >> $GITHUB_ENV
 
       # used to enable Docker caching (see https://github.com/docker/build-push-action)
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1
+        uses: docker/setup-buildx-action@v3
+
+      - name: Create image creation label
+        run: |
+          CREATED_LABEL="org.opencontainers.image.created=$(date --rfc-3339=seconds)"
+          echo "CREATED_LABEL=$CREATED_LABEL" >> $GITHUB_ENV
+
+      - name: Create image metadata
+        id: image-metadata
+        uses: docker/metadata-action@v5
+        with:
+          images: ${{ env.IMAGE_ID }}
+          labels: |
+            ${{ env.IMAGE_LABELS }}
+            ${{ env.CREATED_LABEL }}
+          tags: |
+            # the first 4 tags correspond to the default options
+            type=schedule
+            type=ref,event=branch
+            type=ref,event=tag
+            type=ref,event=pr
+            # use (short) commit hash as tag:
+            type=sha
+            # use latest tag for default branch and with highest priority (1000 is the highest default priority for the other types):
+            type=raw,value=latest,priority=1100,enable={{is_default_branch}}
+
+      - name: Get first tag
+        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV
 
       - name: Build image up to including stage 'build'
+        id: image-build
         # note that the action's name is misleading: this step does NOT push
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v6
         with:
           context: .
           load: true # make the built image available in docker (locally)
           target: build # only build up to and including stage 'build'
           file: workflow-container/Dockerfile
-          tags: ${{ env.IMAGE_TAG }}
-          labels: "runnumber=${{ github.run_id }}"
+          tags: ${{ steps.image-metadata.outputs.tags }}
+          labels: ${{ steps.image-metadata.outputs.labels }}
           push: false
+          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
           # use GitHub cache:
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}
@@ -161,20 +185,21 @@ jobs:
 
       - name: Upload RAM usage
         if: ${{ always() }}
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: pidstat.txt
           path: sync/pidstat.txt
 
       - name: Build entire image
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v6
         with:
           context: .
           load: true # make the built image available in docker (locally)
           file: workflow-container/Dockerfile
-          tags: ${{ env.IMAGE_TAG }}
-          labels: "runnumber=${{ github.run_id }}"
+          tags: ${{ steps.image-metadata.outputs.tags }}
+          labels: ${{ steps.image-metadata.outputs.labels }}
           push: false
+          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
           # use GitHub cache:
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}
@@ -203,21 +228,22 @@ jobs:
 
       - name: Login to Github Packages
         if: env.SHOULD_DEPLOY == 'true'
-        uses: docker/login-action@v1
+        uses: docker/login-action@v3
         with:
           registry: ghcr.io
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Push entire image
         if: env.SHOULD_DEPLOY == 'true'
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v6
         with:
           context: .
           file: workflow-container/Dockerfile
-          tags: ${{ env.IMAGE_TAG }}
-          labels: "runnumber=${{ github.run_id }}"
+          tags: ${{ steps.image-metadata.outputs.tags }}
+          labels: ${{ steps.image-metadata.outputs.labels }}
           push: true
+          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
           # use GitHub cache:
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}

.github/workflows/update-submodules.yml

@@ -0,0 +1,59 @@
+# 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/.
+#
+# Copyright (c) 2011-2022 ETH Zurich.
+
+name: Update Submodules
+
+on:
+  workflow_dispatch: # allow to manually trigger this workflow
+  schedule:
+    - cron: '0 6 1 * *' # run on the first day of each month at 06:00 UTC
+
+jobs:
+  # Update the submodules and create a PR if there are any changes
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      - name: Get current commits
+        run: |
+          echo "PREV_VIPERSERVER_REF=$(git -C viperserver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Update ViperServer submodule
+        run: git checkout master && git pull
+        working-directory: viperserver
+
+      - name: Get new commits
+        run: |
+          echo "CUR_VIPERSERVER_REF=$(git -C viperserver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Open a pull request
+        id: pr
+        uses: peter-evans/create-pull-request@v6
+        if: env.PREV_VIPERSERVER_REF != env.CUR_VIPERSERVER_REF
+        with:
+          # Use viper-admin's token to workaround a restriction of GitHub.
+          # See: https://github.com/peter-evans/create-pull-request/issues/48
+          token: ${{ secrets.VIPER_ADMIN_TOKEN }}
+          commit-message: Updates submodules
+          title: Update Submodules
+          branch: auto-update-submodules
+          delete-branch: true
+          labels: |
+            automated pr
+          body: |
+            * Updates ViperServer from `${{ env.PREV_VIPERSERVER_REF }}` to `${{ env.CUR_VIPERSERVER_REF }}`.
+
+      # - name: Enable auto-merge of PR
+      #   uses: peter-evans/create-or-update-comment@v2
+      #   if: env.PREV_VIPERSERVER_REF != env.CUR_VIPERSERVER_REF
+      #   with:
+      #     token: ${{ secrets.VIPER_ADMIN_TOKEN }}
+      #     issue-number: ${{ steps.pr.outputs.pull-request-number }}
+      #     body: bors merge

.gitignore

@@ -7,6 +7,7 @@ tmp/
 sync/
 
 logger.log
+.DS_Store
 
 *.go.*
 *.gobra.*

README.md

@@ -45,6 +45,33 @@ More information about the available options in Gobra can be found by running `r
 ### Running the Tests
 In the `gobra` directory, run the command `sbt test`.
 
+### Debugging
+By default, Gobra runs in sbt on a forked JVM. This means that simply attaching a debugger to sbt will not work. There
+are two workarounds:
+
+- Run Gobra in a non-forked JVM by first running `set fork := false` in sbt. This will allow you to attach a debugger to
+  sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually
+  only the parsing can really be debugged.
+- Attach the debugger to the forked JVM.
+  - Create a debug configuration in IntelliJ and specify to `Attach to remote JVM`, set `localhost` as host, and 
+     a port (e.g. 5005).
+  - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"`
+     in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be
+    debugged instead of the sbt JVM. This requires starting the debugger again every time a new VM is created,
+    e.g. for every `run`.
+- Let the debugger listen to the forked JVM.
+  - Create a debug configuration in IntelliJ and specify to `Listen to remote JVM`, enable auto restart, set
+    `localhost` as host, and a port (e.g. 5005).
+  - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=n,address=localhost:5005,suspend=y"` in sbt.
+    Thanks to auto restart, the debugger keeps listening even when the JVM is restarted, e.g. for every `run`.
+    Note however that the debugger must be running/listening as otherwise the JVM will emit a connection 
+    refused error.
+
+## Projects verified with Gobra
+- [VerifiedSCION](https://github.com/viperproject/VerifiedSCION)
+- [Security of protocol implementations via refinement w.r.t. a Tamarin model](https://github.com/viperproject/protocol-verification-refinement). In particular, implementations of the signed Diffie-Hellman and WireGuard protocols have been verified.
+- [Security of protocol implementations verified entirely within Gobra](https://github.com/viperproject/SecurityProtocolImplementations). In particular, implementations of the Needham-Schroeder-Lowe, signed Diffie-Hellman, and WireGuard protocols have been verified.
+
 ## Licensing
 Most Gobra sources are licensed under the Mozilla Public License Version 2.0.
 The [LICENSE](./LICENSE) lists the exceptions to this rule.

build.sbt

@@ -34,7 +34,8 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
-    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.9.2",
+    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0",
+    libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT
 
     scalacOptions ++= Seq(
       "-encoding", "UTF-8", // Enforce UTF-8, instead of relying on properly set locales

docs/tutorial.md

@@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) {
 
 Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. 
 
-In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). 
+In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). 
 
 
 ## Interfaces
@@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY]
 To check the full list of flags available in Gobra, run the command
 ```bash
 java -jar gobra.jar -h
-```
+```

project/build.properties

@@ -1,4 +1,4 @@
 # Any copyright is dedicated to the Public Domain.
 # http://creativecommons.org/publicdomain/zero/1.0/
 
-sbt.version = 1.5.7
+sbt.version = 1.7.2