Commit 3251f5af authored by Benoit Viguier's avatar Benoit Viguier
Browse files

bck

parent cc7d9014
\documentclass{article}
\usepackage{geometry}
\geometry{
a4paper,
total={190mm,257mm},
left=10mm,
top=20mm,
}
\usepackage{epsfig}
\usepackage{setup}
\input{macros}
\begin{document}
Generic definition of the ladder:
\begin{lstlisting}[language=Coq]
(* Define a typeclass to encapsulate the operations *)
Class Ops (T T': Type) (Mod: T -> T):=
{
+ : T -> T -> T; (* Add *)
* : T -> T -> T; (* Mult *)
- : T -> T -> T; (* Sub *)
x^2 : T -> T; (* Square *)
C_0 : T; (* Const 0 *)
C_1 : T; (* Const 1 *)
C_121665: T; (* const (a-2)/4 *)
Sel25519: Z -> T -> T -> T;(* CSWAP *)
Getbit: Z -> T' -> Z; (* ith bit *)
}.
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *)
(* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *)
let a := a - c in (* B = x_2 - z_2 *)
let c := b + d in (* C = x_3 + z_3 *)
let b := b - d in (* D = x_3 - z_3 *)
let d := e ^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 --- (1/2) *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 --- (1/3) *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 --- (2/3) *)
let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in (* z_2 = E * (AA + a24 * E) --- (1/3) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) --- (2/3) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) --- (3/3) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 --- (3/3) *)
let b := e ^2 in (* x_3 = (DA + CB)^2 --- (2/2) *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x
end.
Definition get_a (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => a
end.
Definition get_c (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => c
end.
\end{lstlisting}
\newpage
Instanciation of the Class \Coqe{Ops} with operations over $\Z$ and modulo \p.
\begin{lstlisting}[language=Coq]
Definition modP x := Z.modulo x (Z.pow 2 255 - 19).
(* Encapsulate in a module. *)
Module Mid.
Definition getCarry (m:Z) : Z := Z.shiftr m n.
Definition getResidue (m:Z) : Z := m - Z.shiftl (getCarry m) n.
Definition car25519 (n:Z) : Z := 38 * getCarry 256 n + getResidue 256 n.
(* The carry operation is invariant under modulo *)
Lemma Zcar25519_correct: forall n, n:GF = (Mid.car25519 n) :GF.
(* Define Mid.A, Mid.M ... *)
Definition A a b := Z.add a b.
Definition M a b := Mid.car25519 (Mid.car25519 (Z.mul a b)).
Definition Zub a b := Z.sub a b.
Definition Sq a := M a a.
Definition C_0 := 0.
Definition C_1 := 1.
Definition C_121665 := 121665.
Definition Sel25519 (b p q:Z) := if (Z.eqb b 0) then p else q.
Definition getbit (i:Z) (a: Z) :=
if (Z.ltb a 0) then
0
else
if (Z.ltb i 0) then
Z.land a 1
else
Z.land (Z.shiftr a i) 1.
End Mid.
Definition ZPack25519 n :=
Z.modulo n (Z.pow 2 255 - 19).
Definition Zclamp (n : Z) : Z :=
(Z.lor (Z.land n (Z.land (Z.ones 255) (-8))) (Z.shiftl 64 (31 * 8))).
(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z := Z.pow x (Z.pow 2 255 - 21).
(* instantiate over Z *)
Instance Z_Ops : (Ops Z Z modP) := {}.
Proof.
apply Mid.A. (* instantiate + *)
apply Mid.M. (* instantiate * *)
apply Mid.Zub. (* instantiate - *)
apply Mid.Sq. (* instantiate x^2 *)
apply Mid.C_0. (* instantiate Const 0 *)
apply Mid.C_1. (* instantiate Const 1 *)
apply Mid.C_121665. (* instantiate (a-2)/4 *)
apply Mid.Sel25519. (* instantiate CSWAP *)
apply Mid.getbit. (* instantiate ith bit *)
Defined.
(* instantiate montgomery_rec with Z_Ops *)
Definition ZCrypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
\end{lstlisting}
\newpage
\begin{lstlisting}[language=Coq]
Definition Crypto_Scalarmult n p :=
let t := (montgomery_rec 255
(clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1
Low.C_0 Low.C_0 (Unpack25519 p)) in
let a := get_a t in
let c := get_c t in
Pack25519 (Low.M a (Inv25519 c)).
Definition CSM := Crypto_Scalarmult.
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p ->
ZofList 8 (Crypto_Scalarmult n p) =
ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
\end{lstlisting}
\end{document}
This diff is collapsed.
TEX := $(wildcard *.tex)
FILES := $(TEX) $(wildcard tikz/*.tex) $(wildcard *.sty)
tweetverif.pdf: FORCE $(FILES) collection.bib
./latexrun.py tweetverif.tex
depend:
@echo $(FILES)
.PHONY: clean FORCE
clean:
@echo cleaning...
@rm -fr latex.out 2> /dev/null || true
@rm *.pdf 2> /dev/null || true
@rm *.aux 2> /dev/null || true
@rm *.bbl 2> /dev/null || true
@rm *.blg 2> /dev/null || true
@rm *.brf 2> /dev/null || true
@rm *.dvi 2> /dev/null || true
@rm *.fdb_latexmk 2> /dev/null || true
@rm *.fls 2> /dev/null || true
@rm *.log 2> /dev/null || true
@rm *.out 2> /dev/null || true
@rm */*.aux 2> /dev/null || true
spell:
for f in $(TEX) ; do \
aspell -t -c $$f; \
done
% \subsection*{Abstract}
\begin{abstract}
In this paper we formally prove that the C implementation of
X25519 key exchange in the TweetNaCl library matches
the mathematical definition of X25519 from Bernstein's 2006 paper.
The proof is computer-verified using the Coq theorem prover.
To establish the link between C and Coq we use the
Verified Software Toolchain (VST).
\end{abstract}
#!/usr/bin/env python3
import os
import sys
import re
import argparse
config = {}
# Cf manual of bibtex: https://ctan.org/pkg/bibtex
# in short: https://nwalsh.com/tex/texhelp/bibtx-7.html
BIBTEX = {
# An article from a journal or magazine.
'ARTICLE': [['author', 'title', 'journal', 'year'], ['volume', 'number', 'pages', 'month', 'note']],
# A book with an explicit publisher.
'BOOK': [['author', 'editor', 'title', 'publisher', 'year'], ['volume', 'number', 'series', 'address', 'edition', 'month', 'note']],
# A book with an explicit publisher.
'BOOKLET': [['author', 'editor', 'title', 'publisher', 'year'], ['volume', 'number', 'series', 'address', 'edition', 'month', 'note']],
# An article in a conference proceedings.
'CONFERENCE': [['author', 'title', 'booktitle', 'year'], ['editor', 'volume', 'number','series', 'pages', 'address', 'month', 'organization', 'publisher', 'note']],
# A part of a book, which may be a chapter.
'INBOOK': [['author', 'editor', 'title', 'chapter', 'pages', 'publisher', 'year'], ['volume', 'number', 'series', 'type', 'address', 'edition', 'month', 'note']],
# A book with an explicit publisher.
'INCOLLECTION': [['author', 'title', 'booktitle', 'publisher', 'year'], ['editor', 'volume', 'number', 'series', 'type', 'chapter', 'pages', 'address', 'edition', 'month', 'note']],
# An article in a conference proceedings.
'INPROCEEDINGS': [['author', 'title', 'booktitle', 'year'], ['editor', 'volume', 'number','series', 'pages', 'address', 'month', 'organization', 'publisher', 'note']],
# Technical documentation
'MANUAL': [['title'], ['author', 'organization', 'address', 'edition', 'month', 'year', 'note']],
# A Master’s thesis
'MASTERSTHESIS': [['author', 'title', 'school', 'year'], ['type', 'address', 'month', 'note']],
# Use this type when nothing else fits
'MISC': [[], ['author', 'title', 'howpublished', 'month', 'year', 'note']],
# A PhD thesis
'PHDTHESIS': [['author', 'title', 'school', 'year'], ['type', 'address', 'month', 'note']],
# The proceedings of a conference.
'PROCEEDINGS': [['title', 'year'], ['editor', 'volume', 'number','series', 'address', 'month', 'organization', 'publisher', 'note']],
# A document having an author and title, but not formally published
'TECHREPORT': [['author', 'title', 'institution', 'year'], ['type', 'number', 'address', 'month', 'note']],
# A document having an author and title, but not formally published
'UNPUBLISHED': [['author', 'title', 'note'], ['month', 'year']],
}
def Red(skk): return "\033[38;5;009m {}\033[00m".format(skk)
def Green(skk): return "\033[38;5;010m {}\033[00m".format(skk)
def Yellow(skk): return "\033[38;5;011m {}\033[00m".format(skk)
def Orange(skk): return "\033[38;5;202m {}\033[0m".format(skk)
def LightPurple(skk): return "\033[38;5;177m {}\033[00m".format(skk)
def Purple(skk): return "\033[38;5;135m {}\033[00m".format(skk)
def Cyan(skk): return "\033[38;5;014m {}\033[00m".format(skk)
def LightGray(skk): return "\033[38;5;252m {}\033[00m".format(skk)
def DarkGray(skk): return "\033[38;5;242m {}\033[00m".format(skk)
def debug(t):
if config['debug']:
print(t)
def diagnostic(t):
if config['diagnostic']:
print(t)
def save(fn, z):
d = open(fn, 'w', encoding="utf-8")
d.write(z)
d.close()
def read(fn):
data = '';
with open(fn, 'r', encoding="utf-8") as file:
data = file.read()
return data.split('\n')
## block parsing of the data in the bibtex
def find_end_block(data, i):
if data[i].strip()[:1] == '}':
return i;
if data[i].strip()[:1] == '@':
return -1;
else:
return find_end_block(data, i + 1);
def find_block(data, i, list_block):
if len(data) == i:
return list_block;
if data[i].strip()[:1] == '@':
end = find_end_block(data, i + 1);
if end == -1:
# this is a single line case or there is an error in the bibliography.
list_block.append([i,i])
return find_block(data, i + 1, list_block)
else:
list_block.append([i,end])
return find_block(data, end + 1, list_block)
else:
# we are out of a block, we look for the next @
return find_block(data, i + 1, list_block)
# now that we have the block, let's look at what is the content of each.
def find_subblock_end(block, i):
if len(block) == i:
return i - 1
if block[i][-2:] == '},':
return i
else:
return find_subblock_end(block, i + 1)
def find_subblock(block, i, list_subblock):
if len(block) == i:
return list_subblock;
if block[i] == '':
return find_subblock(block, i+1, list_subblock)
idx = block[i].find('=');
if idx != -1:
idx2 = block[i].find('{');
if idx2 != -1:
end = find_subblock_end(block, i)
else:
end = i
list_subblock.append([i,end,idx])
return find_subblock(block, end+1 , list_subblock)
else:
print(Red("this should not happen"))
return list_subblock;
def find_section(parts, section):
for p in parts:
if p[0] == section:
return p[1]
return 'not found'
def find_section_index(parts, section):
i = 0
for p in parts:
if p[0] == section:
return i
i += 1
return -1
def extract_subblock(block, start, end, eq):
s = slice(start, end + 1, 1)
k = block[s][0][0:eq].strip()
# this is to remove the _ we add for non recognized sections
# this is useful if we want to change the kind: Misc -> article etc...
if k[:1] == '_':
k = k[1:]
c = ' '.join(block[s])[eq+1:].strip()
if c[-1:] == ',':
c = c[:-1]
c = re.sub(' +', ' ',c)
debug((k,c))
return [k,c]
def parse(block, output):
debug(DarkGray('--------------------------------'))
i = block[0].find('{')
kind = block[0][1:i]
debug(DarkGray(kind))
referer = block[0][i+1:-1]
debug(DarkGray(referer))
sub_blocks = find_subblock(block,1,[])
debug(DarkGray(sub_blocks))
sections = []
for sub in sub_blocks:
sections.append(extract_subblock(block, sub[0], sub[1], sub[2]))
output.append({'kind': kind, 'referer': referer, 'sections': sections})
# differenciate the onliners from the actual blocks
def parse_blocks(list_block, content, oneliners, blocks):
temp_block = []
for cut in list_block:
if cut[0] == cut[1]:
oneliners.append(content[cut[0]])
else:
s = slice(cut[0], cut[1], 1)
temp_block.append(content[s]);
debug(DarkGray('++++++++++++++++++++++++++++++++'))
for b in temp_block:
parse(b, blocks)
debug(DarkGray('++++++++++++++++++++++++++++++++'))
def authors(s):
list_authors = s.split(' and ')
out = ''
if len(list_authors) > 0:
out = list_authors[0]
for i in range(1, len(list_authors)):
out += ' and\n'
out += ''.rjust(20) + list_authors[i]
return out
def generate_entry(block, summary):
output = '\n';
kind = block['kind'].upper();
c_kind = Yellow(kind).ljust(13)
referer = block['referer'];
c_referer = Orange(referer).ljust(40)
output += '@{}{{{},\n'.format(kind.lower(),referer)
if kind not in BIBTEX:
print(Red('DROPPED:') + '{} {}'.format(c_kind, c_referer))
else:
diagnostic(c_kind + ' ' + c_referer)
# mandatory blocks:
for i,t in {0: 'mandatory', 1: 'optional'}.items():
diagnostic(DarkGray('{}---------------------------'.format(t.ljust(9,'-'))))
if len(BIBTEX[kind][i]) > 0 and i > 0:
output += '\n'
for s in BIBTEX[kind][i]:
idx = find_section_index(block['sections'], s)
if idx == -1:
diagnostic(Red('field not found:'.ljust(17)) + s)
if i != 1 or config['extend']:
output += ' {:15}= {},\n'.format(s,'{}')
if i == 0 and config['summary']:
summary.append(c_kind + ' ' + c_referer)
summary.append(Red('field not found:'.ljust(17)) + s)
else:
c = block['sections'].pop(idx)[1]
if c == '' or c == '{}':
diagnostic(Red('field not found:'.ljust(17)) + s)
if config['extend']:
output += ' {:15}= {},\n'.format(s,'{}')
if i == 0 and config['summary']:
summary.append(c_kind + ' ' + c_referer)
summary.append(Red('field not found:'.ljust(17)) + s)
else:
diagnostic(Green('field found:'.ljust(17)) + s.ljust(13) + c)
if s == 'author':
c = authors(c)
output += ' {:15}= {},\n'.format(s,c)
if len(block['sections']) > 0:
block['sections'].sort(key=lambda a : a[0])
diagnostic(DarkGray('{}---------------------------'.format('ignored'.ljust(9,'-'))))
output += '\n'
for b in block['sections']:
diagnostic(LightPurple('extra field:'.ljust(17)) + b[0].ljust(13) + b[1])
if not config['purify']:
output += ' _{:14}= {},\n'.format(b[0],b[1])
diagnostic(DarkGray('{}---------------------------'.format('done'.ljust(9,'-'))))
output += '}\n'
return output
def is_not_bib(s):
return s != '' and s[-4:] != '.bib'
def check_bib(s):
if is_not_bib(s):
msg = "%r is not a .bib" % s
raise argparse.ArgumentTypeError(msg)
return s
def chose_file(fn = ''):
while fn == '' or is_not_bib(fn):
if fn != '':
print("{} is not a proper bibtex file".format(fn))
fn = input('Please chose a correct file: ')
return fn
def str2bool(v):
return v.lower() in ("yes", "true", "t", "1", "y")
def parse_arguments():
parser = argparse.ArgumentParser(description='Normalize a decently formatted bibtex.')
parser.add_argument('input', nargs='?', default='', help='input: file.bib', type=check_bib)
parser.add_argument('-o','--output', nargs='?', default='', help='ouput: file.bib', type=check_bib)
parser.add_argument('-v','--verbose', action='store_true', help='enable debugger output')
parser.add_argument('--diagnostic', action='store_true', help='check for missing fields (all)')
parser.add_argument('--no-summary', action='store_true', help='Don\'t check for missing fields (only mandatory)')
parser.add_argument('--extend', action='store_true', help='if a field is missing, add it to the generated bibtex.')
parser.add_argument('-p','--purify', action='store_true', help='extra fields are stripped from the generated bibtex.')
parser.add_argument('-i','--interactive', action='store_true', help='Interactive.')
parser.add_argument('-y','--yes', action='store_true', help='Override Interactive and select default answer.')
parser.add_argument('-dr','--dry-run', action='store_true', help='Dry-run.')
args = parser.parse_args()
# print(args)
interactive = args.interactive or args.input == ''
if not interactive:
config['debug'] = args.verbose
config['diagnostic'] = args.diagnostic
config['summary'] = not args.no_summary
config['extend'] = args.extend
config['purify'] = args.purify
config['input'] = args.input
config['output'] = args.output if args.output != '' else args.input
config['dry_run'] = args.dry_run
debug(args)
debug(config)
return
# we are in interactive mode
# are we in YES mode ?
# 1. do we have a file name ?
fn = ''
bibfiles = [x for x in os.listdir('.') if x[-4:] == '.bib']
if args.input != '':
fn = args.input
elif len(bibfiles) == 1:
fn = bibfiles[0]
if args.yes and fn != '':
config['input'] = fn
elif args.yes and fn == '':
print(Red("Could not select automatically the bibtex file."))
elif fn != '':
tmp = input('Input file [{}]: '.format(fn))
if tmp == '':
config['input'] = fn
else:
config['input'] = chose_file(tmp)
elif len(bibfiles) > 2:
fn = input('Multiple bibtex files found, please chose: '+', '.join(bibfiles))
config['input'] = chose_file(fn)
else:
fn = input('No bibtex files found, please enter a file name: ')
config['input'] = chose_file(fn)
if args.yes:
config['debug'] = args.verbose
config['diagnostic'] = args.diagnostic
config['summary'] = not args.no_summary
config['extend'] = args.extend
config['purify'] = args.purify
config['output'] = args.output if args.output != '' else config['input']
config['dry_run'] = args.dry_run
else:
v = args.verbose
tmp = input('Enable verbose mode [{}]? '.format('Y/n' if v else 'y/N'))
config['debug'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
v = args.diagnostic
tmp = input('Enable Diagnostics [{}]? '.format('Y/n' if v else 'y/N'))
config['diagnostic'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
v = not args.no_summary
tmp = input('Enable Summary [{}]? '.format('Y/n' if v else 'y/N'))
config['summary'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
v = args.extend
tmp = input('Add missing field [{}]? '.format('Y/n' if v else 'y/N'))
config['extend'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
v = args.purify
tmp = input('Remove unnecessary fields [{}]? '.format('Y/n' if v else 'y/N'))
config['purify'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
v = args.dry_run
tmp = input('Dry-run [{}]? '.format('Y/n' if v else 'y/N'))
config['dry_run'] = str2bool(tmp if tmp != '' else ('Y' if v else 'n'))
fn = args.output if args.output != '' else config['input']
fn = input('Output file [{}]:'.format(fn))
if fn == '':
fn = config['input']