2 ms·
All the deliverables are accessible here [1], and from the most relevant one (D5.4) the short story seems to be: - The core library's memory safety was verifie
by pbsd 12y ago
All the deliverables are accessible here [1], and from the most relevant one (D5.4) the short story seems to be:
- The core library's memory safety was verified using VCC;
- A Frama-C plugin was used to verify (a limited form of) side-channel resistance.
Correctness verification seems to have been done by reimplementing NaCl in CAO, a language made during CACE for this purpose. It is not a 1:1 match to C, from what I can tell, so this does not imply correctness of the C code.
However, none of this is verifiable at all. The NaCl code has no VCC or Frama-C annotations, or associated CAO; there is absolutely no mention of this in the NaCl page. So we are forced to take the authors of that report at their word, if we want to believe them at all.
[1] https://www.cspforum.eu/documents-reports/description/cace https://www.cspforum.eu/documents-reports/description/cace
- pascal_cuoq 12y agoI 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...