Verification
Verification: the study of showing how something works as designed.
The discipline considers “worst cases” by design.

Lower-level Verifications for Cryptographic Software◮

involving Elliptic Curves and others◮

Tries to show that there are no failure possiblities; andideally identifies possible failures if we cannot verify correctness.

The most well-established application of verification is in chip design.
We will apply it to cryptographic software.

Bo-Yin Yang

Verification in Practice

Academia Sinica

Usually carried out with
ECC 2018, November 20, Osaka

Proof Assistants, such as Coq
Satisfiability Module Theory (SMT) and SAT solvers, e.g. Minisat.
◮ Specifically designed tools◮◮

We will use SAT solvers and some home-brewed tools

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

1 / 42Cryptography and Its Software as a Subject of Study I

Verifying Lower-Level Crypto

2018.11.20

2 / 42Cryptography and Its Software as a Subject of Study II

The sophisticated mathematical structures in modern cryptography
often require complicated arithmetic computation over large numbers.

Cryptography has lots of real world applications from private
communication to digital currency.
Similar to formal verification, cryptography necessarily expects theworst scenario.

In RSA, modulo arithmetic over n = pq where p, q are prime.
In NIST P-256, modular arithmetic over 2256 − 2224 + 2192 + 296 − 1.
◮ In Curve25519, modular arithmetic over 2255 − 19.

◮◮

Modern cryptography uses much sophisticated, complex mathematicalstructures.
Secure cryptosystems must be designed and analyzed thoroughly.
◮

Bo-Yin Yang (Academia Sinica)

Commodity computers only support up to 64-bit integers.
◮

This makes the program even more complicated.

There is little room for trial and error in cryptography.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

3 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

4 / 42

Cryptography and Its Software as a Subject of Study III

An Ideal Research Problem for Verification

To make cryptography practical, cryptographers must design
cryptosystems for security and efficiency.
Parameters are chosen for efficiency, not for a reader’s understanding.
Reduction in GF (2256 − 2224 + 2192 + 296 − 1), performed throughbitwise masking and shifting (NIST P-256);◮ Reduction in GF (2255 − 19) performed by bitwise shifting andmultiplication (X25519).
◮

Moreover, practical cryptographers do appreciate verification.
◮

Not many cryptographers also program assembly language well.

Verifying Lower-Level Crypto

2018.11.20◮

5 / 42

Challenges I

Cryptographic assembly programs perform such computation in
hundreds of bits.

Verifying Lower-Level Crypto

2018.11.20

6 / 42In NIST P-256, modular multiplication is overGF (2256 − 2224 + 2192 + 296 − 1) (256 bits).
◮ In X25519, modular multiplication is over GF (2255 − 19) (255 bits).
◮

For cryptographic assembly programs, every bit and flag count.

Since numbers are different, reduction is computed differently.

Assembly programs are very succinct.
◮

Bo-Yin Yang (Academia Sinica)

An algorithm has different instantiations on different mathematicalstructures.
Consider, say, modular multiplication.

Such programs must be proven correct for all inputs.
◮

Many computer scientists know of OpenSSL.

Challenges II

Verifying non-linear computation is hard.
◮

See comments in OpenSSL

Colleagues recognize the importance of verification when informed ofthis work.

OpenSSL and boringSSL.

Bo-Yin Yang (Academia Sinica)

critical
indispensable◮ complex◮ highly visible◮◮

To attain the best performance, primitive cryptographic algorithms
are even often implemented in assembly.
◮

Not all programs need to be verified.
However, cryptographic programs are◮

Abstraction is unlikely to work.

◮

In NIST P-256, it is implemented by bitwise masks and shifts.
In X25519, it is implemented by bitwise shifts and multiplication.

Each instantiation must be verified.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

7 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

8 / 42

Challenges III

Related Work

Algorithm instance implement differently on different architectures.
Different architectures (x86, ARM) have different instruction sets.

Fiat (MIT) is a C program synthesis tool for cryptographic programs.

Different generations of x86 64 have slightly different instructions.
In OpenSSL, two different implementations for modular multiplication
are available.

Jasmin (INRIA) is a portable assembly language with formal
semantics.

◮

In Broadwell microarchitecture, it is possible to perform two threads ofaddition simultaneously with adox.

Vectorized instructions are also widely used.
◮

HACL* (INRIA) is a verified cryptographic library in F∗ .
Vale (Microsoft Research) is a framework to write correct assembly
programs for different architectures.
None of them really addresses the cryptographic assembly program
verification problem.

