2 ms·
Can anyone comment on the use of formal verification in NaCl? Is it used at all? Would it even be valuable? [0] doesn't mention anything about it. [0] http://n
by ahelwer 12y ago
Can anyone comment on the use of formal verification in NaCl? Is it used at all? Would it even be valuable? [0] doesn't mention anything about it.
[0] http://nacl.cr.yp.to/valid.html http://nacl.cr.yp.to/valid.html
- bradleyjg 12y agoThere's a section in the tweetNaCl paper that discusses some limited formal verification. For some interesting commentary on the difficulty in formally verifying c code (with crypto examples) see: https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html and the followup https://www.imperialviolet.org/2014/09/11/moveprovers.html https://www.imperialviolet.org/2014/09/11/moveprovers.html