3 ms·
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
by gtirloni 12y ago
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.
- Ixiaus 12y agoThey should use cryptol instead which was recently open sourced.
- gsnedders 12y agoAlgorithmic correctness is probably less interesting than the presence of side-channels nowadays, and that's far, far, far harder to model.
- xnull2guest 12y agoI 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.