From 11f05ad93a314f2408d1e2040959739e67f18210 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Thu, 12 Mar 2026 03:05:11 -0400 Subject: [PATCH] attempt test suite 2 --- tests/paper2.yaml | 127 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 tests/paper2.yaml diff --git a/tests/paper2.yaml b/tests/paper2.yaml new file mode 100644 index 0000000..4c46c60 --- /dev/null +++ b/tests/paper2.yaml @@ -0,0 +1,127 @@ +unidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +bidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +# ============================================================================= +# TCP tests +# +# NOTE: The TCP model uses separate send/receive channel pairs +# (AtoN[1], NtoA[0], BtoN[1], NtoB[0]) with no network forwarding process. +# A sends on AtoN but B receives on NtoB; Korg's single-channel attacker +# gadgets cannot bridge this gap. As a result, all single-channel attacks +# are ineffective: consumed/replayed/reordered messages on AtoN never +# reach B (and vice versa). Both TCP processes fall back to Closed via +# timeout transitions, so all properties hold trivially or vacuously. +# +# This demonstrates a structural limitation: Korg's channel-local attackers +# require that communicating processes share the attacked channel. A network +# forwarding process (AtoN -> NtoB, BtoN -> NtoA) would be needed for +# meaningful cross-channel attacks. +# ============================================================================= + +# phi1: safety - half-open prevention +# always (leftClosed implies !rightEstablished) + +tcp-phi1-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: attacker consumes from AtoN but B reads NtoB; no messages are delivered cross-channel so neither side reaches Established, and phi1 holds trivially + +tcp-phi1-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping on both outbound channels still cannot affect the inbound rendezvous channels NtoA/NtoB; no handshake progress occurs + +tcp-phi1-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replayed messages land back on AtoN, which only A writes to; B never reads AtoN so no half-open state can be manufactured + +tcp-phi1-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying on both outbound channels cannot bridge to the rendezvous inbound channels; property holds vacuously + +tcp-phi1-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering on AtoN is invisible to B; the channel architecture prevents any cross-channel effect + +tcp-phi1-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering both outbound channels still cannot deliver messages to the inbound rendezvous channels + +# phi3: liveness - no infinite stalls/deadlocks + +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: no violation + - explanation: timeout transitions in LISTEN and SYN_SENT return both processes to Closed; no permanent stall occurs because no cross-channel delivery happens + +tcp-phi3-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: same as above; both sides cycle through Closed via timeout, preventing any permanent intermediate state + +tcp-phi3-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replayed messages on AtoN do not reach B; both sides timeout-cycle through Closed, so no stall + +tcp-phi3-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering cannot create stalls when messages never cross between the two TCP processes + +# phi5: liveness - SYN_RECEIVED resolution +# SynReceived implies eventually (Established or FinWait1 or Closed) + +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: no violation + - explanation: neither process enters SynReceived because no SYN is ever delivered cross-channel; the property holds vacuously + +tcp-phi5-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: same as above; without cross-channel delivery, SynReceived is never entered + +tcp-phi5-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying on AtoN cannot deliver a SYN to B via NtoB; SynReceived is never reached, so the property holds vacuously + +tcp-phi5-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering on AtoN has no cross-channel effect; property holds vacuously as SynReceived is unreachable + +# phi6: safety - strict closing transitions +# Closing implies next(Closing or Closed) + +tcp-phi6-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: Closing state is never reached without cross-channel message delivery; property holds vacuously + +tcp-phi6-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replay on AtoN cannot drive either process into Closing; property holds vacuously + +tcp-phi6-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying on both outbound channels still cannot bridge to inbound rendezvous channels; Closing never entered + +tcp-phi6-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering both outbound channels has no effect on the rendezvous inbound channels; Closing never entered