Skip to content

Commit d6c162d

Browse files
ArquintLArquintL
committed
Merges branch 'main' into 'dependabot/github_actions/all-bf940bc907'
2 parents 3614e3e + 0e3bbda commit d6c162d

File tree

114 files changed

+5510
-43
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

114 files changed

+5510
-43
lines changed

‎.github/workflows/artifact.yml‎

Lines changed: 55 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
name: Artifact
22

3-
# creates the artifact docker image and
4-
# - verifies the Tamarin model
5-
# - TODO
6-
7-
83
on:
94
push:
105

@@ -79,28 +74,68 @@ jobs:
7974
run: echo "IMAGE_TAG=${{ env.IMAGE_TAG }}" >> $GITHUB_OUTPUT
8075

8176

82-
Test:
77+
Test-DH:
8378
name: ${{ matrix.name }}
8479
runs-on: ubuntu-latest
8580
needs: Build
8681
strategy:
8782
# tests should not be stopped when they fail on one of the OSes:
8883
fail-fast: false
8984
matrix:
90-
name: ["Verify protocol model", "Verify core"]
85+
# name: ["Verify DH protocol model", "Verify DH core", "Verify DH I/O independence", "Verify DH core assumptions"]
86+
name: ["Verify DH protocol model", "Verify DH core"]
9187
include:
92-
- name: "Verify protocol model"
93-
command: "/gobra/verify-model.sh"
94-
timeout-minutes: 15
95-
- name: "Verify core"
96-
command: "/gobra/verify-core.sh"
88+
- name: "Verify DH protocol model"
89+
command: "/gobra/dh/verify-model.sh"
90+
timeout-minutes: 3
91+
- name: "Verify DH core"
92+
command: "/gobra/dh/verify-core.sh"
93+
timeout-minutes: 5
94+
# - name: "Verify DH I/O independence"
95+
# command: "/gobra/dh/verify-io-independence.sh"
96+
# timeout-minutes: 3
97+
# - name: "Verify DH core assumptions"
98+
# command: "/gobra/dh/verify-core-assumptions.sh"
99+
# timeout-minutes: 3
100+
timeout-minutes: ${{ matrix.timeout-minutes }}
101+
steps:
102+
- name: Download artifact
103+
uses: actions/download-artifact@v4
104+
with:
105+
name: ${{ env.IMAGE_WORKFLOW_ARTIFACT_NAME }}
106+
path: /tmp
107+
108+
- name: Load image
109+
run: docker load --input /tmp/image.tar
110+
111+
- name: ${{ matrix.name }}
112+
run: docker run --entrypoint "/bin/bash" ${{ needs.Build.outputs.IMAGE_TAG }} -c "cp -r dh-orig/. dh/; cp -r ssm-agent-orig/. ssm-agent/; ${{ matrix.command }}"
113+
114+
115+
Test-SSM-Agent:
116+
name: ${{ matrix.name }}
117+
runs-on: ubuntu-latest
118+
needs: Build
119+
strategy:
120+
# tests should not be stopped when they fail on one of the OSes:
121+
fail-fast: false
122+
matrix:
123+
# name: ["Verify SSM Agent protocol model", "Verify SSM Agent core", "Verify SSM Agent I/O independence", "Verify SSM Agent core assumptions"]
124+
name: ["Verify SSM Agent protocol model"]
125+
include:
126+
- name: "Verify SSM Agent protocol model"
127+
command: "/gobra/ssm-agent/verify-model.sh"
97128
timeout-minutes: 15
98-
- name: "Verify I/O independence"
99-
command: "/gobra/verify-io-independence.sh"
100-
timeout-minutes: 10
101-
- name: "Verify core assumptions"
102-
command: "/gobra/verify-core-assumptions.sh"
103-
timeout-minutes: 10
129+
# TODO renable once these tasks are fixed
130+
# - name: "Verify SSM Agent core"
131+
# command: "/gobra/ssm-agent/verify-core.sh"
132+
# timeout-minutes: 15
133+
# - name: "Verify SSM Agent I/O independence"
134+
# command: "/gobra/ssm-agent/verify-io-independence.sh"
135+
# timeout-minutes: 10
136+
# - name: "Verify SSM Agent core assumptions"
137+
# command: "/gobra/ssm-agent/verify-core-assumptions.sh"
138+
# timeout-minutes: 10
104139
timeout-minutes: ${{ matrix.timeout-minutes }}
105140
steps:
106141
- name: Download artifact
@@ -113,12 +148,12 @@ jobs:
113148
run: docker load --input /tmp/image.tar
114149

