请咨询作者同意后转载。
Statistical Similarity of Binaries
github https://github.com/tech-srl/esh
| 期刊/会议： | PLDI（A类） |
|---|---|
| 发表时间： | 2016年6月 |
| 发表机构： | Technion, Israel |
前言
主要思想： similarity by composition方法:将代码分解为一些很小的可比较的片段，定义代码片段之间的语义相似性，使用统计学的方法将代码片段的相似性转换成程序间的相似性。
Similarity by composition： 如果一幅图像可以用另一幅图像的区域组成，那么它就相似于另一幅图像，并且这种相似性可以通过统计推理来量化。
Intuition: 例如图1(a)展示了两个query image和一个target image，我们直觉上相信$iq_2$与$it$更为相似。现在我们将query images于target image相似的部分给用序号标记出来，如图1(b)所示，$iq_2$的大部分可以用$it$中图像片段合成出来，而$iq_1$只有小部分，所以我们认为$iq_2$与$it$更为相似。
如图1(c,d,e)所示，将场景迁移到二进制代码片段中，这里我们以数据流切片strand作为比较单位，因为strand可以更好的克服语法上的差异性，$q_2$与$t$共享三条相似的strand，而$q_1$值共享一条，所以我们认为$q_2$与$t$更为相似。
方法概述
Decomposition into strands: 将程序分解为strand作为基本单元来进行比较，再将strand转换为 Intermediatre Verification Language(IVL)，为每个strand的变量添加$q$和$t$后缀来标识不同的strand。
简单的介绍下IVL：寄存器之间传值使用临时变量进行表示，总是使用64-bit的寄存器，当使用寄存器一部分的时候需要使用临时变量和截断。
Comparing a pair of strands: 分为三步：
- 为两个strands的输入增加相等性假设
- 增加断言来检查所有输出变量的相等性。
- 使用程序验证器来检查断言，并统计有多少变量是相等的
Match Probability: : 定义$s_q$与$s_t$之间的相似性为$s_q$中的变量在$s_t$中具有相等变量的百分比，用$VCP(s_q,s_t)$标识，但注意不对称。比如图3的例子，$VCP(s_q,s_t)=1$，而$VCP(s_t,s_q)=8/9$。
在之后呢，我们将使用$VCP(s_q,s_t)$作为基础来导出相等概率$Pr(s_q|s_t)$。
Local Evidence of Similarity: 定义$Pr(s_q|H_0)$为随机为$s_q$寻找一个匹配的概率（$H_0$表示所有可能的strands）。在$t$中为$s_q$寻找的匹配的重要性程度可以被定义为：
\(L E S\left(s_{q} | t\right)=\log \frac{\max _ {s_{s} \in \operatorname{Pr}\left(s_{q} | s_{t}\right)}}{\operatorname{Pr}\left(s_{q} | H_{0}\right)}\)
除以一个随机概率$Pr(s_q|H_0)$可以是的我们抵消掉一些编译器引入的common strand的影响。
Lifting strand similarity into procedure similarity: 两个程序$q$和$t$之间的global evidence of similarity(GES)就是在$q$中对所有的$s_q$的$LES(s_q|t)$进行累加。
3.Strand-Based Similarity by Composition
3.1 Similarity By Composition
定义全局证据分数$GES(q|t)$表示为query程序$q$相似于target 程序$t$的可能性，GES分数是基于对个局部证据分数$LES(s_q|t)$合并得到的： \(G E S(q | t)=\sum_{s_{q} \in q} L E S\left(s_{q} | t\right)=\sum_{s_{q} \in q} \log \frac{\max _{s_{t} \in t} \operatorname{Pr}\left(s_{q} | s_{t}\right)}{\operatorname{Pr}\left(s_{q} | H_{0}\right)} \tag 1\)
公式最右边的$Pr(s_q|H_0)$表示strand$s_q$匹配一个随机源的概率，在我们的上下文中，这意味着这个strand在corpus binaries中都可以找到，不再单独的来识别query程序。
3.2 Procedure Decomposition to Strands
在CFG的block级别来提取strand，Strand是在基本块中需要来计算一个确切变量值的指令集合（变量的后向切片），直到所有切片都被覆盖了，切片才停止。
在处理小程序的时候，使用更长的strand路径会更好
提取算法如下：
其中Def和Ref表示的是给定指令定义和引用的变量。
简单的描述下算法的流程：
- 刚开始将block中所有指令全部加入
unusedInsts - 从
unusedInsts中取出最后一条指令为maxUsed - 从
maxUsed开始向前遍历每一条指令，若此指令所定义的变量与maxUsed所引用的变量相同，则加入strand - 不断的扩充VarRefed和VarDefed，直到处理完所有指令
3.3 Statistical Evidence
首先定义下VCP，正如之前所说的，VCP可以用来计算两条strand的相似性，当给定相同的输入时，输出一样的比率就是strand的相似性。形式化公式后面再展开。
3.3.1 Strand Similarity as a Probability Measure
定义一个strand$s_q$可以在target 程序中找到的概率为
\[\operatorname{Pr}\left(s_{q} | t\right) \triangleq \max _{s_{i} \in H_{t}} \operatorname{Pr}\left(s_{q} | s_{t}\right) \tag 2\]其中两个strand是输入-输出相同的概率$Pr(s_q|s_t)$是通过对两个strand的$VCP$应用sigmoid函数来估计出来的（这里我们设定sigmoid函数的中间点为$x_0=0.5$）
\[\operatorname{Pr}\left(s_{q} | s_{t}\right) \triangleq g\left(\operatorname{VCP}\left(s_{q}, s_{t}\right)\right)=1 /\left(1+e^{-k\left(V C P\left(s_{q}, s_{t}\right)-0.5\right)}\right) \tag 3\]这样当$VCP(s_q,s_t)=1$时，$Pr(s_q|t)$就越接近于1；当$VCP(s_q,s_t)=0$时更接近于0.参数$k=10.0$比较好，用来设置sigmoid曲线的陡峭程度。
3.3.2 The Statistical Significance of a Strand
这里有这么一种情况，如果strand是平凡的(比较常见的)的话，那么通过公式(3)计算出来的相似度就会比较高。所以作者认为一个query strand不仅仅要相似于target，还要对随机产生的有一个低的相似概率。
为此，作者引入了Likelihood Ratio measure： \(L R\left(s_{q} | t\right)=\operatorname{Pr}\left(s_{q} | t\right) / \operatorname{Pr}\left(s_{q} | H_{0}\right) \tag 4\)
其中$Pr(s_q|H_0)$事实上统计的是一个strand的不重要性，高概率代表$s_q$的低重要程度。这里我们通过对所有$Pr(s_q|s_t)$的值进行平均来估计出随机假设$H_0$:
\(\operatorname{Pr}\left(s_{q} | H_{0}\right)=\frac{\sum_{s_{t} \in T} \operatorname{Pr}\left(s_{q} | s_{t}\right)}{|T|}\)
其中$T$为语料中所有target的所有strand的集合。
3.4 Local and Global Evidence Scores
定义LES为likelihood ratio的对数：
\[L E S\left(s_{q} | t\right)=\log L R\left(s_{q} | t\right)=\log \operatorname{Pr}\left(s_{q} | t\right)-\log \operatorname{Pr}\left(s_{q} | H_{0}\right) \tag 5\]LES分数反应了$s_q$在$t$中具有非平凡语义相同strand的可行度等级，而GES分数反应了$q$可以由$t$中的一些非平凡部分组成的可行度等级。
4.1 Similarity Semantics
preliminaries 定义程序状态$\sigma$为一个pair $(l,values)$，在一个确切的程序位置$l \in Loc$上将程序变量的集合映射到其具体的值:$Var \to Val$。 一个程序$P$所有可能状态的集合为$\Sigma_P$ 。程序的trace $\pi \in \Sigma_{P}^*$用来描述程序单个执行的状态序列$<\sigma_0,…,\sigma_n>$。程序$P$的所有可能traces标记为$[[P]]$。我们还定义$first$和$last$来返回trace中第一个和最后一个状态。
Variable correspondence： 两个状态$\sigma_1$,$\sigma_2$间的变量一致性表示为$\gamma:Var_1 \mapsto Var_2$，是从$\sigma_1$到$\sigma_2$中变量的有偏函数。$\Gamma(P_1,P_2)$为程序$(P_1,P_2)$对的所有变量一致性集合。
stata,trace equivalence: 给定两个状态和一个一致性$\gamma$，如果$\forall (v_1,v_2)\in \gamma:\sigma_1(v_1)=\sigma_2(v_2)$，那么我们就可以说对于$\gamma$这些状态是等价的，并且标记为$\sigma_1 \equiv_\gamma \sigma_2$。如果两个traces $last(\pi_1) \equiv_\gamma last(\pi_2)$，我们就成这些traces对于$\gamma$等价的，标记为$\pi_1 \equiv_\gamma \pi_2$。
定义 1(Strand equivalence) 给领两个strands和一个$\gamma$，在下列条件下，我们认为这两个strands是等价的，即$s_1 \equiv_\gamma s_2$。
(i) 在$\gamma$下，每一个来自$s_1$的输入都能与一些来自于$s_2$的输入匹配上。
(ii) 每一对traces $(\pi_1,\pi_2) \in (s_1,s_2)$ 在输入相同的情况下是等价的，即$\pi_1 \equiv_\gamma \pi_2$。
定义2 (State,trace variable containment proportion) ：我们定义query state$\sigma_q$和target state$\sigma_t$的VCP为在$\sigma_q$中匹配到的值得比例，表示为$VCP(\sigma_q,\sigma_t) = \frac{|\gamma_{max}|}{|\sigma_q|}$，其中$\gamma_{max}$为在所有可能的$\gamma$下两边状态等价时最大的变量等价个数。
定义3 (Strand VCP): 我们定义两个strands间的VCP为
