[Math] Finite State Machines (FSMs) for programmers and mere mortals

Finite State Machine (FSM) may be a scary term, but everyone seen it at least in RFCs.

This is a FSM of TCP/IP client/server from RFC 793 (year 1981, how old-school?!), page 22:

                              +---------+ ---------\      active OPEN
|  CLOSED |            \    -----------
+---------+<---------\   \   create TCB
|     ^              \   \  snd SYN
passive OPEN |     |   CLOSE        \   \
------------ |     | ----------       \   \
create TCB  |     | delete TCB         \   \
V     |                      \   \
+---------+            CLOSE    |    \
|  LISTEN |          ---------- |     |
+---------+          delete TCB |     |
rcv SYN      |     |     SEND              |     |
-----------   |     |    -------            |     V
+---------+      snd SYN,ACK  /       \   snd SYN          +---------+
|         |<-----------------           ------------------>|         |
|   SYN   |                    rcv SYN                     |   SYN   |
|   RCVD  |<-----------------------------------------------|   SENT  |
|         |                    snd 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  |
+---------+                   +---------+


Fancier version from Wikipedia:

It's rather called 'TCP Connection State Diagram' in RFC, but to implement TCP/IP stack, you actually need to implement FSM.

See also DHCP client state diagram. Both DHCP client and server must implement FSM for handling all these states and transitions.

FSMs are hard to test and debug. Probably this is why all sorts of protocols shifts towards stateless protocols, like HTTP. They are simpler to work with. (But SSH and TLS has couple of states.)

One infamous case is old-school FTP client/server with highly-complicated state diagrams. FTP servers were prone to bugs and grave vulnerabilities also because of this.

Model checking can be used to debug FSMs.

Also, vulnerabilities/zero days hunters should pay attention to FSMs exactly because of this: FSMs are often poorly tested/debugged. There may be bugs.