GaloisInc / daedalus

The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
66 stars 11 forks source link

Feature Request: Support parsing HTTP/1.1 request sequences #339

Open kenballus opened 1 year ago

kenballus commented 1 year ago

HTTP-1.1.ddl currently parses only the first request in its input, which means that we can't use it to parse pipelined requests. If there were a field in the Daedalus JSON output that reports how many bytes of input were consumed, then I could use the single request parser to implement request stream parsing.

kenballus commented 1 year ago

Update: I can see that requests containing unknown Transfer-Encodings have a "$remaining" field in their body objects that contains the remaining bytes after parsing. Implementing this whenever there are bytes left after parsing would also work for me.

Another solution would be to extend the grammar to support request sequences.

yav commented 1 year ago

@kenballus I am not sure how exactly you interface with HTTP-1.1.ddl, do you just run it with daedalus and you provide an entry parser? If so, the change should be pretty simple---here are a few options, perhaps you can try them out locally and I'd be happy to commit whichever you find useful:

A parser that would parse many requests one after the next (returns a sequence of requests):

def HTTP_requests = Many HTTP_request

A parser that returns the HTTP request, and also the offset after the last consumed byte:

def RequestWithOffset =                                                                       
  block                                                                          
    request = HTTP_request                                                       
    offset  = Offset

Parse a request, and also return the bytes after it:

def RequestWithBytes =
  block
     request = HTTP_request
     remaining = Many $any
kenballus commented 1 year ago

do you just run it with daedalus and you provide an entry parser?

We sure do!

I think option 2 is best, so good requests are parsed correctly even when followed by malformed requests.