115150
- name: ${{ matrix.name }}
116-
run: docker run --entrypoint "/bin/bash" ${{ needs.Build.outputs.IMAGE_TAG }} -c "cp -r model-orig/. model/; cp -r implementation-orig/. implementation/; ${{ matrix.command }}"
151+
run: docker run --entrypoint "/bin/bash" ${{ needs.Build.outputs.IMAGE_TAG }} -c "cp -r dh-orig/. dh/; cp -r ssm-agent-orig/. ssm-agent/; ${{ matrix.command }}"
117152

118153

119154
Publish:
120155
runs-on: ubuntu-latest
121-
needs: [Build, Test]
156+
needs: [Build, Test-DH, Test-SSM-Agent]
122157
timeout-minutes: 5
123158
# set per-job GITHUB_TOKEN permissions such that pushing the Docker image will be possible:
124159
permissions:

‎.gitignore‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,6 @@
22
.idea
33
*.log
44
tmp/
5-
5+
dh-sync/
6+
ssm-agent-sync/
67
argot-proofs/reports/

‎.gitmodules‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
[submodule "implementation"]
2-
path = implementation
2+
path = ssm-agent/implementation
33
url = https://github.com/ArquintL/amazon-ssm-agent
44
branch = diodon
55
[submodule "ar-go-tools"]

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,13 @@ We require an installation of Docker. The following steps have been tested on ma
2424
- We recommend to adapt the Docker settings to provide sufficient resources to Docker. We have tested our artifact on a 2019 16-inch MacBook Pro with 2.3 GHz 8-Core Intel Core i9 running macOS Sonoma 14.0 and configured Docker to allocate up 16 cores (which includes 8 virtual cores), 6 GB of memory, and 1 GB of swap memory. In case you are using an ARM-based Mac, enable the option "Use Rosetta for x86/amd64 emulation on Apple Silicon" in the Docker Desktop Settings, which is available on macOS 13 or newer. Measurements on an Apple M1 Pro Silicon have shown that performing this additional emulation results in 20-25\% longer verification times compared to those reported in the remainder of this artifact appendix.
2525
- Navigate to a convenient folder, in which directories can be created for the purpose of running this artifact.
2626
- Open a shell at this folder location.
27-
- Create two new folders named `model-sync` and `implementation-sync` by executing:
27+
- Create two new folders named `dh-sync` and `ssm-agent-sync` by executing:
2828
```
29-
mkdir model-sync && mkdir implementation-sync
29+
mkdir dh-sync && mkdir ssm-agent-sync
3030
```
3131
- Download and start the Docker image containing our artifact by executing the following command:
3232
```
33-
docker run -it --platform linux/amd64 --volume $PWD/model-sync:/gobra/model --volume $PWD/implementation-sync:/gobra/implementation ghcr.io/arquintl/diodon-artifact:latest
33+
docker run -it --platform linux/amd64 --volume $PWD/dh-sync:/gobra/dh --volume $PWD/ssm-agent-sync:/gobra/ssm-agent ghcr.io/arquintl/diodon-artifact:latest
3434
```
3535
> ⚠️
3636
> Note that this command results in the Docker container writing files to the two folders `model-sync` and `implementation-sync` on your host machine.

‎dh/implementation/.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
.gobra/
2+
local-verify.sh
3+
dh-gobra

‎dh/implementation/.gobra/.gitkeep‎

Whitespace-only changes.

‎dh/implementation/.verification/crypto/hmac/hmac.gobra‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
package hmac

‎dh/implementation/.verification/crypto/rand/rand.gobra‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
package rand

‎dh/implementation/.verification/encoding/hex/hex.gobra‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
package hex

‎dh/implementation/.verification/golang.org/x/crypto/blake2s/blake2s.gobra‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
package blake2s

0 commit comments

Comments
 (0)