Find all bugs. Repair and verify. Optimize safely.
LibTomMath supplies large-integer arithmetic to Tcl and Dropbear SSH, and is an optional provider for LibTomCrypt. In version 1.2.0, Aristotle found and repaired three bugs, proved the repaired routines against their specifications, and optimized two of them.
Verification exposed missing size checks in fast squaring and Montgomery reduction: an oversized direct call could write past the end of a stack array. A comparison helper could also form a pointer before the start of an array when comparing two equal numbers.
Aristotle added the size checks and rewrote the comparison to use indexes, then proved the repaired routines and the helpers they rely on. Next, it optimized both arithmetic routines and proved them against the same specifications for results, memory safety, errors, and stored values.
The size checks harden internal entry points, since the usual dispatchers already block oversized calls. The comparison bug is reachable with ordinary equal inputs.
The results
LibTomMathC
Faster arithmetic, same proved guarantees
The optimized reduction no longer copies through a temporary array. Squaring reuses each loop to compute two output digits at once. Both keep the proved behavior of the repaired baseline.
31–38%
Faster modular exponentiation in benchmarks
2
Arithmetic routines optimized and proved
3
C bugs repaired
| Modulus size | Repaired baseline | Optimized build | Speedup |
|---|---|---|---|
| 1,024 bits | 722.7 µs | 553.0 µs | 1.31× |
| 2,048 bits | 4,387.1 µs | 3,290.6 µs | 1.33× |
| 3,072 bits | 13,360.5 µs | 9,814.7 µs | 1.36× |
| 4,096 bits | 30,306.4 µs | 21,978.2 µs | 1.38× |
Benchmarks ran on an Intel Xeon Platinum 8375C with GCC 14.2 production flags, odd moduli, 31 interleaved rounds, and an identical baseline build as a control. Individual reduction calls ran about 1.28–2.00× faster, and multi-digit squaring about 1.11–1.23×. Single-digit squaring was effectively unchanged. These figures apply to the measured workloads and configuration.
Check our work in the verified project →
Used in
- Tcl
- Dropbear SSH
- LibTomCrypt
What the proof covers
Same arithmetic
Both routines keep the repaired specifications for results, errors, sign, and stored digits. Squaring also covers in-place calls.
Memory safety
When callers meet their obligations, the optimized routines and the helpers they need avoid undefined behavior and memory leaks, including when allocation fails.
Stated assumptions
x86-64 with 60-bit digits and 128-bit intermediates; initialized, owned buffers; the stated arithmetic conditions; and standard C realloc behavior.
Outside the proof
The proofs cover selected routines and helpers. Full modular exponentiation is benchmarked, not proved. Termination, the rest of the library, and performance are not proved.