OpenSSL has 3 Poly1305 implementations (sequential, avx, avx2).

All implementations need to be verified.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

9 / 42Previous Work

Verifying Lower-Level Crypto

2018.11.20

10 / 42

The gfverif Project

Our first idea is to verify cryptographic assembly programs by
SMT/SAT solvers via bit blasting.
In 2014, we use Boolector to verify an academic implementationof modular multiplication in X25519.
It took 4 days (without annotation) or 5 hours (with extensive manual
annotation).
◮ Moreover, we had to prove a simple mathematical property in Coq.
◮

In 2015, Daniel J. Bernstein and Peter Schwabe announces theirgfverif project.
Their tool verifies algebraic properties of C programs using acomputer algebra system.
Idea:
◮
◮

Verifying a hundred of assembly instructions in 4 days is perhaps
better than using proof assistants.

◮

Verifying Lower-Level Crypto

2018.11.20

Translate a C program and its specification to an algebraic problem;
Solve the algebraic problem by a computer algebra system.

It sounds reasonable.

Not very useful!

Bo-Yin Yang (Academia Sinica)

Bo-Yin Yang (Academia Sinica)

11 / 42

Why do we use SMT/SAT solvers to solve algebraic problems?

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

12 / 42

An Almost Certified Automatic Verification Tool

More Recent WorkIn 2017, we extend the idea of gfverif to assembly programs andcertify algebraic results with Coq.
Unfortunately, results from SMT/SAT solvers are yet to be certified.
◮

Efficient certification implies P = coNP.

This tool verifies the same academic implementation of modular
multiplication in 1.5 minutes without annotation.
It also verifies an academic implementation of Montgomery ladderstep(about 1300 instructions) in 5.5 days.
◮

Montgomery ladderstep is used in elliptic curve point operations.

We further optimize our tool.
We verify industrial implementations in OpenSSL and boringSSL.
We verify the OpenSSL multi-precision Montgomery modular
multiplication for RSA, and its implementation for NIST P-256.
We also verify the boringSSL Montgomery ladderstep implementation
for X25519.
◮

We also decide not to certify the tool.

It is probably useful.

◮suitable for production release, not for daily development◮ not industrial implementation◮ we translated from qhasm (X25519), so not many instances◮

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

13 / 42

Bo-Yin Yang (Academia Sinica)

◮

◮

◮

the modeling language for cryptographic assembly programs
the specification language for functional properties◮ the verification algorithm

We also provide a tool chain to
extract assembly programs from execution
translate assembly programs into the modeling language

The tool chain enables us to produce models for verification quickly.
It is essential to tool adoption.

14 / 42

Flags must be specified explicitly.
◮

Bo-Yin Yang (Academia Sinica)

2018.11.20

bvAssign (assignment)
bvAdd, bvAddC, bvAdc, bvAdcC (addition)◮ bvSub, bvSubC, bvSub, bvSbbC(subtraction)◮ bvMul, bvMulf (multiplication)◮ bvShl, bvConcatShl (left shift)◮ bvSplit (splitting)◮ bvCmove (condition move)◮ bvAssert, bvAssume (assertion and assumption)◮◮

Verifying Lower-Level Crypto

CryptoLine covers common assembly instructions used in
cryptographic programs.

The CryptoLine tool consists of three parts:◮

Main reason: lack of manpower.

The CryptoLine Modeling Language I

CryptoLine◮

Previously, we only verify an academic implementation for X25519.

Verifying Lower-Level Crypto

2018.11.20

15 / 42

Missing flags induce under- or over-flow checks (bvAdd and bvSub).

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

16 / 42The CryptoLine Modeling Language II

The CryptoLine Specification Language I

Special instructions are added for modeling purposes.
bvConcatShl (concatenate then shift), Split (split into parts), bvCmove(conditional move)◮ more about this in case study◮

Instructions for verification are available.

The CryptoLine specification language specifies a conjunction ofrange and algebraic properties:

bvAssert and bvAssume

Range properties: E < E ′ or E ≤ E ′ .
◮ Algebraic properties: E = E ′ or E ≡ E ′ mod E ′′ .

There is no branching instruction.

We also add syntactic sugar for common expressions.

◮◮

In practical cryptography, running time is a side channel.
◮ Cryptographic programs need be data-independent (called
constant-time).
◮ Secret-Dependent Branches are not allowed.
◮

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto◮

