init - first working version

README.md

@@ -0,0 +1,15 @@
+# Korg, reborn
+
+# TODO:
+- [x] fix weird spin errors(?)
+- [ ] add attackers that only do specifically n queries
+    - limitation: you cannot choose only *n* queries for the dropping attacker
+- [ ] add attackers to do <= n queries
+- [x] add a test suite
+- [ ] modify the paper? spin workshop?
+- [x] nix flake here lol
+
+# Notes
+- Sound and complete attack discovery for replay, dropping, and reordering attacks on channels
+    - possible because of the finite-state modeling spin does
+- Limiting the number of messages a drop/replay/reorder attacker can reason about has the ability to significantly reduce the searchspace, especially when dealing with larger models. Although KORG is always decidable, sound, and complete, using the unbounded attacker is inadvisable in practice because spin must reason about *all* such permutations of possible drop, replay, and reorder sequences, thereby increasing the search space factorially.

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1761373498,
+        "narHash": "sha256-Q/uhWNvd7V7k1H1ZPMy/vkx3F8C13ZcdrKjO7Jv7v0c=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "6a08e6bb4e46ff7fcbb53d409b253f6bad8a28ce",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -4,26 +4,36 @@
   inputs = {
     nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
     flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs-spin.url = "github:NixOS/nixpkgs/893c51bda8b7502b43842f137258d0128097d7ea";
   };
 
