[noise] Noise Explorer: Generate Software Implementations

[Nadim Kobeissi]

Dear Trevor,

> Could we take this all the way to a simple templating system?

Yes, and I plan to do this for Go and ProVerif before I start working on
WASM, Rust and F*. That way I'll get rid of the remaining technical debt
(which, again, isn't a lot.)

> For example, given the following files:

Yes, I indeed understand your templating example that that's very much what
I have in mind.

> I know you want Noise Explorer to track the official revisions to
> spec.  But it would be very useful to get unofficial proposals
> analyzed (like ss/noss and sig, at the moment).  Is there a way we
> could put these in an "experimental" part of Noise Explorer to
> emphasize they're not to be used, but just for helping our design
> process?

Let me explain a conflict which is currently appearing. Currently, I have
the following tasks, which I want to finish before doing *anything* else
that is Noise Explorer-related:

1. Make sure Go implementations pass Cacophony's test vectors. As of right
now, only 55 out of the 61 Noise Handshake Patterns in the Noise Explorer
compendium do so, so we're still working on this.
2. Improve the performance and cleanliness of the Go code (in particular,
Jason has sent in some very useful and appreciated feedback which I've been
working on integrating. Thanks again, Jason.)
3. Documenting generated Go implementations.
4. Making it such that detailed message pages such as this one show
generated Go code for every message as well as ProVerif code:
https://noiseexplorer.com/patterns/IN/B.html
5. This is unrelated to the rest of the items in this list but still in
progress: finally finish formally verifying IKpsk2. This is long overdue
and I want to get it out of the way.
6. Then, finally, moving towards a 100% template-based system.

After all of the above is finished (which shouldn't take along at all, it's
all already very much underway), I will find myself at a crossroads:
- Either focus on integrating Rust and F*.
- Or, focus on formally verifying "experimental" Noise Protocol Framework
features that do not constitute part of the core spec.

Of course, the third option is to work on Rust/F* and experimental features
at the same time, but expanding Noise Explorer in both directions
simultaneously really feels like it will be a strange juggling feat that I
am not sure is wise to undertake. What do you think, Trevor?

Now, there is a small but serious chance that Noise Explorer might receive
a small grant that would allow me to take in graduate students to help with
Rust and F* code generation. If that happens, then surely we can expect
more of Noise Explorer in a smaller time frame.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Thu, Jan 24, 2019 at 11:12 AM Trevor Perrin <trevp at trevp.net> wrote:

> On Wed, Jan 16, 2019 at 8:48 PM Nadim Kobeissi <nadim at symbolic.software>
> wrote:
> >
> > Q3: Can I help integrate my own language?
> > A3: You should be able to but you'll need to do some tinkering. Noise
> Explorer does indeed use a modular, template-based framework, but despite
> my attempts to clean it up as much as possible it's still fairly
> opinionated and sometimes arbitrary. You can try, and you will likely
> succeed, but you will need to decipher the templates yourself. Happily,
> it's not very hard to do so.
>
> Cool,
>
> There's a lot of "templatized" similarity in the output for different
> patterns.
>
> Could we take this all the way to a simple templating system?
>
> For example, given the following files:
>
> <file>.file_start.txt
> <file>.message_start.txt
> <file>.token_ss.txt
> <file>.token_se.txt
> <file>.token_es.txt
> <file>.token_ee.txt
> <file>.message_end.txt
> <file.file_end.txt
>
> A simple templating tool could concatenate them into a single <file>
> in this order:
>   file_start
>   for MESSAGENUM=0..TOTALMESSAGES:
>     message_start
>     for TOKEN in pattern:
>       token_<TOKEN>
>     message_end
>   file_end
>
> It would also do string replacement within each file, substituting
> {{CIPHER}} with AES256, {{PATTERN}} with XX etc, and substituting
> {{MESSAGENUM}} with an integer.
>
> The hope is this would be sufficient to define some helper functions,
> then define some readMessageX/writeMessageX functions whose bodies are
> just unrolled sequences of MixKey / MixHash as defined by the tokens.
> By being really simple it would entice people to add new languages.
>
> It might be a good exercise to try to regenerate your files in such a
> simple way.  And/or take existing Noise libraries and try to generate
> templatized/unrolled versions of them, to see where this breaks down.
>
>
> > Q7: Any other future plans for Noise Explorer?
> > A7: No. The only things I have on my plate are what was listed above:
> >     - WASM, Rust and F* support.
> >     - More comprehensive automated test suites for generated
> implementations.
> >     - Cipher suite support.
> >     - Keep everything up to spec with upcoming official revisions to the
> Noise Protocol Framework.
>
> I know you want Noise Explorer to track the official revisions to
> spec.  But it would be very useful to get unofficial proposals
> analyzed (like ss/noss and sig, at the moment).  Is there a way we
> could put these in an "experimental" part of Noise Explorer to
> emphasize they're not to be used, but just for helping our design
> process?
>
> Trevor
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20190124/4bfec2c6/attachment.html>