2018.11.20

17 / 42

The CryptoLine Specification Language II

For instance, [c0 : c1 : · · · : ck ] stands for

Bo-Yin Yang (Academia Sinica)

MUL([r0 : r1 : r2 : r3 : r4 ], [a0 : a1 : a2 : a3 : a4 ], [b0 : b1 : b2 : b3 : b4 ])r0 < 252 ∧ r1 < 252 ∧ r2 < 252 ∧ r3 < 252 ∧ r4 < 252
∧
∧
52
104
(a0 + a1 · 2 + a2 · 2+ a3 · 2156 + a4 · 2208 ) × (b0 + b1 · 252 + b2 · 2104 + b3 · 2156 + b4 · 2208 ) ≡
52
104
156
208
+ r3 · 2+ r4 · 2
mod (2255 − 19)
r0 + r1 · 2 + r 2 · 2

2018.11.20

18 / 42)2018.11.20

19 / 42{Prng }
C
{Qrng }

Boolector{Palg }
C
{Qalg }

Singular{Prng ∧
∧Palg }
C
{Qrng ∧
∧Qalg }

Notice that 256-bit numbers are divided into 5 51-bit limbs.

Verifying Lower-Level Crypto

Verifying Lower-Level Crypto

Here is the CryptoLine verification algorithm:

a 0 < 2 ∧ a1 < 2 ∧ a 2 < 2 ∧ a 3 < 2 ∧ a4 < 2 ∧b0 < 252 ∧ b1 < 252 ∧ b2 < 252 ∧ b3 < 252 ∧ b4 < 252∧∧⊤

Bo-Yin Yang (Academia Sinica)

64·i.
i=0 ci × 2

Hybrid Verification Technique

For instance, the multiplication in X25519 is specified by
(
)
52
52
52
52
52

