From c0af251f1741619b6290e5c42151ce538e5b0d49 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Wed, 5 Nov 2025 15:24:56 -0500 Subject: [PATCH] improve replay attacker, add deadlock tests --- README.md | 15 +- .../model_generate.cpython-313.pyc | Bin 16533 -> 20378 bytes src/main-old.py | 146 ++++++++ src/main.py | 333 ++++++++++++------ src/model_generate.py | 174 ++++++++- tests/no-deadlocks/t1-deadlock.pml | 21 ++ tests/replay/weave.pml | 35 ++ tests/tests.yaml | 29 +- 8 files changed, 623 insertions(+), 130 deletions(-) create mode 100644 src/main-old.py create mode 100644 tests/no-deadlocks/t1-deadlock.pml create mode 100644 tests/replay/weave.pml diff --git a/README.md b/README.md index fbb271f..3ea6610 100644 --- a/README.md +++ b/README.md @@ -1,16 +1,25 @@ # Korg, reborn # TODO: +- [x] nix flake here - [x] fix weird spin errors(?) + - jake note: pinned specific working SPIN version using Nix - [x] add attackers that only do specifically n queries - - limitation: you cannot choose only *n* queries for the dropping attacker + - limitation: you cannot choose only *n* queries for the dropping attacker; trace violations can happen at any time - [x] add attackers to do <= n queries +- [x] add attackers that can do attacks with an unbounded number of messages - [x] add a test suite -- [ ] make the impl more robust; do more SWE +- [x] make the impl more robust; do more SWE + - federico gave me a free cursor subscription, so maybe I'll try that out +- [x] add no self-deadlock experiments + - I envision this would be: providing an eventually-style LTL query, sending messages onto an open channel, and asserting that the gadget doesn't somehow deadlock with itself +- [ ] add raft, TCP, SCTP, ABP experiments from old Korg impl to the test suite +- [ ] add labels on trace logging to gadgets - [ ] 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. +- One explicit limitation of the replay attacker is not being able to transition back to listening for packets after replaying +- Maybe change the title to: Korg: Automated analysis of channel faults diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc index a2c4aff8dd3d4e06e7feeaf1106e9ee2de237664..fd345dfd41f1e137d95ac5e868c80aabdf84814f 100644 GIT binary patch delta 1906 zcmbW0Urbw79LIaxTRU$5UBlYacGyb`rR^v%HcAUE3=4?Hu}LWcZgx;QWE46NOr_hL zOQwkr8k%3G%VL5inqc$+)0ZZTX1Ya*zVzyYi*G*b5{!ESA3VQ%<2d zIrsF&HRjejWBT1_9!h zok4OK3uo(fMoF45MsJd|d5-a$i|x#AjoCDpSxS-2h3xcdDwmxthV+Dmw9}#<*1_8y zf#OHZZ8fAi>kWyfpi!k-Vv}sb3(;dfSl8Ii%|SYqV)wx{jot3AvIP|HVaeN4h5>YY*MRj8hqqQQo z2VQKc2aYwEqg9pV$jYj*y~tp7q(`aVtEkGI{qNHX_Ek+(QB&!2Tv7kw^gS*AQmLz_ux$xlZKNNI zG$Fhc`C5TK-QB{x&=3>agqKFl9`+3@(1LID;)7*H$TOW?o5N+f&|cZ7}0{j&5>3_8xU*XXhq-Ym6hrALWZOk zGmELb_6!!t*YpT8Bs0Cx!;vUv#Spy|`A7e`9aa#oaB#=!fgeJ48@K=WBjYqF#)342A>``T0YS<{+9WDiNI%=<;w|CjWMtnY9BHND6>p}*Myxo{l_ zO-8s8ZilywKVGe@;rq09Bl(F#f;J1_Dl%cqhepDd40 zi2Ou(G9&UCkW;cA>%fUP0Hae$`)rqVP9yl`QON`1KSbl^a%vWLkhzlAbw&LgJRULPl zn%>3pItcxGM{&ybCg&n!)UacczxIp}6SA2lpZsY@sRs;hua+cG#oVX0B#CO>y{o-I z#r@*C=VlEv0pVct)#s^!q!4PvS%eKyhj1XK5i^K-#A66-PtpkKI$=*Ti^w3bv2^#y zIaG59CnAD)0Wpv8s3s|;yGVtKOd;A3I50VaIE3gxoJTAmIuTh!7h(}1-N+tP(zRTI zuGScngNvX)Dpb-P~12CpF65pl!-VioZmd>;*HFH?EF$i%d2h6i0=+=3sF;K>u5gkVo{ z8K(Li+#6KV!Bop}c(uNMUbhktrI_s*_`2^q_I29vPn5K4ADYE7jS zvCwOmAA&@D^d?^SB6z7M3&n%@2lyXoKo63FINuEp%x8Y{W9Ii8rul|Ff69zsKA$Fu zvHIul%x2s+LQJ-!6}rGQdm~`i4Es|68&!`;voiPE6aA{!4Sf`6VcqA(Mv27?XN2u| zbgfjZj`QMtWwPOn>0D;r^wrLETTuC_g$WTB?f_xM5m|GrkxNK1_Nv}My=)~KA= zQL5tjno~}`@UZKY4n|jQi3Gn5y1*R}1R)Rscfly=2Lm7v#sD6`$H4@c1XCaera=Mh z0%t%G+ynb1QI;P;m;)o=I4FSx*bS0k2HXcH!7Mlh%HSM03oK9((2qof#7D6?x@4X1 znHQ-o$yu@1R8}T6{ZV-=GOF`A-K#K8bHNa`hQq8*>%k!H%_MZUuKVN#%4hcNd5FS~ zKpdpN5Lg5^=ym3>vLwP2&X 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 Output 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() diff --git a/src/main.py b/src/main.py index 75c5d5b..a7b1b79 100644 --- a/src/main.py +++ b/src/main.py @@ -1,138 +1,243 @@ -# ============================================================================== +# ============================================================================== # 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 +import sys +import subprocess +import os +import shutil +import argparse +from typing import List, Set, Dict, Tuple 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" - +def _parse_channel_selection( + chans_str: str, + mchannels: Dict[str, List[str]], + mchannel_len: Dict[str, int], + channels: Dict[str, List[str]] +) -> Set[str]: + """ + Parses the user's channel selection string (e.g., "ch1,ch2:1-3,ch3:5"). + + Raises: + ValueError: If the format is invalid or ranges are out of bounds. + """ chans_togen = set() - + # first, process the input - mc = chans.split(",") + mc = chans_str.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) + "]" + try: + name, num_extr = chan.split(":", 1) + if name not in mchannel_len: + raise ValueError(f"unknown multi-channel '{name}'") + + max_len = mchannel_len[name] + + if "-" in num_extr: + a_str, b_str = num_extr.split("-", 1) + a, b = int(a_str), int(b_str) + + if not (0 <= a < b < max_len): + raise ValueError(f"invalid range '{a}-{b}' for {name} (max is {max_len-1})") + + for i in range(a, b + 1): + chan_name = f"{name}[{i}]" + chans_togen.add(chan_name) + channels[chan_name] = mchannels[name] + else: + a = int(num_extr) + if not (0 <= a < max_len): + raise ValueError(f"invalid index '{a}' for {name} (max is {max_len-1})") + + chan_name = f"{name}[{a}]" 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] + + except (ValueError, TypeError) as e: + raise ValueError(f"invalid channel format: '{chan}'. {e}") - else : chans_togen.add(chan) + else: + chans_togen.add(chan) + + return chans_togen - 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:] +def _inject_attacker_code(model_content: str, attacker_gadget: str) -> str: + """ + Injects the generated attacker gadget code into the Promela model string. + + Note: This injection method is fragile as it relies on finding the + last '};' or '}' in the file. + """ + try: + # Original logic: find the last '};' or '}' + if model_content.rindex("};") >= model_content.rindex("}"): + idx = model_content.rindex("};") + 2 + return model_content[:idx] + "\n\n" + attacker_gadget + "\n" + model_content[idx:] else: - model = model[:model.rindex("}")+1] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("}")+1:] + idx = model_content.rindex("}") + 1 + return model_content[:idx] + "\n\n" + attacker_gadget + "\n" + model_content[idx:] + except ValueError: + # Fallback: append to the end if no '}' or '};' is found + return model_content + "\n\n" + attacker_gadget - # 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") +def parse_args() -> argparse.Namespace: + """Configures and parses command-line arguments.""" + parser = argparse.ArgumentParser( + description="Synthesize attacker gadgets for Promela models." + ) + + parser.add_argument( + "--model", + type=str, + required=True, + help="Promela model to generate attackers on" + ) + parser.add_argument( + "--attacker", + type=str, + required=True, + choices=["replay", "drop", "reorder"], + help="The type of attacker to synthesize" + ) + parser.add_argument( + "--chan", + type=str, + required=True, + help="Channels to synthesize attackers on. (e.g., 'ch1,ch2:0-2,ch3:4')" + ) + parser.add_argument( + "--mem", + type=str, + default="3", + help="Size of memory. Use 'unbounded' for unbounded memory. (default: 3)" + ) + parser.add_argument( + "--output", + type=str, + help="Output file name. (default: korg-promela-out.pml if --eval is used)" + ) + parser.add_argument( + "--nocheck", + action="store_true", + help="Don't check channel validity" + ) + parser.add_argument( + "--eval", + action="store_true", + help="Evaluate the outputted file with Spin" + ) + parser.add_argument( + "--cleanup", + action="store_true", + help="Clean up the extra files spin creates, including Korg's" + ) + + return parser.parse_args() + + +def main() -> None: + args = parse_args() + + # --- 1. Argument Validation --- + + # Handle output file logic + out_file = args.output + if args.eval and not args.output: + out_file = "korg-promela-out.pml" + elif not args.output: + print("error: --output=path/to/file.pml is required when --eval is not used.", file=sys.stderr) + sys.exit(1) + + # Handle memory logic + unbounded = (args.mem == "unbounded") + mem = 0 + if not unbounded: + try: + mem = int(args.mem) + if mem < 0: + raise ValueError("memory value must be positive") + except ValueError as e: + print(f"error: invalid --mem value. {e}", file=sys.stderr) + sys.exit(1) + + # --- 2. Model Reading and Compilation Check --- + + # Check for file existence and read + model_lines = fileReadLines(args.model) + model_content = fileRead(args.model) + if not model_content: # fileRead returns "" on error + print(f"error: could not read model file at '{args.model}'", file=sys.stderr) + sys.exit(1) + + # Ensure model compiles before proceeding + try: + ensure_compile(args.model) + except AssertionError as e: + print(f"error: Model compilation failed. {e}", file=sys.stderr) + sys.exit(1) + + # --- 3. Model Parsing --- + channels = parse_channels(model_lines) + mchannels, mchannel_len = parse_mchannels(model_lines) + + try: + chans_togen = _parse_channel_selection( + args.chan, mchannels, mchannel_len, channels + ) + except ValueError as e: + print(f"error: Failed to parse --chan argument. {e}", file=sys.stderr) + sys.exit(1) + + print(f"Generating attackers for: {chans_togen}") + + # --- 4. Attacker Generation --- + for i, chan in enumerate(list(chans_togen)): + if not args.nocheck and chan not in channels: + print(f"error: can't find channel '{chan}' in model. (Use --nocheck to override)", file=sys.stderr) + sys.exit(1) + + attacker_gadget = "" + chan_type = channels.get(chan, []) # Default to empty list if not found (and --nocheck) + + match args.attacker: + case "replay": + attacker_gadget = gen_replay_unbounded(chan, chan_type, i) if unbounded \ + else gen_replay(chan, chan_type, mem, i) + case "drop": + attacker_gadget = gen_drop_unbounded(chan, chan_type, i) if unbounded \ + else gen_drop(chan, chan_type, mem, i) + case "reorder": + attacker_gadget = gen_reorder_unbounded(chan, chan_type, i) if unbounded \ + else gen_reorder(chan, chan_type, mem, i) + case _: + # This should be unreachable due to argparse `choices` + print(f"error: invalid attacker model '{args.attacker}'.", file=sys.stderr) + sys.exit(1) + + # Inject the generated gadget into the model + model_content = _inject_attacker_code(model_content, attacker_gadget) + + # --- 5. Write Output --- + try: + with open(out_file, 'w') as file: + file.write(model_content) + except IOError as e: + print(f"error: could not write to output file {out_file}. {e}", file=sys.stderr) + sys.exit(1) + + # --- 6. Evaluate and Cleanup --- + if args.eval: + print(f"\nGenerated Promela file... now running SPIN on {out_file}!\n") eval_model(out_file) - if "--cleanup" in args: + if args.cleanup: print("\nCleaning up Spin files...") cleanup_spin_files() try: @@ -142,5 +247,5 @@ def main() -> None: pass -if __name__== "__main__": +if __name__ == "__main__": main() diff --git a/src/model_generate.py b/src/model_generate.py index 2f3dd4c..0db573e 100644 --- a/src/model_generate.py +++ b/src/model_generate.py @@ -1,6 +1,72 @@ import sys, re, subprocess, os, shutil from typing import List +# def gen_replay_old(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(chan : str, chan_type : List[str], mem : int, index : int) -> str: ret_string = "" @@ -29,10 +95,15 @@ def gen_replay(chan : str, chan_type : List[str], mem : int, index : int) -> str ret_string+=" i--;\n" ret_string+=" if\n" ret_string+=" :: i == 0 -> goto REPLAY;\n" - ret_string+=" :: i != 0 -> goto CONSUME;\n" + ret_string+=" :: i != 0 -> {\n" + ret_string+=" do\n" + ret_string+=" :: goto CONSUME\n" + ret_string+=" :: goto REPLAY\n" + ret_string+=" od\n" + ret_string+=" }\n" ret_string+=" fi\n" ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 CONSUME;\n" @@ -49,16 +120,25 @@ def gen_replay(chan : str, chan_type : List[str], mem : int, index : int) -> str 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+=" do\n" + ret_string+=" :: attacker_mem_"+str(index)+" ? ["+fs+"] -> "+str(chan)+" ! "+fs+"; break;\n" + ret_string+=" :: attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+"; break;\n" + ret_string+=" od\n" ret_string+=" break;\n" ret_string+=" od\n" ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 REPLAY;\n" ret_string+=" od\n" ret_string+=" }\n" + ret_string+=" :: i != 0 -> {\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+=" :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n" ret_string+=" :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n" ret_string+=" od\n" @@ -67,7 +147,7 @@ def gen_replay(chan : str, chan_type : List[str], mem : int, index : int) -> str return ret_string -def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str: +def gen_replay_unbounded(chan : str, chan_type : List[str], mem : int, index : int) -> str: ret_string = "" ret_string+= "chan attacker_mem_"+str(index)+" = [99] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n" @@ -92,11 +172,10 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str: 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+=" :: goto CONSUME\n" + ret_string+=" :: goto REPLAY\n" ret_string+=" od\n" - ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 CONSUME;\n" @@ -113,16 +192,25 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str: 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+=" do\n" + ret_string+=" :: attacker_mem_"+str(index)+" ? ["+fs+"] -> "+str(chan)+" ! "+fs+"; break;\n" + ret_string+=" :: attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+"; break;\n" + ret_string+=" od\n" ret_string+=" break;\n" ret_string+=" od\n" ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 REPLAY;\n" ret_string+=" od\n" ret_string+=" }\n" + ret_string+=" :: {\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+=" :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n" ret_string+=" :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n" ret_string+=" od\n" @@ -131,6 +219,70 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str: return ret_string +# def gen_replay_unbounded_old(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 = "" diff --git a/tests/no-deadlocks/t1-deadlock.pml b/tests/no-deadlocks/t1-deadlock.pml new file mode 100644 index 0000000..cb59a5b --- /dev/null +++ b/tests/no-deadlocks/t1-deadlock.pml @@ -0,0 +1,21 @@ +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!5; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/replay/weave.pml b/tests/replay/weave.pml new file mode 100644 index 0000000..311dc0e --- /dev/null +++ b/tests/replay/weave.pml @@ -0,0 +1,35 @@ +// 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 -> + c!3; + goto PROC2; + od +PROC2: + do + :: c ? 3 -> goto PROC3; + od +PROC3: + do + :: c ? 3 -> goto PROC4; + od +PROC4: + q=0; +} + +ltl proc { + always !(q == 0); +} diff --git a/tests/tests.yaml b/tests/tests.yaml index 8d926a7..f9f1255 100644 --- a/tests/tests.yaml +++ b/tests/tests.yaml @@ -1,3 +1,18 @@ +drop-nodeadlock: + - command: python src/main.py --model=tests/no-deadlocks/t1-deadlock.pml --attacker=drop --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: drop gadget does not deadlock + +replay-nodeadlock: + - command: python src/main.py --model=tests/no-deadlocks/t1-deadlock.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: replay gadget does not deadlock + +reorder-nodeadlock: + - command: python src/main.py --model=tests/no-deadlocks/t1-deadlock.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reorder gadget does not deadlock + 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 @@ -65,12 +80,22 @@ t2-replay: 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 + - intended: property violation + - explanation: can replay the same packet multiple times 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 +weave: + - command: python src/main.py --model=tests/replay/weave.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: consume-replay-consume-replay pattern is able to be found + +weave-lessmem: + - command: python src/main.py --model=tests/replay/weave.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: second consume cannot be completed, as we run out of consumption budget; however, we do have enough memory room for this +