Add packet example and integration test

.github/workflows/main.yml

@@ -48,11 +48,9 @@ jobs:
             --cache-from artifactory.galois.com:5025/pate/pate:refs-heads-master \
             -t pate
 
-      - name: Test Docker Image
+      - name: Docker Integration Test
         run: |
-          docker run --rm --entrypoint cabal pate run pate-test-aarch32 -- -p args-equal > out.log
-          cat out.log
-          grep -e "All .* tests passed" out.log || exit 1
+          docker run --rm --entrypoint tests/integration/packet/packet.exp pate
 
       - name: Push Docker image
         run: |

Dockerfile

@@ -147,7 +147,7 @@ RUN cabal v2-build pate-repl-base
 ENV PATH="/home/src/:/root/.ghcup/bin:${PATH}"
 
 COPY --from=gitbase /home/src/loadrepl.ghci /home/src/loadrepl.ghci
-RUN apt install -y libtinfo5 libtinfo-dev
+RUN apt install -y libtinfo5 libtinfo-dev expect-lite
 ENTRYPOINT ["/home/src/pate.sh"]
 
 

tests/integration/packet/packet.c

@@ -0,0 +1,84 @@
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int check_crc(uint16_t crc, void *data) { return (crc == 0); }
+
+int parse_data(void* buffer, uint8_t size, FILE *stream) {
+  fread(buffer, size, 1, stream);
+  return EXIT_SUCCESS;
+}
+
+#define DATA_MAX 64
+
+#define UNEXPECTED_TARGET 1
+#define UNEXPECTED_SOURCE 2
+#define BAD_SYNC 3
+#define BAD_LENGTH 4
+#define BAD_CRC 5
+
+#define PROTO_SYNC 0x0564
+#define LINK_ACK 0x80
+
+typedef struct {
+  // link layer
+  uint16_t sync;
+  uint8_t length;
+  uint8_t linkControl;
+  uint16_t targetAddress;
+  uint16_t sourceAddress;
+  uint16_t headerCRC;
+  // transport layer
+  uint8_t transportControl;
+  // application layer
+  char applicationData[DATA_MAX];
+} Packet;
+
+Packet IncomingPacket;
+
+int parse_packet(uint16_t host, uint16_t remote, FILE *stream) {
+  // link layer
+  fread(&IncomingPacket.sync, 2, 1, stream);
+  if (IncomingPacket.sync != PROTO_SYNC) {
+    return BAD_SYNC;
+  }
+  fread(&IncomingPacket.length, 1, 1, stream);
+  if (IncomingPacket.length == 0) {
+    return BAD_LENGTH;
+  }
+  fread(&IncomingPacket.linkControl, 1, 1, stream);
+  fread(&IncomingPacket.targetAddress, 2, 1, stream);
+  if (IncomingPacket.targetAddress != host) {
+    return UNEXPECTED_TARGET;
+  }
+  fread(&IncomingPacket.sourceAddress, 2, 1, stream);
+  if (IncomingPacket.sourceAddress != remote) {
+    return UNEXPECTED_SOURCE;
+  }
+  fread(&IncomingPacket.headerCRC, 2, 1, stream);
+  if (check_crc(IncomingPacket.headerCRC, &IncomingPacket)) {
+    return BAD_CRC;
+  }
+
+  // transport layer
+  fread(&IncomingPacket.transportControl, 1, 1, stream);
+
+  // application_layer
+#ifdef PATCHED
+  int size = IncomingPacket.length;
+  if (IncomingPacket.linkControl == LINK_ACK) {
+    size = 0;
+  }
+  printf("[INFO] Reading %d bytes\n", size);
+  return parse_data(&IncomingPacket.applicationData, size, stream);
+#else
+  printf("[INFO] Reading %d bytes\n", IncomingPacket.length);
+  return parse_data(&IncomingPacket.applicationData, IncomingPacket.length, stream);
+#endif
+
+}
+
+int main(int argc, char **argv) {
+  printf("[INFO] Max packet size: %d\n", sizeof(Packet));
+  parse_packet(0, 1, NULL);
+}

tests/integration/packet/packet.exp

@@ -0,0 +1,72 @@
+#!/usr/bin/env -S expect -f
+#
+# This is an expect script modeling the user interaction of PATE on the packet example.
+#
+# Beyond testing basic verifier functionality, this test is also intended to
+# provide an integration test of the 1) terminal user interaction, and 2)
+# resulting equivalence condition, in ways that the other automated tests do not.
+# The test for the "expected" equivalence condition is syntactic, so this test will
+# likely be more brittle (e.g. break if the term simplification changes such that
+# intermediate variable numbers change) and may need to be updated to reflect
+# intended subsequent changes to PATE verification details.
+#
+# This test is intended to be run from the root of the pate directory:
+#    ./tests/integration/packet/packet.exp
+#
+# Note that expected strings must be escaped: double-quotes (\") and brackets (\\\[)
+
+spawn ./pate.sh --original tests/integration/packet/exe/packet.exe --patched tests/integration/packet/exe/packet.patched.exe -s parse_packet
+
+set timeout 480
+
+expect_before {
+        timeout { send_user "\n\nFAILURE: timeout\n"; exit 1 }
+        eof     { send_user "\n\nFAILURE: eof\n";     exit 2 }
+}
+
+expect "Choose Entry Point"
+expect "1: Function Entry \"parse_packet\" (segment1+0x554)"
+expect "?>"
+send "1\r"
+
+expect "Handle observable difference:"
+expect "4: Avoid difference with equivalence condition"
+expect "?>"
+send "4\r"
+
+expect "Continue verification?"
+expect "0: Finish and view final result"
+expect "?>"
+send "0\r"
+
+expect "15: Final Result"
+expect ">"
+send "15\r"
+
+expect "0: Assumed Equivalence Conditions"
+expect "2: Binaries are conditionally, observably equivalent"
+expect ">"
+send "0\r"
+
+# Inspect the specific equivalence condition
+
+expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]"
+expect ">"
+send "0\r"
+
+expect "3: let -- segment1+0x664.. in not v40591"
+expect ">"
+send "3\r"
+
+expect "v40591 = and (eq 0x80:\\\[8\\\] v40584) (not (eq v40587 (bvSum v40584 0x80:\\\[8\\\])))"
+expect "in not v40591"
+expect ">"
+send "\x04" ; # Ctrl-D (EOF)
+
+# remove EOF from expect_before, now that we're expecting it
+expect_before {
+        timeout { send_user "\n\nFAILURE: timeout\n"; exit 1 }
+}
+expect eof
+
+send_user "\nSUCCESS: packet integration test complete\n"

tests/integration/packet/packet.run-config.json

@@ -0,0 +1,7 @@
+{
+  "original": "exe/packet.exe",
+  "patched": "exe/packet.patched.exe",
+  "args": [
+    "-s parse_packet"
+  ]
+}