4 ms·

As well as being the author of the algorithms in NaCl, djb is also a specialist in secure software development, as tptacek mentioned. You can be reasonably sur

As well as being the author of the algorithms in NaCl, djb is also a specialist in secure software development, as tptacek mentioned. You can be reasonably sure that his code is bug free, but they went the extra step of proving the absence of certain types of bugs using static analysis tools. One of the project's deliverables mentioned they used Frama-C to prove the absence of integer overflows, for example. (I will update this comment when I find the specific report.) Other projects take the traditional approach of trusting that the code looks right until someone proves otherwise. Edit: The report was probably one of these, which I can't access anymore: http://www.cace-project.eu/downloads/deliverables-y1/CACE_D5.1_Security_Policies_for_Cryptographic_Software.pdf http://www.cace-project.eu/downloads/deliverables-y1/CACE_D5... http://www.cace-project.eu/downloads/deliverables-y1/CACE_M5.2_Machine-assisted_verficiation_and_certification_tool_specification.pdf http://www.cace-project.eu/downloads/deliverables-y1/CACE_M5... http://www.cace-project.eu/downloads/deliverables-y3/31_CACE_D5.3-V1.1.PDF http://www.cace-project.eu/downloads/deliverables-y3/31_CACE...

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 ago
  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...
higherpurpose 12y ago
Sounds like DJB's job could get much easier if he adopts Rusts once it's stable.
- tptacek 12y ago
  This is like a comment from a Markov generator.
  - stcredzero 12y ago
    How about an inversion of the Turing Test, where human contestants try to convince judges they are a Markov generator? Since it's difficult for people to generate randomness, this should be challenging enough to be interesting. (Not claiming it's intellectually interesting to participate in, however.)
    - tptacek 12y ago
      I can name a couple credible contestants from this site (obviously, if there was an Asshole Test, there'd be no question who'd win it from HN).
      - stcredzero 12y ago
        Would that me positively or negatively correlated with karma? ;)

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 ago
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...

higherpurpose 12y ago

Sounds like DJB's job could get much easier if he adopts Rusts once it's stable.

tptacek 12y ago
This is like a comment from a Markov generator.
- stcredzero 12y ago
  How about an inversion of the Turing Test, where human contestants try to convince judges they are a Markov generator? Since it's difficult for people to generate randomness, this should be challenging enough to be interesting. (Not claiming it's intellectually interesting to participate in, however.)
  - tptacek 12y ago
    I can name a couple credible contestants from this site (obviously, if there was an Asshole Test, there'd be no question who'd win it from HN).
    - stcredzero 12y ago
      Would that me positively or negatively correlated with karma? ;)