add attestation to workflow

.github/workflows/ci-hamr.yml

@@ -2,6 +2,11 @@ name: HAMR-codegen
 
 on: 
   workflow_dispatch:
+    inputs:
+      use_sireum_release:
+        type: boolean
+        description: Use latest Sireum release rather than building from source
+        default: false
   push:
     paths:
       - 'micro-examples/microkit/**'
@@ -12,62 +17,78 @@ jobs:
   container:
     runs-on: ubuntu-latest
     container:
-      image: jasonbelt/microkit_domain_scheduling
+      image: jasonbelt/microkit_domain_scheduling:latest
     name: HAMR-codegen
     steps:
       - name: Checkout
         uses: actions/checkout@v4
         with:
-          path: inspecta
+          path: INSPECTA-models
           submodules: recursive
       - name: Checkout
         uses: actions/checkout@v4
         with:
-          path: kekinian
+          path: Sireum
           repository: sireum/kekinian
           submodules: recursive
       - name: Cache Java
         id: cache-java
         uses: actions/cache@v4
         with:
-          path: kekinian/bin/linux/java
-          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-java
+          path: Sireum/bin/linux/java
+          key: ${{ runner.os }}-${{ hashFiles('Sireum/versions.properties') }}-java
       - name: Cache Scala
         id: cache-scala
         uses: actions/cache@v4
         with:
-          path: kekinian/bin/scala
-          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-scala
+          path: Sireum/bin/scala
+          key: ${{ runner.os }}-${{ hashFiles('Sireum/versions.properties') }}-scala
       - name: Cache Coursier
         id: cache-coursier
         uses: actions/cache@v4
         with:
-          path: kekinian/cache/coursier
-          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-coursier
+          path: Sireum/cache/coursier
+          key: ${{ runner.os }}-${{ hashFiles('Sireum/versions.properties') }}-coursier
       - name: Cache OSATE
         id: cache-osate
         uses: actions/cache@v4
         with:
-          path: kekinian/bin/linux/osate
-          key: ${{ runner.os }}-${{ hashFiles('kekinian/hamr/codegen/jvm/src/main/resources/phantom_versions.properties') }}-osate
+          path: Sireum/bin/linux/osate
+          key: ${{ runner.os }}-${{ hashFiles('Sireum/hamr/codegen/jvm/src/main/resources/phantom_versions.properties') }}-osate
       - name: Build
+        shell: bash
         run: |
+          export HOME=/home/microkit
+          source $HOME/.bashrc
+
           # get the location of the microkit sdk inside the container.  The ci scripts 
           # require MICROKIT_SDK be set in order to build the seL4 images
           export MICROKIT_SDK=$(find /home/microkit/microkit/release/ -type d -name microkit-sdk*)
           export MICROKIT_BOARD=qemu_virt_aarch64
 
-          export HOME=$(pwd)
+          export DEMO_ROOT=$HOME/ku
+
+          mv $(pwd)/INSPECTA-models $DEMO_ROOT/
 
-          export SIREUM_HOME=$HOME/kekinian
+          export SIREUM_HOME=$(pwd)/Sireum
           export PATH=$SIREUM_HOME/bin:$PATH
 
