Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
95ec666f
Commit
95ec666f
authored
Jun 25, 2019
by
Benoit Viguier
Browse files
more words, reorder bibtex
parent
725bf3d8
Changes
3
Hide whitespace changes
Inline
Sidebyside
paper/collection.bib
View file @
95ec666f
...
...
@@ 20,17 +20,6 @@
publisher
=
{ACM}
}
@article
{
Reynolds02separationlogic
,
author
=
{John C. Reynolds}
,
title
=
{Separation Logic: A Logic for Shared Mutable Data Structures}
,
journal
=
{LICS}
,
volume
=
{17}
,
year
=
{2002}
,
pages
=
{5574}
,
note
=
{\url{http://www.cs.cmu.edu/~jcr/seplogic.pdf}}
,
url
=
{http://www.cs.cmu.edu/~jcr/seplogic.pdf}
}
@article
{
2007BlazyCchronique
,
author
=
{Sandrine Blazy}
,
title
=
{Comment gagner confiance en {C} ?}
,
...
...
@@ 44,60 +33,6 @@
pubkind
=
{journalfrmono}
}
@article
{
Leroybackend
,
author
=
{Xavier Leroy}
,
title
=
{A formally verified compiler backend}
,
journal
=
{Journal of Automated Reasoning}
,
volume
=
{43}
,
number
=
{4}
,
pages
=
{363446}
,
year
=
{2009}
,
note
=
{\url{http://gallium.inria.fr/~xleroy/publi/compcertbackend.pdf}}
,
urlpublisher
=
{http://dx.doi.org/10.1007/s1081700991554}
,
hal
=
{http://hal.inria.fr/inria00360768/}
,
pubkind
=
{journalintmono}
}
@article
{
BlazyLeroyClight09
,
author
=
{Sandrine Blazy and Xavier Leroy}
,
title
=
{Mechanized semantics for the {Clight}
subset of the {C} language}
,
year
=
{2009}
,
journal
=
{Journal of Automated Reasoning}
,
volume
=
{43}
,
number
=
{3}
,
pages
=
{263288}
,
note
=
{\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}}
,
hal
=
{http://hal.inria.fr/inria00352524/}
,
urlpublisher
=
{http://dx.doi.org/10.1007/s1081700991483}
}
@inproceedings
{
BGJ+15
,
author
=
{Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and Peter Schwabe and Sjaak Smetsers}
,
title
=
{{TweetNaCl}: A crypto library in 100 tweets}
,
booktitle
=
{Progress in Cryptology  {LATINCRYPT 2014}}
,
editor
=
{Diego Aranha and Alfred Menezes}
,
publisher
=
SV
,
series
=
LNCS
,
volume
=
{8895}
,
year
=
{2015}
,
pages
=
{6483}
,
note
=
{Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}}
,
}
@inproceedings
{
BLS12
,
author
=
{Daniel J. Bernstein and Tanja Lange and Peter Schwabe}
,
title
=
{The security impact of a new cryptographic library}
,
booktitle
=
{Progress in Cryptology  {LATINCRYPT 2012}}
,
editor
=
{Alejandro Hevia and Gregory Neven}
,
publisher
=
SV
,
series
=
LNCS
,
volume
=
{7533}
,
year
=
{2012}
,
pages
=
{159176}
,
note
=
{Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}}
,
}
@inproceedings
{
2012Appel
,
author
=
{Andrew W. Appel}
,
title
=
{Verified Software Toolchain}
,
...
...
@@ 134,12 +69,15 @@
publisher
=
{ACM}
,
}
@misc
{
coqfaq
,
title
=
{{The Coq Proof Assistant}  {Frequently Asked Questions}}
,
author
=
{}
,
note
=
{\url{https://coq.inria.fr/faq}}
,
@book
{
Abrial:1996:BAP:236705
,
author
=
{JeanRaymond Abrial}
,
title
=
{The Bbook: Assigning Programs to Meanings}
,
year
=
{1996}
,
isbn
=
{0521496195}
,
publisher
=
{Cambridge University Press}
,
address
=
{New York, NY, USA}
,
}
note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=onepage&q&f=false}}
@inproceedings
{
Ber06
,
author
=
{Daniel J. Bernstein}
,
...
...
@@ 154,16 +92,92 @@
note
=
{\url{http://cr.yp.to/papers.html\#curve25519}}
,
}
@article
{
Mon85
,
author
=
{Peter L. Montgomery}
,
title
=
{Modular Multiplication Without Trial Division}
,
journal
=
{Mathematics of Computation}
,
publisher
=
{American Mathematical Society}
,
year
=
{1985}
,
volume
=
{44}
,
number
=
{170}
,
pages
=
{519521}
,
note
=
{\url{http://www.ams.org/journals/mcom/198544170/S0025571819850777282X/S0025571819850777282X.pdf}}
,
@misc
{
Ber14
,
title
=
{25519 naming, Posting to the CFRG mailing list}
,
author
=
{Daniel J. Bernstein}
,
year
=
{2008}
,
note
=
{\url{https://www.ietf.org/mailarchive/web/cfrg/current/msg04996.html}}
}
@inproceedings
{
Beringer2015VerifiedCA
,
title
=
{Verified Correctness and Security of OpenSSL HMAC}
,
author
=
{Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel}
,
booktitle
=
{USENIX Security Symposium}
,
year
=
{2015}
,
note
=
{\url{https://www.cs.cmu.edu/~kqy/resources/verifiedhmac.pdf}}
}
@inproceedings
{
BGJ+15
,
author
=
{Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and Peter Schwabe and Sjaak Smetsers}
,
title
=
{{TweetNaCl}: A crypto library in 100 tweets}
,
booktitle
=
{Progress in Cryptology  {LATINCRYPT 2014}}
,
editor
=
{Diego Aranha and Alfred Menezes}
,
publisher
=
SV
,
series
=
LNCS
,
volume
=
{8895}
,
year
=
{2015}
,
pages
=
{6483}
,
note
=
{Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}}
,
}
@article
{
BlazyLeroyClight09
,
author
=
{Sandrine Blazy and Xavier Leroy}
,
title
=
{Mechanized semantics for the {Clight}
subset of the {C} language}
,
year
=
{2009}
,
journal
=
{Journal of Automated Reasoning}
,
volume
=
{43}
,
number
=
{3}
,
pages
=
{263288}
,
note
=
{\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}}
,
hal
=
{http://hal.inria.fr/inria00352524/}
,
urlpublisher
=
{http://dx.doi.org/10.1007/s1081700991483}
}
@inproceedings
{
BLS12
,
author
=
{Daniel J. Bernstein and Tanja Lange and Peter Schwabe}
,
title
=
{The security impact of a new cryptographic library}
,
booktitle
=
{Progress in Cryptology  {LATINCRYPT 2012}}
,
editor
=
{Alejandro Hevia and Gregory Neven}
,
publisher
=
SV
,
series
=
LNCS
,
volume
=
{7533}
,
year
=
{2012}
,
pages
=
{159176}
,
note
=
{Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}}
,
}
@inproceedings
{
Chen2014VerifyingCS
,
title
=
{Verifying Curve25519 Software}
,
author
=
{YuFang Chen and ChangHong Hsu and HsinHung Lin and Peter Schwabe and MingHsien Tsai and BowYaw Wang and BoYin Yang and ShangYi Yang}
,
booktitle
=
{ACM Conference on Computer and Communications Security}
,
year
=
{2014}
,
note
=
{\url{https://cryptojedi.org/papers/verify2551920140428.pdf}}
}
@misc
{
coqfaq
,
title
=
{{The Coq Proof Assistant}  {Frequently Asked Questions}}
,
author
=
{}
,
note
=
{\url{https://coq.inria.fr/faq}}
,
}
@Article
{
CpdtJFR
,
author
=
{Adam Chlipala}
,
title
=
{An Introduction to Programming and Proving with Dependent Types in Coq}
,
volume
=
{3(2)}
,
pages
=
{193}
,
year
=
{2010}
,
journal
=
{Journal of Formalized Reasoning}
,
url
=
{http://adam.chlipala.net/papers/CpdtJFR/}
,
note
=
{\url{http://adam.chlipala.net/papers/CpdtJFR/}}
}
@misc
{
cryptoeprint:2011:646
,
author
=
{Daniel J. Bernstein and Tanja Lange and Peter Schwabe}
,
title
=
{The security impact of a new cryptographic library}
,
howpublished
=
{Cryptology ePrint Archive, Report 2011/646}
,
year
=
{2011}
,
note
=
{\url{https://eprint.iacr.org/2011/646}}
,
}
@inproceedings
{
DBLP:conf/itp/BartziaS14
,
...
...
@@ 179,28 +193,6 @@
note
=
{\url{https://hal.inria.fr/hal01102288}}
}
@article
{
MontgomerySpeeding
,
author
=
{Peter L. Montgomery}
,
title
=
{Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243264}
,
month
=
{01}
,
volume
=
{48}
,
year
=
{1987}
,
pages
=
{243243}
,
journal
=
{Mathematics of Computation  Math. Comput.}
,
doi
=
{10.1090/S00255718198708661137}
,
note
=
{\url{http://links.jstor.org/sici?sici=00255718(198701)48:177<243:STPAEC>2.0.CO;23}}
}
@book
{
Abrial:1996:BAP:236705
,
author
=
{JeanRaymond Abrial}
,
title
=
{The Bbook: Assigning Programs to Meanings}
,
year
=
{1996}
,
isbn
=
{0521496195}
,
publisher
=
{Cambridge University Press}
,
address
=
{New York, NY, USA}
,
}
note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=onepage&q&f=false}}
@article
{
DBLP:journals/corr/BhargavanDFHPRR17
,
author
=
{Karthikeyan Bhargavan and
Antoine Delignat{}Lavaud and
...
...
@@ 226,29 +218,11 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
timestamp
=
{Mon, 13 Aug 2018 16:46:57 +0200}
,
}
@article
{
Zinzindohoue2016AVE
,
title
=
{A Verified Extensible Library of Elliptic Curves}
,
author
=
{Jean Karim Zinzindohoue and EvmorfiaIro Bartzia and Karthikeyan Bhargavan}
,
journal
=
{2016 IEEE 29th Computer Security Foundations Symposium (CSF)}
,
year
=
{2016}
,
pages
=
{296309}
,
note
=
{\url{https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7536383}}
}
@inproceedings
{
Chen2014VerifyingCS
,
title
=
{Verifying Curve25519 Software}
,
author
=
{YuFang Chen and ChangHong Hsu and HsinHung Lin and Peter Schwabe and MingHsien Tsai and BowYaw Wang and BoYin Yang and ShangYi Yang}
,
booktitle
=
{ACM Conference on Computer and Communications Security}
,
year
=
{2014}
,
note
=
{\url{https://cryptojedi.org/papers/verify2551920140428.pdf}}
}
@inproceedings
{
Beringer2015VerifiedCA
,
title
=
{Verified Correctness and Security of OpenSSL HMAC}
,
author
=
{Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel}
,
booktitle
=
{USENIX Security Symposium}
,
year
=
{2015}
,
note
=
{\url{https://www.cs.cmu.edu/~kqy/resources/verifiedhmac.pdf}}
@inproceedings
{
Erbsen2016SystematicSO
,
title
=
{Systematic Synthesis of Elliptic Curve Cryptography Implementations}
,
author
=
{Andres Erbsen and Jason Gross and Adam Chlipala}
,
year
=
{2016}
,
note
=
{\url{https://people.csail.mit.edu/jgross/personalwebsite/papers/2017fiatcryptopldidraft.pdf}}
}
@inproceedings
{
Erbsen2017CraftingCE
,
...
...
@@ 258,20 +232,6 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note
=
{\url{http://adam.chlipala.net/theses/andreser_meng.pdf}}
}
@inproceedings
{
Philipoom2018CorrectbyconstructionFF
,
title
=
{Correctbyconstruction finite field arithmetic in Coq}
,
author
=
{Jade Philipoom}
,
year
=
{2018}
,
note
=
{\url{http://adam.chlipala.net/theses/jadep_meng.pdf}}
}
@inproceedings
{
Erbsen2016SystematicSO
,
title
=
{Systematic Synthesis of Elliptic Curve Cryptography Implementations}
,
author
=
{Andres Erbsen and Jason Gross and Adam Chlipala}
,
year
=
{2016}
,
note
=
{\url{https://people.csail.mit.edu/jgross/personalwebsite/papers/2017fiatcryptopldidraft.pdf}}
}
@inproceedings
{
fiatcrypto
,
title
=
{Simple HighLevel Code For Cryptographic Arithmetic  With Proofs, Without Compromises}
,
author
=
{Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala}
,
...
...
@@ 285,17 +245,6 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note
=
{\url{https://people.csail.mit.edu/jgross/personalwebsite/papers/2019fiatcryptoieeesp.pdf}}
}
@Article
{
CpdtJFR
,
author
=
{Adam Chlipala}
,
title
=
{An Introduction to Programming and Proving with Dependent Types in Coq}
,
volume
=
{3(2)}
,
pages
=
{193}
,
year
=
{2010}
,
journal
=
{Journal of Formalized Reasoning}
,
url
=
{http://adam.chlipala.net/papers/CpdtJFR/}
,
note
=
{\url{http://adam.chlipala.net/papers/CpdtJFR/}}
}
@article
{
gonthier2008formal
,
title
=
{Formal proofthe fourcolor theorem}
,
author
=
{Georges Gonthier}
,
...
...
@@ 307,6 +256,74 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note
=
{\url{https://www.ams.org/notices/200811/tx081101382p.pdf}}
}
@article
{
Leroybackend
,
author
=
{Xavier Leroy}
,
title
=
{A formally verified compiler backend}
,
journal
=
{Journal of Automated Reasoning}
,
volume
=
{43}
,
number
=
{4}
,
pages
=
{363446}
,
year
=
{2009}
,
note
=
{\url{http://gallium.inria.fr/~xleroy/publi/compcertbackend.pdf}}
,
urlpublisher
=
{http://dx.doi.org/10.1007/s1081700991554}
,
hal
=
{http://hal.inria.fr/inria00360768/}
,
pubkind
=
{journalintmono}
}
@article
{
Mon85
,
author
=
{Peter L. Montgomery}
,
title
=
{Modular Multiplication Without Trial Division}
,
journal
=
{Mathematics of Computation}
,
publisher
=
{American Mathematical Society}
,
year
=
{1985}
,
volume
=
{44}
,
number
=
{170}
,
pages
=
{519521}
,
note
=
{\url{http://www.ams.org/journals/mcom/198544170/S0025571819850777282X/S0025571819850777282X.pdf}}
,
}
@article
{
MontgomerySpeeding
,
author
=
{Peter L. Montgomery}
,
title
=
{Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243264}
,
month
=
{01}
,
volume
=
{48}
,
year
=
{1987}
,
pages
=
{243243}
,
journal
=
{Mathematics of Computation  Math. Comput.}
,
doi
=
{10.1090/S00255718198708661137}
,
note
=
{\url{http://links.jstor.org/sici?sici=00255718(198701)48:177<243:STPAEC>2.0.CO;23}}
}
@inproceedings
{
Philipoom2018CorrectbyconstructionFF
,
title
=
{Correctbyconstruction finite field arithmetic in Coq}
,
author
=
{Jade Philipoom}
,
year
=
{2018}
,
note
=
{\url{http://adam.chlipala.net/theses/jadep_meng.pdf}}
}
@article
{
Reynolds02separationlogic
,
author
=
{John C. Reynolds}
,
title
=
{Separation Logic: A Logic for Shared Mutable Data Structures}
,
journal
=
{LICS}
,
volume
=
{17}
,
year
=
{2002}
,
pages
=
{5574}
,
note
=
{\url{http://www.cs.cmu.edu/~jcr/seplogic.pdf}}
,
url
=
{http://www.cs.cmu.edu/~jcr/seplogic.pdf}
}
@misc
{
rfc4253
,
author
=
{Tatu Yl\"{o}nen and Chris Lonvick}
,
title
=
{{RFC 4253}  The Secure Shell {(SSH)} Transport Layer Protocol}
,
note
=
{\url{https://tools.ietf.org/html/rfc4253}}
,
}
@misc
{
rfc7748
,
author
=
{Adam Langley and Mike Hamburg and Sean Turner}
,
title
=
{{RFC 7748}  Elliptic Curves for Security}
,
note
=
{\url{https://tools.ietf.org/html/rfc7748}}
,
}
@misc
{
thisthatusecurve25519
,
title
=
{Things that use Curve25519}
,
...
...
@@ 315,6 +332,15 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note
=
{\url{https://ianix.com/pub/curve25519deployment.html}}
}
@article
{
Zinzindohoue2016AVE
,
title
=
{A Verified Extensible Library of Elliptic Curves}
,
author
=
{Jean Karim Zinzindohoue and EvmorfiaIro Bartzia and Karthikeyan Bhargavan}
,
journal
=
{2016 IEEE 29th Computer Security Foundations Symposium (CSF)}
,
year
=
{2016}
,
pages
=
{296309}
,
note
=
{\url{https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7536383}}
}
@inproceedings
{
zinzindohoue2017hacl
,
title
=
{HACL*: A verified modern cryptographic library}
,
author
=
{JeanKarim Zinzindohou{\'e} and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche}
,
...
...
@@ 323,13 +349,9 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
year
=
{2017}
,
organization
=
{ACM}
,
note
=
{\url{https://eprint.iacr.org/2017/536.pdf}}
}
@misc
{
Ber14
,
title
=
{25519 naming, Posting to the CFRG mailing list}
,
author
=
{Daniel J. Bernstein}
,
year
=
{2008}
,
note
=
{\url{https://www.ietf.org/mailarchive/web/cfrg/current/msg04996.html}}
@misc
{
zmq
,
title
=
{ZeroMQ}
,
note
=
{\url{http://zeromq.org/}}
}
Daniel J. Bernstein. 25519 naming. , 2014. . 2
paper/intro.tex
View file @
95ec666f
XXX: NaCl
XXX: TweetNaCl (find realworld use of TweetNaCl?)
Mega.nz uses tweetnacljs (as JS port of tweetnacl) for their webclient https://mega.nz/
Keybase client: https://github.com/keybase/nodenacl/blob/master/lib/tweetnacl.js
Zeromq a messaging queue system uses tweetnacl to provide portability to it's users. http://zeromq.org/
XXX:
NaCl~
\cite
{
BLS12
}
is an easytouse highsecurity highspeed software library
for network communication, encryption, decryption, signatures, etc.
TweetNaCl~
\cite
{
BGJ+15
}
is its compact reimplementation.
It does not aim for high speed application and has been optimized for source
code compactness (100 tweets). It maintains some degree of readability in order
to be easily auditable.
TweetNaCl is being used by ZeroMQ~
\cite
{
zmq
}
messaging queue system to provide
portability to its users.
``TweetNaCl is the
first cryptographic library that allows correct functionality to be verified
by auditors with reasonable effort''
by auditors with reasonable effort''
~
\cite
{
BGJ+15
}
XXX: One core component of TweetNaCl (and NaCl) is X25519, mention use
of X25519 in the wild.
Originally, the name ``Curve25519'' referred to this keyexchange protocol,
but Bernstein suggested to rename the scheme to X25519 and to use the name
Curve25519 for the underlying elliptic curve~
\cite
{
Ber14
}
.
We make use of this notation in this paper.
% XXX: TweetNaCl (find realworld use of TweetNaCl?)
% Mega.nz uses tweetnacljs (as JS port of tweetnacl) for their webclient https://mega.nz/
% Keybase client: https://github.com/keybase/nodenacl/blob/master/lib/tweetnacl.js
TweetNaCl~
\cite
{
BGJ+15
}
is a compact reimplementation of the
NaCl~
\cite
{
BLS12
}
high security cryptographic library.
It does not aim for high speed application and has been optimized for source
code compactness (100 tweets). It maintains some degree of readability in order
to be easily auditable.
One core component of TweetNaCl (and NaCl) is the key exchange protocol X25519~
\cite
{
rfc7748
}
.
This protocol is being used by a wide variety of applications~
\cite
{
thisthatusecurve25519
}
such as SSH~
\cite
{
rfc4253
}
, Signal Protocol, Tor, Zcash, TLS to establish a shared secret over
an insecure channel.
This library makes use of Curve25519~
\cite
{
Ber06
}
, a function over a
\F
{
p
}
restricted
$
x
$
coordinate computing a scalar multiplication on
$
E
(
\F
{
p
^
2
}
)
$
, where
$
p
$
is
the prime number
$
\p
$
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
This function is used by a wide variety of applications~
\cite
{
thisthatusecurve25519
}
to establish a shared secret over an insecure channel.
Originally, the name ``Curve25519'' referred to this keyexchange protocol,
but Bernstein suggested to rename the scheme to X25519 and to use the name
Curve25519 for the underlying elliptic curve~
\cite
{
Ber14
}
.
We make use of this notation in this paper.
\subheading
{
Contribution of this paper
}
\todo
{
Proof that TweetNaCl's X25519 code correctly implements math definition from 25519 paper
}
\todo
{
State additional contributions, e.g., extension of EC framework by Bartiza and Strub.
}
...
...
paper/preliminaries.tex
View file @
95ec666f
...
...
@@ 178,3 +178,148 @@ $\exists x,y \in$ \TNaCle{gf} such that
\end{lstlisting}
\subsection
{
Coq and VST
}
Verifying
\texttt
{
crypto
\_
scalarmult
}
also implies to verify all the functions
subsequently called:
\texttt
{
unpack25519
}
;
\texttt
{
A
}
;
\texttt
{
Z
}
;
\texttt
{
M
}
;
\texttt
{
S
}
;
\texttt
{
car25519
}
;
\texttt
{
inv25519
}
;
\texttt
{
set25519
}
;
\texttt
{
sel25519
}
;
\texttt
{
pack25519
}
.
We prove that the implementation of Curve25519 is
\textbf
{
sound
}
\ie
\begin{itemize}
\item
absence of access outofbounds of arrays (memory safety).
\item
absence of overflows/underflow on the arithmetic.
\end{itemize}
We also prove that TweetNaCl's code is
\textbf
{
correct
}
:
\begin{itemize}
\item
Curve25519 is correctly implemented (we get what we expect).
\item
Operations on
\texttt
{
gf
}
(
\texttt
{
A
}
,
\texttt
{
Z
}
,
\texttt
{
M
}
,
\texttt
{
S
}
)
are equivalent to operations (
$
+
,

,
\times
,x
^
2
$
) in
\Zfield
.
\item
The Montgomery ladder does compute a scalar multiplication between a natural number and a point.
\end{itemize}
In order to prove the soundness and correctness of
\texttt
{
crypto
\_
scalarmult
}
,
we first create a skeleton of the Montgomery ladder with abstract operations which
can be instanciated over lists, integers, field elements...
A high level specification (over a generic field
$
\K
$
) allows use to prove the
correctness of the ladder with respect to the curves theory.
This high specification does not rely on the parameters of Curve25519.
By instanciating
$
\K
$
with
$
\Zfield
$
, and the parameters of Curve25519 (
$
a
=
486662
, b
=
1
$
),
we define a middle level specification.
Additionally we also provide a low level specification close to the
\texttt
{
C
}
code
(over lists of
$
\Z
$
). We show this specification to be equivalent to the
\textit
{
semantic version
}
of C (
\texttt
{
CLight
}
) with VST.
This low level specification gives us the soundness assurance.
By showing that operations over instances (
$
\K
=
\Zfield
$
,
$
\Z
$
, list of
$
\Z
$
) are
equivalent we bridge the gap between the low level and the high level specification
with Curve25519 parameters.
As such we prove all specifications to equivalent (Fig.
\ref
{
tk:ProofStructure
}
).
This garantees us the correctness of the implementation.
\begin{figure}
[h]
\include
{
tikz/specifications
}
\caption
{
Structural construction of the proof
}
\label
{
tk:ProofStructure
}
\end{figure}
\subsection
{
Correctness Specification
}
We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function.
This defines the equivalence between the Clight representation and a Coq definition of the ladder.
\begin{CoqVST}
Definition crypto
_
scalarmult
_
spec :=
DECLARE
_
crypto
_
scalarmult
_
curve25519
_
tweet
WITH
v
_
q: val, v
_
n: val, v
_
p: val, c121665:val,
sh : share,
q : list val, n : list Z, p : list Z
(**)
PRE [
_
q OF (tptr tuchar),
_
n OF (tptr tuchar),
_
p OF (tptr tuchar) ]
PROP (writable
_
share sh;
Forall (fun x => 0 <= x < 2
^
8) p;
Forall (fun x => 0 <= x < 2
^
8) n;
Zlength q = 32; Zlength n = 32;
Zlength p = 32)
LOCAL(temp
_
q v
_
q; temp
_
n v
_
n; temp
_
p v
_
p;
gvar
__
121665 c121665)
SEP (sh [
{
v
_
q
}
] <<(uch32) q;
sh [
{
v
_
n
}
] <<(uch32) mVI n;
sh [
{
v
_
p
}
] <<(uch32) mVI p;
Ews [
{
c121665
}
] <<(lg16) mVI64 c
_
121665)
(**)
POST [ tint ]
PROP (Forall (fun x => 0 <= x < 2
^
8) (CSM n p);
Zlength (CSM n p) = 32)
LOCAL(temp ret
_
temp (Vint Int.zero))
SEP (sh [
{
v
_
q
}
] <<(uch32) mVI (CSM n p);
sh [
{
v
_
n
}
] <<(uch32) mVI n;
sh [
{
v
_
p
}
] <<(uch32) mVI p;
Ews [
{
c121665
}
] <<(lg16) mVI64 c
_
121665
\end{CoqVST}
In this specification we state as preconditions:
\begin{itemize}
\item
[]
\VSTe
{
PRE
}
:
\VSTe
{_
p OF (tptr tuchar)
}
\\
The function
\texttt
{
crypto
\_
scalarmult
}
takes as input three pointers to
arrays of unsigned bytes (
\VSTe
{
tptr tuchar
}
)
\VSTe
{_
p
}
,
\VSTe
{_
q
}
and
\VSTe
{_
n
}
.
\item
[]
\VSTe
{
LOCAL
}
:
\VSTe
{
temp
_
p v
_
p
}
\\
Each pointer represent an address
\VSTe
{
v
_
p
}
,
\VSTe
{
v
_
q
}
and
\VSTe
{
v
_
n
}
.
\item
[]
\VSTe
{
SEP
}
:
\VSTe
{
sh [
{
v
_
p
$
\!\!\}\!\!
]
\!\!\!
$
<<(uch32) mVI p
}
\\
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
p
}
points
to a list of integer values
\VSTe
{
mVI p
}
.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Forall (fun x => 0 <= x < 2
^
8) p
}
\\
In order to consider all the possible inputs, we assumed each
elements of the list
\texttt
{
p
}
to be bounded by
$
0
$
included and
$
2
^
8
$
excluded.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Zlength p = 32
}
\\
We also assumed that the length of the list
\texttt
{
p
}
is 32. This defines the
complete representation of
\TNaCle
{
u8[32]
}
.
\end{itemize}
As Postcondition we have:
\begin{itemize}
\item
[]
\VSTe
{
POST
}
:
\VSTe
{
tint
}
\\
The function
\texttt
{
crypto
\_
scalarmult
}
returns an integer.
\item
[]
\VSTe
{
LOCAL
}
:
\VSTe
{
temp ret
_
temp (Vint Int.zero)
}
\\
The returned integer has value
$
0
$
.
\item
[]
\VSTe
{
SEP
}
:
\VSTe
{
sh [
{
v
_
q
$
\!\!\}\!\!
]
\!\!\!
$
<<(uch32) mVI (CSM n p)
}
\\
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
q
}
points
to a list of integer values
\VSTe
{
mVI (CSM n p)
}
where
\VSTe
{
CSM n p
}
is the
result of the
\VSTe
{
crypto
_
scalarmult
}
over
\VSTe
{
n
}
and
\VSTe
{
p
}
.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Forall (fun x => 0 <= x < 2
^
8) (CSM n p)
}
\\
\VSTe
{
PROP
}
:
\VSTe
{
Zlength (CSM n p) = 32
}
\\
We show that the computation for
\VSTe
{
CSM
}
fits in
\TNaCle
{
u8[32]
}
.
\end{itemize}
This specification shows that
\VSTe
{
crypto
_
scalarmult
}
in C computes the same
result as
\VSTe
{
CSM
}
in Coq provided that inputs are within their respective
bounds.
By converting those array of 32 bytes into their respective littleendian value
we prove the correctness of
\VSTe
{
crypto
_
scalarmult
}
(Theorem
\ref
{
CSMcorrect
}
)
in Coq (for the sake of simplicity we do not display the conversion in the theorem).
\begin{theorem}
\label
{
CSMcorrect
}
For all
$
n
\in
\N
, n <
2
^{
255
}$
and where the bits 1, 2, 5 248, 249, 250
are cleared and bit 6 is set, for all
$
P
\in
E
(
\F
{
p
^
2
}
)
$
,
for all
$
p
\in
\F
{
p
}$
such that
$
P.x
=
p
$
,
there exists
$
Q
\in
E
(
\F
{
p
^
2
}
)
$
such that
$
Q
=
nP
$
where
$
Q.x
=
q
$
and
$
q
$
=
\VSTe
{
CSM
}
$
n
$
$
p
$
.
\end{theorem}
A more complete description in Coq of Theorem
\ref
{
CSMcorrect
}
with the associated conversions
is as follow:
\begin{lstlisting}
[language=Coq]
Theorem Crypto
_
Scalarmult
_
Correct:
forall (n p:list Z) (P:mc curve25519
_
Fp2
_
mcuType),
Zlength n = 32 >
Zlength p = 32 >
Forall (fun x => 0 <= x /
\
x < 2
^
8) n >
Forall (fun x => 0 <= x /
\
x < 2
^
8) p >
Fp2
_
x (ZUnpack25519 (ZofList 8 p)) = P#x0 >
ZofList 8 (Crypto
_
Scalarmult n p) =
(P *+ (Z.to
_
nat (Zclamp (ZofList 8 n))))
_
x0.
\end{lstlisting}
% Its proof is explained in the next section.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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