I reviewed the optional checks which are enabled by mypy --strict. The following checks seem to be useful:

warn_unused_configs = True
disallow_any_generics = True
disallow_subclassing_any = True
disallow_untyped_calls = True
disallow_incomplete_defs = True
check_untyped_defs = True

The following options seem not that useful to me at the moment:

disallow_untyped_decorators = True
no_implicit_optional = True
warn_return_any = True
no_implicit_reexport = True

Cf. AdaCore/RecordFlux#194

Correctly verified message specifications are not sufficient, as such specification can still turn out to be invalid in practice (e.g., by misinterpreted descriptions in English prose). A test tool should be created which validates that specified messages are correctly parsed (and serialized). The tool should take a specification and a set of known valid and invalid messages as input and should check, if all messages are correctly classified as valid or invalid. The basis for the tool should be PyRFLX. There is already a very small number of test files available for Ethernet and IPv4 in tests.data.captured which could be used for the beginning. For a larger test HTTP/2 should be used (#3).

Tasks

• Create validation tool tools/validate_spec.py
  • Input: specification file, message identifier, directory for valid messages (optional), directory for invalid messages (optional))
  • Output: return value, list of failed validations (message identifier, test file, error message) on stdout, detailed output in JSON file (optional)
• Add existing test data from RecordFlux to test/data
• Extend test in tests/test_spec.py by call of validation tool (in a generic way, i.e. it should not be necessary to add invocations for new specifications or test data of the validation tool manually)

Adapt specifications to style enforced by style checker implemented in AdaCore/RecordFlux#799.

I tried parsing the tls_record.rflx example and get this result:

$ rflx generate ../tls_record.rflx
Parsing ../tls_record.rflx
../tls_record.rflx:13:21: parser: error: Expected {{"First" - "=>" - MathematicalExpression} | {"Length" - "=>" - MathematicalExpression}}

Using rflx v0.4.1, Python 3.7.3.

• Dependency RecordFlux develop/0.5
• Python dependencies?

IANA provides XML documents listing assigned numbers. Currently, we have a tool which generates a specification from the IANA Assigned Internet Protocol Numbers document. The tool could be made more generic and also used for other documents, e.g., TLS Parameters.

Naming of specification files

<registry xmlns="http://www.iana.org/assignments" id="bootp-dhcp-parameters"> -> Bootp_Dhcp_Parameters.rflx

The HTTP/2 specification contains a name conflict. The issue is found now due to the changes in AdaCore/RecordFlux#520. All identifiers are correctly considered as case-insensitive now.

http_2.rflx:215:10: model: error: name conflict for field "Data" in "HTTP_2::Frame"
http_2.rflx:6:7: model: info: conflicting enumeration literal

https://github.com/Componolit/RecordFlux-specifications/runs/1514712305?check_suite_focus=true

The test coverage of all Python code should be checked. Full test coverage should be enforced as in RecordFlux.

The validation tool (especially once we have coverage analysis) should become a subcommand of rflx.

Depends on AdaCore/RecordFlux#743.

Idea on how to provide values for the parameters:

Every test binary is augmented with a configuration file that contains a value for every parameter of the respective message. A YAML configuration file could look like this:

Param1_Name: 512
Param2_Name: 1024

Specifications which have a checksum attached, currently raise an exception (even on correct input data):

$ ./tools/validate_spec.py -s igmp.rflx -m IGMP::Message -v tests/data/igmp/valid/
Traceback (most recent call last):
  File "./tools/validate_spec.py", line 334, in <module>
    sys.exit(cli(sys.argv))
  File "./tools/validate_spec.py", line 82, in cli
    validation_main(args)
  File "./tools/validate_spec.py", line 135, in validation_main
    validation_result = validator.validate_message(msg)
  File "./tools/validate_spec.py", line 206, in validate_message
    parsed_message.bytestring == original_message.bytes
  File "/home/senier/.local/lib/python3.7/site-packages/rflx/pyrflx/typevalue.py", line 1046, in bytestring
    if not self._skip_verification and not self.valid_message:
  File "/home/senier/.local/lib/python3.7/site-packages/rflx/pyrflx/typevalue.py", line 1103, in valid_message
    for checksum in self._checksums.values()
  File "/home/senier/.local/lib/python3.7/site-packages/rflx/pyrflx/typevalue.py", line 1103, in <genexpr>
    for checksum in self._checksums.values()
  File "/home/senier/.local/lib/python3.7/site-packages/rflx/pyrflx/typevalue.py", line 981, in _calculate_checksum
    f"cannot calculate checksum for {checksum.field_name}: "
rflx.pyrflx.error.PyRFLXError: pyrflx: error: cannot calculate checksum for Checksum: no callable checksum function provided

