[noise] Noise Explorer: Generate Software Implementations

[Nadim Kobeissi]

Hello everyone,
After some internal discussions, we've decided to limit Noise Explorer's
language support plans to:
- Go (already implemented. Generated code is optimized, fairly side-channel
resistant and passes all test vectors.)
- WASM (next on the list.)
- Rust (work on Rust started today.)
- F* (will be investigated soon.)

This means that Noise Explorer explicitly *will not support* any other
language. Attempting to expand it to support other languages is considered
unwelcome and counter-productive.

This decision has come after realizing that the more languages we support,
the more we will encounter a direct barrier to expanding Noise Explorer's
ability to account for, model, verify and generate implementations for
newer Noise Protocol Framework features such as signatures. So, this is
meant as a way to not over-commit to code generation but also allow the
entire Noise Explorer ecosystem to continue evolving along with the spec as
Trevor works on expanding it.

Trevor, I'll have an update for you soon w.r.t. formally verifying
signatures and such, as soon as I have a solid plan in place for how we
plan to support Go, WASM, Rust and F*.

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


On Sat, Jan 26, 2019 at 10:00 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20190130/281eb76b/attachment.html>