Xen project Mailing List

Hi all,

I just developped Encore which, from combinators, make an `angstrom` decoder AND an encoder. By this way, we ensure isomorphism between them. You can see the project here: https://github.com/dinosaure/encore

I will integrate soon Encore to ocaml-git to ensure, again, isomorphism between Git object decoder and Git object encoder (and ensure, we don't miss something, we don't produce some noises and we produce exactly the same output from an input - and by this way, keep the same hash).

I need to improve the API and may be we need to optimize encoder but it's a good start to have a safe way to produce a decoder and an encoder automatically by a description of a format.

On Sun, Mar 18, 2018 at 12:39 PM Richard Mortier <richard.mortier@xxxxxxxxxxxx> wrote:

Came across this, might be of interest:

https://arxiv.org/abs/1803.04870
https://arxiv.org/pdf/1803.04870.pdf

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from
Binary Formats
Sorawit Suriyakarn, Clément Pit--Claudel, Benjamin Delaware, Adam Chlipala
(Submitted on 13 Mar 2018)
Every injective function has an inverse, although constructing the
inverse for a particular injective function can be quite tricky. One
common instance of inverse-function pairs is the binary encoders and
decoders used to convert in-memory data into and out of a structured
binary format for network communication. Ensuring that a given decoder
is a proper inverse of the original encoder is particularly important,
as any error has the potential to introduce security vulnerabilities or
to corrupt or lose data in translation.
In this paper, we present a synthesis framework, Narcissus, that
eliminates both the tedium and the potential for error in building the
inverse of a binary encoder. The starting point of the process is a
binary format, expressed as a functional program in the nondeterminism
monad, that precisely captures all the valid binary encodings of an
arbitrary datatype instance. From this specification, Narcissus
synthesizes a decoder that is guaranteed to be the inverse of this
relation, drawing on an extensible set of decoding strategies to
construct the implementation. Each decoder is furthermore guaranteed to
detect malformed encodings by failing on inputs not included in this
relation. The derivation is carried out inside the Coq proof assistant
and produces a proof trail certifying the correctness of the synthesized
decoder. We demonstrate the utility of our framework by deriving and
evaluating the performance of decoders for all packet formats used in a
standard network stack.

...and from the eval:

The decoders that our framework produces are reasonably
efficient and sufficiently full-featured to be used as a drop-in
replacements for all parsing components of a typical TCP/IP
stack. We support this claim by extracting our decoders
to OCaml and integrating the resulting code into the pureOCaml
TCP/IP stack of MirageOS.

--
Richard Mortier
richard.mortier@xxxxxxxxxxxx

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/mirageos-devel

Re: [MirageOS-devel] Deriving encoders/decoders