diff --git a/src/utility.py b/src/utility.py index c4c569b..4448a80 100644 --- a/src/utility.py +++ b/src/utility.py @@ -25,12 +25,17 @@ def parse_channels(model : str) -> dict(): for line in model: if line.startswith("#define"): data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line) + if data is None : continue + if not data.group(1) or not data.group(2) : continue + print(data) 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 + if data is None : continue + if not data.group(1) or not data.group(2) : continue name, ctype = data.group(1), data.group(2).replace(" ","").split(",") channels[name] = list(tuple(ctype)) @@ -47,7 +52,7 @@ def parse_channels(model : str) -> dict(): # channels[m_name] = (m_cvalue, m_ctype) else : continue - # print(channels) + return channels def parse_mchannels(model : str) -> (dict(), dict()): @@ -57,11 +62,17 @@ def parse_mchannels(model : str) -> (dict(), dict()): for line in model: if line.startswith("#define"): data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line) + if data is None : continue + if not data.group(1) or not data.group(2) : continue 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 is None: + continue + 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 @@ -78,7 +89,6 @@ def parse_mchannels(model : str) -> (dict(), dict()): else : continue - # print(channels) return channels, channel_lens @@ -110,14 +120,6 @@ def eval_model(model_path : str) -> None: 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() @@ -139,7 +141,7 @@ def eval_model(model_path : str) -> None: # Convert bytes to string stdout = stdout.decode() stderr = stderr.decode() - + print(stdout) else: print() diff --git a/tests/paper.yaml b/tests/paper.yaml index e37883d..061fb04 100644 --- a/tests/paper.yaml +++ b/tests/paper.yaml @@ -48,31 +48,6 @@ tcp-phi1-reorder-bidirectional: - intended: property violation - explanation: reordering on both channels maximizes desynchronization potential for half-open -tcp-phi2-drop-AtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: dropping A's SYN prevents the handshake from completing, violating the liveness property that A should eventually reach Established - -tcp-phi2-drop-BtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: dropping B's SYN+ACK response prevents A from ever completing the handshake - -tcp-phi2-drop-bidirectional: - - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: dropping on both channels trivially prevents connection establishment - -tcp-phi2-replay-AtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: replaying A's messages does not prevent establishment; extra SYNs are handled by B's wildcard receives - -tcp-phi2-reorder-AtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: reordering A's handshake messages can prevent B from following the correct SYN/ACK sequence, stalling establishment - tcp-phi3-drop-AtoN: - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - intended: acceptance cycle @@ -93,26 +68,6 @@ tcp-phi3-reorder-bidirectional: - intended: acceptance cycle - explanation: reordering on both channels can desynchronize both sides into permanently mismatched states -tcp-phi4-drop-AtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: during simultaneous open, dropping A's SYN prevents B from advancing, breaking the simultaneous open guarantee - -tcp-phi4-drop-bidirectional: - - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: dropping both sides' SYNs trivially prevents simultaneous open from resolving - -tcp-phi4-replay-AtoN: - - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: replaying SYN messages during simultaneous open should not prevent eventual establishment; the protocol handles duplicate SYNs - -tcp-phi4-reorder-bidirectional: - - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: reordering handshake messages during simultaneous open can prevent the SYN+ACK exchange from completing correctly - tcp-phi5-drop-AtoN: - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 - intended: acceptance cycle