-  outputs = { self, nixpkgs, flake-utils, nixpkgs-spin, ... } @ inputs:
+  outputs = { self, nixpkgs, flake-utils, ... }@inputs:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = nixpkgs.legacyPackages.${system};
-        pkgs-spin = nixpkgs-spin.legacyPackages.${system};
-      in {
+
+        pkgs-spin = import (builtins.fetchTarball {
+          url = "https://github.com/NixOS/nixpkgs/archive/893c51bda8b7502b43842f137258d0128097d7ea.tar.gz";
+          sha256 = "0wydvj05k9cjx557gvr1am7rzl482zv9ml0p3zamxm1gx7whzja6";
+        }) { inherit system; }; 
+
+        spinPkg = pkgs-spin.spin;
+
+      in
+      {
         packages.default = pkgs.stdenv.mkDerivation {
           pname = "korg";
-          src     = ./.;
+          src = self;
+          installPhase = ''
+            mkdir -p $out/bin
+            echo "placeholder" > $out/bin/korg
+          '';
         };
 
         devShells.default = pkgs.mkShellNoCC rec {
-          buildInputs = with pkgs; [
-            # spin
-            python3
-          ] ++ [
-            pkgs-spin.spin
+          buildInputs = [
+            pkgs.python3  
+            spinPkg      
+            pkgs.python313Packages.pyyaml
           ];
 
           shellHook = ''

src/main.py

@@ -0,0 +1,146 @@
+#  ==============================================================================
+# Author    : Jake Ginesin
+# Authored  : 14 June 2024
+# Purpose   : synthesize attacker gadgets for attackers that can drop, 
+#             replay, and reorder messages on a channel
+# ==============================================================================
+import sys, re, subprocess, os, shutil
+from typing import List
+
+from utility import *
+from model_generate import *
+
+def show_help() -> None:
+    msg=(
+    "Usage: \n"
+    "    python main.py [arguments] \n\n"
+    "Arguments: \n"
+    "    --model=path/to/model.pml                   Promela model to generate attackers on\n"
+    "    --attacker=[replay,drop,reorder] \n"
+    "    --chan=[chan1, chan2:int, ...]   Channels to synthesize attackers on. When specifying over ranges of\n"
+    "                                                channels, you can give ranges or a list of values\n"
+    "       --nocheck                                Don't check channel validity\n"
+    # "       --nchan=[nat, nat, ...]             If the channel is a set of channels, how many attackers to synthesize?\n"
+    "    --mem=[num]                                 Size of memory. Defaults to '3' \n"
+    "       --mem=unbounded                          Use the unbounded memory gadget version (not recommended)\n"
+    "    --output=path/to/file.pml                   Outputted file name\n"
+    "    --eval                                      Evaluate the outputted file with Spin\n"
+    "    --cleanup                                   Clean up the extra files spin creates, including Korg's \n"
+    )
+    print(msg)
+
+    # assert "syntax error" not in stdout, "there seems to be a syntax error in the model"
+    # assert "processes created" in stdout, "the spin model creates no processes ... check to see if it compiles"
+
+def main() -> None:
+    args = sys.argv[1:]  
+    if len(args) == 0 or args[0] in ["help", "--help", "-h", "-help"]:
+        show_help()
+        sys.exit()
+
+    mem = 3 # default
+
+    for arg in args:
+        if arg.startswith("--model="):
+            model_path = arg.split("=", 1)[1]
+        elif arg.startswith("--attacker="):
+            attacker = arg.split("=", 1)[1]
+        elif arg.startswith("--mem="):
+            mem_read = arg.split("=", 1)[1]
+        elif arg.startswith("--chan="):
+            chans = arg.split("=", 1)[1]
+        elif arg.startswith("--output="):
+            out_file = arg.split("=", 1)[1]
+
+    if "--eval" in args and not "--output" in args:
+        out_file = "korg-promela-out.pml"
+
+    if not model_path or not attacker or not mem or not chans or not out_file:
+        print("error: all arguments are required. \n")
+        show_help()
+        sys.exit(1)
+
+    unbounded = mem_read == "unbounded"
+    if not unbounded : mem = int(mem_read)
+
+    ensure_compile(model_path)
+    model = fileRead(model_path)
+
+    channels = parse_channels(fileReadLines(model_path))
+    mchannels, mchannel_len = parse_mchannels(fileReadLines(model_path))
+    model_with_attacker = str;
+    assert mem >= 0, "memory value must be positive"
+
+    chans_togen = set()
+
+    # first, process the input
+    mc = chans.split(",")
+    for chan in mc:
+        if ":" in chan:
+            name, num_extr = chan[:chan.index(":")], chan[chan.index(":")+1:]
+            if "-" in num_extr:
+                a, b = list(map(lambda a: int(a), num_extr.split("-")))
+                assert a < b
+                assert a >= 0
+                assert b < mchannel_len[name]
+                for i in range(a,b+1):
+                    chan_name = str(name) + "[" + str(i) + "]"
+                    chans_togen.add(chan_name)
+                    channels[chan_name] = mchannels[name]
+            else:
+                a = int(num_extr)
+                assert a >= 0
+                assert a < mchannel_len[name]
+                chan_name = str(name) + "[" + str(a) + "]"
+                chans_togen.add(chan_name)
+                channels[chan_name] = mchannels[name]
+
+        else : chans_togen.add(chan)
+
+    print(chans_togen)
+
+    for i in range(len(chans_togen)):
+        chan = list(chans_togen)[i]
+
+        if not "--nocheck" : assert chan in channels, "can't find "+str(chan)+" in model"
+
+        match attacker:
+            case "replay":
+                if unbounded : attacker_gadget = gen_replay_unbounded(chan, channels[chan], i)
+                else : attacker_gadget = gen_replay(chan, channels[chan], mem, i)
+            case "drop":
+                if unbounded : attacker_gadget = gen_drop_unbounded(chan, channels[chan], i)
+                else : attacker_gadget = gen_drop(chan, channels[chan], mem, i)
+            case "reorder":
+                if unbounded : attacker_gadget = gen_reorder_unbounded(chan, channels[chan], i)
+                else : attacker_gadget = gen_reorder(chan, channels[chan], mem, i)
+            case _:
+                print("error: inputted an invalid attacker model. \n")
+                sys.exit(1)
+
+        if model.rindex("};") >= model.rindex("}"):
+            model = model[:model.rindex("};")+2] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("};")+2:]
+        else:
+            model = model[:model.rindex("}")+1] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("}")+1:]
+
+    # Write the modified model to the output file
+    with open(out_file, 'w') as file:
+        file.write(model)
+
+    if "--eval" in args:
+        print()
+        print("generated Promela file with attacker model gadget... now running SPIN on "+str(out_file) + "!\n")
+        eval_model(out_file)
+
+        if "--cleanup" in args:
+            print("\nCleaning up Spin files...")
+            cleanup_spin_files()
+            try:
+                os.remove(out_file)
+                print(f"Removed: {out_file}")
+            except OSError:
+                pass
+
+
+if __name__== "__main__":
+    main()

src/model_generate.py

@@ -0,0 +1,346 @@
+import sys, re, subprocess, os, shutil
+from typing import List
+
+def gen_replay(chan : str, chan_type : List[str], mem : int, index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "chan attacker_mem_"+str(index)+" = ["+str(mem)+"] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n"
+    ret_string+= "\n"
+
+    ret_string+= "active proctype attacker_replay_"+str(index)+"() {\n"
+
+    item_arr = []
+    item_count = 0
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+
+    ret_string+="int i = "+str(mem)+";\n"
+    ret_string+="int b;\n"
+    ret_string+="CONSUME:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="   "+str(chan)+" ? <"+fs+"> -> attacker_mem_"+str(index)+" ! "+fs+";\n"
+    ret_string+="    i--;\n"
+    ret_string+="    if\n"
+    ret_string+="    :: i == 0 -> goto REPLAY;\n"
+    ret_string+="    :: i != 0 -> goto CONSUME;\n"
+    ret_string+="    fi\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto CONSUME;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  od\n"
+    ret_string+="REPLAY:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: atomic {\n"
+    ret_string+="    int am;\n"
+    ret_string+="    select(am : 0 .. len(attacker_mem_"+str(index)+")-1);\n"
+    ret_string+="    do\n"
+    ret_string+="    :: am != 0 ->\n"
+    ret_string+="      am = am-1;\n"
+    ret_string+="      attacker_mem_"+str(index)+" ? "+fs+" -> attacker_mem_"+str(index)+" ! "+fs+";\n"
+    ret_string+="    :: am == 0 ->\n"
+    ret_string+="      attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+";\n"
+    ret_string+="      break;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto REPLAY;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n"
+    ret_string+="  :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string
+
+def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "chan attacker_mem_"+str(index)+" = [99] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n"
+    ret_string+= "\n"
+
+    ret_string+= "active proctype attacker_replay_"+str(index)+"() {\n"
+
+    item_arr = []
+    item_count = 0
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+
+    ret_string+="int b;\n"
+    ret_string+="CONSUME:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="   "+str(chan)+" ? <"+fs+"> -> attacker_mem_"+str(index)+" ! "+fs+";\n"
+    ret_string+="    do\n"
+    ret_string+="    :: goto REPLAY;\n"
+    ret_string+="    :: goto CONSUME;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto CONSUME;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  od\n"
+    ret_string+="REPLAY:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: atomic {\n"
+    ret_string+="    int am;\n"
+    ret_string+="    select(am : 0 .. len(attacker_mem_"+str(index)+")-1);\n"
+    ret_string+="    do\n"
+    ret_string+="    :: am != 0 ->\n"
+    ret_string+="      am = am-1;\n"
+    ret_string+="      attacker_mem_"+str(index)+" ? "+fs+" -> attacker_mem_"+str(index)+" ! "+fs+";\n"
+    ret_string+="    :: am == 0 ->\n"
+    ret_string+="      attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+";\n"
+    ret_string+="      break;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto REPLAY;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n"
+    ret_string+="  :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string
+
+
+def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "chan attacker_mem_"+str(index)+" = ["+str(mem)+"] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n"
+    ret_string+= "\n"
+
+    ret_string+= "active proctype attacker_reorder_"+str(index)+"() priority 99 {\n"
+
+    item_arr = []
+    item_count = 0
+
+    attacker_mem = "attacker_mem_" + str(index)
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+    ret_string+="int i = "+str(mem)+";\n"
+    ret_string+="int b;\n"
+    ret_string+="INIT:\n"
+    ret_string+="do\n"
+    #  ret_string+="  :: true -> {\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> {\n"
+    ret_string+="      b = len("+str(chan)+");\n"
+    ret_string+="      do\n"
+    ret_string+="      :: b != len("+str(chan)+") -> goto INIT;\n"
+    ret_string+="      od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: goto CONSUME;\n"
+    ret_string+="od\n"
+    ret_string+="CONSUME:\n"
+    ret_string+="do\n"
+    ret_string+="  :: "+str(chan)+" ? "+str(fs)+" -> atomic {\n"
+    ret_string+="    "+str(attacker_mem)+" ! "+str(fs)+";\n"
+    ret_string+="    i--;\n"
+    ret_string+="    if\n"
+    ret_string+="    :: i == 0 -> goto REPLAY;\n"
+    ret_string+="    :: i != 0 -> goto CONSUME;\n"
+    ret_string+="    fi\n"
+    ret_string+="  }\n"
+    ret_string+="od\n"
+    ret_string+="REPLAY:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: atomic {\n"
+    ret_string+="  int am;\n"
+    ret_string+="    select(am : 0 .. len("+str(attacker_mem)+")-1);\n"
+    ret_string+="    do\n"
+    ret_string+="    :: am != 0 -> \n"
+    ret_string+="      am = am-1;\n"
+    ret_string+="      "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(attacker_mem)+" ! "+str(fs)+";\n"
+    ret_string+="    :: am == 0 ->\n"
+    ret_string+="      "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(chan)+" ! "+str(fs)+";\n"
+    ret_string+="      break;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: empty("+str(attacker_mem)+") -> goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string
+
+def gen_reorder_unbounded(chan : str, chan_type : List[str], index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "chan attacker_mem_"+str(index)+" = [99] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n"
+    ret_string+= "\n"
+
+    ret_string+= "active proctype attacker_reorder_"+str(index)+"() priority 99 {\n"
+
+    item_arr = []
+    item_count = 0
+
+    attacker_mem = "attacker_mem_" + str(index)
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+    ret_string+="int b;\n"
+    ret_string+="INIT:\n"
+    ret_string+="do\n"
+    #  ret_string+="  :: true -> {\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> {\n"
+    ret_string+="      b = len("+str(chan)+");\n"
+    ret_string+="      do\n"
+    ret_string+="      :: b != len("+str(chan)+") -> goto INIT;\n"
+    ret_string+="      od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: goto CONSUME;\n"
+    ret_string+="od\n"
+    ret_string+="CONSUME:\n"
+    ret_string+="do\n"
+    ret_string+="  :: "+str(chan)+" ? "+str(fs)+" -> atomic {\n"
+    ret_string+="    "+str(attacker_mem)+" ! "+str(fs)+";\n"
+    ret_string+="    do\n"
+    ret_string+="    :: goto REPLAY;\n"
+    ret_string+="    :: goto CONSUME;\n"
+    ret_string+="    od\n"
+    ret_string+="  }\n"
+    ret_string+="od\n"
+    ret_string+="REPLAY:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: atomic {\n"
+    ret_string+="  int am;\n"
+    ret_string+="    select(am : 0 .. len("+str(attacker_mem)+")-1);\n"
+    ret_string+="    do\n"
+    ret_string+="    :: am != 0 -> \n"
+    ret_string+="      am = am-1;\n"
+    ret_string+="      "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(attacker_mem)+" ! "+str(fs)+";\n"
+    ret_string+="    :: am == 0 ->\n"
+    ret_string+="      "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(chan)+" ! "+str(fs)+";\n"
+    ret_string+="      break;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: empty("+str(attacker_mem)+") -> goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string
+
+def gen_drop(chan : str, chan_type : List[str], mem : int, index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "active proctype attacker_drop_"+str(index)+"() {\n"
+
+    # proctype variables
+    item_arr = []
+    item_count = 0
+
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+
+    ret_string+="byte i = "+str(mem)+";\n"
+    ret_string+="int b;\n"
+    ret_string+="MAIN:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: "+str(chan)+" ? ["+fs+"] -> atomic {\n"
+    ret_string+="    if\n"
+    ret_string+="    :: i == 0 -> goto BREAK;\n"
+    ret_string+="    :: else ->\n"
+    ret_string+="      "+str(chan)+" ? "+fs+";\n"
+    ret_string+="       i = i - 1;\n"
+    ret_string+="       goto MAIN;\n"
+    ret_string+="    fi\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto MAIN;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string
+
+def gen_drop_unbounded(chan : str, chan_type : List[str], index : int) -> str:
+    ret_string = ""
+
+    ret_string+= "active proctype attacker_drop_"+str(index)+"() {\n"
+
+    # proctype variables
+    item_arr = []
+    item_count = 0
+
+    # formulate string of general message input variables
+    for item in chan_type:
+        item_arr.append("b_" + str(item_count))
+        ret_string+= str(item) + " " + item_arr[item_count] + ";\n"
+        item_count+=1
+
+    fs = (str([item for item in item_arr])[1:-1]).replace("'","")
+
+    ret_string+="int b;\n"
+    ret_string+="MAIN:\n"
+    ret_string+="  do\n"
+    ret_string+="  :: "+str(chan)+" ? ["+fs+"] -> atomic {\n"
+    ret_string+="    do \n"
+    ret_string+="    :: goto BREAK;\n"
+    ret_string+="    :: true ->\n"
+    ret_string+="      "+str(chan)+" ? "+fs+";\n"
+    ret_string+="       goto MAIN;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n"
+    ret_string+="    b = len("+str(chan)+");\n"
+    ret_string+="    do\n"
+    ret_string+="    :: b != len("+str(chan)+") -> goto MAIN;\n"
+    ret_string+="    od\n"
+    ret_string+="    }\n"
+    ret_string+="  :: goto BREAK;\n"
+    ret_string+="  od\n"
+    ret_string+="BREAK:\n"
+    ret_string+="}\n"
+
+    return ret_string

src/utility.py

@@ -0,0 +1,168 @@
+import sys, re, subprocess, os, shutil
+from typing import List
+
+def fileReadLines(fileName : str) -> str:
+	try:
+		txt = None
+		with open(fileName, 'r') as fr:
+			txt = fr.readlines()
+		return txt
+	except Exception:
+		return ""
+
+def fileRead(fileName : str) -> str:
+	try:
+		txt = None
+		with open(fileName, 'r') as fr:
+			txt = fr.read()
+		return txt
+	except Exception:
+		return ""
+
+def parse_channels(model : str) -> dict():
+    channels = {}
+    define_mapping = {}
+    for line in model:
+        if line.startswith("#define"):
+            data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line)
+            define_mapping[data.group(1)] = int(data.group(2))
+        if line.startswith("chan"):
+            # parsing regular channels
+            data = re.search(r"chan\s*([a-zA-Z\_\-]+).*\{(.+)\}", line)
+            # note, we don't have to think very hard about parsing Promela types.
+            # this is because mtype:whatever, mtype, and generic types are interchangable in Promela grammar
+            name, ctype = data.group(1), data.group(2).replace(" ","").split(",")
+            channels[name] = list(tuple(ctype))
+
+            # data_multichan = re.search(r"chan\s*([A-Za-z\_\-0-9]+)\[([A-Za-z0-9\_\-]+)\].*\{(.+)\}", line)
+            # m_name, m_cvalue, m_ctype = data.group(1), data.group(2), data.group(3).replace(" ","").split(",")
+
+            #  try:
+                #  m_cvalue = int(c_value)
+            #  except ValueError:
+                #  if type(m_cvalue) == str:
+                    #  assert m_cvalue in define_mapping, "{c_value} isn't defined, yet your Promela file still parsed. Did you recursively define {c_value}?"
+                    #  m_cvalue = define_mapping[m_cvalue]
+
+            #  channels[m_name] = (m_cvalue, m_ctype)
+
+        else : continue
+    # print(channels)
+    return channels
+
+def parse_mchannels(model : str) -> (dict(), dict()):
+    channels = {}
+    channel_lens = {}
+    define_mapping = {}
+    for line in model:
+        if line.startswith("#define"):
+            data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line)
+            define_mapping[data.group(1)] = int(data.group(2))
+            # print(define_mapping)
+        if line.startswith("chan"):
+            # parsing multichannels
+            data_multichan = re.search(r"chan\s*([A-Za-z\_\-0-9]+)\[([A-Za-z0-9\_\-]+)\].*\{(.+)\}", line)
+            if data_multichan:
+                m_name, m_cvalue, m_ctype = data_multichan.group(1), data_multichan.group(2), data_multichan.group(3).replace(" ","").split(",")
+            else : continue
+
+            try:
+                m_cvalue = int(m_cvalue)
+            except ValueError:
+                if type(m_cvalue) == str:
+                    assert m_cvalue in define_mapping, "{m_cvalue} isn't defined, yet your Promela file still parsed. Did you recursively define {c_value}?"
+                    m_cvalue = define_mapping[m_cvalue]
+
+            channels[m_name] = m_ctype
+            channel_lens[m_name] = m_cvalue
+
+
+        else : continue
+    # print(channels)
+
+    return channels, channel_lens
+
+def ensure_compile(model_path : str) -> None:
+    cmd = ['spin', '-a', model_path]
+    proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+    stdout, stderr = proc.communicate()
+    filename = os.path.basename(model_path)
+    userdir = os.getcwd()
+
+    # Convert bytes to string
+    stdout = stdout.decode()
+    stderr = stderr.decode()
+    assert "error" not in stdout, "there seems to be a syntax error in the model!"
+    # assert "syntax error" not in stdout, "there seems to be a syntax error in the model"
+    # assert "processes created" in stdout, "the spin model creates no processes ... check to see if it compiles"
+
+def eval_model(model_path : str) -> None:
+    cmd = ['spin', '-run', '-a', '-DNOREDUCE', model_path]
+    # Set text=True to get string output
+    proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True)
+
+    out = ""
+    while True:
+        output = proc.stdout.readline()
+        if output == '' and proc.poll() is not None:
+            break
+        if output:
+            out+=output
+            print(output, end='')
+
+    # No need to decode since output is already a string
+    #  stdout, stderr = proc.communicate()
+
+    #  filename = os.path.basename(model_path)
+    #  userdir = os.getcwd()
+
+    #  print(stderr)
+
+    if "pan: wrote" in out: # we know we wrote a trail
+        print("attack trace found!!!! printing!\n")
+        cd = os.getcwd()
+        if "/" in model_path:
+            od = cd + model_path[model_path.rindex("/"):] + ".trail"
+            shutil.copy(od, model_path + ".trail")
+            shutil.copy(cd + "/pan", model_path[:model_path.rindex("/"):] + "/pan")
+        else:
+            od = cd + model_path + ".trail"
+            # shutil.copy(od, model_path + ".trail")
+            # shutil.copy(cd + "/pan", model_path[:model_path.rindex("/"):] + "/pan")
+
+        cmd = ['spin', '-t0', '-s', '-r', model_path]
+        proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+        stdout, stderr = proc.communicate()
+        filename = os.path.basename(model_path)
+        userdir = os.getcwd()
+
+        # Convert bytes to string
+        stdout = stdout.decode()
+        stderr = stderr.decode()
+        
+        print(stdout)
+    else:
+        print()
+        print("Korg's exhaustive search is complete, no attacks found :)")
+
+def cleanup_spin_files() -> None:
+    """Remove files generated by Spin"""
+    files_to_remove = [
+        'pan', 'pan.*', '*.trail', '_spin_nvr.tmp',
+        '*.tcl', 'pan.b', 'pan.c', 'pan.h', 'pan.m', 'pan.t'
+    ]
+    for pattern in files_to_remove:
+        if '*' in pattern:
+            import glob
+            for f in glob.glob(pattern):
+                try:
+                    os.remove(f)
+                    print(f"Removed: {f}")
+                except OSError:
+                    pass
+        else:
+            try:
+                os.remove(pattern)
+                print(f"Removed: {pattern}")
+            except OSError:
+                pass

test_harness.py

@@ -0,0 +1,65 @@
+import yaml, sys
+import sys, re, subprocess, os, shutil
+from typing import List
+
+passed = 0
+failed = 0
+
+def show_help() -> None:
+    msg="""  Usage:
+    python3 test_harness.py tests/tests.yaml
+    """
+    print(msg)
+
+def run_spin_test(name, data):
+    global passed
+    global failed
+    data = {k: v for d in data for k, v in d.items()}
+    cmd = data['command']
+    intended = data['intended']
+    explanation = data['intended']
+
+    proc = subprocess.Popen(cmd.split(" "), stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True)
+
+    out = ""
+    while True:
+        output = proc.stdout.readline()
+        if output == '' and proc.poll() is not None:
+            break
+        if output:
+            out += output
+
+    res = None
+    if "assertion violated" in out:
+        res = "property violation"
+    elif "acceptance cycle" in out:
+        res = "acceptance cycle"
+    else : res = "no violation"
+
+    if res == intended:
+        print("passed: " + name)
+        passed+=1
+    else:
+        print("FAILED: " + name + " - got '" + res + "', expected '" + intended + "'")
+        failed+=1
+
+
+def main() -> None:
+    args = sys.argv[1:]  
+
+    if len(args) == 0 or args[0] in ["help", "--help", "-h", "-help"]:
+        show_help()
+        sys.exit()
+
+    test_file = args[0]
+
+    file = open(test_file, 'r')
+    data = yaml.safe_load(file)
+    for i in data:
+        run_spin_test(i, data[i])
+
+    print("")
+    print("SUMMARY:")
+    print("passed: " + str(passed) + "; failed: " + str(failed))
+
+main()

tests/drop/t1-drop.pml

@@ -0,0 +1,20 @@
+// INTENDED BEHAVIOR: acceptance cycle
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/drop/t2-drop.pml

@@ -0,0 +1,22 @@
+// INTENDED BEHAVIOR: no violation
+// explanation: attacker can only drop one message, but two are on the channel
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/drop/t3-drop.pml

@@ -0,0 +1,22 @@
+// INTENDED BEHAVIOR: violation
+// explanation: attacker should be able to drop both messages
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/drop/t4-drop.pml

@@ -0,0 +1,24 @@
+// INTENDED BEHAVIOR: violation
+// explanation: drop attacker should be able to find the attack in the middle of the chan
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!3;
+c!5;
+c!6;
+
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/drop/t5-drop-multi.pml

@@ -0,0 +1,24 @@
+// INTENDED BEHAVIOR: acceptance cycle
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+c!5;
+c!5;
+c!5;
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/drop/t6-drop-overwhelm.pml

@@ -0,0 +1,24 @@
+// INTENDED BEHAVIOR: acceptance cycle
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+c!5;
+c!5;
+c!5;
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/reorder/t1-reorder.pml

@@ -0,0 +1,30 @@
+// intended behavior: no violation
+// explanation: the rearrange attacker gadget shouldn't be able to violate the claim, as 
+// it doesn't have enough mem
+chan c = [8] of { byte };
+byte q=0;
+
+init {
+c!3;
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> 
+    q = q+1; 
+    goto B1;
+  od
+B1:
+  do 
+  :: c ? 3 ->
+    q = q + 1;
+    goto END;
+  od
+END:
+}
+
+ltl proc {
+  always !(q==2);
+}

tests/reorder/t2-reorder.pml

@@ -0,0 +1,36 @@
+// intended behavior: violation
+// explanation: rearrange attacker has enough mem to do the rearrange attack
+chan c = [8] of { byte };
+byte q=0;
+
+init {
+c!3;
+c!5;
+c!7;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 7 -> 
+    q = q+1; 
+    goto B1;
+  od
+B1:
+  do 
+  :: c ? 5 ->
+    q = q + 1;
+    goto B2;
+  od
+B2:
+  do 
+  :: c ? 3 ->
+    q = q + 1;
+    goto END;
+  od
+END:
+}
+
+ltl proc {
+  always !(q==3);
+}

tests/reorder/t3-reorder.pml

@@ -0,0 +1,36 @@
+// intended behavior: no violation
+// explanation: rearrange attacker does not have enough mem
+chan c = [8] of { byte };
+byte q=0;
+
+init {
+c!3;
+c!5;
+c!7;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 7 -> 
+    q = q+1; 
+    goto B1;
+  od
+B1:
+  do 
+  :: c ? 5 ->
+    q = q + 1;
+    goto B2;
+  od
+B2:
+  do 
+  :: c ? 3 ->
+    q = q + 1;
+    goto END;
+  od
+END:
+}
+
+ltl proc {
+  always !(q==3);
+}

tests/reorder/t4-reorder.pml

@@ -0,0 +1,34 @@
+// intended behavior: violation
+// explanation: rearrange attacker does not have enough mem
+chan c = [1] of { byte };
+byte q=0;
+
+init {
+c!3;
+c!5;
+c!7;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 3 -> 
+    goto B1;
+  od
+B1:
+  do 
+  :: c ? 7 ->
+    goto B2;
+  od
+B2:
+  do 
+  :: c ? 5 ->
+    goto END;
+  od
+END:
+q = 1;
+}
+
+ltl proc {
+  always !(q == 1);
+}

tests/replay/3-jump.pml

@@ -0,0 +1,29 @@
+// INTENDED BEHAVIOR: no violation
+// explanation: can only replay once
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC1;
+  od
+PROC1:
+  do 
+  :: c ? 5 -> goto PROC2;
+  od
+PROC2:
+  do 
+  :: c ? 5 -> goto PROC3;
+  od
+PROC3:
+  q=0;
+}
+
+ltl proc {
+  always !(q == 0);
+}

tests/replay/replay-out-of-order.pml

@@ -0,0 +1,34 @@
+// INTENDED BEHAVIOR: violation
+// explanation: replay, but in a different order than received
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+c!3;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC1;
+  od
+PROC1:
+  do 
+  :: c ? 3 -> goto PROC2;
+  od
+PROC2:
+  do 
+  :: c ? 3 -> goto PROC3;
+  od
+PROC3:
+  do 
+  :: c ? 5 -> goto PROC4;
+  od
+PROC4:
+  q=0;
+}
+
+ltl proc {
+  always !(q == 0);
+}