(

Pk

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

20 / 42

Verifying Range Specifications

Verifying Algebraic Specifications I

CryptoLine translates a program and its range specification to a
formula in the SMT quantifier-free bit vector theory.
The formula is unsatisfiable iff the program fulfills its range
specification.

A set I ⊆ Z[x0 , x1 , . . . , xn ] is an ideal if f + g , p · f ∈ I for every
f , g ∈ I and p ∈ Z[x0 , x1 , . . . , xn ].
◮ Given an ideal I and a polynomial p ∈ Z[x0 , x1 , . . . , xn ], the ideal
membership problem asks if p ∈ I .
◮

We use Boolector to check the satisfiability of the formula.
Boolector+Minisat works better for most cases.
A handful of cases need Boolector+Lingeling.

p ∈ I implies the program fulfills its algebraic specification.

Both Boolector and Z3 fail for a number of realistic assembly
programs.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

CryptoLine first checks there is no overflow using SMT/SAT.
It then translates a program and its algebraic specification to the ideal
membership problem.

We use Singular to solve the ideal membership problem.

21 / 42

Verifying Algebraic Specifications II

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

22 / 42

Verification Flow
Here are the verification steps:
1

To see how it works, consider a system of polynomial equations
fi (x) = 0 derived from assembly instructions.
◮⋆2

For instance, mul %rcx translates to%rdx ′ × 264 + %rax ′ = %rax × %rcx.

g (x) =

Pi hi (x)fi (x) = 0 for any x such that

V

3
4

5
6

Verifying Lower-Level Crypto

2018.11.20

23 / 42More about this later.

Run the tool.
⋆

Bo-Yin Yang (Academia Sinica)

to bvdsl.py ecp nistz256 mul mont.gas >ecp nistz256 mul mont.cl

Manually add pre- and post-conditions.
Manually tune the CryptoLine program to match semantics.
⋆

7

itrace.py a.out ecp nistz256 mul mont >ecp nistz256 mul mont.gas

Manually add x86 64 to CryptoLine translation rules.
Apply the translation rules.
⋆

i fi (x) = 0.

gcc ecp nistz256 mul.c $OPENSSLDIR/libcrypto.a

Extract execution trace.
⋆

Suppose we want to prove an equality g (x) = 0.
V
Formally, we want to show ∀x. i fi (x) = 0 =⇒ g (x) = 0.
Then
V g (x) ∈ hf1 (x), f2 (x), . . . , fk (x)i implies∀x. i fi (x) = 0 =⇒ g (x) = 0.
◮Compile into a standalone program.

cv.native ecp nistz256 mul mont.cl

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

24 / 42Current Requirements

Translation Rules

The Python script to bvdsl.py translates x86 64 assembly to
CryptoLine by rules provided by users.
All available for stock Ubuntu server install.
O’Caml Package Manager (opam)

Consider the following rule:
mov $1v, $2v -> bvAssign $2v (bvVar $1v)

With O’Caml 4.07.0◮ With lwt, lwt ppx, num packages◮

It translates mov %rbp, %rax to bvAssign rax (bvVar rbp).
Here is another rule:

Singular version 4

add $1v, $2v -> bvAddC carry $2v (bvVar $1v) (bvVar $2v)

Boolector-3.0.0 with Lingeling, Minisat, Edical.

It translates add %rax, %r9 to bvAddC carry r9 (bvVar rax)
(bvVar r9).
Most assembly instructions are thus translated automatically.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

25 / 42

Fine Tune

Bo-Yin Yang (Academia Sinica)

Consider the fragment:
mov %r8, %rbp
shl $0x20, %r8
shr $0x20, %rbp

OpenSSL

What it does is to assign◮

2018.11.20

26 / 42

Evaluation on a 2.8GHz Broadwell Xeon
library◮

Verifying Lower-Level Crypto

the high 32 bits of old %r8 to the low 32 bits of %rbp; andthe low 32 bits of old %r8 to the high 32 bits of %r8.

boringSSL

Manual translation is needed.
Here is the correct translation:
bvSplit rbp r8 (bvVar r8) 32;
bvShl r8 (bvVar r8) 32;
Only 4 manual translations are needed in ecp nistz256 mul mont.

mbedTLS

programecp nistz256 add
ecp nistz256 sub
ecp nistz256 from mont
ecp nistz256 mul mont
ecp nistz256 mul mont+
ecp nistz256 mul by 2
ecp nistz256 sqr mont
ecp nistz256 sqr mont+x86 64 mont 2
x86 64 mont 4
x25519 x86 64 mul
x25519 x86 64 sqr
x25519 x86 64 ladderstep
mbedtls mpi mul mpi 2
mbedtls mpi mul mpi 4

ln
89
88
82
192
153
49
148
131
228
490
226
171
1459
76
249

assert0.44
832.608279.87
0.46
12.85

range
4.17
18.54
0.41
21.49
15.43
0.05
16.43
22.50
13.41
523.2728.73
6.14
2921.82
0.42
9.27

alg
0.03
˜0
0.02
0.03
0.03
0.02
0.03
0.03
0.03
0.91
0.03
0.03
107.93
0.03
0.02

total
4.63
18.55
0.45
21.53
15.47
0.08
16.47
22.54
846.058804.06
28.78
6.18
3029.78
0.92
22.16

Time is in seconds; + is for Broadwell architectures
In 2017, X25519 modular multiplication and Montgomery ladderstep
took 90 seconds and 5.5 days respectively.
CryptoLine is useful even for daily development!

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

27 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

28 / 42Recent Activity

Verification of Postquantum Crypto I

Active Research on CryptoLine

Lattice-based encryption schemes

CryptoLine now supports compositional reasoning and ismulti-threaded.
Montgomery ladderstep in boringSSL is verified in 307 seconds.
◮

NTT-based Ring-LWE: Kyber, NewHope
non-NTT based Ring-LWE: NTRU, NTRU Prime
Others: Frodo

was 3029 seconds

For multi-precision Montgomery modular multiplication:NTT-based Ring-LWE

256-bit version is verified in 7.5 seconds (was 8804 seconds).
◮ 1024-bit version is verified in 295 seconds.
◮

Verified n = 256 NTT and inverse NTT (mod 7681) for Kyber.
working ongoing on the similar NewHope

New stuff
We are extending our efforts to postquantum crypto

non-NTT-based Ring-LWE

We are extending verification to compiler intermediate representations

NTRU and NTRU Prime should be doable, under study

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

29 / 42

Verification of Postquantum Crypto II

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

30 / 42

Verification of Compiler Intermediate Representations

Why not Assembly
Other classes of PQC than Lattices with Work in Progress:

We can’t have assembly for every architecture

Multivariates: should be doable, operations in GF (2k ) or small GF (p).
Coding-bases: should be doable, operations in GF (2k ).

For reference implementations, clarity and correctness are more
important than efficiency

Supersingular Isogenies: experience from ECC/RSA valuable?

Similarly for prototypes of algorithms.

Why not C itself?

Not on the docket

Compcert and similar certified compilers are seldom used for
production work.

Hash-based: not our domainStandard compilers (gcc and clang) do strange things to your code.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

31 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

32 / 42clang Strangeness on OpenSSL code I

clang Strangeness on OpenSSL code II
From function fe51 mul in curve25519.c
g2 = (uint64 t)h2 & MASK51;
g2 += (uint64 t)(h1 >> 51);
g3 += g2 >> 51;
g2 &= MASK51;

Taken from https://github.com/openssl/openssl/blob/
OpenSSL 1 1 1-stable/crypto/ec/curve25519.

From fe51 mul121666 in curve25519.c
u128 h2 = f[2] * (u128)121666;
g2 = (uint64 t)h2 & MASK51;
Constant MASK51=0x7FFFFFFFFFFFF

clang IR output
conv109 = trunc h2...
shr122 = lshr i128 h1 51
conv123 = trunc shr122
g2 = and i64 conv109 0x7FFFFFFFFFFFF
add124 = add i64 conv123 g2...
fold = add i64 conv123 conv109
and135 = and i64 fold 0x7FFFFFFFFFFFF

clang Intermediate Representation
h2 = mul i128 f 2 121666;
conv15 = trunc h2;
g2 = and i64 conv15 0x7FFFFFFFFFFFE

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

33 / 42What we have done with clang IR I

Bo-Yin Yang (Academia Sinica)//(uint64 t)h2//(uint64 t)(h1>>51)//g3 += g2>>51

Verifying Lower-Level Crypto

2018.11.20

34 / 42What we have done with clang IR II
programecp nistp224.cfunction
felem diff 128 64
felem difffelem mul reduce
felem mul
felem neg
felem reduce
felem scalar
felem square reduce
felem square
felem sum
widefelem diffwidefelem scalarloc (IR)
30
30
99
60
47
75
15
79
43
22
54
31

modified
×
×
X
×
X
X
×
X
×
×
×
×

time (s)
0.35
0.26
18.10
5.34
0.74
1.40
0.10
16.40
0.97
0.15
0.77
1.19

ecp nistp521.c

felem diff128
felem diff64
felem neg
felem scalar128
felem scalar64
felem scalar
felem sum64
felem reduce
felem diff 128 64
felem mul
felem square

61
61
43
36
35
43
52
144
70
289
158

×
×
×
×
×
×
×
X
×
×
×

0.44
0.50
0.34
0.62
0.21
0.24
0.19
1.81
-

Identify a subset llvmCryptoLine of clang IR in use for crypto
Translate llvmCryptoLine to CryptoLine.
Add assertions and assumptions as needed.
Hand-adjust as needed.
Verify.

Note that the three unverified programs contain anomalies which wesuspect are possible mistakes in range specification.
Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

35 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

36 / 42What we have done with clang IR III
programecp nistp256.c

curve25519.c1function
felem shrink
felem small mul
felem small sum
felem sumsmallfelem mul
smallfelem neg
smallfelem square
fe51 add
fe51 mul121666
fe51 mul
fe51 sqfe51 subx25519 scalar mult1

loc (IR)
63
111
26
22
109
22
70
32
57
124
94
37
1235

Conclusions
modified
X
×
×
×
X
×
X
×
X
X
X
×
X

time (s)
1.33
10.24
0.14
0.14
1.79
0.07
1.80
0.06
0.18
1.88
0.79
0.11
871.00For the first time, we are able to verify industrial low-level
cryptographic programs practically.
◮

5 minutes for 1400 assembly instructions!

This project combines several techniques:◮

SMT/SAT solving and computer algebra

Formal verification and practical cryptography is a perfect match.
◮◮

Practical cryptography needs efficient and correct programs.
Formal verification needs real applications.

Lots of new opportunities in high assurance cryptographic software.

Only the part of Montgomery Ladderstep is verified.

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

37 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

38 / 42Thanks to

My Colleagues at IIS, Sinica
Ming-Hsien Tsai

Thank you for your attention.

Bow-Yaw Wang

Question?

Also must thank these smart people
Jiaxiang Liu and Xiaomu Shi, Shenzhen University
Andy Polyakov, OpenSSL

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

39 / 42

Bo-Yin Yang (Academia Sinica)

Verifying Lower-Level Crypto

2018.11.20

40 / 42