-          $SIREUM_HOME/bin/build.cmd setup
-          rm -rf $SIREUM_HOME/out
+          echo "${{ github.event.inputs.use_sireum_release }}"
+          
+          if [ "${{ github.event.inputs.use_sireum_release }}" = "true" ]; then
+            #(DIR=Sireum && export SIREUM_V=master && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
+            (DIR=Sireum && export SIREUM_V=master && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
+          else
+            $SIREUM_HOME/bin/build.cmd setup
+            rm -rf $SIREUM_HOME/out
+          fi
           
           sireum
 
           sireum slang run $SIREUM_HOME/hamr/codegen/bin/build.cmd install-osate-gumbo
           export OSATE_HOME=$SIREUM_HOME/bin/linux/osate
 
-          $HOME/inspecta/.github/workflows/hamr-ci.cmd
+          export ASP_BIN=/home/microkit/ku/asp-libs/bin
+
+          #env
+          $DEMO_ROOT/INSPECTA-models/.github/workflows/hamr-ci.cmd

.github/workflows/hamr-ci.cmd

@@ -33,6 +33,7 @@ def findCIs(p: Os.Path): Unit = {
     if(p.isFile && p.name == "ci.cmd") {
       val r = proc"$sireum slang run $p".console.echo.run()
       result = result + r.exitCode
+      result = result + Tasks.attestation(p.up.up)
     } else if(p.isDir) {
       p.list.foreach((m: Os.Path) => findCIs(m))
     }
@@ -41,3 +42,57 @@ def findCIs(p: Os.Path): Unit = {
 findCIs(rootDir)
 
 Os.exit(result)
+
+
+
+object Tasks {
+  def run(title: String, verbose: B, proc: OsProto.Proc): Z = {
+    println(s"$title ...")
+    val r = (if (verbose) proc.console.echo else proc).run()
+
+    if (r.exitCode != 1) { // TODO Test.sh script grep needs to be updated
+      println(s"$title failed!")
+      cprintln(F, r.out)
+      cprintln(T, r.err)
+    }
+    return if (r.exitCode == 1) 0 else 1
+  }
+
+  def attestation(p: Os.Path): Z = {
+
+    val attestationDir = p / "attestation"
+    if (Os.env("MICROKIT_SDK").nonEmpty && Os.env("DEMO_ROOT").nonEmpty && attestationDir.exists) {
+      println()
+      val testsDir = Os.path(Os.env("DEMO_ROOT").get) / "am-cakeml" / "tests"
+
+      val micro_composite = testsDir / "DemoFiles" / "goldenFiles"/ "micro_composite.txt"
+      val cached_micro_composite = p / "attestation" / "micro_composite.txt"
+
+      var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h",
+        "-m", (attestationDir / "model_args.json").value, "-s", (attestationDir / "system_args.json").value)
+
+      if (ops.ISZOps(Os.cliArgs).contains("provision")) {
+        aargs = aargs :+ "-p"
+        var result = run(s"Provisioning $p", F, Os.proc(aargs))
+        if (result == 0) {
+          micro_composite.copyOverTo(cached_micro_composite)
+        }
+        return result
+      } else {
+        var result = 1
+        for(retry <- 0 until 5 if result != 0) {
+          cached_micro_composite.copyOverTo(micro_composite)
+          result = run(s"Appraising $p${if (retry > 0) s": Retry $retry" else ""}", F, Os.proc(aargs))
+          assert (result == 0, result)
+
+          val resp = testsDir / "DemoFiles" / "Generated" / "output_resp.json"        
+          println(resp.read)
+          result = if (resp.read == "Resolute Policy check:  SUCCESS") 0 else 1
+        }
+        println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!")
+        return result
+      }
+    }
+    return 0
+  }
+}

isolette/attestation/micro_composite.txt

@@ -0,0 +1 @@
+����h���XPq���QI�j���fi�bv��

isolette/attestation/model.golden

@@ -0,0 +1 @@
+;�
��&�j��ST�����>M3]A|�h:��u

isolette/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/isolette/sysml/Isolette.sysml",
+ "filepath-golden":"/INSPECTA-models/isolette/attestation/model.golden"}

isolette/attestation/system.golden

@@ -0,0 +1 @@
+-o8�R�s9��b�ΈO����7;ٗ�^"��

isolette/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/isolette/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/isolette/attestation/system.golden"}

micro-examples/domain-scheduling-models/three_domain_simple/attestation/micro_composite.txt

@@ -0,0 +1 @@
+x�Vʠ]��pvR�X�]CB��,�R�+�
Gi�

micro-examples/domain-scheduling-models/three_domain_simple/attestation/model.golden

