设计即安全与保持精简：通过自动化提供形式化密码学证明

liumuhui 4小时前阅读数 1 #区块链

我仍然感到惊讶的是，安全性没有被嵌入到系统设计中，而且无法在真正意义上证明一个系统是安全的。总的来说，设计者经常把一些本应安全的程序片段组合在一起，然后就假设整个系统是安全的。这引出了许多问题。我们如何确信正在使用的模块在数学上确实正确？又如何确信，当所有这些模块组合到一起时，解决方案仍然是正确的？

问题

如今，密码学论文似乎变得越来越复杂，尤其是在 AI 正在攻破密码方法的领域。当某个漏洞被提出时，可能会引起一些混乱，而头条新闻往往把“方法被攻破”当作事实——尽管该论文实际上并未经过同行评审。其中一个例子就与 DCP 问题被攻破有关，见此处：

图：此处

这样一来，Dihedral Coset Problem 就可以与 Module-LWE（定义 ML-KEM 的基础困难性问题）联系起来。如果这一证明成立，它将为近似最短向量问题以及 LWE（带误差学习，Learning With Errors）生成一个多项式时间的量子算法，而 LWE 正是抗量子密码学中使用的许多格基方法的基础。但就在本周，我们看到一篇新论文驳斥了这一说法，见此处：

那么，研究人员究竟该如何以某种形式化分析来证明他们的方法，而不必深入钻研证明中的数学呢？嗯，越来越多的研究人员开始为此转向 Lean 编程语言。

Lean 编程语言

Lean 是一种相对较新的开源编程语言，能够对数学和软件进行形式化证明。这使得开发人员可以证明他们的程序符合某种数学形式。在密码学中，这可以用来证明程序在数学上能够匹配 SHA-256 哈希方法，或者证明程序符合 AES 加密方法。

那么，让我们来尝试一个基本示例。为此，我们可以使用如下公式：

y^2 = a (mod p)

在这里，我们必须证明 $y$ 的平方等于 $a$ 对 $p$ 取模。例如，我们可以有：

$$1031^2 = 35 \pmod{97}$$

在 Python 中，我们可以证明这是正确的：

>>> pow(1031,2,97)
35

对于 Lean，我们可以使用 % 运算符（用于取模）来编写，也可以使用内置的数学函数：

import Mathlib
example : (1031^2) % 97 = 35 := by
 norm_num

example : Nat.ModEq 97 (1031 ^2) 35 := by
 norm_num [Nat.ModEq]

然后我们可以运行：

lake env lean square.lean

如果没有错误，就说明我们已经证明了该数学等式。如果我们使用一个不正确的关系式：

import Mathlib

example : Nat.ModEq 97 (1031^2) 32 := by
  norm_num [Nat.ModEq]

我们会得到：

square.lean:3:38: error: unsolved goals
⊢ False

接下来，我们可以为我们的等式创建一个定理：

import Mathlib

theorem square_root_mod_p
    (y a p : Nat)
    (h : y^2 % p = a % p) :
    Nat.ModEq p (y^2) a := by
  exact h

-- 证明 35 是 1031 对 97 取模的一个平方根

example : Nat.ModEq 97 (1031^2) 35 := by

  apply square_root_mod_p 1031 35 97

  norm_num

如果我们运行：

lake env lean square2.lean

我们不会得到任何错误，但如果给出一个不正确的证明：

import Mathlib

theorem square_root_mod_p
    (y a p : Nat)
    (h : y^2 % p = a % p) :
    Nat.ModEq p (y^2) a := by
  exact h

-- 证明 35 是 1031 对 97 取模的一个平方根

example : Nat.ModEq 97 (1031^2) 32 := by

  apply square_root_mod_p 1031 32 97

  norm_num

我们会得到一个错误：

square2.lean:12:38: error: unsolved goals
⊢ False

这难道不是非常漂亮吗？

我们还可以定义一个所需的假设（$h$），然后调用该定理：

import Mathlib

theorem square_root_mod_p
    (y a p : Nat)
    (h : y^2 % p = a % p) :
    Nat.ModEq p (y^2) a := by
  exact h

example : Nat.ModEq 97 (1031^2) 35 := by

  have h : 1031^2 % 97 = 35  % 97 := by
    norm_num

  exact square_root_mod_p 1031 35 97 h

同样，这不会产生任何错误，因此该假设得到了证明。我们还可以针对给定的 $a$ 和 $p$ 值求解平方根：

$$y^2 = a \pmod{p}$$

在下面的示例中，我们可以找到以下方程的平方根：

$$y^2 = 2 \pmod{97}$$

其中一个解为 $y=14$。还有：

$$y^2 = 5 \pmod{31}$$

其中一个解为 $y=6$。还有：

$$y^2 = 3 \pmod{19}$$

没有任何解。Lean 代码如下：

import Mathlib

/-
  检查 y 是否是以 p 为模时 a 的平方根。
-/
def isSquareRootMod (y a p : Nat) : Bool :=
  (y * y) % p == a % p

/-
  在 y = 0, 1, ..., p-1 中搜索 a 对 p 取模的平方根。

  返回：
    some y   如果 y² ≡ a (mod p)
    none     否则
-/
def findSquareRootMod (a p : Nat) : Option Nat :=
  if p = 0 then
    none
  else
    (List.range p).find? fun y =>
      (y * y) % p = a % p

##eval findSquareRootMod 2 97
##eval findSquareRootMod 5 31
##eval findSquareRootMod 3 19

运行结果为：

some 14
some 6
none

我们还可以找到给定素数的平方根。对于 $p=97$，我们可以定义：

import Mathlib

def quadraticResidues (p : Nat) : List Nat :=
  (List.range p).map (fun x => (x * x) % p) |>.eraseDups

##eval quadraticResidues 97

运行后，我们会得到如下的二次剩余：

[0, 1, 4, 9, 16, 25, 36, 49, 64, 81, 3, 24, 47, 72, 2, 31, 62, 95, 33, 70, 12, 53, 96, 44, 91, 43, 94, 50, 8, 65, 27, 88, 54, 22, 89, 61, 35, 11, 86, 66, 48, 32, 18, 6, 93, 85, 79, 75, 73]

因此：

$$y^2 = a \pmod{97}$$

对于 $a=1, 2, 4, 6, 9$ 等值有解。但对于 $a=5$、$a=7$ 或 $a=10$ 没有解。我们可以在此证明：https://asecuritysite.com/primes/modsq?aval=5&pval=97。