Programming Between Math and Machines

Programming Between
Math and Machines

Reasoning about Cryptographic Programs with Fixed-Width IMP

$(a + b)\cdot c$

+ 1

$\langle 255 + 1\rangle_{8} = 0$

Genie comic: 'I wish I had 0 wishes' — 'You have 4,294,967,295 wishes left'

wishes := 0;
wishes := wishes − 1

$\langle 0 - 1\rangle_{32} = 4{,}294{,}967{,}295$

Comic: programmerhumor.io/programming-memes/genie-overflow-bsgo

Ariane 51996

64-bit float → 16-bit integer. The value didn't fit.

Lost 37 s after launch · ≈ $370M

184,467,440,737

bitcoin, from nothing

Bitcoin2010

Two huge outputs summed in a 64-bit integer. The sum wrapped and passed the check.

Cap: 21 million · patched in 5 h

Boeing 7872015

A 32-bit counter overflows after 248 days of continuous power.

All AC power lost · FAA directive

Ariane 501 Inquiry Board Report (ESA/CNES, 1996) · Bitcoin Wiki, “Value overflow incident” (CVE-2010-5139) · FAA AD 2015-09-07, Federal Register 2015-10066
Photos: ESA–CNES–Arianespace / JM Guillon (CC BY 4.0) via Wikimedia Commons · KLM 787-9 at Schiphol, Wikimedia Commons (public domain)

Experts write code

→

Public code

→

LLMs learn

→

LLMs write code

It is human to make errors.
But then, how can we trust code?

Pearce et al., Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions

“…given the vast quantity of unvetted code that Copilot has processed, it is certain that the language model will have learned from exploitable, buggy code.”

≈ 40%

of 1,689 generated programs
were vulnerable

H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, R. Karri. Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions. IEEE S&P 2022

How do we trust code,
no matter who wrote it?

Math

FIMP

C

reason about it

✓

✗

run it fast

✗

✓

Best of both worlds, in a limited context.

$\mathbb{F}_{251}$

$\{0, 1, \dots, 250\}$ with $+$ and $\cdot$ modulo 251

$251$ is prime $\;\Longrightarrow\;$ every $x \neq 0$ has an $x^{-1}$ with $x \cdot x^{-1} \equiv 1 \pmod{251}$

$251 < 2^8$, so every element fits in one byte

$70 \cdot 40 = 2800 = 11 \cdot 251 + 39 \quad\Longrightarrow\quad 70 \cdot 40 \equiv 39 \pmod{251}$

$\mathrm{Enc}_k(x) = k \cdot x \bmod 251 \qquad\qquad \mathrm{Dec}_k(c) = k^{-1} \cdot c \bmod 251$

$k = 40,\quad k^{-1} = 182 \qquad\text{since}\qquad 40 \cdot 182 = 7280 = 29 \cdot 251 + 1$

specification

$\forall x \in \mathbb{F}_{251}.\quad \mathrm{Dec}_k(\mathrm{Enc}_k(x)) = x$

\[\begin{aligned} \mathrm{Dec}_k(\mathrm{Enc}_k(x)) &\equiv k^{-1} \cdot (k \cdot x) \\ &\equiv (k^{-1} \cdot k) \cdot x \\ &\equiv x \pmod{251} \end{aligned}\]

Both sides lie in $\{0, \dots, 250\}$, so they are equal.

$K, X, C : \mathsf{w8}$

C := K × X

$\sigma'(C) = \langle \sigma(K) \cdot \sigma(X) \rangle_8 = \sigma(K) \cdot \sigma(X) \bmod 2^8$

$\langle 40 \cdot 70 \rangle_8 = 2800 - 10 \cdot 256 = 240$

$240 \neq 39$

lemma

For $0 \le Z < 2^{16}$, let $H = \lfloor Z / 2^8 \rfloor$ and $L = Z \bmod 2^8$. Then

$Z \equiv 5H + L \pmod{251}$

$Z = 2^8 H + L = 251\,H + (5H + L)$

$\langle Z \gg 8, \sigma \rangle \to \lfloor Z / 2^8 \rfloor = H$

$\langle Z \mathbin{\&} 255, \sigma \rangle \to Z \bmod 2^8 = L$

$Z \;\longmapsto\; 5 \cdot (Z \gg 8) + (Z \mathbin{\&} 255)$

$X, Y, R : \mathsf{w8} \qquad Z : \mathsf{w16}$

1Z := (w16) X × (w16) Y;
2while ¬(Z ≫ 8 = 0) do
3  Z := 5 × (Z ≫ 8) + (Z & 255);
4R := (w8) Z;
5if 251 ≤ R then R := R − 251

theorem

For all $X, Y \in \mathbb{W}_8$, the program terminates with $R = X \cdot Y \bmod 251$.

Line 1

$X \cdot Y \le 255^2 = 65025 < 2^{16}$, so $Z = \langle X \cdot Y \rangle_{16} = X \cdot Y$

Invariant

$Z \equiv X \cdot Y \pmod{251} \;\wedge\; Z < 2^{16}$

Line 3

$5H + L \le 5 \cdot 255 + 255 = 1530 < 2^{16}$, so nothing wraps, and $5H + L \equiv Z$ by the lemma

Termination

while $H > 0$: $\;5H + L < 2^8 H + L = Z$, so $Z$ strictly decreases

