Protocol Specification - Network Performance Behaviour

[CMCDragonkai]

This issue tracks the purpose of Protocol Specification.

Found a couple links that relate to purpose 2. We might split this out into a separate issue to track:

• https://pdfs.semanticscholar.org/61f1/d88d7f40e08b0bb1137d0f9f4914c49feac2.pdf - Spicy Unified DPI Framework
• http://spw17.langsec.org/papers/tse-validating-session-protocols.pdf - A Framework for Validating Session Protocols
• http://www.scs.stanford.edu/16wi-cs240h/projects/duffy_denton.pdf - Embedded Haskell BPF
• https://github.com/iovisor/bcc/tree/master/examples/networking/http_filter - BCC/BPF Example of Filtering HTTP Packets
• https://medium.com/@cjoudrey/capturing-http-packets-the-hard-way-b9c799bfb6

The research group primarily interested in this purpose 2 appears to be http://langsec.org/

[CMCDragonkai]

Just in the middle of reading "A Framework for Validating Session Protocols". This paper describes a simple idea of using Haskell to create an embedded DSL for protocol parsing.

The paper focuses on parsing protocol messages for stateful protocols. Not the correctness of the individual packet, but whether the packet's message state is a valid message within the state of the protocol. That is certain packets are illegal within a particular state of the protocol.

To do this, they create types:

• ProtocolStatus - An enum of potential "status" for a given protocol
• HostInfo - Information about the host for the connection
• State - An arbitrary record containing the various mutable properties of the protocol. This could contain ProtocolStatus and various fields of HostInfo. This changes depending on what protocol you want to parse.
• Test - A tagged function (named) that tests the state and message and returns a boolean telling us whether this message is valid.
• Effect - A tagged effect taking 2 states and a message and returning the new state.
• Transition - A transition is a tuple of a list of Test and list of Effect.
• DFA - a DFA is a list of tuples containing status and a list of Transition.
• Message - The relevant properties of a protocol frame.

The main idea is that you can run a "session parser" defined in terms of the DFA on a sequence of messages for a given protocol. The end result is whether the sequence of messages is correct. You can also just do a "micro test" which tests a single message within a artificially constructed state.

The paper does not get to the part about of generating C code to be later embedded into the OS kernel. It is left to later. This part is probably what is most interesting to us. But we would most likely want to figure out how to compile to BPF and other userspace code.

The design of the session parser is then simple, because it doesn't actually try to parse the byte format of the message itself, it is assumed that it is already correct. This certainly means that if we can just embed Haskell code within the Architect language (which would mean Architect language is a superset of Haskell, or perhaps allows quasiquotation internal DSLs) we could apply this kind of parser.

I'm a bit confused about how this would interact with session types, since session types also have overlap with specifying the communication behaviour, whereas this is about verifying the communication behaviour at runtime.

[CMCDragonkai]

As our protocol spec has reached quite an interesting stage, I think it's a good idea to start prototyping how they would be interpreted as BPF monitoring code that verifies the protocol via network sampling @olligobber

[CMCDragonkai]

This work involves the Racket language combined with an embedded solver to produce interesting DSLs: http://emina.github.io/rosette/index.html

[CMCDragonkai]

This issue was moved to MatrixAI/Overwatch#13