@@ -0,0 +1 @@
+$c�aux��(C�J=����$�t��R��

micro-examples/domain-scheduling-models/three_domain_simple/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/aadl/test_data_port_periodic_three_domains.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model.golden"}

micro-examples/domain-scheduling-models/three_domain_simple/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system.golden"}

micro-examples/microkit/Dockerfile

@@ -32,7 +32,14 @@ WORKDIR ${HOME}
 
 SHELL ["/bin/bash", "-c"]
 
-RUN wget -O rustup-init.sh https://sh.rustup.rs && sh ${HOME}/rustup-init.sh -y && rm ${HOME}/rustup-init.sh && . ${HOME}/.cargo/env && \
+# don't use cache on next step if any of the repos have a new commit
+ADD "https://api.github.com/repos/sel4/sel4/pulls/1308/commits?per_page=1" latest_sel4_commit
+ADD "https://api.github.com/repos/sel4/microkit/pulls/175/commits?per_page=1" latest_microkit_commit
+ADD "https://api.github.com/repos/ku-sldg/am-cakeml/commits/resolute?per_page=1" latest_am-cakeml_commit
+ADD "https://api.github.com/repos/ku-sldg/asp-libs/commits/resolute?per_page=1" latest_asp-libs_commit
+
+RUN rm -rf latest_am-cakeml_commit latest_asp-libs_commit latest_sel4_commit latest_microkit_commit && \
+    wget -O rustup-init.sh https://sh.rustup.rs && sh ${HOME}/rustup-init.sh -y && rm ${HOME}/rustup-init.sh && . ${HOME}/.cargo/env && \
     rustup target add x86_64-unknown-linux-musl && rustup target add aarch64-unknown-linux-musl && \
     echo "************************************************" && \
     echo "* Building Microkit SDK with domain scheduling *" && \

micro-examples/microkit/aadl_port_types/data/array/attestation/micro_composite.txt

@@ -0,0 +1 @@
+oq~�?!�#([��/h���̅�>~�����v�

micro-examples/microkit/aadl_port_types/data/array/attestation/model.golden

@@ -0,0 +1 @@
+u� ��û!���_�W��8n�۸��4a���4

micro-examples/microkit/aadl_port_types/data/array/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/aadl/data_1_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/data/array/attestation/system.golden

@@ -0,0 +1 @@
+�"i!빋��EY*S\�����֕w���.V�

micro-examples/microkit/aadl_port_types/data/array/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit.golden

@@ -0,0 +1 @@
+�"i!빋��EY*S\�����֕w���.V�

micro-examples/microkit/aadl_port_types/data/base_type/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/aadl/data_1_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/data/base_type/attestation/system.golden

@@ -0,0 +1 @@
+�C/��؉a�8t�����L��D}�!Zn5�

micro-examples/microkit/aadl_port_types/data/base_type/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit.golden"}

micro-examples/microkit/aadl_port_types/data/struct/attestation/model.golden

@@ -0,0 +1 @@
+�vü2���ˊp��\5+��+�-��i%`�d

micro-examples/microkit/aadl_port_types/data/struct/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/aadl/data_1_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/data/struct/attestation/system.golden

@@ -0,0 +1 @@
+�"i!빋��EY*S\�����֕w���.V�

micro-examples/microkit/aadl_port_types/data/struct/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/event/attestation/micro_composite.txt

@@ -0,0 +1 @@
+��)�(�Ȏ��}sc�T��0�Ga	d��V�

micro-examples/microkit/aadl_port_types/event/attestation/model.golden

@@ -0,0 +1 @@
+@B-5��t�'�J�ŭ���@���T��L�

micro-examples/microkit/aadl_port_types/event/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/aadl/event_2_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/event/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/event_data/array/attestation/micro_composite.txt

@@ -0,0 +1 @@
+;��31�͊�;����]קc�J�zq/`���x

micro-examples/microkit/aadl_port_types/event_data/array/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/aadl/event_data_2_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/event_data/array/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/micro_composite.txt

@@ -0,0 +1 @@
+���Z�a�����CP~<i����Yu�AHl

micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model.golden

@@ -0,0 +1 @@
+L��p��~@W	���������ߌv�\Ƚ�W

micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/aadl/event_data_2_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system.golden"}

micro-examples/microkit/aadl_port_types/event_data/struct/attestation/micro_composite.txt

