Сразу оговорюсь, что обычно я не занимаюсь компьютерной безопасностью и не интересуюсь, а занимаюсь алгоритмами и структурами данных - в прикладном применении это оптимизация быстродействия, высокопроизводительные вычисления типа CUDA, AVX512, многопоточность, что применяется например для майнеров криптовалют. Так я влез в криптоанализ, ибо области, получается, соприкасаются. Был у меня заказ от человека, который хотел очень быстро на видеокартах перемножать 256-битные числа в 512-битные произведения. Я конечно сделал как он хотел, но вот пришла идея: так а зачем перемножать бесчисленное количество чисел, если в принципе можно разложить на множители 512-битное число имея текущие технологии? Об этом дальше и речь.
Дано:
512-битное число
Нету P=NP, но существуют быстрые BSAT солверы типа kissat и cryptominisat5 (второй устанавливается на Ubuntu типа
sudo apt install cryptominisat libcryptominisat5-dev, первый выигрывает соревнования, но ставится из исходников)Linux машина (далее инструкции будут для Ubuntu 24.04)
Программа CBMC (устанавливается
sudo apt install cbmc)Допустим вы собрали из исходников и установили kissat, доступный т.о. как команда по имени
Надо:
Найти два 256-битных числа, чьё произведение (т.е. если их перемножить в длинной арифметике) дают заданное 512-битное число.
Решение.
Во-первых, как мы знаем например из университетского курса криптологии (или даже школьных олимпиадных алгоритмов), не существует полиномиального (т.е., грубо говоря, быстрого) алгоритма факторизации больших чисел (т.е. разложения числа на множители). На этом держится криптография (например, RSA) и может быть некоторые криптовалюты, мало ли.
Однако, факторизация в свою очередь держится на предположении что P != NP, т.е. якобы не существует быстрого алгоритма решения задачи выполнимости булевых формул (над чем я сейчас и работаю, поэтому взялась такая статья). Дело в том что любую программу, в том числе и программу произведения двух длинных чисел, можно переписать как булеву формулу в КНФ (конъюнктивной нормальной форме), распределив по булевым переменным биты состояния программы в каждый момент времени от
0, ..., t-1, t, t+1, ..., T. Что успешно и делает вышеназванная CBMC для программ на языке C.Таким образом, если как-то быстро решить выполнимость булевой формулы (эвристиками?), то и большое число будет разложено на искомые делители. Что успешно и делает kissat за 3.5 часа работы на старом и пыльном ноутбучном процессоре 13th Gen Intel(R) Core(TM) i9-13980HX.
CBMC далее по решению булевой формулы строит контрпример. Т.е. в C-программе мы утверждаем, будто разложить нельзя, а CBMC в контрпримере нам говорит "нет, и вот как" - далее следуют присвоенные значения каждой недетерменированной переменной программы. Это и есть наши делители.
Подробности.
Вот программа на C, файл mul256cbmc.c , которая перемножает два недетерменированных 256-битных числа в искомое 512-битное число (захардкожено - можете сменить на что вам угодно).
#include <stdint.h>
#include <string.h>
#include <assert.h>
/* CBMC nondeterministic generator: “nondet_*” is recognized and each call yields
an unconstrained fresh value. */
unsigned long long nondet_unsigned_long_long(void);
/* 256x256 -> 512 (little-endian 64-bit limbs) */
static void mul256_u64le(const uint64_t a[4], const uint64_t b[4], uint64_t r[8]) {
for (int i = 0; i < 8; ++i) {
r[i] = 0;
}
#if defined(__SIZEOF_INT128__)
for (size_t i = 0; i < 4; ++i) {
__uint128_t carry = 0;
for (size_t j = 0; j < 4; ++j) {
__uint128_t t = (__uint128_t)a[i] * (__uint128_t)b[j];
t += (__uint128_t)r[i + j];
t += carry;
r[i + j] = (uint64_t)t;
carry = t >> 64;
}
/* bounded ripple: at most 4 remaining limbs */
for (size_t step = 0, k = i + 4; step < 4 && carry != 0; ++step, ++k) {
__uint128_t t = (__uint128_t)r[k] + carry;
r[k] = (uint64_t)t;
carry = t >> 64;
}
}
#else
# error "This file expects unsigned __int128; if unavailable, ask for the 64-bit fallback."
#endif
}
static int eq_u512(const uint64_t a[8], const uint64_t b[8]) {
for (int i = 0; i < 8; ++i) if (a[i] != b[i]) return 0;
return 1;
}
int main(void) {
/* Make p1, p2 nondeterministic */
uint64_t p1[4], p2[4];
for (int i = 0; i < 4; ++i) {
p1[i] = nondet_unsigned_long_long();
p2[i] = nondet_unsigned_long_long();
}
/* Expected is the fixed 512-bit product of:
secp256k1 prime (p_secp) *
P-256 prime (p_p256)
p_secp = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F
p_p256 = 0xFFFFFFFF00000001000000000000000000000000FFFFFFFFFFFFFFFFFFFFFFFF
*/
const uint64_t expected[8] = {
0x00000001000003d1ULL, 0xfffffc2f00000000ULL,
0xfffffffffffffffeULL, 0x000003cffffffc2eULL,
0xfffffffefffffc2fULL, 0x00000000ffffffffULL,
0x0000000000000000ULL, 0xffffffff00000001ULL
};
uint64_t prod[8];
mul256_u64le(p1, p2, prod);
/* FAIL IFF p1*p2 == expected */
__CPROVER_assert(!eq_u512(prod, expected), "p1*p2 must not equal expected");
return 0;
}Вот файл cbmc-kissat.sh скрипт-адаптер чтобы CBMC решал булеву формулу топовым солвером kissat. После сохранения файла в текущую директорию, не забудьте выполнить `chmod +x cbmc-kissat.sh` чтобы ОС могла выполнять этот файл.
#!/usr/bin/env bash
set -euo pipefail
# Config
solver=${KISSAT_BIN:-kissat}
ts=$(date +%Y%m%d-%H%M%S)
user="${USER:-u}"
# Figure out CNF input mode (arg path vs stdin)
if [[ $# -ge 1 && -r "$1" ]]; then
cnf_in="$1"
base="$(basename "$cnf_in")"; base="${base%.cnf}"
src="arg"
else
base="stdin"
src="stdin"
fi
# Workdir for artifacts (readable names)
workdir="${CBMC_KISSAT_WORKDIR:-/tmp}/${user}/cbmc-kissat/${base}_${ts}_$$"
mkdir -p "$workdir"
cnf_copy="$workdir/formula.cnf"
raw_log="$workdir/kissat.stderr" # kissat stats
sol_out="$workdir/kissat.stdout" # kissat model/output (what CBMC needs)
# Prepare CNF file for kissat and for your inspection
if [[ "$src" == "arg" ]]; then
cp -f "$cnf_in" "$cnf_copy"
else
cat > "$cnf_copy"
fi
# Run kissat, forward stdout DIRECTLY to CBMC, and tee both streams to files.
# Important: CBMC reads ONLY stdout; do not print anything else to stdout here.
# kissat prints "s SATISFIABLE"/"s UNSATISFIABLE" and "v ..." model lines to stdout.
# Stats go to stderr; we capture them separately.
"$solver" "$cnf_copy" > >(tee "$sol_out") 2> >(tee "$raw_log" >&2)
rc=$?
# Helpful pointers (stderr only; won't confuse CBMC)
{
echo "[cbmc-kissat] workdir: $workdir"
echo "[cbmc-kissat] cnf: $cnf_copy"
echo "[cbmc-kissat] stdout: $sol_out (tail -f to watch model)"
echo "[cbmc-kissat] stderr: $raw_log (stats)"
} >&2
# Propagate kissat's exit code (10=SAT, 20=UNSAT)
exit $rc
Далее запускаем CBMC следующим образом, считая что вы уже установили CBMC и kissat:
cbmc mul256cbmc.c --c11 --64 \
--no-standard-checks \
--no-built-in-assertions \
--drop-unused-functions \
--reachability-slice \
--slice-formula \
--property main.assertion.1 \
--unwind 9 --trace --external-sat-solver ./cbmc-kissat.sh | tee cbmc-trace.txtПолучаем из этого вывод на экран и в файл cbmc-trace.txt.
Проверяем что kissat начал решать задачу:
ls /tmp/$USER/cbmc-kissat/
# находим вглубине директорий файл kissat.stdout, и далее например
tail -f /tmp/serge/cbmc-kissat/external-sat30893.2AZwWy_20250818-133907_30909/kissat.stdoutДалее ждём несколько часов, в зависимости от производительности вашего компьютера в одном ядре процессора (да, к сожалению kissat - однопоточный).
Далее kissat завершается чем-то типа такого:
c ---- [ profiling ] ---------------------------------------------------------
c
c 11334.31 91.22 % search
c 5683.98 45.75 % stable
c 5650.32 45.48 % focused
c 1089.66 8.77 % simplify
c 1059.92 8.53 % probe
c 896.59 7.22 % vivify
c 110.43 0.89 % sweep
c 45.68 0.37 % reduce
c 21.33 0.17 % substitute
c 18.08 0.15 % factor
c 15.42 0.12 % eliminate
c 15.03 0.12 % walking
c 8.31 0.07 % transitive
c 3.41 0.03 % congruence
c 2.89 0.02 % subsume
c 1.76 0.01 % backbone
c 0.99 0.01 % preprocess
c 0.26 0.00 % fastel
c 0.09 0.00 % parse
c 0.05 0.00 % lucky
c 0.01 0.00 % extend
c =============================================
c 12425.11 100.00 % total
c
c ---- [ statistics ] --------------------------------------------------------
c
c chronological: 798548 1 % conflicts
c conflicts: 70322440 5659.70 per second
c congruent: 14702 7 % variables
c decisions: 503054267 7.15 per conflict
c eliminated: 77788 38 % variables
c factored: 660 0 % variables
c fast_eliminated: 588 1 % eliminated
c fast_strengthened: 175 0 % per strengthened
c fast_subsumed: 2577 1 % per subsumed
c iterations: 79 0 % variables
c propagations: 115164469837 9268685 per second
c reductions: 2232 31506 interval
c reordered: 118 595953 interval
c rephased: 109 645160 interval
c restarts: 2193054 32 interval
c strengthened: 332326 0 % checks
c substituted: 15998 8 % variables
c subsumed: 206142 0 % checks
c switched: 178 395070 interval
c vivified: 6679374 18 % checks
c walks: 36 1953401 interval
c
c ---- [ glue usage ] --------------------------------------------------------
c
c focused glue 1 used 243800208 clauses 71.95% accumulated 71.95% tier1
c focused glue 2 used 29184284 clauses 8.61% accumulated 80.56%
c focused glue 3 used 18037928 clauses 5.32% accumulated 85.89%
c focused glue 4 used 12070423 clauses 3.56% accumulated 89.45%
c focused glue 5 used 8128688 clauses 2.40% accumulated 91.85% tier2
c
c stable glue 1 used 315710656 clauses 59.86% accumulated 59.86% tier1
c stable glue 2 used 46150963 clauses 8.75% accumulated 68.61%
c stable glue 3-6 used 99177292 clauses 18.81% accumulated 87.42%
c stable glue 7 used 9677189 clauses 1.83% accumulated 89.25%
c stable glue 8 used 7056415 clauses 1.34% accumulated 90.59% tier2
c
c ---- [ resources ] ---------------------------------------------------------
c
c maximum-resident-set-size: 248938496 bytes 237 MB
c process-time: 3h 27m 5s 12425.11 seconds
c
c ---- [ shutting down ] -----------------------------------------------------
c
c exit 10
И тогда CBMC выводит долгожеланную трассировку.
Далее с помощью этого Python скрипта (файл parse_cbmc_trace.py) парсим трассировку и проверяем:
#!/usr/bin/env python3
import sys, re
def parse_cbmc_trace(text: str):
"""
Parse CBMC plain trace lines like:
p1[0l]=18446744073709551615ul (...)
p2[3l]=0xFFFFFFFFFFFFFFFF (...)
Returns two lists of limbs (little-endian), each index -> 64-bit limb.
"""
# Collect latest assignments seen for each limb (in case of reassignments)
p = {1: {}, 2: {}}
# Accept index with or without trailing 'l' and numbers in dec or hex
pat = re.compile(r'\bp([12])\[(\d+)l?\]\s*=\s*(0x[0-9a-fA-F]+|\d+)', re.I)
for line in text.splitlines():
m = pat.search(line)
if not m:
continue
which = int(m.group(1)) # 1 or 2
idx = int(m.group(2)) # limb index
val_s = m.group(3) # number literal (dec or hex)
val = int(val_s, 0) # auto base
p[which][idx] = val & ((1 << 64) - 1)
def limbs_to_list(d):
if not d:
return [0, 0, 0, 0]
max_idx = max(d.keys())
arr = [0] * (max_idx + 1)
for i, v in d.items():
arr[i] = v
return arr
p1_limbs = limbs_to_list(p[1])
p2_limbs = limbs_to_list(p[2])
return p1_limbs, p2_limbs
def limbs_to_int(limbs):
n = 0
for i, limb in enumerate(limbs):
n |= (int(limb) & ((1 << 64) - 1)) << (64 * i)
return n
def fmt_hex(n: int) -> str:
if n == 0:
return "0x0"
nbytes = (n.bit_length() + 7) // 8
return "0x" + n.to_bytes(nbytes, "big").hex()
def main():
data = sys.stdin.read()
if not data:
print("Usage: cbmc ... --trace | python3 parse_cbmc_trace.py", file=sys.stderr)
sys.exit(2)
p1_limbs, p2_limbs = parse_cbmc_trace(data)
p1 = limbs_to_int(p1_limbs)
p2 = limbs_to_int(p2_limbs)
prod = p1 * p2
print("p1 =", fmt_hex(p1))
print("p2 =", fmt_hex(p2))
print("p1 * p2 =", fmt_hex(prod))
if __name__ == "__main__":
main()
Запускаем его следующим образом:
python3 parse_cbmc_trace.py < cbmc-trace.txtИ получаем что-то типа такой картинки:
Думаю за какую недельку вычислений kissat возьмёт и используемый сейчас широко RSA-2048, а если не возьмёт, то ждём моих следующих статей, где я собираюсь рассказать про:
Синтез микропрограмм на основе решения булевых формул. Смысл в том, что решив булеву формулу, можно создать программу на примитивном языке (8 команд и однобитные регистры), но всё ещё полном по Тьюрингу. Преимущество такого подхода состоит в том, что алгоритм сразу получается доказанным как теорема, и что можно синтезировать программы, до которых не додумались человеческие умы. Вот только в 192 ГБ памяти на моём ноутбуке поместится разве что формула для микропрограммы из всего лишь нескольких тысяч шагов.
Быстрые решения булевых формул - тут всё ясно должно быть теоретически.