Lines 4–5

on exit $H = 0$, so $R = Z \le 255 < 2 \cdot 251$; subtracting 251 at most once gives $R \in [0, 251)$

C  := mul(40, X);
X' := mul(182, C)

$X' = 182 \cdot (40 \cdot X \bmod 251) \bmod 251 = X \qquad \text{for all } X < 251$

The FIMP program meets the specification.

$c_1$

Z := (w16) X × (w16) Y;
while ¬(Z ≫ 8 = 0) do
  Z := 5 × (Z ≫ 8) + (Z & 255);
R := (w8) Z;
if 251 ≤ R then R := R − 251

≡ ?

$c_2$

Z := (w16) X × (w16) Y;
Z := 5 × (Z ≫ 8) + (Z & 255);
Z := 5 × (Z ≫ 8) + (Z & 255);
Z := 5 × (Z ≫ 8) + (Z & 255);
T := Z − 251;
Z := T + (T ≫ 15) × 251;
R := (w8) Z

$Z_0 \le 65025$

$\Rightarrow$

$H \le 254$

$\Rightarrow$

$Z_1 \le 5 \cdot 254 + 255 = 1525$

$Z_1 \le 1525$

$\Rightarrow$

$H \le 5$

$\Rightarrow$

$Z_2 \le 5 \cdot 5 + 255 = 280$

$Z_2 \ge 256$

$\Rightarrow$

$H = 1,\ L \le 24$

$\Rightarrow$

$Z_3 \le 5 + 24 = 29$

$Z_2 \le 255$

$\Rightarrow$

$H = 0$

$\Rightarrow$

$Z_3 = Z_2 \le 255$

When $H = 0$, a fold is the identity: $\;5 \cdot 0 + L = L = Z$

all $\mathsf{w16}$, $\;Z \le 255$

T := Z − 251;
Z := T + (T ≫ 15) × 251

$Z \ge 251:\quad T = Z - 251 < 2^{15} \;\Rightarrow\; T \gg 15 = 0 \;\Rightarrow\; Z := Z - 251$

$Z < 251:\quad T = 2^{16} + Z - 251 \ge 2^{15} \;\Rightarrow\; T \gg 15 = 1 \;\Rightarrow\; Z := \langle T + 251 \rangle_{16} = Z$

$E:\ \ y^2 = x^3 - x + 1$

$P + Q = R$, all arithmetic in $\mathbb{F}_p$

$\lambda = (y_Q - y_P)\cdot $$(x_Q - x_P)^{-1}$

$x_R = \lambda^2 - x_P - x_Q$

$y_R = \lambda\,(x_P - x_R) - y_P$

251

$2^{255} - 19$

Curve25519: $\ y^2 = x^3 + 486662\,x^2 + x$

D. J. Bernstein, Curve25519: new Diffie-Hellman speed records, PKC 2006 · RFC 7748 (2016)

x4  = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * UINT8_C(0x13)));
x7  = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13)));
x9  = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13)));
x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13)));
x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0]));
x26 = (x25 + (x10 + (x9 + (x7 + x4))));
x27 = (uint64_t)(x26 >> 51);
x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff));

▼

$A_i, B_i : \mathsf{w64} \qquad X_4, \dots, X_{26} : \mathsf{w128} \qquad X_{27}, X_{28} : \mathsf{w64}$

X4  := (w128) A4 × (w128) (B1 × 19);
X7  := (w128) A3 × (w128) (B2 × 19);
X9  := (w128) A2 × (w128) (B3 × 19);
X10 := (w128) A1 × (w128) (B4 × 19);
X25 := (w128) A0 × (w128) B0;
X26 := X25 + (X10 + (X9 + (X7 + X4)));
X27 := (w64) (X26 ≫ 51);
X28 := (w64) (X26 & (2⁵¹ − 1))

github.com/mit-plv/fiat-crypto · fiat-c/src/curve25519_64.c · fiat_25519_carry_mul

$a \cdot b \ \ \text{in}\ \ \mathbb{Z}_q[x]/(x^{256} + 1), \qquad q = 3329$

Multiplication, but faster.

$O(n^2) \;\longrightarrow\; O(n \log n)$

NIST FIPS 203, Module-Lattice-Based Key-Encapsulation Mechanism Standard (ML-KEM, 2024)

void ntt(int16_t r[256]) {  unsigned int len, start, j, k;  int16_t t, zeta;  k = 1;  for(len = 128; len >= 2; len >>= 1) {    for(start = 0; start < 256; start = j + len) {      zeta = zetas[k++];      for(j = start; j < start + len; j++) {        t = fqmul(zeta, r[j + len]);        r[j + len] = r[j] - t;        r[j] = r[j] + t;      }    }  }}

Can we rewrite this?

github.com/pq-crystals/kyber · ref/ntt.c

t = fqmul(zeta, r[j + len]);

▼

all $\mathsf{w64}$, $\ Z, B < 3329$

T := Z × B;
T := T − ((T × 20158) ≫ 26) × 3329;
T := T − 3329;
T := T + (T ≫ 63) × 3329

github.com/pq-crystals/kyber · ref/ntt.c. The FIMP version uses unsigned Barrett reduction; the reference code uses signed Montgomery reduction.

Write it like a machine. Reason about it like math.