@@ -0,0 +1 @@
+�.8��V��Q�:�~+�
ſ	�Oδ���3

micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model.golden

@@ -0,0 +1 @@
+��sf����'�M���6j�g�3d/l��([

micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/aadl/event_data_2_prod_2_cons.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model.golden"}

micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system.golden"}

micro-examples/microkit/port_queues/event_data_array/attestation/micro_composite.txt

@@ -0,0 +1 @@
+�O�[=N�1�ۦ�A�7��$VTF�/�8��

micro-examples/microkit/port_queues/event_data_array/attestation/model.golden

@@ -0,0 +1,2 @@
+jǽ}
+�H耫.�mq��8����T��H�

micro-examples/microkit/port_queues/event_data_array/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/aadl/event_data_port_queues.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/model.golden"}

micro-examples/microkit/port_queues/event_data_array/attestation/system.golden

@@ -0,0 +1 @@
+5(+�~��HLn�D$�s=�n�Pp֔):�BvRuW~

micro-examples/microkit/port_queues/event_data_array/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/system.golden"}

micro-examples/microkit/port_queues/event_data_base_types/attestation/micro_composite.txt

@@ -0,0 +1,2 @@
+-ׂ/�G!Mvo‰��6�e]�)m�\
+#��C�P

micro-examples/microkit/port_queues/event_data_base_types/attestation/model.golden

@@ -0,0 +1 @@
+]Rh]$�~l���@V��-!�0�D�a%��

micro-examples/microkit/port_queues/event_data_base_types/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/aadl/event_data_port_queues.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/model.golden"}

micro-examples/microkit/port_queues/event_data_base_types/attestation/system.golden

@@ -0,0 +1 @@
+5(+�~��HLn�D$�s=�n�Pp֔):�BvRuW~

micro-examples/microkit/port_queues/event_data_base_types/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/system.golden"}

micro-examples/microkit/port_queues/event_data_struct/attestation/micro_composite.txt

@@ -0,0 +1 @@
+�Z俧�k�P=jհ7�(�[%�j��9���<

micro-examples/microkit/port_queues/event_data_struct/attestation/model.golden

@@ -0,0 +1,2 @@
+Ż\�т«��*7��C!�zMր���
+�

micro-examples/microkit/port_queues/event_data_struct/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/aadl/event_data_port_queues.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/model.golden"}

micro-examples/microkit/port_queues/event_data_struct/attestation/system.golden

@@ -0,0 +1 @@
+5(+�~��HLn�D$�s=�n�Pp֔):�BvRuW~

micro-examples/microkit/port_queues/event_data_struct/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/system.golden"}

micro-examples/microkit/vms/data/receiver/attestation/model.golden

@@ -0,0 +1 @@
+y�m�^lT��1w,r�-d��wI����nVS�H

micro-examples/microkit/vms/data/receiver/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/aadl/vmR_data.aadl",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/model.golden"}

micro-examples/microkit/vms/data/receiver/attestation/system.golden

@@ -0,0 +1,2 @@
+L`l�%k�B]����k�͟
+f�T�ͧ
�X,yJ7B

micro-examples/microkit/vms/data/receiver/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/hamr/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/system.golden"}

open-platform-models/isolate-ethernet-simple/attestation/micro_composite.txt

@@ -0,0 +1 @@
+E��-�A��Mj�/���}<�oFf���&�f��-

open-platform-models/isolate-ethernet-simple/attestation/model.golden

@@ -0,0 +1 @@
+��@3�bߕ��!P�p�YGY��yJ�����

open-platform-models/isolate-ethernet-simple/attestation/model_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/aadl/platform.aadl",
+ "filepath-golden":"/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/model.golden"}

open-platform-models/isolate-ethernet-simple/attestation/system.golden

@@ -0,0 +1 @@
+4�d=��h�vi�䳒A*K���+8fYB�����

open-platform-models/isolate-ethernet-simple/attestation/system_args.json

@@ -0,0 +1,2 @@
+{"filepath":       "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/microkit/microkit.system",
+ "filepath-golden":"/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/system.golden"}