merged

viperproject · Apr 11, 2024 · 158bbe8 · 158bbe8
2 parents 0d86667 + b1bf999
commit 158bbe8
Show file tree

Hide file tree

Showing 100 changed files with 5,927 additions and 4,211 deletions.
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -0,0 +1,12 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: "/"
+    schedule:
+      interval: monthly
+      day: monday
+    groups:
+      all:
+        patterns:
+          - "*"
diff --git a/.github/workflows/license-check.yml b/.github/workflows/license-check.yml
@@ -16,7 +16,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Gobra
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Check license headers
         uses: viperproject/check-license-header@v2
         with:

diff --git a/.github/workflows/test.yml b/.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@v3
+        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@v2
+        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@v3
+        uses: docker/build-push-action@v5
         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@v3
+        uses: actions/upload-artifact@v4
         with:
           name: pidstat.txt
           path: sync/pidstat.txt
 
       - name: Build entire image
-        uses: docker/build-push-action@v3
+        uses: docker/build-push-action@v5
         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@v2
+        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@v3
+        uses: docker/build-push-action@v5
         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 }}
diff --git a/.github/workflows/update-submodules.yml b/.github/workflows/update-submodules.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: true
 
@@ -35,7 +35,7 @@ jobs:
 
       - name: Open a pull request
         id: pr
-        uses: peter-evans/create-pull-request@v4
+        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.

diff --git a/README.md b/README.md
@@ -67,6 +67,11 @@ are two workarounds:
     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.

diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -91,3 +91,6 @@ PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
+OPAQUE      : 'opaque' -> mode(NLSEMI);
+REVEAL      : 'reveal';
+BACKEND     : '#backend';
diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -25,7 +25,6 @@ stmtOnly: statement EOF;
 
 typeOnly: type_ EOF;
 
-
 // Identifier lists with added addressability modifiers
 maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressableIdentifier)*;
 
@@ -167,10 +166,17 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 
 // Specifications
 
-specification returns[boolean trusted = false, boolean pure = false;]:
-  ((specStatement | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+specification returns[boolean trusted = false, boolean pure = false, boolean opaque = false;]:
+  // Non-greedily match PURE to avoid missing eos errors.
+  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
   ;
 
+backendAnnotationEntry: ~('('|')'|',')+;
+listOfValues: backendAnnotationEntry (COMMA backendAnnotationEntry)*;
+singleBackendAnnotation: backendAnnotationEntry L_PAREN listOfValues? R_PAREN;
+backendAnnotationList: singleBackendAnnotation (COMMA singleBackendAnnotation)*;
+backendAnnotation: BACKEND L_BRACKET backendAnnotationList? R_BRACKET eos;
+
 specStatement
   : kind=PRE assertion
   | kind=PRESERVES assertion
@@ -232,11 +238,11 @@ new_: NEW L_PAREN type_ R_PAREN;
 
 // Added specifications and parameter info
 
-specMember: specification (functionDecl[$specification.trusted, $specification.pure] | methodDecl[$specification.trusted, $specification.pure]);
+specMember: specification (functionDecl[$specification.trusted, $specification.pure, $specification.opaque] | methodDecl[$specification.trusted, $specification.pure, $specification.opaque]);
 
-functionDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
+functionDecl[boolean trusted, boolean pure, boolean opaque]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
 
-methodDecl[boolean trusted, boolean pure]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
+methodDecl[boolean trusted, boolean pure, boolean opaque]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
 
 
 
@@ -382,7 +388,9 @@ primaryExpr:
   | primaryExpr slice_ #slicePrimaryExpr
   | primaryExpr seqUpdExp #seqUpdPrimaryExpr
   | primaryExpr typeAssertion #typeAssertionPrimaryExpr
+  // "REVEAL? primaryExpr arguments" doesn't work due to mutual left recursion
   | primaryExpr arguments #invokePrimaryExpr
+  | REVEAL primaryExpr arguments #revealInvokePrimaryExpr
   | primaryExpr arguments AS closureSpecInstance #invokePrimaryExprWithSpec
   | primaryExpr predConstructArgs #predConstrPrimaryExpr
   | call_op=(