Bit-precise encode/decode?

[nathaniel-bennett]

First off, I wanted to say that this is an amazing piece of work--well done! I've always thought there should be some kind of protocol description language for auto-generating parsers with better flexibility than protobuf/ASN.1 for existing protocols, and you all went ahead and made a formally-verified one!

I'm interested to find out if vest supports bit-precise fields, or whether adding such support would be straightforward or not. If I had a protocol that defined distinct fields chunked as a four bit, a two bit and two one-bit fields, would vest be able to enforce constraints on these fields or would it treat them as a single u8? As a more extreme example, if a protocol encoded seven-bit ASCII into a byte array with a variable-sized length field prepended to it, could I model this kind of constraint (or at least parse out the length field) with vest?

[y1ca1]

Hi, thanks for your interest!!

As stated in the last section (Future Work) of our latest USENIX Security paper, bit-precise formats would be interesting future work but currently unsupported by Vest.

We have ad-hoc, verified combinators for bit-precise formats (e.g., here and here), and from our limited experience, efficient implementations of those formats are far from easy to verify.

That being said, with the powerful bit vector solver that Verus (the Rust verifier we're using) provides and the library of lemmas on bit operations, extending Vest to support bit-precise formats (generally and robustly such that one can integrate them with arbitrary constraints (Refined) and dependencies (Pair)) is definitely possible (if not straightforward).

Finally, if you are interested, free feel to open a PR and I'd be happy to help with your questions and work together on this feature! A good starting point would be to look at how EverParse3D supports the Bitfields (though they only provide a validator for their formats).