<div dir="ltr"><div dir="ltr"><div dir="ltr">Hello everyone,<div>Just another quick update that we've integrated Noise Explorer's new automated test generation suite for Go implementations.</div><div><br></div><div>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:</div><div><a href="https://twitter.com/kaepora/status/1089265449097940992">https://twitter.com/kaepora/status/1089265449097940992</a></div><div><br></div><div>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 (<a href="https://hackage.haskell.org/package/cacophony">https://hackage.haskell.org/package/cacophony</a>).</div><div><br></div><div>I'd like to extend my sincere thanks to Georgio Nicholas (<a href="https://georgio.xyz">https://georgio.xyz</a>), 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!<br clear="all"><div><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><br></div><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div></div></div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 24, 2019 at 5:35 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">(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.)<br clear="all"><div><div dir="ltr" class="gmail-m_7994053289412737430gmail_signature"><div dir="ltr"><div><div dir="ltr"><br></div><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div></div></div><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail-m_7994053289412737430gmail_attr">On Thu, Jan 24, 2019 at 3:57 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr">Dear Trevor,<div><br></div><div>>

Could we take this all the way to a simple templating system?<br><div><div dir="ltr" class="gmail-m_7994053289412737430gmail-m_5432940710266678971gmail_signature"><div dir="ltr"><div dir="ltr"><br></div><div>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.)</div><div><br></div><div>> For example, given the following files:</div><div><br></div><div>Yes, I indeed understand your templating example that that's very much what I have in mind.</div><div><br></div><div>> I know you want Noise Explorer to track the official revisions to<br>> spec.  But it would be very useful to get unofficial proposals<br>> analyzed (like ss/noss and sig, at the moment).  Is there a way we<br>> could put these in an "experimental" part of Noise Explorer to<br>> emphasize they're not to be used, but just for helping our design<br>> process?  <br></div><div dir="ltr"><br></div><div>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:</div><div><br></div><div>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.</div><div>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.)</div><div>3. Documenting generated Go implementations.</div><div>4. Making it such that detailed message pages such as this one show generated Go code for every message as well as ProVerif code: <a href="https://noiseexplorer.com/patterns/IN/B.html" target="_blank">https://noiseexplorer.com/patterns/IN/B.html</a></div><div>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.  <br></div><div>6. Then, finally, moving towards a 100% template-based system.</div><div><br></div><div>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:</div><div>- Either focus on integrating Rust and F*.</div><div>- Or, focus on formally verifying "experimental" Noise Protocol Framework features that do not constitute part of the core spec.</div><div><br></div><div>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?</div><div><br></div><div>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.</div><div dir="ltr"><br></div><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div></div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail-m_7994053289412737430gmail-m_5432940710266678971gmail_attr">On Thu, Jan 24, 2019 at 11:12 AM Trevor Perrin <<a href="mailto:trevp@trevp.net" target="_blank">trevp@trevp.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Wed, Jan 16, 2019 at 8:48 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br>
><br>
> Q3: Can I help integrate my own language?<br>
> 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.<br>
<br>
Cool,<br>
<br>
There's a lot of "templatized" similarity in the output for different patterns.<br>
<br>
Could we take this all the way to a simple templating system?<br>
<br>
For example, given the following files:<br>
<br>
<file>.file_start.txt<br>
<file>.message_start.txt<br>
<file>.token_ss.txt<br>
<file>.token_se.txt<br>
<file>.token_es.txt<br>
<file>.token_ee.txt<br>
<file>.message_end.txt<br>
<file.file_end.txt<br>
<br>
A simple templating tool could concatenate them into a single <file><br>
in this order:<br>
  file_start<br>
  for MESSAGENUM=0..TOTALMESSAGES:<br>
    message_start<br>
    for TOKEN in pattern:<br>
      token_<TOKEN><br>
    message_end<br>
  file_end<br>
<br>
It would also do string replacement within each file, substituting<br>
{{CIPHER}} with AES256, {{PATTERN}} with XX etc, and substituting<br>
{{MESSAGENUM}} with an integer.<br>
<br>
The hope is this would be sufficient to define some helper functions,<br>
then define some readMessageX/writeMessageX functions whose bodies are<br>
just unrolled sequences of MixKey / MixHash as defined by the tokens.<br>
By being really simple it would entice people to add new languages.<br>
<br>
It might be a good exercise to try to regenerate your files in such a<br>
simple way.  And/or take existing Noise libraries and try to generate<br>
templatized/unrolled versions of them, to see where this breaks down.<br>
<br>
<br>
> Q7: Any other future plans for Noise Explorer?<br>
> A7: No. The only things I have on my plate are what was listed above:<br>
>     - WASM, Rust and F* support.<br>
>     - More comprehensive automated test suites for generated implementations.<br>
>     - Cipher suite support.<br>
>     - Keep everything up to spec with upcoming official revisions to the Noise Protocol Framework.<br>
<br>
I know you want Noise Explorer to track the official revisions to<br>
spec.  But it would be very useful to get unofficial proposals<br>
analyzed (like ss/noss and sig, at the moment).  Is there a way we<br>
could put these in an "experimental" part of Noise Explorer to<br>
emphasize they're not to be used, but just for helping our design<br>
process?<br>
<br>
Trevor<br>
</blockquote></div>
</blockquote></div>
</blockquote></div>