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
a7d1882d
Commit
a7d1882d
authored
Mar 27, 2020
by
benoit
Browse files
added asymmetric primitive details
parent
75a8e35b
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/answer-Usenix.md
View file @
a7d1882d
...
...
@@ -10,10 +10,10 @@ REVIEW 1:
*
What made TweetNaCl the right choice for this project?
One goal of the project was to investigate how suitable the combination of
VST+Coq is for verifying correctness of existing C code
. The X25519
implementation in TweetNaCl was chosen because it is
relatively simple, it has
some real-world use cases, and the original paper
claims that the library
should be verifiable.
VST+Coq is for verifying correctness of existing C code
for asymmetric
primitives. The X25519
implementation in TweetNaCl was chosen because it is
relatively simple, it has
some real-world use cases, and the original paper
claims that the library
should be verifiable.
*
Would following the same approach for other implementation radically change
the proof effort?
...
...
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