synchronous/korg-distributed
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

tcp

Browse Source
This commit is contained in:
Jake Ginesin
2026-03-12 02:40:33 -04:00
parent f5820eb211
commit 6c55a8400b
21 changed files with 1473 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
._n_i_p_s_ Normal file
View File

@@ -0,0 +1,21 @@
ltl phi3 {
!(eventually (((always (state[0] == 2)) ||
(always (state[0] == 3)) ||
(always (state[0] == 4)) ||
(always (state[0] == 5)) ||
(always (state[0] == 6)) ||
(always (state[0] == 7)) ||
(always (state[0] == 8)) ||
(always (state[0] == 9)) ||
(always (state[0] == 10)))
&&
((always (state[1] == 2)) ||
(always (state[1] == 3)) ||
(always (state[1] == 4)) ||
(always (state[1] == 5)) ||
(always (state[1] == 6)) ||
(always (state[1] == 7)) ||
(always (state[1] == 8)) ||
(always (state[1] == 9)) ||
(always (state[1] == 10)))))
}

BIN
src/__pycache__/model_generate.cpython-313.pyc
View File

Binary file not shown.

1
src/model_generate.py
View File

@@ -283,7 +283,6 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], mem : int, index : i
# return ret_string # return ret_string
def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str: def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str:
ret_string = "" ret_string = ""

59
tests/abp/abp.pml Normal file
View File

@@ -0,0 +1,59 @@
mtype = { DATA0, DATA1, ACK0, ACK1 }
chan AtoB = [1] of { mtype }
chan BtoA = [1] of { mtype }
mtype ackA, ackB;
byte seqA = 0;
byte seqB = 0;
mtype packetA, packetB;
active proctype A()
{
do
::
if
:: seqA == 0 -> packetA = DATA0
:: else -> packetA = DATA1
fi;
AtoB!packetA;
do
:: BtoA?ackA ->
if
:: (seqA == 0 && ackA == ACK0) || (seqA == 1 && ackA == ACK1) ->
seqA = 1 - seqA;
break
:: else -> skip;
fi
::
AtoB!packetA
od
od
}
active proctype B()
{
do
:: AtoB?packetB ->
if
:: (seqB == 0 && packetB == DATA0) || (seqB == 1 && packetB == DATA1) ->
if
:: seqB == 0 -> ackB = ACK0
:: else -> ackB = ACK1
fi;
BtoA!ackB;
seqB = 1 - seqB;
:: else ->
if
:: seqB == 0 -> ackB = ACK1
:: else -> ackB = ACK0
fi;
BtoA!ackB;
fi
od
}
ltl liveness {
always ((packetA != packetB) implies eventually (packetA == packetB))
}

154
tests/paper.yaml Normal file
View File

@@ -0,0 +1,154 @@
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-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: dropping A's outbound messages alone is insufficient to create a half-open state; B cannot reach Established without receiving from A
tcp-phi1-drop-BtoN:
- command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1
- intended: no violation
- explanation: dropping B's outbound messages prevents B from progressing; A times out back to Closed, no half-open
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 directions prevents any handshake progress; neither side reaches Established
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: property violation
- explanation: replaying A's SYN can drive B into Established via a forged handshake while A returns to Closed, creating a half-open state
tcp-phi1-replay-BtoN:
- command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=BtoN --output=temp.pml --eval --cleanup --mem=1
- intended: property violation
- explanation: replaying B's SYN+ACK can cause A to believe handshake completed; if A then closes, B may remain Established
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: property violation
- explanation: replaying on both channels gives the attacker maximum ability to manufacture a half-open state
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: property violation
- explanation: reordering A's messages (e.g., delivering ACK before SYN) can desynchronize the handshake, leading to half-open
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: 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
- explanation: dropping A's messages can cause B to stall indefinitely in SynReceived or similar waiting states
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: acceptance cycle
- explanation: dropping on both channels can strand both sides in intermediate states with no timeout recovery
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: acceptance cycle
- explanation: replaying stale messages can trap B in a loop re-processing old handshake messages
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: 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
- explanation: if A's ACK is dropped, B remains stuck in SynReceived with no timeout to recover
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: acceptance cycle
- explanation: dropping B's SYN+ACK means A never sends ACK, leaving the initiator-side SynReceived unresolved
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 A's messages provides additional ACKs that can help resolve SynReceived
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: acceptance cycle
- explanation: reordering can deliver A's SYN after the ACK, confusing B's state machine and trapping it in SynReceived
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: dropping A's messages while in Closing does not cause A to transition to an unexpected state; A remains in Closing or eventually times out
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: property violation
- explanation: replaying a FIN while in Closing could cause a transition to TimeWait instead of the expected Closing or Closed
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: property violation
- explanation: replaying on both channels maximizes the chance of injecting an unexpected ACK that transitions Closing to TimeWait, violating the next-state constraint
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: property violation
- explanation: reordering close-sequence messages can cause ACK delivery at unexpected times, violating the strict Closing transition property

BIN
tests/tcp/pan Executable file
View File

Binary file not shown.

4
tests/tcp/props/phi1.pml Normal file
View File

