摘要¶

论文[^1]

1. 语义等价的代码块：
   1. 代码块的语义由代码块的输入输出关系的符号公式（symbolic formulas）定义
   2. 用 定理证明器theorem prover来验证两个代码块之间的语义等价
2. 以代码块作为基本元素，用最长子序列模糊匹配的方式来计算两段程序路径（path）的语义相似度

一堆问题：

1. 二进制？ 0101？反向工程？我还真没玩过这玩意
2. obfuscation-resilient， 代码混淆？ 大概类似于编译后的min.js代码文件无法阅读？还有多种
3. 最长公共子序列（子代码块）， 这个简单， 动态规划
4. 语义等价 semantical equivalence？这个能做到？就用一组符号公式？
5. 代码块 怎么算个代码块
6. 定理证明器又是什么
7. 路径的定义是什么， 二进制代码的一次执行？

对我来说，最没概念的就是反向工程reverse engineering这块了

导论¶

三个层次的语义：

1. 基本代码块
2. 路径Path
3. 整个程序

symbolic execution technique 获得 一组符号公式， 以表示代码块的输入输出关系。

导论和摘要永远差不多的~~~

总览¶

方法论¶

给两段程序（原告和被告）， 要判断抄袭、重复的话， 不只是整段相似， 可能是其中一段、核心部分抄袭。

现有的方法中，基于程序语法 syntax, 和 基于系统调用依赖图 system call dependency graphs的方法都不是很靠谱

所以提出基于 formal program semantics 的方法， 但问题是 formal logic 有相等而少相似

本文结合了2种技术，在基本块、路径、函数、程序四个不同层次（怎么又多了一层） 定义代码定义。

一种技术是在二进制代码的基本块层次 进行形式语义定义， 不仅有语义等价，还要有语义相似度。

第二种技术在执行路径层面上定义语义， 在两段路径间， 计算语义等价基本块的最长公共子序列。

用子序列长度与原长度的比， 作为路径的语义相似度。 验证 一些输出公式是否在嫌疑代码中也等价存在。

定义两个基本代码块的语义相似程度， 大于阈值， 则为等价

进而在LCS计算过程中使用。

块相似¶

严格语义等价¶

At the binary code level, these variables are represented as registers and memory cells

所以 binary code 其实是汇编语言？

Via symbolic execution, we get two symbolic formulas

但没有解释 theorem prover 是什么

相似度¶

严格等价很容易被糊弄过去，比如随便加个新变量

所以， 作者提出对原告代码的每个输出变量进行独立检验， 验证嫌疑代码中是否存在一个对应。

形式化¶

定义两组变量X和Y， 定义X和Y 变量对等价公式Pair-wise Equivalence Formulas of Input Variables

$$ p(X, \pi(Y)) = \Lambda_{i=0}^{n} (X_i = \pi_i(Y))$$

Let π(Y ) be a permutation of the variables in Y

定义输出等价~~~

∀y 1 ∈ Y 1 . ∃y 2 ∈ Y 2 ,p(X 1 ,π(X 2 )). p(X 1 ,π(X 2 )) =⇒ y 1 = y