A reader's challenge
A couple of days ago, faithful reader David Gil sent in a challenge:
The reference code for Keccak/SHA-3 has a correctness bug in the Optimized64 implementation. Can the value analysis plugin find it?
Of course Value Analysis produces (many) warnings on the Keccak code, but I was unable to find settings that provided sufficient precision to recognize this bug as especially serious. (If you would like a hint, correctness depends on the color of your bird.)
The many warnings Value Analysis produced spurred me to substantially rewrite the Keccak Team's implementation. My version, with some ASCL annotations is in a very preliminary state. I am sure there are many bugs... There are some attempts at verification in the directory verification/frama-c
It is a great pleasure for me to discover that this blog has reached its independence. It has had more comments than posts for a little while, and now, with readers sending in their own posts, I might as well move to a start-up that, in collaboration with my previous employer CEA LIST, provides products and services based on Frama-C. I may even publish a blurb there from time to time when something newsworthy comes up.
My facetious colleague Virgile Prevosto will hopefully continue to provide insights on the more subtle aspects of ACSL's semantics here. I know I will read them.