From 33ff1af2b766d2c8583ca1fbf53871454176d04c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 6 Apr 2024 16:41:16 -0700 Subject: [PATCH] TCP according to RFC 9293. (#131) TCP according to RFC 9293. [Feature] Signed-off-by: Markus Alexander Kuppe --- README.md | 3 +- manifest.json | 43 +++++ specifications/tcp/MCtcp.cfg | 27 +++ specifications/tcp/MCtcp.tla | 32 ++++ specifications/tcp/tcp.tla | 330 +++++++++++++++++++++++++++++++++++ 5 files changed, 434 insertions(+), 1 deletion(-) create mode 100644 specifications/tcp/MCtcp.cfg create mode 100644 specifications/tcp/MCtcp.tla create mode 100644 specifications/tcp/tcp.tla diff --git a/README.md b/README.md index 15e3d390..4de97f34 100644 --- a/README.md +++ b/README.md @@ -87,7 +87,8 @@ Here is a list of specs included in this repository, with links to the relevant | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | | [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | | [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | -| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | +| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | +| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | | ## Examples Elsewhere Here is a list of specs stored in locations outside this repository, including submodules. diff --git a/manifest.json b/manifest.json index 09188eda..4385e8f3 100644 --- a/manifest.json +++ b/manifest.json @@ -5144,6 +5144,49 @@ ] } ] + }, + { + "path": "specifications/tcp", + "title": "TCP as defined in RFC 9293", + "description": "Transmission Control Protocol (TCP)", + "sources": ["https://datatracker.ietf.org/doc/html/rfc9293"], + "authors": [ + "Markus Kuppe" + ], + "tags": [], + "modules": [ + { + "path": "specifications/tcp/tcp.tla", + "communityDependencies": [ + "SequencesExt" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/tcp/MCtcp.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/tcp/MCtcp.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "state constraint", + "liveness" + ], + "result": "success", + "distinctStates": 1182, + "totalStates": 6322, + "stateDepth": 14 + } + ] + } + ] } ] } diff --git a/specifications/tcp/MCtcp.cfg b/specifications/tcp/MCtcp.cfg new file mode 100644 index 00000000..0b4087b2 --- /dev/null +++ b/specifications/tcp/MCtcp.cfg @@ -0,0 +1,27 @@ +CONSTANTS + A = A + B = B + +CONSTANT + Peers <- peers + Init <- MCInit + +\* Disable symmetry reduction when checking liveness. +\* SYMMETRY +\* Symmetry + +SPECIFICATION + Spec + +INVARIANT + TypeOK + Inv + +PROPERTY + Prop + +CONSTRAINT + NoRetransmission + +ACTION_CONSTRAINT + SingleActiveOpen diff --git a/specifications/tcp/MCtcp.tla b/specifications/tcp/MCtcp.tla new file mode 100644 index 00000000..e0cee03e --- /dev/null +++ b/specifications/tcp/MCtcp.tla @@ -0,0 +1,32 @@ +---- MODULE MCtcp ---- +EXTENDS tcp, TLC + +CONSTANTS A, B +peers == {A, B} +Symmetry == Permutations(peers) + +MCInit == + \* One node starts in the SYN-SENT state, i.e., one node has already received the active open command. The other node + \* is in the listen state, i.e., it has received the passive open command. + \E node \in Peers: + /\ tcb = [p \in Peers |-> TRUE] + /\ connstate = [p \in Peers |-> IF p = node THEN "SYN-SENT" ELSE "LISTEN"] + /\ network = [p \in Peers |-> IF p = node THEN <<>> ELSE << "SYN" >>] + +NoRetransmission == + \A p \in Peers : + \A i \in 1..Len(network[p]) - 1 : + network[p][i] # network[p][i + 1] + +SingleActiveOpen == + \* A real system will allow infinitely many active opens of TCP connections. An + \* explicit state model checker like TLC cannot enumerate infinitely many states. + \* Thus, do not allow multiple active opens (the first active open is implicit in Init). + ~ \E local, remote \in Peers: + \/ ACTIVE_OPEN(local, remote) + \/ PASSIVE_OPEN(local, remote) + \/ SEND(local, remote) + +============================================================================= +\* Modification History +\* Created Tue Apr 02 10:38:50 PDT 2024 by markus diff --git a/specifications/tcp/tcp.tla b/specifications/tcp/tcp.tla new file mode 100644 index 00000000..be6ca906 --- /dev/null +++ b/specifications/tcp/tcp.tla @@ -0,0 +1,330 @@ +------------------------------- MODULE tcp ---------------------------------- +(* +https://datatracker.ietf.org/doc/html/rfc9293 + +This spec abstracts from many details such as sequence numbers in RFC9293 and +focuses on the state transitions of the TCP finite state machine shown in the +diagram at the end of this file. +*) +EXTENDS Integers, Sequences, SequencesExt, FiniteSets + +CONSTANT + Peers + +ASSUME Cardinality(Peers) = 2 + +States == {"LISTEN", "CLOSED", "SYN-SENT", "SYN-RECEIVED", "ESTABLISHED", + "FIN-WAIT-1", "FIN-WAIT-2", "CLOSING", "CLOSE-WAIT", "LAST-ACK", + "TIME-WAIT"} + +VARIABLE + tcb, + connstate, + network + +vars == <> + +TypeOK == + /\ tcb \in [ Peers -> BOOLEAN ] + /\ connstate \in [ Peers -> States ] + /\ network \in [ Peers -> Seq({"SYN", "SYN,ACK", "ACK", "RST", "FIN"} \cup {"ACKofFIN"}) ] + +Init == + /\ tcb = [p \in Peers |-> FALSE] + /\ connstate = [p \in Peers |-> "CLOSED"] + /\ network = [p \in Peers |-> <<>>] + +\* Action triggered by user commands: + +PASSIVE_OPEN(local, remote) == + \* User command: PASSIVE-OPEN + /\ local # remote + /\ connstate[local] = "CLOSED" + /\ UNCHANGED network + /\ connstate' = [connstate EXCEPT ![local] = "LISTEN"] + /\ tcb' = [tcb EXCEPT ![local] = TRUE] + +ACTIVE_OPEN(local, remote) == + \* User command: ACTIVE-OPEN + /\ local # remote + /\ connstate[local] = "CLOSED" + /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN")] + /\ connstate' = [connstate EXCEPT ![local] = "SYN-SENT"] + /\ tcb' = [tcb EXCEPT ![local] = TRUE] + +CLOSE_SYN_SENT(local, remote) == + \* User command: CLOSE + /\ local # remote + /\ connstate[local] = "SYN-SENT" + /\ UNCHANGED network + /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"] + /\ tcb' = [tcb EXCEPT ![local] = FALSE] + +CLOSE_SYN_RECEIVED(local, remote) == + \* User Command: CLOSE + /\ local # remote + /\ connstate[local] = "SYN-RECEIVED" + /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")] + /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-1"] + /\ UNCHANGED tcb + +SEND(local, remote) == + \* User command: SEND + /\ local # remote + /\ connstate[local] = "LISTEN" + /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN")] + /\ connstate' = [connstate EXCEPT ![local] = "SYN-SENT"] + /\ UNCHANGED tcb + +CLOSE_LISTEN(local, remote) == + \* User command: CLOSE + /\ local # remote + /\ connstate[local] = "LISTEN" + /\ UNCHANGED network + /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"] + /\ tcb' = [tcb EXCEPT ![local] = FALSE] + +CLOSE_ESTABLISHED(local, remote) == + \* User command: CLOSE + /\ local # remote + /\ connstate[local] = "ESTABLISHED" + /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")] + /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-1"] + /\ UNCHANGED tcb + +CLOSE_CLOSE_WAIT(local, remote) == + \* User command: CLOSE + /\ local # remote + /\ connstate[local] = "CLOSE-WAIT" + /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")] + /\ connstate' = [connstate EXCEPT ![local] = "LAST-ACK"] + /\ UNCHANGED tcb + +User == + \E local, remote \in Peers : + \/ ACTIVE_OPEN(local, remote) + \/ PASSIVE_OPEN(local, remote) + \/ CLOSE_SYN_SENT(local, remote) + \/ CLOSE_SYN_RECEIVED(local, remote) + \/ CLOSE_LISTEN(local, remote) + \/ CLOSE_ESTABLISHED(local, remote) + \/ CLOSE_CLOSE_WAIT(local, remote) + \/ SEND(local, remote) + +----------------------------------------------------------------------------- + +SynSent(local, remote) == + /\ local # remote + /\ connstate[local] = "SYN-SENT" + /\ UNCHANGED tcb + /\ \/ /\ IsPrefix(<<"SYN">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN,ACK"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "SYN-RECEIVED"] + \/ /\ IsPrefix(<<"SYN,ACK">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "ACK"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "ESTABLISHED"] + +SynReceived(local, remote) == + /\ local # remote + /\ connstate[local] = "SYN-RECEIVED" + /\ UNCHANGED tcb + /\ \/ /\ IsPrefix(<<"RST">>, network[local]) \* TODO: note 1 in RFC 9293 (must have gotten here from a *passive* OPEN, i.e., LISTEN) + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "LISTEN"] + \/ /\ IsPrefix(<<"ACK">>, network[local]) \* TODO: ACK of SYN + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "ESTABLISHED"] + +Listen(local, remote) == + /\ local # remote + /\ connstate[local] = "LISTEN" + /\ UNCHANGED tcb + /\ \/ /\ IsPrefix(<<"SYN">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN,ACK"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "SYN-RECEIVED"] + +Established(local, remote) == + /\ local # remote + /\ connstate[local] = "ESTABLISHED" + /\ UNCHANGED tcb + /\ IsPrefix(<<"FIN">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "CLOSE-WAIT"] + +----------------------------------------------------------------------------- + +FinWait1(local, remote) == + /\ local # remote + /\ connstate[local] = "FIN-WAIT-1" + /\ UNCHANGED tcb + /\ \/ /\ IsPrefix(<<"FIN">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "CLOSING"] + \/ /\ IsPrefix(<<"ACKofFIN">>, network[local]) + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-2"] + +FinWait2(local, remote) == + /\ local # remote + /\ connstate[local] = "FIN-WAIT-2" + /\ UNCHANGED tcb + /\ IsPrefix(<<"FIN">>, network[local]) + /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"), + ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"] + +Closing(local, remote) == + /\ local # remote + /\ connstate[local] = "CLOSING" + /\ UNCHANGED tcb + /\ IsPrefix(<<"ACKofFIN">>, network[local]) + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"] + +LastAck(local, remote) == + /\ local # remote + /\ connstate[local] = "LAST-ACK" + /\ UNCHANGED tcb + /\ IsPrefix(<<"ACKofFIN">>, network[local]) + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"] + +TimeWait(local, remote) == + /\ local # remote + /\ connstate[local] = "TIME-WAIT" + /\ tcb[local] + /\ UNCHANGED network + /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"] + /\ tcb' = [tcb EXCEPT ![local] = FALSE] + \* TODO: Timeout=2MSL + +Note2(local, remote) == + (* Note 2: A transition from FIN-WAIT-1 to TIME-WAIT if a FIN is received + and the local FIN is also acknowledged. *) + /\ local # remote + /\ connstate[local] = "FIN-WAIT-1" + /\ UNCHANGED tcb + \* The local FIN is also acknowledged, i.e., skipping the CLOSING state. + /\ IsPrefix(<< "FIN", "ACKofFIN" >>, network[local]) + \* ??? The RFC doesn't explictly mention this, but we send the ACKofFIN here. + /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"), + ![local] = SubSeq(network[local], 3, Len(network[local]))] + /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"] + +System == + \E local, remote \in Peers : + \/ SynSent(local, remote) + \/ SynReceived(local, remote) + \/ Listen(local, remote) + \/ Established(local, remote) + \/ FinWait1(local, remote) + \/ FinWait2(local, remote) + \/ Closing(local, remote) + \/ LastAck(local, remote) + \/ TimeWait(local, remote) + \/ Note2(local, remote) + +Note3(local, remote) == + (* Note 3: A RST can be sent from any state with a corresponding transition + to TIME-WAIT (see [70] for rationale). Similarly, receipt of a RST from + any state results in a transition to LISTEN or CLOSED. *) + \* ??? "...can be sent from any state with a corresponding transition to TIME-WAIT" + \* ??? could also be interpreted as those states from where we can tranisiton to TIME-WAIT, + \* ??? i.e., FIN-WAIT-1, FIN-WAIT-2, CLOSING. + /\ local # remote + /\ UNCHANGED tcb + /\ \/ /\ tcb[local] \* ??? RFC 9293 doesn't mention this, but it seems impossible to send a RST without a TCB. + /\ network' = [ network EXCEPT ![remote] = Append(@, "RST")] + /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"] + \/ /\ IsPrefix(<<"RST">>, network[local]) + /\ network' = [ network EXCEPT ![local] = Tail(network[local])] + /\ \/ connstate' = [connstate EXCEPT ![local] = "LISTEN"] + \/ connstate' = [connstate EXCEPT ![local] = "CLOSED"] + +Reset == + \E local, remote \in Peers : + Note3(local, remote) + +Next == + \/ System + \/ Reset + \/ User + +Spec == + /\ Init + /\ [][Next]_vars + /\ WF_vars(System) + \* Would get stuck in SYN-SENT if we don't assert a user command. + /\ WF_vars(\E local, remote \in Peers: CLOSE_SYN_SENT(local, remote)) + +----------------------------------------------------------------------------- + +Inv == + \* If there are no messages in flight and one node is in the ESTABLISHED + \* state, then the other node is also in the ESTABLISHED state. When + \* message are in flight, the state of the nodes can be different. + \A local, remote \in { p \in Peers : network[p] = <<>> } : + connstate[local] = "ESTABLISHED" <=> connstate[remote] = "ESTABLISHED" + +Prop == + \A p \in Peers : + connstate[p] = "SYN-SENT" ~> connstate[p] \in {"ESTABLISHED", "LISTEN", "CLOSED"} + +============================================================================= +\* Modification History +\* Created Tue Apr 02 10:38:50 PDT 2024 by markus + + + +From RFC 9293: + + +---------+ ---------\ active OPEN + | CLOSED | \ ----------- + +---------+<---------\ \ create TCB + | ^ \ \ snd SYN + passive OPEN | | CLOSE \ \ + ------------ | | ---------- \ \ + create TCB | | delete TCB \ \ + V | \ \ + rcv RST (note 1) +---------+ CLOSE | \ + -------------------->| LISTEN | ---------- | | + / +---------+ delete TCB | | + / rcv SYN | | SEND | | + / ----------- | | ------- | V ++--------+ snd SYN,ACK / \ snd SYN +--------+ +| |<----------------- ------------------>| | +| SYN | rcv SYN | SYN | +| RCVD |<-----------------------------------------------| SENT | +| | snd SYN,ACK | | +| |------------------ -------------------| | ++--------+ rcv ACK of SYN \ / rcv SYN,ACK +--------+ + | -------------- | | ----------- + | x | | snd ACK + | V V + | CLOSE +---------+ + | ------- | ESTAB | + | snd FIN +---------+ + | CLOSE | | rcv FIN + V ------- | | ------- ++---------+ snd FIN / \ snd ACK +---------+ +| FIN |<---------------- ------------------>| CLOSE | +| WAIT-1 |------------------ | WAIT | ++---------+ rcv FIN \ +---------+ + | rcv ACK of FIN ------- | CLOSE | + | -------------- snd ACK | ------- | + V x V snd FIN V ++---------+ +---------+ +---------+ +|FINWAIT-2| | CLOSING | | LAST-ACK| ++---------+ +---------+ +---------+ + | rcv ACK of FIN | rcv ACK of FIN | + | rcv FIN -------------- | Timeout=2MSL -------------- | + | ------- x V ------------ x V + \ snd ACK +---------+delete TCB +---------+ + -------------------->|TIME-WAIT|------------------->| CLOSED | + +---------+ +---------+ +