当前位置：首页 > news >正文

分治思想用于SAT求解的应用（ToSC2025-3）

news 2025/11/3 10:26:37

大约是一个对论文《Divide-and-Conquer SAT for Exploring Optimal Differential and Linear Characteristics and Its Applications》的理解和学习SAT求解以及MILP的记录。

Abstract

我们常常会采用SAT求解器和MILP方法，利用差分和线性特征中某些约束条件进行最优化搜索，而这些搜索通常会始于对于S盒的处理和建模。现阶段的研究更多是对于大S盒的特征进行分析，那么对于大S盒的建模以及求解约束，以及怎样处理因为S盒较大而产生的不必要的计算就成为一个值得考虑的问题。那么这篇论文目的在于提出更高效且能处理“大S盒/复杂扩散”场景的自动搜索工具，主要提出的是DC-SAT的方法，并用它得到许多实际密码的新或更强的最优特征及相应的攻击结论。

Main Idea

主要想法是把规模很大的SAT模型采用分治思想划分成多个较小的SAT子问题。对每个子问题利用正确的约束排除那些必定无解的布尔变量赋值空间，以达到显著减少求解量与求解时间的目的。该策略结合了MILP与SAT的优点，用MILP的约束来缩小搜索空间，再用SAT精确枚举，是利用分治思想达到剪枝目的的操作。同时，提出了一种对于大S盒的建模方式，在原有的S盒建模方法基础上进行了改进，很大程度上解决了SAT求解中S盒建模中使用的大规模布尔变量的问题。

本文中的求解条件是对于S盒权值的朴素枚举，以期得到最优的差分、线性特征。将差分传播概率和线性特征总体相关性使用整数w来表示，极大的方便了枚举和计算。

主要参考值w：

在考虑差分特征时，将权值w与差分传播概率结合如下：

$w=-log_{2}DP(C))$

其中DP 是单轮的差分传播概率，这样的显著优点是使得概率的连乘变成了加法，在SAT/MILP中更容易处理，也将最优的差分特征转化为了求解权值最小的路径。

在考虑线性特征是，将权值w与线性特征的总体相关性结合如下：

$w=-log_{2}(Cor^{2}(C))$

其中Cor表示单轮线性传播的相关系数，需要注意平方是因为线性偏差通常以平方概率衡量攻击成功率。

Divide-and-Conquer SAT Model

S-box Modeling

对于S盒的建模，本论文的主要目标是减少辅助变量。在传统的S盒建模中，若DDT中最大权值为μ，那么将会为每个S盒创建μ个布尔变量，用来表示该S盒对应的传播概率。例如该对应传播概率为 $2^{-3}$ 时，就令三个布尔变量为1，其余为0（主要原因是SAT一般处理加法更为方便），那么我们就可以在SAT层面添加约束：

$\Sigma _{j=0}^{\mu }u_{j}=3$

这样的话，每个S盒都需要μ个变量，r轮×s个S盒就会需要r×s×μ个辅助变量，导致了传统方法中变量的规模巨大，开销极高。

那么本文提出了一种减小这个规模的方式：采用压缩向量u*，只保留实际区分不同传播概率所需的独立变量，具体表示如下：

$u^{*}=(u_{0}^{*}, u_{1}^{*}, ..., u_{W}^{*}) ,W=w_{max}-w_{min}$

即仅考虑概率范围内且对于权值有贡献的变量，基于这个方法，提出对于S盒的特征统计方法：

$X_{j}=\sum_{i=0}^{s\cdot r-1}u_{j}^{*(i)},(0\leq j\leq W)$

那么我们的整体目标、最显然的约束就可以表示为：

$\sum_{j=0}^{W-1}X_{j}+w_{min}X_{W}\leq k$

k为权值w的值，我们的枚举是从最小概率开始依次枚举，以求得到最优差分、线性特征。

