Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
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
cae3b1c7
Commit
cae3b1c7
authored
Oct 02, 2020
by
Peter Schwabe
Browse files
Added some missing references
parent
6be9aa83
Changes
2
Hide whitespace changes
Inline
Side-by-side
paper/collection.bib
View file @
cae3b1c7
@STRING
{
LNCS
=
{LNCS}
}
@STRING
{
LNCS
=
{LNCS}
}
@STRING
{
SV
=
{Springer}
}
@STRING
{
SV
=
{Springer}
}
@inproceedings
{
DBLP:conf/pldi/CauligiDGTSRB20
,
author
=
{Sunjay Cauligi and
Craig Disselkoen and
Klaus von Gleissenthall and
Dean M. Tullsen and
Deian Stefan and
Tamara Rezk and
Gilles Barthe}
,
title
=
{Constant-time foundations for the new spectre era}
,
booktitle
=
pldi
,
pages
=
{913--926}
,
publisher
=
{{ACM}}
,
year
=
{2020}
}
@inproceedings
{
ABB+16
,
author
=
{Jos\'e Bacelar Almeida and Manuel Barbosa and Gilles Barthe and François Dupressoir and Michael Emmi}
,
title
=
{Verifying Constant-Time Implementations}
,
booktitle
=
{Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security}
,
publisher
=
{ACM}
,
year
=
{2016}
,
series
=
{CCS ’17}
,
pages
=
{53--70}
,
note
=
{\url{https://www.usenix.org/system/files/conference/usenixsecurity16/sec16_paper_almeida.pdf}}
,
}
@inproceedings
{
DBR20
,
author
=
{Lesly-Ann Daniel, S\'ebastien Bardin, Tamara Rezk}
,
title
=
{\textsc{Binsec/Rel}: Efficient Relational SymbolicExecution for Constant-Time at Binary-Level}
,
booktitle
=
{2020 IEEE Symposium on Security and Privacy}
,
year
=
{2020}
,
pages
=
{1021--1038}
,
note
=
{\url{https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf}}
,
}
@article
{
1969-Hoare
,
@article
{
1969-Hoare
,
author
=
{C. A. R. Hoare}
,
author
=
{C. A. R. Hoare}
,
title
=
{An Axiomatic Basis for Computer Programming}
,
title
=
{An Axiomatic Basis for Computer Programming}
,
...
...
paper/intro.tex
View file @
cae3b1c7
...
@@ -57,10 +57,10 @@ As a consequence, the result of this paper can readily be used in mechanized pro
...
@@ -57,10 +57,10 @@ As a consequence, the result of this paper can readily be used in mechanized pro
arguing about the security of cryptographic constructions on the more abstract
arguing about the security of cryptographic constructions on the more abstract
level of operations in groups and related problems, like the elliptic-curve
level of operations in groups and related problems, like the elliptic-curve
discrete-logarithm (ECDLP) or elliptic-curve Diffie-Hellman (ECDH) problem.
discrete-logarithm (ECDLP) or elliptic-curve Diffie-Hellman (ECDH) problem.
\todo
{
Add examples of such mechanized proofs?
}
%
\todo{Add examples of such mechanized proofs?}
Also, connecting our formalization of the RFC to the mathematical definition
Also, connecting our formalization of the RFC to the mathematical definition
significantly increases trust into the correctness of the formalization and
significantly increases trust into the correctness of the formalization and
reduces the effort of manual auditing
of that
formalization.
reduces the effort of manual
ly
auditing
the
formalization.
\subheading
{
The bigger picture of high-assurance crypto.
}
\subheading
{
The bigger picture of high-assurance crypto.
}
This work fits into the bigger area of
\emph
{
high-assurance
}
cryptography,
This work fits into the bigger area of
\emph
{
high-assurance
}
cryptography,
...
@@ -77,7 +77,8 @@ of cryptographic software:
...
@@ -77,7 +77,8 @@ of cryptographic software:
through computer-checked reductions from some assumed-to-be-hard mathematical problem.
\label
{
hacs:secure
}
through computer-checked reductions from some assumed-to-be-hard mathematical problem.
\label
{
hacs:secure
}
\end{enumerate}
\end{enumerate}
A recent addition to this triplet (or rather an extension of implementation security)
A recent addition to this triplet (or rather an extension of implementation security)
is security also against speculative attacks. See, e.g.,~
\cite
{
XXX
}
.
is security also against attacks expoiting speculative execution.
See, e.g.,~
\cite
{
DBLP:conf/pldi/CauligiDGTSRB20
}
.
This paper targets only the first point and attempts to make results
This paper targets only the first point and attempts to make results
immediately usable for verification efforts of cryptographic security.
immediately usable for verification efforts of cryptographic security.
...
@@ -85,8 +86,8 @@ Verification of implementation security is probably equally important as
...
@@ -85,8 +86,8 @@ Verification of implementation security is probably equally important as
verification of correctness, but working on the C language level as we do
verification of correctness, but working on the C language level as we do
in this paper is not helpful. To obtain guarantees of security against
in this paper is not helpful. To obtain guarantees of security against
timing-attack we recommend verifying
\emph
{
compiled
}
code on LLVM level with,
timing-attack we recommend verifying
\emph
{
compiled
}
code on LLVM level with,
e.g., ct-verif~
\cite
{
XXX
}
,
e.g., ct-verif~
\cite
{
ABB+16
}
,
or even better on binary level with, e.g., Bin
S
ec/Rel~
\cite
{
XXX
}
.
or even better on binary level with, e.g.,
\textsc
{
Bin
s
ec/Rel
}
~
\cite
{
DBR20
}
.
\subheading
{
Related work.
}
\subheading
{
Related work.
}
The field of computer-aided cryptography, i.e., using computer-verified proofs
The field of computer-aided cryptography, i.e., using computer-verified proofs
...
...
Write
Preview
Markdown
is supported
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