tests/replay/t1-replay.pml

@@ -0,0 +1,24 @@
+// INTENDED BEHAVIOR: violation
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC1;
+  od
+PROC1:
+  do 
+  :: c ? 5 -> goto PROC2;
+  od
+PROC2:
+  q=0;
+}
+
+ltl proc {
+  always !(q == 0);
+}

tests/replay/t2-replay.pml

@@ -0,0 +1,19 @@
+chan c = [8] of { byte };
+byte q=1;
+
+init {
+c!5;
+}
+
+active proctype consume() {
+MAIN:
+  do 
+  :: c ? 5 -> goto PROC;
+  od
+PROC:
+  q=0;
+}
+
+ltl proc {
+  eventually (q == 0);
+}

tests/tests.yaml

@@ -0,0 +1,76 @@
+t1-reorder:
+  - command: python src/main.py --model=tests/reorder/t1-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: the reorder attacker gadget shouldn't be able to violate the claim, as it doesn't have enough mem
+
+t1-reorder-more-mem:
+  - command: python src/main.py --model=tests/reorder/t1-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2
+  - intended: property violation
+  - explanation: the reorder attacker now has enough mem
+
+t2-reorder:
+  - command: python src/main.py --model=tests/reorder/t2-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=3
+  - intended: property violation
+  - explanation: rearrange attacker has enough mem to do the reorder attack
+
+t3-reorder:
+  - command: python src/main.py --model=tests/reorder/t3-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: rearrange attacker does not have enough mem
+
+t4-reorder:
+  - command: python src/main.py --model=tests/reorder/t4-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: rearrange attacker does not have enough mem
+
+t1-drop:
+  - command: python3 src/main.py --model=tests/drop/t1-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup
+  - intended: acceptance cycle
+  - explanation: drop attacker is able to remove the single message on the channel, preventing the eventually LTL property from ever satisfying
+
+t2-drop:
+  - command: python3 src/main.py --model=tests/drop/t2-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup
+  - intended: no violation
+  - explanation: drop attacker is not able to remove both the messages on the channel, so the LTL property remains satisfying
+
+t3-drop:
+  - command: python3 src/main.py --model=tests/drop/t3-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=2 --eval --cleanup
+  - intended: acceptance cycle
+  - explanation: attacker should drop both messages
+
+t4-drop:
+  - command: python3 src/main.py --model=tests/drop/t4-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup
+  - intended: acceptance cycle
+  - explanation: drop attacker should be able to find the attack in the middle of the chan
+
+t5-drop-multi:
+  - command: python3 src/main.py --model=tests/drop/t5-drop-multi.pml --attacker=drop --chan=c --output=temp.pml --mem=5 --eval --cleanup
+  - intended: acceptance cycle
+  - explanation: attacker can drop all five messages
+
+t6-drop-overwhelm:
+  - command: python3 src/main.py --model=tests/drop/t6-drop-overwhelm.pml --attacker=drop --chan=c --output=temp.pml --mem=4 --eval --cleanup
+  - intended: no violation
+  - explanation: attacker can't drop all five messages
+  
+t1-replay:
+  - command: python src/main.py --model=tests/replay/t1-replay.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1
+  - intended: property violation
+  - explanation: since the attacker is able to replay "5" on c, they can progress the consume proctype from PROC1, then PROC2
+
+t2-replay:
+  - command: python src/main.py --model=tests/replay/t2-replay.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: the attacker must eventually replay the packet onto the channel
+
+3-jump: 
+  - command: python src/main.py --model=tests/replay/3-jump.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: can only replay the packet once
+
+replay-out-of-order:
+  - command: python src/main.py --model=tests/replay/replay-out-of-order.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=2
+  - intended: property violation
+  - explanation: replay, but in a different order than received
+
+