本文深入探讨了对于现代安全研究人员而言至关重要的数学领域,包括线性代数、非线性建模、抽象代数、数论和数理逻辑。文章详细解释了这些数学概念在密码学、零知识证明系统、DeFi 协议分析、漏洞挖掘和形式化验证中的应用,并提供了进一步学习的资源。
你不需要懂得很多数学也能成为一名成功的安全研究员。但如果你想看到矩阵,你需要变得精通数学。

关于数学是被发现的还是被发明的,一直存在着古老的哲学辩论。小时候,我两者都不想做。数学感觉很抽象,与现实脱节,像是一套需要记住的任意规则。很长一段时间,我都在积极地尝试尽可能少地接触数学。
然而,当我开始学习机器学习基础知识时,我的观点开始转变。后来,深入研究零知识证明开启了一个更广阔的数学世界。现在,我享受数学本身带来的乐趣,但它也为我的日常工作提供了更深入的理解。
在本文中,我将介绍一些数学领域,虽然它们不总是严格意义上的“必不可少”,但对于现代安全研究人员来说,具有很高的杠杆作用。但请注意,我也会稍微绕道进入机器学习和物理学。
最简单地说,代数是在固定规则下操作符号的艺术。当我们解 $2x + 3 = 11$ 时,“代数”就是减去 3 并除以 2 来分离 $x$。在 19 世纪,像 高斯 这样的数学家系统化了如何解决这类方程,从而产生了矩阵的概念和操作矩阵的算法。
线性代数是运算保持线性的分支(见下文)。如今,它支撑着 3D 图形、推荐引擎和机器学习。大型语言模型本质上是一个巨大的矩阵乘法堆栈,其中混合了非线性。
人们有时会用“线性”作为“简单”的简写,但在数学中,它是一种结构约束。如果转换 $L$ 满足两个规则,则它是线性的:
用通俗易懂的语言来说:如果你转换两个事物并添加结果,你得到的结果与先添加它们然后再转换相同。如果你在转换之前缩放某个事物,那么与先转换然后再缩放相同。
从几何角度考虑:如果你有一个网格,线性变换可能会旋转、拉伸或剪切它,但网格线保持平行且间距均匀。它永远不会弯曲或扭曲空间。
向量 只是一个数字列表,例如 $v = (v₁, v₂, …, vₙ)$。你可以将其视为空间中的一个点或指向某个方向的箭头。我们通常将向量视为 向量空间 ℝⁿ(所有 n 维实数列表的集合)中的列向量。
矩阵 是转换向量的数字网格。如果 $A$ 是矩阵,$x$ 是向量,则将它们相乘 ($A \cdot x$) 会产生一个新向量。将矩阵视为机器:你输入一个向量,它吐出一个转换后的向量。
让我们将一个 2×2 矩阵乘以一个向量:
A = | 2 3 | x = | 5 |
| 4 -1 | | 2 |
A·x = | 2×5 + 3×2 | = | 10 + 6 | = | 16 |
| 4×5 + (-1)×2 | | 20 - 2 | | 18 |
$A$ 的每一行都与 $x$ “点积”:将对应的条目相乘并求和。这种运算是每个神经网络层、每个 3D 旋转和 马尔可夫链 中的每个状态转换在底层的工作方式。
点积: $⟨x, y⟩ = xᵀy = Σᵢ xᵢyᵢ$。这会将对应的条目相乘并将它们加起来。它衡量两个向量的“对齐”程度;如果它们指向相似的方向,则点积很大且为正。向量的长度是 $‖x‖ = √⟨x,x⟩$(到原点的 欧几里得距离)。
矩阵乘法: $(AB)ᵢⱼ = Σₖ AᵢₖBₖⱼ$。组合两个线性变换(先做 $A$,然后做 $B$)等价于将它们的矩阵相乘。
单位矩阵和逆矩阵: 单位矩阵 $Iₙ$ 在对角线上有 1,其他地方有 0 — 它是“什么都不做”的变换。当存在 $A⁻¹$ 使得 $AA⁻¹ = I$ 时,矩阵 $A$ 是可逆的。求逆可以让你“撤消”变换。
一个非常普遍的应用是在现代机器学习中使用的 embeddings。训练大型语言模型会将每个 token(单词或单词片段)定位为高维空间中的一个点,将相关的 token 推在一起,并将不相关的 token 分开。
一个经典的例子:取 国王 的向量,减去 男人,加上 女人,结果会非常接近 女王:
国王 - 男人 + 女人 ≈ 女王
之所以有效,是因为模型学习到“国王”和“女王”的差异与“男人”和“女人”的方向大致相同——我们可以称之为“性别”的方向。我们正在进行“意义计算”,这有多棒!你可以通过利用这些几何关系来构建语义搜索、聚类或提示引导工具。
零知识证明系统通常将验证简化为检查一堆线性方程。关键的见解是,任何计算都可以编码为 有限域 上的一组线性约束。这个过程称为“算术化”。
一种常见的表示是 Rank-1 约束系统 (R1CS)。我们证明我们知道一个秘密解向量 s(称为“见证”),对于许多向量三元组 (a, b, c):
(s · a) × (s · b) = s · c
如果所有这些等式都成立(使用点积),则程序逻辑已正确执行。证明者证明了对 s 的了解,而没有透露它。
假设我们要证明我们知道 $x$ 使得 $x³ + x + 5 = 35$(剧透:答案是 $x = 3$)。
步骤 1:展平为二次门
R1CS 只能处理每个约束一次乘法,因此我们引入中间变量来分解三次项:
步骤 2:构建见证向量
s = [1, x, v₁, v₂, out] = [1, 3, 9, 27, 35]
开头的“1”是一个常数项,它允许我们在约束中对加法和常数进行编码。
步骤 3:编码为 R1CS 约束
每个乘法门变成 $(s \cdot a) × (s \cdot b) = (s \cdot c)$:
约束 | a | b | c | 检查
─────────────────┼───────────────┼───────────────┼───────────────┼─────────────
v₁ = x × x | [0,1,0,0,0] | [0,1,0,0,0] | [0,0,1,0,0] | 3 × 3 = 9 ✓
v₂ = v₁ × x | [0,0,1,0,0] | [0,1,0,0,0] | [0,0,0,1,0] | 9 × 3 = 27 ✓
out = v₂ + x + 5 | [5,1,0,1,0] | [1,0,0,0,0] | [0,0,0,0,1] | 35 × 1 = 35 ✓
最后一个约束使用了一个技巧:我们将 $(v₂ + x + 5)$ 乘以 1,以将加法编码为“乘法”。
在审查 Groth16 电路时,你要检查这些约束矩阵是否正确地编码了预期的计算。缺少约束或错误的系数意味着证明者可以作弊。有关更详细的介绍,请参阅 Vitalik 的经典 QAP 博文 和 RareSkills ZK Book。
DeFi 不变量几乎总是乘积或比率的幂(Uniswap v2 的 x·y=k,Balancer 的加权几何平均数,Curve 的两者的组合)。我们可以通过将它们转换为线性方程来解锁强大的分析技术,然后可以使用高中代数、电子表格或矩阵运算来解决这些线性方程(是的,成功的安全审计员 使用电子表格)。关键技术是 对数线性化。
对数具有神奇的属性:它们将乘法转换为加法。
ln(a × b) = ln(a) + ln(b)
ln(aⁿ) = n · ln(a)
这意味着任何由乘法和求幂构建的方程都可以转换为加法和标量乘法,这正是“线性”的含义:
原始形式 → 线性化形式
─────────────────────────────────────────────────────────
x · y = k → ln(x) + ln(y) = ln(k)
xᵃ · yᵇ = k → a·ln(x) + b·ln(y) = ln(k)
(x/y)ᵃ · zᵇ = k → a·ln(x) - a·ln(y) + b·ln(z) = ln(k)
自动做市商维护一个可以线性化的不变量。以 Balancer 式的池为例,其储备金为 $x = (xₐ, xᵦ, xᵧ)$,权重为 $w = (0.5, 0.3, 0.2)$。不变量是:
xₐ^0.5 × xᵦ^0.3 × xᵧ^0.2 = k
这是一个非线性方程,到处都是乘积和指数。你无法在电子表格中轻松解决这个问题。但是,看看当我们对两边取对数时会发生什么:
起始方程:
xₐ^0.5 × xᵦ^0.3 × xᵧ^0.2 = k
对两边取 ln():
ln(xₐ^0.5 × xᵦ^0.3 × xᵧ^0.2) = ln(k)
应用 ln(a × b) = ln(a) + ln(b):
ln(xₐ^0.5) + ln(xᵦ^0.3) + ln(xᵧ^0.2) = ln(k)
应用 ln(aⁿ) = n·ln(a):
0.5·ln(xₐ) + 0.3·ln(xᵦ) + 0.2·ln(xᵧ) = ln(k)
现在替换变量。令 $vₐ = ln(xₐ), vᵦ = ln(xᵦ), vᵧ = ln(xᵧ)$:
0.5·vₐ + 0.3·vᵦ + 0.2·vᵧ = ln(k)
这是 $v$ 变量中的一个 线性方程!以向量形式:
w · v = c
其中 w = [0.5, 0.3, 0.2], v = [vₐ, vᵦ, vᵧ], c = ln(k)
假设池开始于 $x = (1000, 800, 600)$。交易者想要添加 100 个 A 单位,并且只移除 B。我们需要找到 $Δᵦ$,以便不变量保持不变。
对数空间中的变化必须满足 $w \cdot Δv = 0$(不变量常数不变):
0.5 × ln(1100/1000) + 0.3 × ln((800-Δᵦ)/800) + 0.2 × 0 = 0
逐步解决:
0.5 × 0.0953 + 0.3 × ln((800-Δᵦ)/800) = 0
0.0477 + 0.3 × ln((800-Δᵦ)/800) = 0
ln((800-Δᵦ)/800) = -0.159
(800-Δᵦ)/800 = e^(-0.159) = 0.853
Δᵦ ≈ 117.6
一阶近似(用于快速实验):
对于小的变化,ln(1 + δ) ≈ δ。这给出了更简单的矩阵形式:
w · (Δx / x) = 0
[0.5, 0.3, 0.2] · [100/1000, -Δᵦ/800, 0]ᵀ = 0
0.5 × 0.1 + 0.3 × (-Δᵦ/800) = 0
Δᵦ ≈ 133.33
线性近似略微高估,但可以快速进行完整性检查。审计师使用它来限制滑点或检测闪电贷序列期间的不变量违规。
永续期货 交易所维护着复杂的风险引擎,可以使用线性代数优雅地建模。虽然实现方式各不相同,但数学结构是通用的。
核心组件:
偿付能力测试 变成一个简单的矩阵不等式:
C · (P · p) ≥ m
其中 m 是最小权益向量。换句话说:将头寸乘以价格以获得美元价值,应用保证金系数,检查你是否高于最低限额。
压力测试 通过敏感度矩阵 S 应用冲击向量 s(例如,“BTC 下跌 20%,ETH 下跌 30%”):
C · (P · (p + S·s)) ≥ m
如果此操作失败,则会触发清算。
每个步骤都是一个带有安全防护的矩阵向量乘法。通过以这种方式建模系统,你可以:
理解这种结构可以让你审计清算逻辑并找到头寸从裂缝中滑落的边缘情况。
如果你在阅读本文后对线性代数情有独钟,请查看以下链接:
我们刚刚学习了线性代数及其用途。但是现实世界是混乱的,并且有很多事情无法用线性关系建模。
例如,如果神经网络仅由线性层组成,它们将崩溃为单个巨大的矩阵乘法。在数学上,依次应用矩阵 $A$ 然后 $B$ ($A × B × x$) 与应用一个新矩阵 $C$ 相同,其中 $C = AB$。无论你堆叠多少层,如果它们都是线性的,则整个网络只是一个线性运算。它无法学习任何复杂的东西。
考虑 XOR 函数(异或)。仅当输入不同时,它才输出 1:
输入 → 输出
──────────────────
(0,0) → 0
(1,1) → 0
(0,1) → 1
(1,0) → 1
想象一下将这些绘制在纸上。你在左下角和右上角有两个“0”点,在左上角和右下角有两个“1”点。
现在拿起尺子,尝试绘制一条直线,将 0 与 1 分开。
你不能。这是 线性不可分性。线性分类器在这里 100% 失败。为了解决这个问题,神经网络在线性层之间应用 非线性 激活函数(如 ReLU 和 Sigmoid)。最常见的是 ReLU(线性整流单元):**。](https://en.wikipedia.org/wiki/Group_(mathematics))、[环](https://en.wikipedia.org/wiki/Ring_(mathematics)) 和 域。它将算术推广到数字之外,推广到对称运算、矩阵或你可以在特定规则下组合的函数。
该领域诞生于解决多项式方程的尝试。在 19 世纪 30 年代,埃瓦里斯特·伽罗瓦是一位才华横溢的数学家,20 岁时在一场决斗中丧生——他意识到多项式根的对称性形成了一种代数结构。他展示了为什么一般的五次多项式没有使用根式的公式,并且在此过程中发明了群论。
群 是一个集合 $G$,带有一个运算 $·$,该运算满足四个规则:
经典示例:加法下的整数 (ℤ, +)。单位元是 0,并且 $n$ 的逆元是 -$n$。
从整数的例子中,群和对称之间的联系并不明显。为了看到它,考虑一个更几何的例子:等边三角形的对称性。
你可以通过一些方式转换等边三角形,使其看起来完全相同:将其旋转 120°,将其旋转 240°,或者沿着三个轴中的任何一个翻转它。包括“什么都不做”,你正好有 6 个对称运算。这些运算构成一个群:
这是 二面体群 D₃ ——等边三角形的对称群。](https://en.wikipedia.org/wiki/Noether%27s_theorem) 证明了历史上最深刻的定理之一:物理系统的每个连续对称性都对应于一个守恒定律。
事实证明,自然界的基本力量也源于对称性!物理学家写 SU(3) × SU(2) × U(1) 来描述 粒子物理学的标准模型。该公式中的每个群都对应于一种力:
力携带粒子的数量由群的数学决定。U(1) 有 1 个生成元,因此电磁学有 1 个力载体(光子)。SU(2) 有 3 个生成元,给出 3 个弱玻色子。SU(3) 有 8 个生成元,因此有 8 个胶子。
基本上,物理学家们问道:“如果我们要求物理定律在某些局部变换下保持不变会怎么样?” 这个要求,称为规范不变性,在数学上迫使力携带粒子的存在。数学决定了物理学。
即使是引力也符合这个模式。广义相对论 源于要求物理学在任意坐标变换下是不变的(微分同胚不变性)。时空曲率(我们体验为引力)是保持这种对称性的“规范场”。
这可以说是现代物理学中最深刻的见解:现实的结构不是任意的。力、粒子及其相互作用是抽象对称性要求的必然结果。宇宙似乎本质上是一个定理。
将软件漏洞视为对称性破坏是一种强大的思维模型。安全的系统依赖于不变量——无论发生什么有效交易,都必须保持为真的属性。漏洞只是破坏对称性的转换。
当你审核智能合约时,你实际上是在检查该微观宇宙的“物理定律”在所有可能的运算下是否成立。可以通过输入模糊测试和形式验证等过程检查不变量(见下文)。
环 是一个具有两个运算(+ 和 ×)的集合,其中加法形成一个群,并且乘法是结合律的并且分配在加法上。将其视为“加法和乘法,但也许你并不总是可以除法”。
域 是一个你也可以除法的环(每个非零元素都有一个乘法逆元)。这是大多数密码学存在的代数结构。
模 n 的整数(写为 ℤ/nℤ 或 ℤₙ)形成一个环。它们仅当 n 是素数时才形成一个域——这就是为什么密码学喜欢素数。
在 ℤ₇(模 7 的整数)中,我们进行算术运算,然后取除以 7 时的余数:
加法:5 + 4 = 9 ≡ 2 (mod 7)
乘法:5 × 4 = 20 ≡ 6 (mod 7)
逆元:5⁻¹ = ? (找到 x 使得 5x ≡ 1 mod 7)
5 × 3 = 15 ≡ 1 (mod 7),所以 5⁻¹ = 3
除法:4/5 = 4 × 5⁻¹ = 4 × 3 = 12 ≡ 5 (mod 7)
扩展欧几里得算法 系统地找到逆元:
def extended_gcd(a, b):
if b == 0:
return a, 1, 0
gcd, x1, y1 = extended_gcd(b, a % b)
return gcd, y1, x1 - (a // b) * y1
def mod_inverse(a, n): # 求模逆
gcd, x, _ = extended_gcd(a, n)
if gcd != 1:
raise ValueError("No inverse exists")
return x % n
群同态 是群之间的函数 $f: G → H$,它尊重运算:](https://rareskills.io/post/groth16) 和 PLONK 证明将程序约束嵌入到群元素中,以便验证方程简化为检查同态是否保留了结构。
此时,暂停一下,注意刚刚发生了什么。“结构保留”只是对称性的另一个名称。相同的想法出现在几何学、物理学和密码学中,因为现实在每个层面上都是由对称性构建的!
索尼以惨痛的代价出名地学习了抽象代数。他们在他们的 ECDSA 实现中重复使用了一个随机 nonce $k$。
ECDSA 的工作原理:
对于私钥 $d$ 和消息哈希 $z$:
签名是 $(r, s)$。
漏洞:
如果你对两个不同的消息 $z₁$ 和 $z₂$ 使用相同的 $k$:
s₁ = k⁻¹(z₁ + r·d)
s₂ = k⁻¹(z₂ + r·d)
相减:
s₁ - s₂ = k⁻¹(z₁ - z₂)
因此:
k = (z₁ - z₂)/(s₁ - s₂)
一旦你有了 k:
d = (s₁·k - z₁)/r
Sony 的私钥可以用简单的代数计算出来 :)
人类已经追逐数论难题数千年了。毕达哥拉斯学派 崇拜整数,并且偶然发现了非理性。皮埃尔·德·费马 在他的臭名昭著的关于幂和的空白处写下了他的笔记。卡尔·弗里德里希·高斯将数论称为“数学女王”,并用他的算术研究将其变成了一门学科。
几个世纪以来,它是纯粹数学的典型代表:没有实际应用的美丽难题。然后 1970 年代到来了,公共密钥密码学让素数发挥了作用。
安全性中典型的数论问题是 因式分解。给定两个大素数 $p$ 和 $q$,计算 $n = p × q$ 是微不足道的。但是反过来——仅给定 $n$ 找到 $p$ 和 $q$ ——对于大数来说在计算上是不可行的。
RSA 的安全性依赖于这种单向难度。
让我们用小素数构建 RSA,以进行数学运算:
步骤 1:选择素数
p = 61,q = 53
n = p × q = 3233
步骤 2:计算Euler函数
φ(n) = (p-1)(q-1) = 60 × 52 = 3120
(Euler函数计算小于 n 且与 n 没有共同因子的数字)
步骤 3:选择公钥指数
e = 17(必须与 φ(n) 互质,这意味着它们没有共同因子)
步骤 4:计算私钥指数
d = e⁻¹ mod φ(n)
17d ≡ 1 (mod 3120)
d = 2753 (验证:17 × 2753 = 46801 = 15 × 3120 + 1)
公钥: (n=3233, e=17)
私钥: (n=3233, d=2753)
加密(消息 m=123):
c = mᵉ mod n = 123¹⁷ mod 3233 = 855
解密:
m = cᵈ mod n = 855²⁷⁵³ mod 3233 = 123
```它为什么有效:Euler定理表明,对于与 $n$ 互质的 $m$,有 $m^{φ(n)} ≡ 1 \pmod{n}$。由于 $ed ≡ 1 \pmod{φ(n)}$,对于某个 $k$,我们有 $ed = 1 + k \cdot φ(n)$:
cᵈ = (mᵉ)ᵈ = m^(ed) = m^(1 + k·φ(n)) = m × (m^φ(n))^k ≡ m × 1^k = m (mod n)
### 离散对数问题
另一个要点:给定 $gˣ \mod p$,找到 $x$。对于大的素数,目前还没有已知的有效算法。
```markdown
例子:找到 x,其中 5ˣ ≡ 20 (mod 23)
暴力破解:
5¹ = 5
5² = 25 ≡ 2
5³ = 10
5⁴ = 50 ≡ 4
5⁵ = 20 ✓
所以 x = 5。
对于 2048 位的素数,暴力破解所需时间比宇宙的年龄还长。这是迪菲-赫尔曼密钥交换的基础。
### 椭圆曲线算术
有限域上的椭圆曲线为我们提供了具有难解离散对数问题但运算效率高的群。
域 𝔽ₚ 上的椭圆曲线:y² = x³ + ax + b (mod p)
**点加:** 对于 P = (x₁, y₁) 和 Q = (x₂, y₂):
如果 P ≠ Q: 斜率 m = (y₂ - y₁)/(x₂ - x₁) mod p
如果 P = Q(点加倍): 斜率 m = (3x₁² + a)/(2y₁) mod p
结果 R = P + Q: xᵣ = m² - x₁ - x₂ mod p yᵣ = m(x₁ - xᵣ) - y₁ mod p
所有算术运算都发生在域 𝔽ₚ 中,包括除法(实际上是乘以模逆)。
## 费马小定理
在我们离开经典数论之前,让我向你展示其中一个最优雅的结论。
[**费马小定理**](https://en.wikipedia.org/wiki/Fermat%27s_little_theorem)**:** 如果 p 是素数,且 a 不能被 p 整除,那么: ](https://en.wikipedia.org/wiki/Schwartz%E2%80%93Zippel_lemma) 是我最喜欢的定理之一。它使得在几毫秒内验证任意长的证明成为可能!
**问题:** 假设我有两个多项式,并且想要检查它们是否相同。朴素的方法是比较所有系数 —— 对于高阶多项式来说,这非常昂贵。但这里有一个捷径。
**Schwartz-Zippel 引理:** 设 P(x) 是域 𝔽 上的一个非零多项式,其阶数为 d。如果你从 𝔽 中选择一个随机点 r,那么 P(r) = 0 的概率最多为 d/\|𝔽\|。
换句话说:相对于域的大小,非零多项式具有非常少的根。
考虑 P(x) = x³ — 6x² + 11x — 6 = (x-1)(x-2)(x-3)。这个 3 阶多项式恰好有 3 个根:{1, 2, 3}。
如果我们在 𝔽₁₀₁ 中工作(模 101 的整数),那么随机求值落在根上的概率最多为 3/101 ≈ 3%。一次随机检查让我们有 97% 的信心认为该多项式是非零的。这会将多项式恒等式测试从 O(d) 系数比较转换为 O(1) 点求值:
想要证明:对于所有 x,P(x) = Q(x)
等价于:对于所有 x,P(x) - Q(x) = 0
测试:选择一个随机 r,检查 P(r) - Q(r) = 0 是否成立 如果 P ≠ Q,则差多项式的阶数 ≤ d, 因此它在 |𝔽| 个可能性中最多有 d 个根。 随机 r 命中根的概率 ≤ d/|𝔽|。
对于密码学领域的大小(\|𝔽\| ≈ ²²⁵⁶),即使是百万阶的多项式,碰撞概率也只有 ≈ 1⁰⁶/²²⁵⁶ ≈ 0。
现代 ZK 系统(Groth16、PLONK、STARKs)将计算编码为多项式约束。证明者想要说服验证者“我正确地执行了此计算”,而不泄露输入。
该协议通常按如下方式工作:
1. **将计算编码为多项式:** 正确的执行轨迹满足对于某个域中的所有 x,P(x) = 0
2. **证明者提交多项式:** 使用隐藏系数的密码学承诺
3. **验证者选择随机挑战 r:** 在承诺之后(因此证明者无法作弊)
4. **证明者揭示 P(r):** 仅一个域元素
5. **验证者检查 P(r) = 0:** 如果为真,则以极大的概率接受
根据 Schwartz-Zippel 引理,提交**错误**多项式的作弊证明者将无法通过检查, 其概率 ≥ 1 — d/\|𝔽\| ≈ 1。
因此,验证一个需要数百万步的计算可以简化为检查**单个点!** 这就是为什么 ZK 证明是“简洁的” —— 证明大小和验证时间与原始计算相比非常小。
### 数论的延伸阅读
- [密码学 I (Coursera)](https://www.coursera.org/learn/crypto) — Dan Boneh 的传奇课程
- [Least Authority 的 Moon math manual](https://github.com/LeastAuthority/moonmath-manual) — 解释了理解零知识证明所需的所有数学知识
## 数学逻辑:证明的限制
在 20 世纪 30 年代,艾伦·图灵和阿隆佐·邱奇从不同的角度解决了计算的基础问题。当图灵想象一台带有磁带的机器时,邱奇发明了一种称为 [**Lambda Calculus**](https://en.wikipedia.org/wiki/Lambda_calculus) 的纯函数系统。值得注意的是,它们是等价的 —— 你可以用循环和状态做任何事情,你都可以用递归函数来做。 ](https://github.com/a16z/halmos), [Mythril](https://github.com/ConsenSysDiligence/mythril) 和 [hevm](https://github.com/argotorg/hevm) 在资源限制范围内探索执行路径,并由 SMT 求解器指导。
在形式验证中,我们基本上将分析的代码转换为数学方程式,以便我们可以创建某些属性的数学证明。
### 符号执行:将代码转换为代数
符号执行的核心思想具有欺骗性地简单:我们不用像“x = 5”这样的具体值来运行程序,而是用**符号**值(如“x = α”(一些未知值))来运行它。 随着程序的执行,我们建立代数表达式来表示每个变量所拥有的值。
考虑一个简单的 withdraw 函数:
function withdraw(uint256 amount) public { require(balances[msg.sender] >= amount); balances[msg.sender] -= amount; payable(msg.sender).transfer(amount); }
当我们用 `amount = α`(符号)来符号执行它时,会发生以下情况:
1. **初始状态:** `balances[msg.sender] = β`(也是符号——我们不知道余额)
2. **在 require 语句处:** 我们记录一个**路径约束**:`β ≥ α`
3. **减法后:** `balances[msg.sender] = β - α`
4. **在转账时:** 我们注意到 `α` wei 离开了合约
现在,符号执行器已将此代码路径转换为一组代数表达式:
路径约束: β ≥ α 最终余额: β - α 转账金额: α
### 代数表达式的样子
在探索所有路径之后,符号执行器会收集一系列公式。 对于易受攻击的合约,这些可能看起来像:
路径 1(正常取款): 约束:β ≥ α ∧ α > 0 事后状态:balance' = β - α
路径 2(重入攻击路径): 约束:β ≥ α ∧ attacker_is_contract 事后状态:balance' = β - α - α(提取了两次!) 违规:balance' < 0(下溢!)
这些表达式使用标准代数符号以及位向量算术(因为 EVM 使用 256 位整数)、数组理论(用于存储映射)和未解释的函数(用于哈希和外部调用)。
### SMT 求解器:寻找漏洞
像 [Z3](https://github.com/Z3Prover/z3) 这样的 [**SMT(理论模可满足性)求解器**](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) 接受这些代数约束并回答:“是否存在使该公式可满足的值分配?” ](https://github.com/ConsenSys/mythril) 是第一个为 EVM 智能合约实施此技术的工具之一。 基于 Mythril,[Scrooge McEtherface](https://github.com/muellerberndt/scrooge-mcetherface)(在 DEF CON 2019 上展示)更进一步:它自动生成可运行的漏洞利用交易,从易受攻击的合约中提取 ETH。
像 [Halmos](https://github.com/a16z/halmos) 这样的较新工具将符号测试直接集成到 Foundry 开发工作流程中。 你无需编写单独的规范,而是使用符号输入编写测试:
function check_withdraw(uint256 amount) public { uint256 balanceBefore = token.balanceOf(address(this)); token.withdraw(amount); uint256 balanceAfter = token.balanceOf(address(this));
// 此断言会针对 amount 的所有可能值进行检查
assert(balanceAfter <= balanceBefore);
}
Halmos 以符号方式探索 `amount` 的所有 ²²⁵⁶ 个可能值,而不是单独运行它们,而是通过构建约束并查询解算器。 如果任何值违反断言,Halmos 将报告一个反例。
### 数学逻辑的延伸阅读
- [斯坦福百科全书:哥德尔不完备性定理](https://plato.stanford.edu/entries/goedel-incompleteness/)
- [斯坦福百科全书:停机问题](https://plato.stanford.edu/entries/turing-machine/)
- [哥德尔、埃舍尔、巴赫](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach) 作者:道格拉斯·霍夫施塔特
## 其他值得探索的领域
虽然以上各节涵盖了最直接适用于智能合约审计和密码学的数学,但还有其他几个领域值得了解。
### 微积分:变化的数学
芝诺的埃利亚提出了一个著名的[悖论](https://en.wikipedia.org/wiki/Zeno%27s_paradoxes):要穿过一个房间,你必须首先走一半路程,然后走剩下路程的一半,然后再走一半。 由于有无限个一半,因此你永远无法到达另一侧。 数学用 **微积分** 解决了这个问题 —— 对极限和无穷级数的研究。 我们可以证明,无限个越来越小的量之和收敛到一个有限的数字:1/2 + 1/4 + 1/8 + … = 正好是 1。
微积分为我们提供了两个基本工具:**导数** 衡量函数对小输入变化的敏感程度(这对于基于梯度的 ML 模型攻击和理解数值稳定性至关重要),而 **积分** 衡量随时间的累积(用于侧信道分析,其中微小的功率泄漏会跨数千个迹线求和,直到信号从噪声中出现)。 如果你冒险进入对抗性机器学习、差分隐私或硬件安全领域,那么微积分就变得至关重要。 对于纯粹的智能合约工作,你通常可以在没有它的情况下完成,但理解极限有助于在推理重复操作中的精度损失时。
### 离散数学:图、组合学和计数
**图论** 对对象之间的关系进行建模 —— 通过边连接的顶点。 在安全性方面,图无处不在:网络拓扑(攻击者能否从 Web 服务器转移到数据库?)、智能合约调用图(哪些函数可以调用哪些函数?是否存在指示重入风险的循环?)、二进制分析中的控制流图(哪些基本块主导着漏洞的路径?)和状态机(哪些交易序列是可能的?)。 邻接矩阵表示将图论重新连接到线性代数:如果 A 是邻接矩阵,则 (Aᵏ)ᵢⱼ 计算节点 i 和节点 j 之间长度为 k 的路径数。
**组合学** —— 计数的数学 —— 有助于分析搜索空间的大小(有多少个可能的密钥?有多少个执行路径?),理解生日攻击和碰撞概率,并推理暴力攻击与巧妙攻击的复杂性。 当有人说“256 位安全性”时,他们就是在对穷举搜索的不可行性进行组合论证。 这些领域与算法分析和复杂性理论有很大重叠,后者是我们理解是什么让密码学问题“难以解决”的基础。
## 汇集在一起
这些数学领域直接与我们在安全方面所做的工作相关:
- **线性代数** 让你能够阅读 ZK 电路,理解 AMM 不变量,并分析神经网络漏洞
- **抽象代数** 为你提供了密码学的语言 —— 群、域、同态 —— 并解释了 PS3 黑客攻击为何有效
- **数论** 是 RSA、迪菲-赫尔曼和椭圆曲线的基础,每次实现细节中都潜藏着攻击
- **逻辑** 提醒我们,完美的验证是不可能的,但矛盾的是,这使得安全性更有趣,而不是更少
如果你对数学、编码和安全的融合感到兴奋,那么现在是深入研究的最佳时机。 免费课程、视频和热情的社区随处可见。 无论你从用 3Blue1Brown 可视化矩阵开始,还是通过编写你自己的 Groth16 实现开始,你都将获得一次大开眼界的体验。
- 原文链接: muellerberndt.medium.com...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!