Re:GnuPG 2.1.2 released
by gtirloni on Thursday February 12, 2015 @06:42AM
(#9038387)
Is there any work being done to formally prove GnuPG' algorithms correctness? Just curious since there are other topic around Coq in the front page and I couldn't find much by searching.
[ Parent
| on HN ]
They should use cryptol instead which was recently open sourced.
Algorithmic correctness is probably less interesting than the presence of side-channels nowadays, and that's far, far, far harder to model.
Re:GnuPG 2.1.2 released
by xnull2guest on Friday February 13, 2015 @02:12AM
(#9043257)
I do know of one researcher working on this: Julian Bangert at MIT out of Dartmouth has modeled x86 family processors in SMT, and is able to prove that all paths through a particular piece of code compile so that all cache hits are identical, CPU ticks are identical, etc. Brilliant young man - I expect we'll be seeing a lot more from him.