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
75a8e35b
Commit
75a8e35b
authored
Mar 27, 2020
by
Peter Schwabe
Browse files
Added comment on CompCert vs. gcc performance
parent
cecbd9c8
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/answer-Usenix.md
View file @
75a8e35b
...
...
@@ -24,8 +24,16 @@ REVIEW 1:
implementation).
*
Does compiling TweetNaCl with CompCert rather than gcc impact the performance
beyond what is acceptable? If so, what trust do you consider this proof effort
to bring to a gcc compiled implementation?
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?
We are not aware of any bugs that were introduced into ECC software by bugs in
gcc; so from a practical, crypto-engineering point of view we rule out all
...
...
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