Commit 8aab04a1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

update to ACM CSS template

parent ec1b306b
......@@ -123,7 +123,6 @@ The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
%% BLABLA about VST. Does not belong here.
% The Verifiable Software Toolchain uses a strongest postcondition strategy.
% The user must first write a formal specification of the function he wants to verify in Coq.
......
This diff is collapsed.
......@@ -9,16 +9,16 @@
\refstepcounter{section}
\sectionmark{#1}}
\newenvironment{proof}[1][Proof]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{definition}[1][Definition]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{example}[1][Example]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{remark}[1][Remark]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newcommand{\qed}{\nobreak \ifvmode \relax \else
% \newenvironment{proof}[1][Proof]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{definition}[1][Definition]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{example}[1][Example]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{remark}[1][Remark]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\renewcommand{\qed}{\nobreak \ifvmode \relax \else
\ifdim\lastskip<1.5em \hskip-\lastskip
\hskip1.5em plus0em minus0.5em \fi \nobreak
\vrule height0.75em width0.5em depth0.25em\fi}
......
\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts % this enables the \thanks command
% \documentclass[conference]{IEEEtran}
\documentclass[format=sigconf, screen=true, review=false, authordraft=true]{acmart}
\usepackage{setup}
\fancyhf{} % Remove fancy page headers
\fancyhead[C]{Anonymous submission \#9999 to ACM CCS 2020} % TODO: replace 9999 with your paper number
\fancyfoot[C]{\thepage}
\setcopyright{none} % No copyright notice required for submissions
\acmConference[Anonymous Submission to ACM CCS 2020]{ACM Conference on Computer and Communications Security}{Due 20 January 2020}{Orlando, TBD}
\acmYear{2019}
\settopmatter{printacmref=false, printccs=true, printfolios=true} % We want page numbers on submissions
%%\ccsPaper{9999} % TODO: replace with your paper number once obtained
\newif\ifpublic
\publicfalse
% to display line numbers and page numbers
\newif\ifwip
\wipfalse
% \newif\ifwip
% \wipfalse
% what is iffull used for ??? O.o
\newif\iffull
......@@ -19,9 +31,26 @@
\begin{document}
\ifwip
\linenumbers
\fi
% TODO: replace this section with code generated by the tool at https://dl.acm.org/ccs.cfm
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10002978.10002986.10002990</concept_id>
<concept_desc>Security and privacy~Logic and verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Security and privacy~Logic and verification}
% -- end of section to replace with generated code
\keywords{Formal Verification, Cryptographic Implementations, Elliptic Curves} % TODO: replace with your keywords
% \ifwip
% \linenumbers
% \fi
%don't want date printed
\date{}
......@@ -30,36 +59,33 @@
\title{\Large \bf A Coq proof of the correctness of X25519 in TweetNaCl}
%for single author (just remove % characters)
\ifpublic
\author{
\IEEEauthorblockN{Peter Schwabe}
\IEEEauthorblockA{Radboud University,\\
% \ifpublic
\author{Peter Schwabe}
\affiliation{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Beno\^it Viguier}
\IEEEauthorblockA{Radboud University,\\
\author{Beno\^it Viguier}
\affiliation{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Timmy Weerwag}
\IEEEauthorblockA{XXX: Affiliation,\\
\author{Timmy Weerwag}
\affiliation{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Freek Wiedijk}
\IEEEauthorblockA{Radboud University,\\
\author{Freek Wiedijk}
\affiliation{Radboud University,\\
The Netherlands}
}
\else
% just to remove complains from compilation
\author{}
\fi
% \else
% % just to remove complains from compilation
% \author{}
% \fi
\input{_abstract}
\maketitle
\ifwip
% add page numbers : https://tex.stackexchange.com/questions/52729/forcing-page-numbers-with-ieeetran/52785
\thispagestyle{plain}
\pagestyle{plain}
\fi
% \ifwip
% % add page numbers : https://tex.stackexchange.com/questions/52729/forcing-page-numbers-with-ieeetran/52785
% \thispagestyle{plain}
% \pagestyle{plain}
% \fi
%XXX: Figure out how to put this somewhere nice
%\thanks{
......@@ -74,7 +100,7 @@ The Netherlands}
\intput{main}
\vspace*{1cm}
{\footnotesize \bibliographystyle{IEEEtran}
{\bibliographystyle{ACM-Reference-Format}
\bibliography{collection}}
\begin{appendix}
......
\usepackage{epsfig}
\usepackage{epsfig} % NOT WHITELISTED
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[switch]{lineno}
\usepackage[pdf]{pstricks}
\usepackage[pdf]{pstricks} % NOT WHITELISTED
\usepackage{amsfonts,amsmath,amscd,amscd,amssymb,array}
\usepackage{type1cm}
\usepackage{amsfonts,amsmath,amscd,amssymb,array}
\usepackage{type1cm} % NOT WHITELISTED
\newcommand{\lstsize}{\fontsize{8.5pt}{8.5pt}\selectfont}
\usepackage{algorithm, algorithmic}
\usepackage{xspace}
\usepackage{xspace} % NOT WHITELISTED
\usepackage{listings}
\usepackage{booktabs}
\usepackage{multirow}
\usepackage{ntheorem}
\usepackage{textcomp}
\usepackage{bussproofs}
\usepackage{xcolor}
\usepackage{cite}
\usepackage{dsfont}
\usepackage{bussproofs} % NOT WHITELISTED
\usepackage{xcolor} % NOT WHITELISTED
% \usepackage{cite} % NOT WHITELISTED
\usepackage{dsfont} % NOT WHITELISTED
\usepackage{float}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\definecolor{linkcolor}{rgb}{0.65,0,0}
\definecolor{citecolor}{rgb}{0,0.45,0}
\definecolor{urlcolor}{rgb}{0,0,0.65}
\usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
\usepackage{tikz}
\usetikzlibrary{arrows}
% \usepackage[amsthm, hyperref]{ntheorem} % NOT WHITELISTED
% \definecolor{linkcolor}{rgb}{0.65,0,0}
% \definecolor{citecolor}{rgb}{0,0.45,0}
% \definecolor{urlcolor}{rgb}{0,0,0.65}
% \usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
\renewcommand{\algorithmicrequire}{\textbf{Input:\ }}
\renewcommand{\algorithmicensure}{\textbf{Output:\ }}
......@@ -52,7 +52,7 @@
\newcounter{subListing@save}
\renewcommand{\thesubListing}{\alph{subListing}}
\usepackage[framemethod=tikz]{mdframed}
\usepackage[framemethod=tikz]{mdframed} % NOT WHITELISTED
\mdfsetup{leftmargin=0cm,skipabove=0.1cm,hidealllines=true,%
innerleftmargin=0.05cm,innerrightmargin=0.05cm,
innertopmargin=-0.10cm,innerbottommargin=-0.20cm,
......@@ -357,8 +357,8 @@ literate=
basicstyle=\ttfamily\small,
% morecomment=[f][\lstbg{red!20}]<,
% morecomment=[f][\lstbg{green!20}]>,
morecomment=[f][\color{doc@lstidentifiers2}]<,
morecomment=[f][\color{doc@lstfunctions}]>,
morecomment=[f][\color{doc@lstidentifiers2}]-,
morecomment=[f][\color{doc@lstfunctions}]+,
morecomment=[f][\color{gray}\textit]{@@},
%morecomment=[f][\textit]{---},
%morecomment=[f][\textit]{+++},
......
8c8
< typedef long long i64;
---
--- tweetnacl.c
+++ tweetnaclVerifiableC.c
@@ -5,7 +5,7 @@
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
@@ We tell VST that long long
@@ are aligned on 8 bytes.
> typedef long long i64
> __attribute__((aligned(8)));
277,281c277,279
< FOR(i,16) {
< o[i]+=(1LL<<16);
< c=o[i]>>16;
< o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
< o[i]-=c<<16;
---
@@ We separate the loop iteration:
@@ 0-14 and 15 as the last.
@@ also simplify the carry propagation code.
> FOR(i,15) {
> o[(i+1)]+=o[i]>>16;
> o[i]&=0xffff;
282a281,282
> o[0]+=38*(o[15]>>16);
> o[15]&=0xffff;
285c285
-typedef long long i64;
+typedef long long i64 __attribute__((aligned(8)));
typedef i64 gf[16];
extern void randombytes(u8 *,u64);
@@ -273,18 +273,16 @@
@@ We remove the undefined behavior and
@@ simplify the carry propagation.
sv car25519(gf o)
{
int i;
- i64 c;
FOR(i,16) {
- o[i]+=(1LL<<16);
- c=o[i]>>16;
- o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
- o[i]-=c<<16;
+ o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
+ o[i]&=0xffff;
}
}
@@ b is a mask of 64 bits.
< sv sel25519(gf p,gf q,int b)
---
> sv sel25519(gf p,gf q,i64 b)
287c287,288
< i64 t,i,c=~(b-1);
---
-sv sel25519(gf p,gf q,int b)
+sv sel25519(gf p,gf q,i64 b)
{
@@ For-loop indexes have to be int.
> int i;
> i64 t,c=~(b-1);
297,299c298,301
< int i,j,b;
< gf m,t;
< FOR(i,16) t[i]=n[i];
---
- i64 t,i,c=~(b-1);
+ int i;
+ i64 t,c=~(b-1);
FOR(i,16) {
t= c&(p[i]^q[i]);
p[i]^=t;
@@ -294,9 +292,10 @@
sv pack25519(u8 *o,const gf n)
{
@@ For-loop indexes have to be int.
@@ b is a 64 bit mask.
@@ Initialize m to simplify verification.
> int i,j;
> i64 b;
> gf t,m={0};
> set25519(t,n);
310d311
< b=(m[15]>>16)&1;
312c313,314
< sel25519(t,m,1-b);
---
- int i,j,b;
- gf m,t;
- FOR(i,16) t[i]=n[i];
+ int i,j;
+ i64 b;
+ gf t,m={0};
+ set25519(t,n);
car25519(t);
car25519(t);
car25519(t);
@@ -307,9 +306,9 @@
m[i-1]&=0xffff;
}
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
- b=(m[15]>>16)&1;
m[14]&=0xffff;
@@ Computations in arguments
@@ are not allowed in VST.
> b=1-(m[15]>>16)&1;
> sel25519(t,m,b);
332c334
< return d[0]&1;
---
- sel25519(t,m,1-b);
+ b=1-((m[15]>>16)&1);
+ sel25519(t,m,b);
}
FOR(i,16) {
o[2*i]=t[i]&0xff;
@@ -329,7 +328,7 @@
{
u8 d[32];
pack25519(d,a);
@@ Force the casting.
> return d[0]&(u8)1;
356,359c358,365
< i64 i,j,t[31];
< FOR(i,31) t[i]=0;
< FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
< FOR(i,15) t[i]+=38*t[i+16];
---
- return d[0]&1;
+ return d[0]&(u8)1;
}
sv unpack25519(gf o, const u8 *n)
@@ -353,10 +352,14 @@
sv M(gf o,const gf a,const gf b)
{
@@ For-loop indexes have to be int.
> int i,j;
> i64 t[31], aux;
> FOR(i,31) t[i]= 0;
> FOR(i,16) {
@@ introduce an auxiliary variable to
@@ simplify verification (loop invariants).
> aux = a[i];
> FOR(j,16) t[i+j]+=aux*b[j];
> }
> FOR(i,15) t[i]+=(i64)38*t[i+16];
374c380
< FOR(a,16) c[a]=i[a];
---
- i64 i,j,t[31];
- FOR(i,31) t[i]=0;
- FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
- FOR(i,15) t[i]+=38*t[i+16];
+ int i,j;
+ i64 t[31], aux;
+ FOR(i,31) t[i]= 0;
+ FOR(i,16) {
+ aux = a[i];
+ FOR(j,16) t[i+j]+=aux*b[j];
+ }
+ FOR(i,15) t[i]+=(i64)38*t[i+16];
FOR(i,16) o[i]=t[i];
car25519(o);
car25519(o);
@@ -371,7 +374,7 @@
{
gf c;
int a;
- FOR(a,16) c[a]=i[a];
@@ gain 5 bytes.
> set25519(c,i);
397,398c403,405
< i64 x[80],r,i;
< gf a,b,c,d,e,f;
---
+ set25519(c,i);
for(a=253;a>=0;a--) {
S(c,c);
if(a!=2&&a!=4) M(c,c,i);
@@ -394,8 +397,9 @@
int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)
{
u8 z[32];
@@ x only needs gf.
@@ For-loop indexes have to be int.
> i64 r;
> int i;
> gf x,a,b,c,d,e,f;
433,441c440,442
< FOR(i,16) {
< x[i+16]=a[i];
< x[i+32]=c[i];
< x[i+48]=b[i];
< x[i+64]=d[i];
< }
< inv25519(x+32,x+32);
< M(x+16,x+16,x+32);
< pack25519(q,x+16);
---
- i64 x[80],r,i;
- gf a,b,c,d,e,f;
+ i64 r;
+ int i;
+ gf x,a,b,c,d,e,f;
FOR(i,31) z[i]=n[i];
z[31]=(n[31]&127)|64;
z[0]&=248;
@@ -430,15 +434,9 @@
sel25519(a,b,r);
sel25519(c,d,r);
}
@@ simplify
> inv25519(c,c);
> M(a,a,c);
> pack25519(q,a);
- FOR(i,16) {
- x[i+16]=a[i];
- x[i+32]=c[i];
- x[i+48]=b[i];
- x[i+64]=d[i];
- }
- inv25519(x+32,x+32);
- M(x+16,x+16,x+32);
- pack25519(q,x+16);
+ inv25519(c,c);
+ M(a,a,c);
+ pack25519(q,a);
return 0;
}
8c8
< typedef long long i64;
---
> typedef long long i64 __attribute__((aligned(8)));
277,281c277,279
< FOR(i,16) {
< o[i]+=(1LL<<16);
< c=o[i]>>16;
< o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
< o[i]-=c<<16;
---
> FOR(i,15) {
> o[(i+1)]+=o[i]>>16;
> o[i]&=0xffff;
282a281,282
> o[0]+=38*(o[15]>>16);
> o[15]&=0xffff;
285c285
< sv sel25519(gf p,gf q,int b)
---
> sv sel25519(gf p,gf q,i64 b)
287c287,288
< i64 t,i,c=~(b-1);
---
> int i;
> i64 t,c=~(b-1);
297,299c298,301
< int i,j,b;
< gf m,t;
< FOR(i,16) t[i]=n[i];
---
> int i,j;
> i64 b;
> gf t,m={0};
> set25519(t,n);
310d311
< b=(m[15]>>16)&1;
312c313,314
< sel25519(t,m,1-b);
---
> b=1-(m[15]>>16)&1;
> sel25519(t,m,b);
332c334
< return d[0]&1;
---
> return d[0]&(u8)1;
356,359c358,365
< i64 i,j,t[31];
< FOR(i,31) t[i]=0;
< FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
< FOR(i,15) t[i]+=38*t[i+16];
---
> int i,j;
> i64 t[31], aux;
> FOR(i,31) t[i]= 0;
> FOR(i,16) {
> aux = a[i];
> FOR(j,16) t[i+j]+=aux*b[j];
> }
> FOR(i,15) t[i]+=(i64)38*t[i+16];
374c380
< FOR(a,16) c[a]=i[a];
---
> set25519(c,i);
397,398c403,405
< i64 x[80],r,i;
< gf a,b,c,d,e,f;
---
> i64 r;
> int i;
> gf x,a,b,c,d,e,f;
433,441c440,442
< FOR(i,16) {
< x[i+16]=a[i];
< x[i+32]=c[i];
< x[i+48]=b[i];
< x[i+64]=d[i];
< }
< inv25519(x+32,x+32);
< M(x+16,x+16,x+32);
< pack25519(q,x+16);
---
> inv25519(c,c);
> M(a,a,c);
> pack25519(q,a);
--- tweetnacl.c 2019-07-31 14:05:27.916394829 +0200
+++ tweetnaclVerifiableC.c 2019-12-28 16:31:25.596762941 +0100
@@ -5,7 +5,7 @@
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
@@ We tell VST that long long
@@ are aligned on 8 bytes.
-typedef long long i64;
+typedef long long i64 __attribute__((aligned(8)));
typedef i64 gf[16];
extern void randombytes(u8 *,u64);
@@ -273,18 +273,16 @@
@@ We remove the undefined behavior and
@@ simplify the carry propagation.
sv car25519(gf o)
{
int i;
- i64 c;
FOR(i,16) {
- o[i]+=(1LL<<16);
- c=o[i]>>16;
- o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
- o[i]-=c<<16;
+ o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
+ o[i]&=0xffff;
}
}
@@ b is a mask of 64 bits.
-sv sel25519(gf p,gf q,int b)
+sv sel25519(gf p,gf q,i64 b)
{
@@ For-loop indexes have to be int.
- i64 t,i,c=~(b-1);
+ int i;
+ i64 t,c=~(b-1);
FOR(i,16) {
t= c&(p[i]^q[i]);
p[i]^=t;
@@ -294,9 +292,10 @@
sv pack25519(u8 *o,const gf n)
{
@@ For-loop indexes have to be int.
@@ b is a 64 bit mask.
@@ Initialize m to simplify verification.
- int i,j,b;
- gf m,t;
- FOR(i,16) t[i]=n[i];
+ int i,j;
+ i64 b;
+ gf t,m={0};
+ set25519(t,n);
car25519(t);
car25519(t);
car25519(t);
@@ -307,9 +306,9 @@
m[i-1]&=0xffff;
}
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
- b=(m[15]>>16)&1;
m[14]&=0xffff;
@@ Computations in arguments
@@ are not allowed in VST.
- sel25519(t,m,1-b);
+ b=1-((m[15]>>16)&1);
+ sel25519(t,m,b);
}
FOR(i,16) {
o[2*i]=t[i]&0xff;
@@ -329,7 +328,7 @@
{
u8 d[32];
pack25519(d,a);
@@ Force the casting.
- return d[0]&1;
+ return d[0]&(u8)1;
}
sv unpack25519(gf o, const u8 *n)
@@ -353,10 +352,14 @@
sv M(gf o,const gf a,const gf b)
{
@@ For-loop indexes have to be int.
@@ introduce an auxiliary variable to
@@ simplify verification (loop invariants).
- i64 i,j,t[31];
- FOR(i,31) t[i]=0;