[noise] Noise Explorer: Generate Software Implementations

[Nadim Kobeissi]

Hello everyone,
Just another quick update that we've integrated Noise Explorer's new
automated test generation suite for Go implementations.

I've posted a short 1-minute video that shows it in action, it's a short
viewing experience (and has fun music!) so I recommend you take a look:
https://twitter.com/kaepora/status/1089265449097940992

As you can see, the automatically generated Go code passes all of the test
vectors stipulated by Cacophony, the Haskell implementation of the Noise
Protocol Framework (https://hackage.haskell.org/package/cacophony).

I'd like to extend my sincere thanks to Georgio Nicholas (
https://georgio.xyz), a computer science student from the Lebanese American
University, who undertook a good deal of the effort with writing the
automated test generation suite. Georgio will also hopefully be helping out
with supporting more cipher suites (we're still stuck with only
25519_ChaChaPoly_Blake2s) and also will potentially help with Rust code
generation. Thank you, Georgio!

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


On Thu, Jan 24, 2019 at 5:35 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> (We are now passing Go test vectors for all 61/61 Noise Handshake
> Pattrerns in Noise Explorer -- the 6 that weren't passing turned out to be
> one-way handshake patterns that weren't operating in half-duplex mode.)
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Thu, Jan 24, 2019 at 3:57 PM Nadim Kobeissi <nadim at symbolic.software>
> wrote:
>
>> 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/20190126/ec1ea14e/attachment.html>