Сразу оговорюсь, что обычно я не занимаюсь компьютерной безопасностью и не интересуюсь, а занимаюсь алгоритмами и структурами данных - в прикладном применении это оптимизация быстродействия, высокопроизводительные вычисления типа 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, а если не возьмёт, то ждём моих следующих статей, где я собираюсь рассказать про:

1. Синтез микропрограмм на основе решения булевых формул. Смысл в том, что решив булеву формулу, можно создать программу на примитивном языке (8 команд и однобитные регистры), но всё ещё полном по Тьюрингу. Преимущество такого подхода состоит в том, что алгоритм сразу получается доказанным как теорема, и что можно синтезировать программы, до которых не додумались человеческие умы. Вот только в 192 ГБ памяти на моём ноутбуке поместится разве что формула для микропрограммы из всего лишь нескольких тысяч шагов.

2. Быстрые решения булевых формул - тут всё ясно должно быть теоретически.