We currently have no way to provide a checksum function to the validation tool.

The following needs to be done additionally as part of this ticket:

• Fix checksum in TCP specification (cf. #63).

https://www.beyondlogic.org/usbnutshell/usb5.shtml

When parsing a Server Hello message, the following error occurs:

E       AssertionError: unresolved field conditions in Server_Hello.Extensions_Length: Random /= [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#, 16#1D#, 16#8C#, 16#2#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#, 16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#7#, 16#9E#, 16#9#, 16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#], Random = [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#, 16#1D#, 16#8C#, 16#2#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#, 16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#7#, 16#9E#, 16#9#, 16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#]

Cf. AdaCore/RecordFlux#297

#18 seems to have introduced an error into the Ethernet frame specification. Since this change only Ethernet II frames can have VLAN tags, but not IEEE 802.3 frames (i.e. the current specification only allows a EtherType field after a VLAN tag, but not a Length field). I'm not aware that IEEE 802.1Q is restricted to Ethernet II.

https://tools.ietf.org/html/rfc826

Remove the PyRFLX API that is going to be removed in AdaCore/RecordFlux#783 from the validation tool (and if necessary other tools).

This field should allow other values than 0 .. 0. The server selects a method from the suggestions the client sent in Client Hello, so I would assume it should allow values 0 .. 2 ** 8 - 1. This is not explicitly stated in the RFC.

pyrflx: error: Error while parsing nested message TLS_Handshake::Server_Hello
pyrflx: error: cannot set value for field Legacy_Compression_Method
pyrflx: error: value 1 not in type range 0 .. 0

https://tools.ietf.org/html/rfc1035

#18 (comment)

Cf. AdaCore/RecordFlux#528

The tool should be able to extract all packets of a specified protocol layer from a PCAP file and write the byte representation of each packet into a separate file.

All Python code in this repository should be checked by the same tools/linters as in our other repositories. The necessary configs and CI jobs should be added.

https://tools.ietf.org/html/rfc675

There are 2 tests currently failing because RecordFlux is now printing model: warning: model verification skipped when the model verification is disabled. The expected test output does not match that.

• Gather valid real-world messages of HTTP/2
• Derive set of invalid messages (by manual invalidation)
• Add test data to test/data

Resources

RFC7540
Tools for debugging, testing and using HTTP/2

• Base spec: https://tools.ietf.org/html/rfc8200
• Protocol parameters: https://www.iana.org/assignments/ipv6-parameters/ipv6-parameters.xhtml

It would be helpful to determine the test coverage of the message specifications. The validation tool (#7) would need to analyze how many paths of the message graph are covered by the existing test data.

Implementation Plan

MessageValue

• Add attribute (property) covered_links: List[Link]
• Add _next_link(field_name) -> Link method which returns the next valid link
• Call next_link inside next_field and store the last returned link in covered_links
• Add get_sdu_messages -> List[MessageValue] which returns the list of all messages contained in all fields of type OpaqueValue and ArrayValue
• Add tests

Validation Tool

• create dict to store the coverage of all involved messages (models) - total coverage
• method to update the total coverage on every iteration
• generate output
• tests

Output

Short Output:

------------------------------------------------------------------------------
                     RecordFlux Validation Coverage Report
Directory: .
------------------------------------------------------------------------------
File                                       Links    Used   Coverage  
------------------------------------------------------------------------------
ethernet.rflx                                100     100   100%
in_ethernet.rflx                              34      34   100%
ipv4.rflx                                    206      97    47%   
------------------------------------------------------------------------------
TOTAL                                        340     231    68%
------------------------------------------------------------------------------

Full Output:
<file_name>:<line>:<col>: error: missing link <link_source_field> -> <link_target_field>: <link_condition>

https://tools.ietf.org/html/rfc2608

See AdaCore/RecordFlux#738.

The style for enumeration types should be consistent (cf. AdaCore/RecordFlux#561).

The field value of TLS Client Hello: Legacy_Compression_Methods_Length is contraint to 1..1 but should allow values 1..2^8-1 (see RFC 5246).

This occured while parsing the sample tests/data/tls_handshake/handshake/valid/client_hello_0_header_removed.raw which is currently on the issue_10 branch.

pyrflx: error: Error while parsing nested message TLS_Handshake::Client_Hello
pyrflx: error: cannot set value for field Legacy_Compression_Methods_Length
pyrflx: error: value 2 not in type range 1 .. 1

When changing this in the specification and repeating the parsing test (with compression length = 2), the outgoing conditions of Legacy_Compression_Methods fail.

AssertionError: unresolved field conditions in Client_Hello.Legacy_Compression_Methods: 1255 / 8 /= 351 / 8, 1255 / 8 = 351 / 8`