Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
d16cfd19
Commit
d16cfd19
authored
Mar 27, 2020
by
benoit
Browse files
fix URL
parent
f1d6788c
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/answer-Usenix.md
View file @
d16cfd19
...
...
@@ -25,14 +25,14 @@ REVIEW A:
does not change for other implementations.
*
Does compiling TweetNaCl with CompCert rather than gcc impact the performance
beyond what is acceptable?
beyond what is acceptable?
For the X25519 implementation in TweetNaCl, CompCert generates code that is
about 6x slower than code generated with gcc. While this sounds like a lot, it
may not be too much of an issue for projects that use TweetNaCl, because they
chose for a library that prioritizes simplicity over performance in the first
place. A more serious issue however can be the non-free CompCert license.
*
If so, what trust do you consider this proof effort to bring to a gcc compiled
implementation?
...
...
@@ -70,7 +70,7 @@ REVIEW C:
We were not able to reproduce this failure. We prepared a VM image together
with a README to rule out any kind of system dependencies; see
https://github.com/coq-verif-tweetnacl/coq-verif-tweetnacl
-VM
https://github.com/coq-verif-tweetnacl/coq-verif-tweetnacl
*
Demonstrate a security benefit relative to [12]: what bugs does this
eliminate? What specific correctness properties does it add?
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment