Checksum specification

[treiher]

Checksum fields should be verified and generated.

Protocols with messages containing checksum fields:

• Ethernet (Ethernet Componolit/systematization-binary-formats#31)
• IPv4 (IPv4 Componolit/systematization-binary-formats#22)
• ATM (ATM Componolit/systematization-binary-formats#30)
• NTP (NTP Componolit/systematization-binary-formats#37)
• ICMP (ICMP Componolit/systematization-binary-formats#36)
• Bluetooth Low Energy Link Layer (Bluetooth Low Energy Link Layer Componolit/systematization-binary-formats#39)
• TCP (TCP Componolit/systematization-binary-formats#25)
• UDP (UDP Componolit/systematization-binary-formats#24)

TCP and UDP use also values of the underlying protocol layer (IP header) for checksum generation.

[senier]

We need to think about the following aspects:

• Specification
  • How to express fields covered by checksum
    • Start/End field for checksum (Start => F1, End => F8, Exclude => (F3, F4))
      (+) Can cover multiple paths between Start and End
      (+) Simple to specify
      (-) "holes" cannot be supported directly
      (-) checksums where start/end exist on multiple paths cannot be expresses
    • List of covered fields (F1, F2, F5, F6, F7, F8)
      (+) Holes are supported
      (-) Will be lengthy for some formats
      (-) No inherent support for multiple paths
    • List of covered slices ((F1'First .. F2'Last), (F5'First .. F8'Last))
      (+) Holes are supported
    • Function with message-specific parameter list
      (+) Holes are supported
      (+) Non-checksum input (e.g. Key ID in NTP) can be passed
      (-) Will be lengthy for some formats
      (-) No inherent support for multiple paths
  • Irregularities
    • Assumed values for checksum calculation, e.g. checksum field set to 0 for calculation
    • Support for state (e.g. key database in NTP) for functions
    • Holes or rearranged fields (e.g. virtual headers in TCP and UDP)
  • Syntax for checksums
    • Field aspect

      type Message is
      message
         F1 : T;
         F2 : T;
         F3 : T;
         FCS : U32
            with Checksum => (Start => F1, End => F4, Exclude => (F3, FCS));
         F4 : T;
      end message;

    • Checksum function

      type Message is
      message
         F1 : T;
         F2 : T;
         F3 : T;
         FCS : U32
            then F4
               if FCS = Checksum (F1'First, F4'Last);
         F4 : T;
      end message;

    • Message aspect

      type Message is
      message
         F1 : T;
         F2 : T;
         F3 : T;
         FCS : U32;
         FCS2 : U32;
         F4 : T
            then null if FCS'Valid_Checksum and FCS2'Valid_Checksum;
      end message
          with Checksum => (FCS  => (F1'First, F4'Last),
                            FCS2 => (F2'First, F3'First));

    • Field aspect alternative

      type Message is
      message
         F1 : T;
         F2 : T;
         F3 : T;
         FCS : U32 is Checksum (FCS, F1'First, F4'Last);
         F4 : T
            then null if FCS'Valid_Checksum;
      end message;

• Parsing
  • Is checksum checked automatically once all required inputs have been processed?
• Generation
  • Is checksum generated automatically once all required inputs have been processed?
• Verification
  • How do we add preconditions to checksum function?
  • Do checksum functions need post-conditions
• SPARK
  • How are checksum functions provided to generated code
• Python
  • How are checksum functions provided

[treiher]

Just to summarize the result of our offline discussion:

• Specification
  • How to express fields covered by checksum
    • List of parameters: indices, field values
  • Irregularities
    • Assumed values for checksum calculation
      • not covered by specification; should be realized in checksum function
    • Support for state (e.g. key database in NTP)
      • can be passed as parameter, but functionality should be covered in separate issue
  • Syntax for checksums
    • Message aspect

      type Message is
         message
            F1 : T;
            F2 : T;
            F3 : T;
            FCS : U32;
            FCS2 : U32;
            F4 : T
               then null
                  if FCS'Valid_Checksum and FCS2'Valid_Checksum;
         end message
            with Checksum => (FCS  => (F1'First .. F2'Last, F4, F3'First .. F3'Last, F2),
                              FCS2 => (F2'First .. F3'First));

• Parsing
  • Is checksum checked automatically once all required inputs have been processed?
    • Checksum is only checked by explicit condition.
• Generation
  • Is checksum generated automatically once all required inputs have been processed?
    • SPARK: Checksum must be generated manually.
    • Python: Checksum is set automatically by _preset_fields method.
• Verification
  • How do we add preconditions to checksum function?
    • Lemma function, if needed.
  • Do checksum functions need post-conditions?
    • Lemma function, if needed.
• SPARK
  • How are checksum functions provided to generated code
    • Generic parameter
• Python
  • How are checksum functions provided
    • Callable as parameter of MessageValue