TCP.3d

/*


  Specifying the format of TCP headers, from RFC 793, augmented to
  support more recent TCP option kinds and TCP flags.


    0                   1                   2                   3
    0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |          Source Port          |       Destination Port        |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                        Sequence Number                        |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                    Acknowledgment Number                      |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |  Data |     |N|C|E|U|A|P|R|S|F|                               |
   | Offset| Rese|S|W|C|R|C|S|S|Y|I|            Window             |
   |       | rved| |R|E|G|K|H|T|N|N|                               |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |           Checksum            |         Urgent Pointer        |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                    Options                    |    Padding    |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                             data                              |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+

  Parsing variable length data is hard and TCP option parsing is no
  exception.

  Even in code that's been in the Linux TCP/IP stack for 20 years or
  more, memory safety bugs have been found and patched, as recently as
  in 2019. See:

  https://github.com/torvalds/linux/commit/9609dad263f8bea347f41fddca29353dbf8a7d37

  This file contains a 3D specification of the TCP headers.
  The main interesting bit is the specification of variable length TCP options in the header,
    and reading them into a parse tree of the programmer's choosing.
  Below we parse the options into a struct similar to the one used in the Linux kernel

*/

typedef UINT16BE PORT;
typedef UINT32BE SEQ_NUMBER;
typedef UINT32BE ACK_NUMBER;
typedef UINT16BE WINDOW;
typedef UINT16BE CHECK_SUM;
typedef UINT16BE URGENT_PTR;

#define OPTION_KIND_END_OF_OPTION_LIST 0x00
#define OPTION_KIND_NO_OPERATION 0x01
#define OPTION_KIND_MAX_SEG_SIZE 0x02
#define OPTION_KIND_WINDOW_SCALE 0x03
#define OPTION_KIND_SACK_PERMITTED 0x04
#define OPTION_KIND_SACK 0x05
#define OPTION_KIND_TIMESTAMP 0x08

#define TCP_MAX_WSCALE        14
#define TCP_SACK_SEEN         1

//
// We parse TCP options into the following struct,
//   similar to the one defined in the TCP/IP implementation in the Linux kernel
//   see struct tcp_options_received in include/linux/tcp.h in the Linux kernel code
//

output
typedef struct _TCP_OPTIONS_RECEIVED
{
  UINT32        TS_RECENT_STAMP;
  UINT32        TS_RECENT;
  UINT32        RCV_TSVAL;
  UINT32        RCV_TSECR;
  UINT16        SAW_TSTAMP  : 1;
  UINT16        TSTAMP_OK   : 1;
  UINT16        DSACK       : 1;
  UINT16        WSCALE_OK   : 1;
  UINT16        SACK_OK     : 3;
  UINT16        SMC_OK      : 1;
  UINT16        SND_WSCALE  : 4;
  UINT16        RCV_WSCALE  : 4;
  UINT8         SAW_UNKNOWN : 1;
  UINT8         UNUSED      : 7;
  UINT8         NUM_SACKS;
  UINT16        USER_MSS;
  UINT16        MSS_CLAMP;
} TCP_OPTIONS_RECEIVED;

typedef struct _WINDOW_SCALE_PAYLOAD(Bool WindowScaleAllowed,
                                     mutable TCP_OPTIONS_RECEIVED *OptRx)
where WindowScaleAllowed
{
  UINT8 Length
  {
    Length == 3
  };
  UINT8 WindowScale
  {:act
    OptRx->WSCALE_OK = 1;
    if((WindowScale <= TCP_MAX_WSCALE)){
      OptRx->SND_WSCALE = WindowScale;
    } else {
      OptRx->SND_WSCALE = TCP_MAX_WSCALE;
    }};
} WINDOW_SCALE_PAYLOAD;

typedef struct _MAX_SEG_SIZE_PAYLOAD(Bool MaxSegSizeAllowed,
                                     mutable TCP_OPTIONS_RECEIVED *OptRx)
where MaxSegSizeAllowed
{
  UINT8 Length
  {
    Length == 4
  };
  UINT16BE MaxSegSize
  {:act
    OptRx->MSS_CLAMP = MaxSegSize;
  };
} MAX_SEG_SIZE_PAYLOAD;

typedef struct _TIMESTAMP_PAYLOAD(Bool TimeStampAllowed,
                                  mutable TCP_OPTIONS_RECEIVED *OptRx)
where TimeStampAllowed
{
  UINT8        Length
  {
    Length == 10
  };
  UINT32BE     Tsval;
  UINT32BE     Tsecr
  {:act
    OptRx->SAW_TSTAMP = 1;
    OptRx->RCV_TSVAL = Tsval;
    OptRx->RCV_TSECR = Tsecr;
  };
} TIMESTAMP_PAYLOAD;

typedef struct _SackPerm_PAYLOAD(Bool SackPermAllowed,
                                 mutable TCP_OPTIONS_RECEIVED *OptRx)
