I must say, as a non-participant, I am slightly disappointed in how the deliverables of the CACE project were handled. Nevertheless, one thing that is “left” f

I must say, as a non-participant, I am slightly disappointed in how the deliverables of the CACE project were handled. Nevertheless, one thing that is “left” from the verification effort is hidden options -experimental-mem-deps and -experimental-path-deps for Frama-C. These are on the automatic side of Frama-C analyses: they require a value analysis to pass on the target code, but they do not require it to be precise. And it is fun to see input length and error conditions pop up as things the execution time depend on (and in the case of a typical AES implementation, the input buffer itself): http://blog.frama-c.com/index.php?post/2011/12/31/Do-not-use-AES-in-a-context-where-timing-attacks-are-possible http://blog.frama-c.com/index.php?post/2011/12/31/Do-not-use...