@@ -0,0 +1,4 @@
/* safety: half-open prevention */
ltl phi1 {
always ( leftClosed implies !rightEstablished )
}

5
tests/tcp/props/phi2.pml Normal file
View File

@@ -0,0 +1,5 @@
/* liveness: verifying connection establishment */
ltl phi2 {
( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) )
implies ( eventually ( state[0] == 4 ) ) )
}

22
tests/tcp/props/phi3.pml Normal file
View File

@@ -0,0 +1,22 @@
/* liveness: no infinite stalls/deadlocks */
ltl phi3 {
!(eventually (((always (state[0] == SynSentState)) ||
(always (state[0] == SynRecState)) ||
(always (state[0] == EstState)) ||
(always (state[0] == FinW1State)) ||
(always (state[0] == CloseWaitState)) ||
(always (state[0] == FinW2State)) ||
(always (state[0] == ClosingState)) ||
(always (state[0] == LastAckState)) ||
(always (state[0] == TimeWaitState)))
&&
((always (state[1] == SynSentState)) ||
(always (state[1] == SynRecState)) ||
(always (state[1] == EstState)) ||
(always (state[1] == FinW1State)) ||
(always (state[1] == CloseWaitState)) ||
(always (state[1] == FinW2State)) ||
(always (state[1] == ClosingState)) ||
(always (state[1] == LastAckState)) ||
(always (state[1] == TimeWaitState)))))
}

11
tests/tcp/props/phi4.pml Normal file
View File

@@ -0,0 +1,11 @@
/* liveness: simultanous open */
ltl phi4 {
always (
(state[0] == SynSentState &&
state[1] == SynSentState)
implies
((eventually state[0] == EstState) &&
(eventually state[1] == EstState)))
}

13
tests/tcp/props/phi5.pml Normal file
View File

@@ -0,0 +1,13 @@
/* liveness: SYN_RECEIVED resolution*/
ltl phi5 {
always (
(state[0] == SynRecState)
implies (
eventually (
(state[0] == EstState ||
state[0] == FinW1State ||
state[0] == ClosedState)
)
)
)
}

9
tests/tcp/props/phi6.pml Normal file
View File

@@ -0,0 +1,9 @@
/* safety: strict closing transitions */
ltl phi6 {
always (
(state[0] == ClosingState)
implies
(next (state[0] == ClosingState ||
state[0] == ClosedState))
)
}

149
tests/tcp/tcp-phi1.pml Normal file
View File

@@ -0,0 +1,149 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* safety: half-open prevention */
ltl phi1 {
always ( leftClosed implies !rightEstablished )
}

149
tests/tcp/tcp-phi2.pml Normal file
View File

@@ -0,0 +1,149 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* liveness: verifying connection establishment */
ltl phi2 {
( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) )
implies ( eventually ( state[0] == 4 ) ) )

55
tests/tcp/tcp-phi2.pml.trail Normal file
View File

@@ -0,0 +1,55 @@
-2:2:-2
-4:-4:-4
1:0:121
2:1:114
3:0:121
4:1:115
5:0:121
6:1:116
7:0:121
8:1:117
9:0:121
10:3:0
11:0:121
12:3:1
13:0:121
14:3:2
15:0:121
16:3:9
17:0:121
18:2:0
19:0:121
20:2:1
21:0:121
22:2:2
23:0:121
24:2:9
25:0:121
26:3:17
27:0:121
28:3:1
29:0:121
30:3:3
31:0:121
32:3:22
33:0:119
34:2:17
35:0:126
36:2:1
37:0:121
38:2:3
39:0:121
40:2:22
41:0:121
42:2:42
43:0:121
44:2:1
-1:-1:-1
45:0:121
46:2:2
47:0:121
48:2:9
49:0:119
50:2:17
51:0:126
52:2:1

167
tests/tcp/tcp-phi3.pml Normal file
View File

@@ -0,0 +1,167 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* liveness: no infinite stalls/deadlocks */
ltl phi3 {
!(eventually (((always (state[0] == SynSentState)) ||
(always (state[0] == SynRecState)) ||
(always (state[0] == EstState)) ||
(always (state[0] == FinW1State)) ||
(always (state[0] == CloseWaitState)) ||
(always (state[0] == FinW2State)) ||
(always (state[0] == ClosingState)) ||
(always (state[0] == LastAckState)) ||
(always (state[0] == TimeWaitState)))
&&
((always (state[1] == SynSentState)) ||
(always (state[1] == SynRecState)) ||
(always (state[1] == EstState)) ||
(always (state[1] == FinW1State)) ||
(always (state[1] == CloseWaitState)) ||
(always (state[1] == FinW2State)) ||
(always (state[1] == ClosingState)) ||
(always (state[1] == LastAckState)) ||
(always (state[1] == TimeWaitState)))))
}

156
tests/tcp/tcp-phi4.pml Normal file
View File

@@ -0,0 +1,156 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* liveness: simultanous open */
ltl phi4 {
always (
(state[0] == SynSentState &&
state[1] == SynSentState)
implies
((eventually state[0] == EstState) &&
(eventually state[1] == EstState)))
}

43
tests/tcp/tcp-phi4.pml.trail Normal file
View File

