<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 22, 2016 at 10:43 PM, Josh Adams <span dir="ltr"><<a target="_blank" href="mailto:josh.rubyist@gmail.com">josh.rubyist@gmail.com</a>></span> wrote:<br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">This all sounds amazing and like a thing I'd like to encourage the world to adopt.</blockquote></div><br></div><div class="gmail_extra">The world seems to agree. A recent news article touches on the subject[0], where Jeanette Wing (and probably her research group) are working on building a formal model of TLS.<br><br></div><div class="gmail_extra">There are a couple of viable avenues you can adopt. One of the more promising is to write down a formal specification from which you can derive test cases. But if constructed correctly, they can also be executed at the same time. Erlang isn't a nice vehicle for this since you are lack (Standard) ML style functors, but the ideas are certainly transferable.<br><br></div><div class="gmail_extra">Because you can also execute the model, you can use it as a driver in a QuickCheck test case and make sure that some other implementation is correct w.r.t to the executable specification.<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">The way to approach this kind of thing is to crawl before walking. Start out with a small ping-pong protocol which base64 encodes its queries and responses. Then show this correct and use that to build gradually more complex stuff. Most of the full quickcheck developments starts in a corner of the full system and then gradually extend themselves. Trying to attack a full system from day 1 is usually hard.<br><br></div><div class="gmail_extra">Also, you have to learn some tricks in order to handle standard protocol problems. By targeting toys with those problems it is often easier to figure out how to handle them, before trying to do it on the full system. Model building is fun, but it takes the same thought process as when you are trying to solve an abstract math problem: the answer will come to you why you are doing other stuff, muddling on the question.<br></div><div class="gmail_extra"><br>[0] <a href="https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/">https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/</a><br></div><div class="gmail_extra"><br clear="all"><br>-- <br><div class="gmail_signature">J.</div>
</div></div>