另一种情况，若是权值w含有小数，本文提出将该权值拆分为整数部分和小数两个部分，分别进行计算和讨论。整数部分用u二进制表示整数部分，小数部分采用indicator变量v代表小数的类别，并额外添加α变量表示该S盒是否为活跃S盒，那么整个模型的全局目标则对应地变为：

$\sum_{i}\sum_{j}2^{W^{'}-j}u_{j}^{*(i)}+\sum_{i} \sum_{t}a_{t}v_{t}^{(i)}\leq k$

其中 $W^{'}=\left \lfloor log_{2}w_{max} \right \rfloor$ ， $a_{t}$ 是小数部分的具体实数。

本博客主要讨论DC-SATint部分，即讨论权值w为整数的情况。

根据主要思路的方向，我们的DC-SAT过程氛围两个部分：使用MILP将SAT必定无解的情况删除，再使用SAT将具体的数据进行枚举并得出结果。那么在S盒的建模方法之后，下一部分将要介绍的则是如何对于SAT/MILP进行添加约束条件以达到剪枝盒缩小搜索空间的。

下列给出的五个约束条件我们看来是显然的：

Constraint 1 $\sum_{i=0}^{W-1}X_{i}+w_{minX_{W}}< k$

若某个向量使左侧＜k，那么说明其对应的权值≤k-1。因为我们是升序检查k，那么k-1必然是UNSAT，那么这一类的空间必然属于UNSAT。

Constraint 2 $X_{i}< 0$ $(0\leq i\leq W)$

根据前面对于 $X_{i}$ 的定义，该变量不可能为负值，那么受这个条件所约束的显然属于UNSAT。

Constraint 3 $X_{i}> X_{W}$ $(0\leq i\leq W-1)$

局部约束 $u_{i}^{*}\leq u_{W}^{*}$ ，那么显然全局约束同样成立。则约束条件下必然是UNSAT。

Constraint 4 $X_{W}< AS_{low}$

其中等式右侧是已知的某轮数下活跃S盒的下界（可以用MILP或已有的下界推导得到），那么若全局S盒计数小于这个下界，显然UNSAT。

Constraint 5 $\sum_{i=0}^{W-1}X_{i}+w_{minX_{W}}\geq k$

在论文中，这个条件限制的属于还未经过搜索的空间，即下一个k值的涵盖范围，但是这个条件对于本轮搜索并没有帮助，可以直接跳过。

那么基于上述条件和思路，可以得到如下伪代码：

解释：从line4-line11的主要操作是while循环，直到找到一个满足条件的最小k；首先使用前面的约束将UNSAT空间排除，在解空间里再进行SAT求解；直到找到一个k，那么这个k就是最优解。因为我们概率可以近似认为是 $2^{-k}$ ，k越小概率越大。

Additional conditions

同时，在论文中作者同样引入了Matsui界的概念，为SAT/MILP加入了新的界限。这个基于Matsui在1994年提出的分支界限策略，核心用途为：

在搜索r轮最优差分/线性特征时，利用已知的子轮最优概率信息来提前剪枝——如果当前搜索分支乘以剩余轮可达到的最优上限仍不足以超过当前已知的候选（或达不到目标），那就不往下搜索该分支。

将该思想引入本文中可以表示如下：设已有t轮的部分传播概率为乘积 $\prod_{i=1}^{t}DP(c_{i-1}\rightarrow c_{i})$ ，并且我们已知 $DP_{best}(r-t)$ 表示剩余r-t轮的最优可能概率，则若

$\prod_{i=1}^{t}DP(c_{i-1}\rightarrow c_{i})\cdot DP_{best}(r-t)< DP_{est}(r)$

那么说明以当前前缀继续向下构造任意完整r轮特征也不会优于当前已知的估计 $DP_{est}(r )$ ，所以可以进行剪枝。实际上在论文《Accelerating the Search of Differential and Linear Characteristics with the SAT Method》中已经可以将该思想转化为与权值w相关的不等式如下：