[Cryptech Tech] cryptol

[Joachim Strömbergson]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Aloha!

Randy Bush wrote:
> has anyone done work on validation of the toolchain?  how would we
> do so?

Not that I'm aware of. Cryptol is written in Haskell which might make it
harder to do a validation. At least I'm not very Haskellish.

What makes Cryptol interesting is that you can write a model and have
the tool perform a formal verification of it. That model could be used
as reference, comparison to another implementation (not generated by the
Cryptol). A formally verified second opinion, basically.

- -- 
Med vänlig hälsning, Yours

Joachim Strömbergson - Alltid i harmonisk svängning.
========================================================================
 Joachim Strömbergson          Secworks AB          joachim at secworks.se
========================================================================
-----BEGIN PGP SIGNATURE-----
Version: GnuPG/MacGPG2 v2.0.22 (Darwin)
Comment: GPGTools - http://gpgtools.org
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iQIcBAEBCAAGBQJTX19eAAoJEF3cfFQkIuyN5TkP/AkWxpfW4lftTO3DcWUcG38W
5uKwFiAr4U9zOmLaw1S6N1ASmH/4liJ38qv6nfZ/8F2EkqGthivYuIkBAYOO7jqH
yUu68fRKjvXw2LUEPR/eIAifPOcCf/oZzlHK0UFvTBFWRLuKkchgtDLNra3p3ym2
hUOGTMqcMkd3tOxwI3G5TvHuOFVUxZ6nIAcK30bIW9BOoaBTo5UnrufBmyIlbtMa
sytU/jx9MMtBnRPNlGA2q9b+4tgtO8ggXif9/GaFuUJ10Fu7c4S2c45qTw63aHYB
1m3c7c+Y4/L3GzZiUqAXDnDfXOUMxGu13v/7dzKtr8sff/G+bOKa5xCqj515Xo4A
JR36C9K9l4D3qHHjj/gcAwWAKDR1doqPU3z4uOgRNkSprwrW2yDKHql4bA8lC9Ww
Gxk4UB0sgyL+UnIcZDoHdJMKmuwFJpOHaSr1YgjDF1lS14yfyYNWOugEJjt7dj6l
KUMGCKk9NR3DMtdvxcGKsTUIynASuJJkzlAT0kKB871+/OwdgxtD3tIfA2O7f//k
ZVfLxW5CBTAI1bzAkeAXo5BCXR6ChwgAuJoW+j1HnCHapC4zocvyXTjIudql4uLl
0ACYCdzIPX7+B5RKTNN9njAoV0KRggzQ6ZQWucDqG91mmdV09T0MGjtD6QuRNhiW
FohYld0Y9EEmyW+8IqwE
=9kZ+
-----END PGP SIGNATURE-----