where SackPermAllowed
{
  UINT8        Length
  {
    Length == 2
  };
  unit         Noop
  {:act
    OptRx->SACK_OK = TCP_SACK_SEEN;
    OptRx->DSACK = 0;
    OptRx->NUM_SACKS = 0;};
} SackPermPayload;

typedef struct _SELECTIVE_ACK_PAYLOAD(mutable PUINT8 *SackPayload)
{
  UINT8 Length
  {
    Length == 10 ||
    Length == 18 ||
    Length == 26 ||
    Length == 34
  };
  UINT8 SelectiveAck[:byte-size (Length - 2)]
  {:act
    var x = field_ptr;
    *SackPayload = x;};
} SELECTIVE_ACK_PAYLOAD;

casetype _OPTION_PAYLOAD(UINT8 OptionKind,
                         Bool WindowScaleAllowed,
                         Bool MaxSegSizeAllowed,
                         Bool TimeStampAllowed,
                         Bool SackPermAllowed,
                         mutable PUINT8 *SackPayload,
                         mutable TCP_OPTIONS_RECEIVED *OptRx)
{
  switch(OptionKind)
  {
     case OPTION_KIND_END_OF_OPTION_LIST:
       all_zeros EndOfList;
       
     case OPTION_KIND_NO_OPERATION:
       unit Noop;

     case OPTION_KIND_MAX_SEG_SIZE:
       MAX_SEG_SIZE_PAYLOAD(MaxSegSizeAllowed, OptRx) MaxSegSizePayload;

     case OPTION_KIND_WINDOW_SCALE:
       WINDOW_SCALE_PAYLOAD(WindowScaleAllowed, OptRx) WindowScalePayload;

     case OPTION_KIND_SACK_PERMITTED:
       SackPermPayload(SackPermAllowed, OptRx) SackPermittedPayload;

     case OPTION_KIND_SACK:
       SELECTIVE_ACK_PAYLOAD(SackPayload) SelectiveAckPayload;

     case OPTION_KIND_TIMESTAMP:
       TIMESTAMP_PAYLOAD(TimeStampAllowed, OptRx) TimestampPayload;
  } 
} OPTION_PAYLOAD;

typedef struct _OPTION(Bool WindowScaleAllowed,
                       Bool MaxSegSizeAllowed,
                       Bool TimeStampAllowed,
                       Bool SackPermAllowed,
                       mutable PUINT8 *SackPayload,
                       mutable TCP_OPTIONS_RECEIVED *OptRx)

{
   UINT8 OptionKind;
   OPTION_PAYLOAD(OptionKind,
                  WindowScaleAllowed,
                  MaxSegSizeAllowed,
                  TimeStampAllowed,
                  SackPermAllowed,
                  SackPayload,
                  OptRx)                  OptionPayload;
} OPTION;

/*++
  The top-level type of a TCP Header

  Arguments:

  * UINT32 SegmentLength, the size of the packet,
    including both header and data, passed in by the caller
  * Estab, a boolean that determines whether certain options are expected in the header
      We replicate the logic used in the Linux kernel
  * SackPayload, an out pointer to return the SACK option payload to the caller
  * OptRx, struct to parse the TCP options into
  --*/
entrypoint
typedef struct _TCP_HEADER(UINT32 SegmentLength,
                           Bool Estab,
                           mutable PUINT8 *SackPayload,
                           mutable TCP_OPTIONS_RECEIVED *OptRx)
{
  PORT            SourcePort;
  PORT            DestinationPort;
  SEQ_NUMBER      SeqNumber;
  ACK_NUMBER      AckNumber;
  UINT16BE        DataOffset:4
  { //DataOffset is in units of 32 bit words
    sizeof(this) == 20 && //Sanity check: static size in bytes of this type, excluding the variable length elements, is 20
    sizeof(this) <= DataOffset * 4 && //DataOffset points after the static fields
    DataOffset * 4 <= SegmentLength
  };
  UINT16BE        Reserved:3
  {
    Reserved == 0 //Reserved bytes are unused
  };
  UINT16BE        NS:1;
  UINT16BE        CWR:1;
  UINT16BE        ECE:1;
  UINT16BE        URG:1;
  UINT16BE        ACK:1
  {
      AckNumber == 0 ||
      ACK == 1 //AckNumber can only be set if the ACK flag is set
  } ;
  UINT16BE        PSH:1;
  UINT16BE        RST:1;
  UINT16BE        SYN:1;
  UINT16BE        FIN:1;
  WINDOW          Window;
  CHECK_SUM       CheckSum;
  URGENT_PTR      UrgentPointer
  {
      UrgentPointer == 0 ||
      URG == 1 //UrgentPointer can only be set if the URG flag is set
  };
  //The SYN=1 condition indicates when MAX_SEG_SIZE option can be received
  //This is an array of options consuming
  OPTION(SYN==1,
         Estab,
         Estab,
         SYN==1&&(!Estab),
         SackPayload,
         OptRx)        Options[:byte-size (DataOffset * 4) - sizeof(this)];
  UINT8                Data[SegmentLength - (DataOffset * 4)];
} TCP_HEADER;