@@ -0,0 +1,43 @@
-2:2:-2
-4:-4:-4
1:0:122
2:1:114
3:0:122
4:1:115
5:0:122
6:1:116
7:0:122
8:1:117
9:0:122
10:3:0
11:0:122
12:3:1
13:0:122
14:3:2
15:0:122
16:3:9
17:0:122
18:2:0
19:0:122
20:2:1
21:0:122
22:2:2
23:0:122
24:2:9
25:0:122
26:3:17
27:0:122
28:3:1
29:0:122
30:3:3
31:0:122
32:3:22
33:0:122
34:2:17
35:0:122
36:2:1
37:0:122
38:2:3
39:0:122
40:2:22
41:0:119

158
tests/tcp/tcp-phi5.pml Normal file
View File

@@ -0,0 +1,158 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* liveness: SYN_RECEIVED resolution*/
ltl phi5 {
always (
(state[0] == SynRecState)
implies (
eventually (
(state[0] == EstState ||
state[0] == FinW1State ||
state[0] == ClosedState)
)
)
)
}

154
tests/tcp/tcp-phi6.pml Normal file
View File

@@ -0,0 +1,154 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}
/* safety: strict closing transitions */
ltl phi6 {
always (
(state[0] == ClosingState)
implies
(next (state[0] == ClosingState ||
state[0] == ClosedState))
)
}

144
tests/tcp/tcp.pml Normal file
View File

@@ -0,0 +1,144 @@
// models: phi1, phi2, phi3, phi5
// does not model: phi4, phi7
// not yet implemented: phi6
mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN }
chan AtoN = [1] of { mtype };
chan NtoA = [0] of { mtype };
chan BtoN = [1] of { mtype };
chan NtoB = [0] of { mtype };
int state[2];
int pids[2];
#define ClosedState 0
#define ListenState 1
#define SynSentState 2
#define SynRecState 3
#define EstState 4
#define FinW1State 5
#define CloseWaitState 6
#define FinW2State 7
#define ClosingState 8
#define LastAckState 9
#define TimeWaitState 10
#define EndState -1
#define leftConnecting (state[0] == ListenState && state[1] == SynSentState)
#define leftEstablished (state[0] == EstState)
#define rightEstablished (state[1] == EstState)
#define leftClosed (state[0] == ClosedState)
proctype TCP(chan snd, rcv; int i) {
pids[i] = _pid;
CLOSED:
state[i] = ClosedState;
do
/* Passive open */
:: goto LISTEN;
/* Active open */
:: snd ! SYN; goto SYN_SENT;
/* Terminate */
:: goto end;
od
LISTEN:
state[i] = ListenState;
do
:: rcv ? SYN ->
atomic {
snd ! SYN;
snd ! ACK;
goto SYN_RECEIVED;
}
/* Simultaneous LISTEN */
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED;
od
SYN_SENT:
state[i] = SynSentState;
do
:: rcv ? SYN;
if
/* Standard behavior */
:: rcv ? ACK -> snd ! ACK; goto ESTABLISHED;
/* Simultaneous open */
:: snd ! ACK; goto SYN_RECEIVED;
fi
:: rcv ? ACK;
do
:: rcv ? SYN ->
snd ! ACK;
goto ESTABLISHED;
:: rcv ? _ -> skip;
od
:: rcv ? _ -> skip;
:: timeout -> goto CLOSED; /* Timeout */
od
SYN_RECEIVED:
state[i] = SynRecState;
do
:: rcv ? ACK -> goto ESTABLISHED;
:: rcv ? _ -> skip;
od
/* We may want to consider putting a timeout -> CLOSED here. */
ESTABLISHED:
state[i] = EstState;
do
/* Close - initiator sequence */
:: snd ! FIN; goto FIN_WAIT_1;
/* Close - responder sequence */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSE_WAIT;
:: rcv ? _ -> skip;
od
FIN_WAIT_1:
state[i] = FinW1State;
do
/* Simultaneous close */
:: rcv ? FIN ->
snd ! ACK;
goto CLOSING;
/* Standard close */
:: rcv ? ACK -> goto FIN_WAIT_2;
:: rcv ? _ -> skip;
od
CLOSE_WAIT:
state[i] = CloseWaitState;
do
:: snd ! FIN; goto LAST_ACK;
:: rcv ? _ -> skip;
od
FIN_WAIT_2:
state[i] = FinW2State;
do
:: rcv ? FIN ->
snd ! ACK;
goto TIME_WAIT;
:: rcv ? _ -> skip;
od
CLOSING:
state[i] = ClosingState;
do
:: rcv ? ACK -> goto TIME_WAIT;
:: rcv ? _ -> skip;
od
LAST_ACK:
state[i] = LastAckState;
do
:: rcv ? ACK -> goto CLOSED;
:: rcv ? _ -> skip;
od
TIME_WAIT:
state[i] = TimeWaitState;
goto CLOSED;
end:
state[i] = EndState;
}
init {
state[0] = ClosedState;
state[1] = ClosedState;
run TCP(AtoN, NtoA, 0);
run TCP(BtoN, NtoB, 1);
}