Abstract
中文
Linux 内核更新频繁，更新过程会提供新的特性和提供代码补丁，但也会引入新的代码问题和安全问题。同时，当前的工具中虽然具有静态检测漏洞的能力，但由于完整的分析会缺乏时效性，无法跟上Linux更新频率。针对这个问题，可以利用增量分析来解决，但受到Linux庞大内核和高误报率的问题，利用增量分析会面临一些挑战。
在该论文中，作者设计和开发了INCRELUX，用于Linux内核的增量分析工具。INCRELUX可以对新旧代码展开漏洞检测，以及跟踪漏洞的生命周期。INCRELUX的设计思路是，采用一个自底向上的、基于函数摘要的分析方式，并采用符号执行来提高精度，降低误报率，从而实现在完整分析的基础上，对新版本快速分析。
通过大量在UBI问题（Use Before Initialization）上的检测实验验证，INCRELUX有以下优势：
- 快速检测 UBI 问题
- 通过基于历史的分析，可以对问题的生命周期进行追踪
- 与完整分析对比，增量分析可以做到几乎一致的分析精度
此外，得益于增量分析技术的引入，与过去完整的分析时间对比，大大缩减分析时间。
implement 实施，执行
Our approach hinges on 我们的方法取决于
via 通过；Via extensive experiments on the challenging problem of finding use-before-initialization (UBI) bugs …
I. INTRODUCTION
中文
Linux 内核开发周期迭代迅速，开发人员一般没有足够的时间对提交的代码进行安全分析，同时下游分发的版本也存在更新延迟的问题，导致会产生长期潜伏的安全漏洞，这一问题可能会导致漏洞在野利用。
目前业界和学术界在Linux内核的安全检测问题上，已有大量基于动态测试或静态分析的研究。在动态测试上，模式测试因测试结果零假阳性的特性，已成为检测内核安全最流行和最高效的方式。静态分析的方式，可以提供极高的代码覆盖率，也可以通过域敏感、流敏感、上下文敏感等软件分析技术，减低误报率和漏报率。但在内核的安全检测上，若将高精度的静态分析引入内核存在高昂的技术成本，提供完整的静态分析也会存在高昂的时间成本。
在静态分析技术中引入增量分析，可以有以下优势：
- 将昂贵的静态分析，带入开发过程中
- 维护者可以快速验证补丁的安全性
- 提供模糊测试无法实现的代码覆盖率
在利用UBITest完整检测Linux内核UBI问题的基础上，作者提出一个针对内核的增量分析框架，并命名为INCRELUX。INCRELUX拥有流敏感、域敏感、上下文敏感、路径敏感这些分析技术，来调高静态分析的精度。
该论文的主要贡献如下：
- 利用INCRELUX可以实现对UBI问题的增量检测，和漏洞生命周期追踪。
- 实现了针对UBI问题的路径敏感分析技术
- 与完整分析对比，增量分析的引入，可以降低分析时间。
downstream distributions 下游分布
ample time 充足的时间
alleviate v 减轻
aforementioned 上述的
leverage v 充分利用
commercial 商业的
academic 学术的
state-of-the-art 最先进的
ill-suited 不合适的
integrate 使。。。成为一体
dramatically 明显地
precision 精确度
II. BACKGROUN
A. Linux Kernel Development
Linux内核是有上万个开发者维护和维护，并根据不同的场景和需求，会有不同的项目分支和特性。Linux的各类发行版本从Linux主线版本、稳定版本、长期支持版中继承代码。
Linux主线版本主要是添加新特性和修复代码问题，稳定版本只是用于修复主线版本中的问题，长期支持版表明当前Linux分支还会长期维护。
主线版本和稳定版本遵循以下版本规章：
Major Versions.
主要版本对应Linux的主要版本，版本的命名规则通常为x.y，新版本一般会在两个月后更新，添加新功能和修复问题，需要关注主要版本中的新功能和新特性，这是产生BUG的主要来源。
Minor Versions.
次要版本，表示稳定版本从主要版本分支出来，但只进行版本维护，需要关注版本更新中代码修复问题。
Release Candidates.
发布版本，是指候选下一个主要版本的次要版本，表示主要版本的中间状态，也需分析。
B. Bottom Up, Summary-based Static Analysis
基于摘要的自底向上的分析，是在得到流程控制图的基础上，从叶节点（函数内部没有调用其他函数）到父节点依次进行函数摘要，并保留分析结果。
C. UBITect: Summary-based Analysis for Detecting UBI Bugs
UBI（Use-before-Initialization）问题是指由使用未初始化的变量，引起的一种内存错误，主要存在代码执行和信息泄漏这两类安全问题。Linux针对UBI问题，并设计了 INIT_STACK_ALL 选项，可以对所有的未初始化变量设置默认参数。Zhai等人针对UBI问题，设计了UBITest。
UBITest也采用基于摘要的自底向上的分析框架，通过流敏感的静态分析和路径敏感的符号执行来提高精确度。UBITest通过创建全局调用图，对叶节点中的变量初始化和变量使用进行函数摘要，再利用子节点的摘要信息迭代，对子节点的调用者进行摘要分析，从而识别直接调用和间接调用中的UBI问题。
在函数摘要中，主要记录以下两种信息，作为函数调用者与函数被调用者间的联系：
- 输入参数是否被要求初始化，描述了对被调用函数输入参数的期望，以确保函数没有UBI错误。
- 函数内代码执行结束后，函数返回值和参数是否被更新
The requirements describe what states are expected from the caller in order for the function to ensure no UBI bugs, whereas the updates describe the state updates of the variables after the function finishes executing.
在通过自底向上的方式，获取所有函数有关Requirements和Updatas的摘要后，可从中大致分析出UBI漏洞是否存在，再通过路径敏感的符号执行，来查看UBI漏洞是否可以被触发，以此来提高准确率。
An Example
以图1为例，来详细说明UBITest的分析过程。在图1中，存在两个函数，stm32_dfsdm_irq和regmap_read。因为stm32_dfsdm_irq函数中调用regmap_read函数，所以regmap_read函数是当前CFG（Call Flow Grpah，控制流图）中的叶函数，并从此开始进行函数摘要。
在regmap_read函数中，reg用于判断逻辑，val用于间接寻址，所以reg和val都需要在传参前，进行初始化，对应的需求（Requirements）都为init。同时，在regmap_read函数中，reg和val都没有进行赋值操作，对应的更新（Updatas）状态不变，更新（Updatas）值为no。
对于val指向的变量val_object，因为只涉及到赋值语句，同时if(reg) return -EINVAL;使val_object可能不赋值，但考虑到调用val_object参数的调用函数的UBI分析，作者认为val_object的需求（Requirements）和更新（Updatas）都为no。同时，为了避免符号执行探索当前语句（*val = some_init_number），需要将当前语句添加到avoidlist。
val_object的上界分析（May分析）见下：
val_obj 存在两种状态：
- 被赋值
- 没有被赋值
即，Updates(val_obj) = {init, no}。
如果保持 val_obj 为
init，这表明 val_obj 已经被初始化，但该假设会产生一个问题：如果在caller的后面代码中，val_obj 被 要求Requirements(val_obj) = init，且实际上Updates(val_obj) = no，MayAnalysis(Updates(val_obj)) = init，将会产生false negative，漏报val_obj的UBI问题。
针对regmap_read的返回值而言，其值只能为-EINVAL或者0，所以regmap_read的更新（Updatas）只能为init。到此，函数regmap_read的摘要已经全部完成，所有参数的需求和更新值见表1。
之后UBITest会检查调用函数stm32_dfsdm_irq代码，在10、11行代码段，检测到对regmap_read函数的调用，引入regmap_read的函数摘要，对status、&status、int_en和&int_en的进行检查和更新。&status和&int_en指针地址变量，满足Requirements(val) = init的约束条件，函数执行后的初始化状态和执行前的状态保持一致。对于status和int_en而言，根据Updates(val_obj) = no，可以推断出，函数执行后的初始化状态还是未初始化。在13和14行，分别存在对status和int_en的变量访问，但status和int_en的初始化状态在执行后依旧为未初始化，由此可以判断出13和14行，存在status和int_en的UBI问题。
最后，UBITest会将UBI的检查结果和avoidlist带入符号执行，可以计算出status和int_en的UBI触发条件为reg为空。
scenarios 场景
conservative 保守的
N/A Not applicable 不适用的
C. UBITect: Summary-based Analysis for Detecting UBI Bugs 中，通过先说明Linux对UBI问题也有关注，并设计了 INIT_STACK_ALL 选项对所有的未初始化变量设置默认参数，之后再引入UBITEST话题。
avoidlist的作用，我还是没有明白。
如果avoidlist是指忽视代码段，那reg是否为空，都可以推出UBI的存在条件。
我的评价avoidlist的存在可能是个鸡肋。
III. DESIGN OF INCRELUX
中文
A. Motivating example
以图2为例，作者说明INCRELUX是如何做到基于历史的增量分析。图2中展示的是Linux内核4.15-rc1到4.16的部分代码变化，添加了mlx5e_params_calculate_tx_min_inline函数。INCRELUX针对4.16进行函数摘要，mlx5_query_min_inline和mlx5_query_nic_vport_min_inline函数摘要在4.15-rc1中已经生成且无代码变动，新添加的mlx5e_params_calculate_tx_min_inline函数需要对其进行函数摘要 。得到所有函数的摘要信息后，对mlx5e_params_calculate_tx_min_inline函数进行UBI问题分析时，发现min_inline_mode存在UBI问题，且存在对应的触发条件。
B. Considerations
以下三点是设计INCRELUX需要考虑的问题。
Consideration 1: Correctness compared to the wholeprogram analysis.
从理论上来说，增量分析和完整分析的结果相同，两者分析的摘要信息一致，只是增量分析只对修改的代码进行重新函数摘要，从而实现降低分析时间的目的。
Consideration 2: Function summary design and re-analysis scope.
在函数摘要中，INCRELUX对调用函数与被调用函数之间参数的约束条件（如，需求和更新状态）进行摘要。在重新分析过程中，INCRELUX只需要对被影响的调用函数重新分析对应的安全问题。
论文中也提及是否对全局变量分析，但全局变量分析在提高分析精度的前提下，会使增量分析复杂化，与INCRELUX的目不一致。
INCRELUX希望在利用增量分析的基础上，对所有需要重新分析的代码段进行分析。自底向上的函数摘要分析保留了函数间的调用关系，可以用于找出所有需要重新分析的函数，所以INCRELUX采用了自底向上的函数摘要的方法。
通过本段，可以发现作者考虑到了 high-order taint vulnerabilities的问题。但对全局变量的分析，不是本篇论文的主要目的，作者在后续中也就没有继续讨论了。
Consideration 3: Extensibility.
在本小节中，作者观察到识别UBI问题的方式，实际上就是采用数据流分析的方式。UBI问题的检测方式，也可以视为污点分析来进行检测，将可能产生UBI问题的语句认为是污点汇聚点，未初始化变量认为是污点源。
C. System Overview
INCRELUX在分析新版本时，会先与旧版本进行比对，找到哪些函数发生了变化。其次，执行依赖分析来计算函数之间的依赖关系图。为了检测UBI问题，INCRELUX还对新版本的全局调用图（包含间接调用）进行分析。同时，INCRELUX还计算调用图调用图的强连通分支( SCC )，以便为不动点分析做好准备。最后，INCRELUX将执行实际的增量分析，该步骤将静态分析和欠约束符号执行( UCSE )相结合，生成上一版本和当前版本之间不同的bug集合。
D. Bottom-up, Summary-based Incremental Analysis
算法1，是INCRELUX中分析算法的伪代码，具体描述了如何实现基于摘要的自底向上的增量分析算法。
注意，INCRELUX会对每个SCC都执行不动点分析，这意味着循环或者递归函数会被分析多次，直到它们的摘要收敛。一旦没有摘要更改，INCRELUX就从DiffSet中的下一个函数开始分析。在DiffSet中的所有函数都被处理之后，可以确定所有需要分析的函数都被重新分析了，并且所有发生更改的函数摘要都已被完全收集。
Tracking Warnings Changes.
在上面的分析结束后，将会自动产生漏洞警告信息，并分成三类：
- 问题已修复
- 问题依旧存在
- 引入新的问题
Under-Constrained Symbolic Execution (UCSE)
与UBITEST会对所有的漏洞报告进行符号执行不同，INCRELUX只符号执行新漏洞或者那些被重新分析的存在警告的相关函数。
全局变量确实会对符号执行的判断有影响，但作者认为，通过Under-Constraint，全局变量不会影响到INCRELUX分析的代码。
由于KLEE中路径调度的不确定，INCRELUX的UCSE组件的结果与UBITEST的结果存在微小差距。但作者并不认为这并是INCRELUX的一个缺陷，因为同样的非决定算法也会影响同一分析的两个不同运行的结果。
feasibility n. 可行性，可能性
significantly adv 显著地
expedite v. 加速，促进
aggressively adv. 积极进取地
Progressively adv. 渐进地；日益增多地
aggressively adj. 随后的，接着的；（河，谷）后成的
considerations n. 考虑；注意事项（consideration 的复数形式）；体贴
Correctness n. 正确性
Extensibility n. 展开性；可延长性
identical adj. 完全相同的；同一的；（双胞胎）同卵的；恒等的
Indeed, we make the observation that the UBI bugs are fundamentally bugs that can be discovered by data flow analysis. 事实上，我们观察到UBI bug是可以通过数据流分析来发现。
semantics n. 语义学；语义论
initializes vt. 初始化（initialize 的第三人称单数）
converge v. （使）汇聚，集中；（观点、目标）趋同；（数）收敛
retain v. 保持，保留；保存，储存；记住；付定金聘定（尤指律师）；留用（员工）
categories n. 种类，分类； 范畴（category 的复数）
fundamental adj. 根本的，基本的；必需的，必不可少的；不能再分的
identical adj. 完全相同的；同一的；（双胞胎）同卵的；恒等的
C. System Overview中的不动点分析的作用，是处理循环和迭代的调用关系。
之前的笔记没有翻译出
fixed-point analysis的含义，应该是不动点分析（达到收敛目的），太尴尬了。
A function is associated with a warning if it is a transitive caller or callee of the function containing the warning’s variable declaration; these are the functions that could possibly affect path feasibility. 如果函数是包含警告变量声明的函数的传递调用者或被调用者，则该函数与警告关联；这些函数可能会影响路径可行性。
全局变量确实会对符号执行的判断有影响，但作者认为，通过Under-Constraint，全局变量不会影响到INCRELUX分析的代码。
IV. IMPLEMENTATION
中文
相较于完整分析的UBITest，INCRELUX添加的主要功能如下：
- 函数对比
- 函数摘要
- 重新使用函数摘要的逻辑
- 对漏洞进行欠约束的符号执行的逻辑
Compiling kernel source code.
作者使用-O0的优化选项（不进行优化）和启动调试信息的方式，从内核源代码中生成IR字节码文件，以确保INCRELUX有识别问题所需的源代码位置和变量名信息。
Indirect Call Resolution.
通常有三种类型的间接调用解析技术被广泛用于Linux内核的静态分析：
- 来自KINT的指针分析
- 来自Unisan的基于类型的分析
- 结合两者的基于类型的多层次分析
为了避免在SCC分析上花费大量时间，INCRELUX采用指针分析的方式来对间接调用进行分析。同时作者也计划研究利用基于类型的分析，生成合适数量的SCC。
Diff Function Extraction
函数的变化主要有两个来源，第一个是源代码的直接修改；第二个是整个文件的添加或者删除，INCRELUX完全支持这两种类型的更改。
UBI warning detector.
在UBI问题的检测上，沿用UBITEST的检测规则。同时作者提出，可以将漏洞检测的分析上，向污点分析方向进行研究。
Guided Symbolic Execution.
尽管采用增量的方式来应用符号执行，避免重复计算的问题，但符号执行的成本依旧十分高昂，存在路径爆炸的问题。对此，INCRELUXE根据抽样实验的经验，对执行分析的占用内存和时间进行限制。
Bug Identification and Tracking Across Versions.
考虑到存在一个变量名对应多个未初始化漏洞的情况，INCRELUX在漏洞报告中将其进行关联。此外，为了研究问题的生命周期，INCRELUX将相同变量的不同内核版本的问题视为同一个问题。
bloating v. 鼓胀，胀大（bloat 的现在分词形式）
downside n. 缺点，不利方面；复数 downsides
V. EVALUATIONS
中文
为了评估INCRELUX的能力和增量分析的优势，作者对Linux内核采取一个大规模实验，范围选取上以Linux内核v.4.14-rc1版本作为基准，增加到Linux4.19版本，覆盖一年的开发周期。同时，INCRELUX对4.14.y和4.15.y这类长期维持版本，和主要版本的更新变动进行测试。此外，作者还在论文中展示了INCRELUX的分析结果，包括分析速度改进、新bug的发现、补丁确认和等价性分析(即，检查增量分析和全程式分析的结果是否保持一致)。
A. Evaluation Scope
在实验中，作者发现主要版本的第一个候选版本后面更新的其他候选版本，含有更多的函数变化。对稳定版本的测试中，发现稳定版本由于只涉及到代码修复，提交中的函数变化相对于其他版本要少很多。
B. Speed Improvement Analysis
Incremental Analysis for the Mainline Versions.
表2中展示了INCRELUX的主要分析结果，INCRELUX针对大量变化的候选版本也能缩减分析时间。在压力测试时，INCRELUX对从4.19到5.4和从5.4到5.9，进行直接的增量分析，实验结果显示优势不明显。因此作者建议大版本更新时，采用完整分析，对于持续的版本更新，可以采用增量分析的方式来安全检测。
Incremental Analysis for Stable Versions.
表3和表4分别给出了稳定版本v4.14和v4.15内核的增量分析结果，可以观察到，增量分析可以达到快速分析的目的。
Relations between the number of functions reanalyzed and the time that the incremental analysis incurs.
图4中描述了不同版本的分析结果，表明了被分析函数的数量与分析时间存在线性关系。
Incremental Analysis for Each Patch.
如表5所示，作者展示了INCRELUX可以快速对代码提交进行分析，可以帮助贡献者快速检测错误和确认补丁的有效性。
C. Time Breakdown
在图5中，以v4.14到v4.15 – rc1的分析结果为例，展示了增量静态分析的时间占用情况。此外，对于不同函数而言，占用的时间也不相同。
D. Correctness/Equivalence Analysis
作者通过对v4.14.20和v4.15的内核代码分别进行增量分析和完整分析，两者在产生的警告集上保持一致。符号执行的验证阶段中，两种分析的结果只存在细微差距，作者认为这是由KLEE的不确定性导致。
E. Bug Finding Results
Reported warnings.
作者随机采样了v4.14到v4.19的所有警告中的44个bug，其中有22正确结果，这些问题都是由rv1候补版本引入，17个报告被维护者采纳，剩余5个未被采纳。
False Positives and False Negatives.
44中的另外22个结果，被证实为错误结果，14个错误结果，是静态分析的完整引导缺失导致；7个错误结果，是因为缺乏精确的间接调用分析；最后一个错误结果，是因为缺乏对数组的识别。在假阴性的评估上，作者发现漏报是由不精确的间接调用分析和缺少堆的模型。
Security Impact.
作者对被接受的17个报告进行安全分析，并认为存在以下触发条件：
- 未初始化的变量是否会导致控制流偏离。
- 该变量是否表示对象的大小。
- 未初始化的变量是否会传播到用户空间
F. Patch Identification Results
Reported Patches.
INCRELUX可以帮助开发人员判断补丁是否按预期工作。在v4.14到v4.19的增量分析中，INCRELUX正确地识别出两处UBI问题修复补丁。
False Positives and False Negatives.
理论上，由于补丁分析存在假阳性，可能在未修复的的情况下，分析结果已认定漏洞已经修复。同样，补丁分析也存在假阴性的可能，分析可能会错过真正的修复补丁。但具体的分析过程中，作者没有发现上述两种情况的发生，归因于补丁分析中的符号执行。
Bug Lifetime and Case Study.
图6展示的是INCRELUX追踪到的完整的漏洞生命周期。INCRELUX通过增量分析，可以检测到在v4.15-rc1中的UBI漏洞，也可以检查到v4.16-rc1版中代码发现变化，重新对函数分析后，发现err在所有分支中都已被初始化，问题已得到修复。
demonstrate v. 证明；示范，演示；表露；游行，示威
efficacy n. 功效，效力
progressively adv. 渐进地；日益增多地
consecutive adj. 连续的，不间断的
consistent adj. 始终如一的，一贯的；持续的，连续的；固守的，坚持的；一致的，吻合的
exhaustive adj. 详尽的，彻底的；消耗的
initial adj. 开始的，最初的；（字母）位于词首的
compelling adj. 令人信服的，有说服力的；引人入胜的，扣人心弦的；非常强烈的，不可抗拒的
imprecision n. 不精确；不严密
non-trivial 非平凡的
VI. RELATED WORK
中文
A. Bug Detection Tools for the Linux Kernel
Static Analysis Tools for the Linux Kernel.
目前相关研究中，已经有多种的工具来发现Linux内核中的bug，有些是针对特定类型的bug，有些具有扩展性。同时存在商用的静态增量分析工具，但作者认为缺少符号执行工具，且处理更新的代码逻辑存在问题，容易产生误报。
Bug detection frameworks for the Linux Kernel.
有关Linux Kernel的漏洞检测框架的研究中，有针对函数输入的污点分析框架、针对枚举交叉污染流的分析工具、类型限定推荐的框架和过程内分析。
Dynamic Analysis Tools for the Linux Kernel.
动态分析被广泛应用于在运行时捕获Linux内核中的bug。这类技术包括基于管理程序的检测和模糊测试。动态分析的基本限制时，无法测试未执行的代码段。
B. Incremental Analysis and Regression Test
在增量分析框架上，Facebook Infer可以实现对多种漏洞的静态增量分析。但与INCRELUX比较，存在UBI问题检测过于激进、函数摘要拓展性差、缺少不动点分析等问题。回归验证是另一个与代码变更相关的概念，主要是检查软件回归，并确保一个旧的功能仍然在新版本中工作，但目前没有用于Linux内核的增量分析。
C. Security patches
在识别安全补丁的研究上，第一种方式是利用提交的消息，对commit进行分类，但并非所有的commit都添加标签。第二种方式是利用静态分析和符号执行来自动区分安全补丁和正常的代码提交。
inspection n. 视察；检查，审视
insufficient adj. 不充分的，不够重要的
erroneous adj. 错误的，不正确的
type qualifier framework 类型限定框架
VII. DISCUSSION
中文
INCRELUX使用原则性的方式对Linux内核进行增量分析。虽然INCRELUX在实现目标方面非常有效，但在UBI缺陷检测方面也存在一定的局限性。首先，INCRELUX只跟踪了未初始化的栈变量，而不是未初始化的全局状态变量(即堆或全局变量)。其次，INCRELUX也不跟踪未初始化的堆栈变量传播到后续被使用的全局状态。最后，INCRELUX只检测单个线程中的UBI bug，还不能处理跨多个线程中的安全问题。
as opposed to 与……相反
VIII. CONCLUSIONS
中文
在本文中，作者设计并实现了INCRELUX，这是一个对Linux内核进行原则性增量分析的框架。INCRELUX在主线版本和稳定版本中都是有效的，并且提供了一种有效的渐进方法来检测bug，与现在昂贵的完整的内核分析相比，每次发布新的Linux内核版本都需要执行。这种加速帮助开发人员在合并发生之前快速识别bug，从而实现更安全的Linux内核版本发布。通过跟踪Linux版本中的bug生命周期，INCRELUX能够识别潜在的难以利用的bug以及需要立即关注的新bug。同样的特性也允许INCRELUX有效地从其他正常提交中消除错误修复。作者在相当大的一组Linux版本上对INCRELUX的评估表明，INCRELUX极大地减少了检测bug的分析时间与对同一版本的整体全部分析相比，它通过对新版本的增量分析得出的结论能够达到几乎完美的一致。作者指出了INCRELUX的未来工作。
问题（三个）
- 能否通过模糊测试的方式，或者其他方式，进一步提高识别精度？
模糊测试确实可以（无假阳性），但如何设计合理的测试方案，又将是一个新问题。
- 其他针对内核的静态分析工具，可否延用INCRELUX的增量设计思路？主要难点在于哪里？
可以，但需要设计的新的函数摘要。以整数溢出问题的增量分析来说，需要对函数内部的每个整数变量的区间分析结果进行摘要，之后再调用INCRELUX的分析框架。
10/31 Note：在 IV.UBI问题检测上，作者提出了这个设想。
However, as mentioned earlier in §III, it is possible to add additional taint-style bug detectors, e.g., integer overflow, which we leave as future work.
- INCRELUX的设计方案是否存在遗漏或者设计问题？
a. index-sensitive 即对于复杂结构的变量没有详细分析，如 a.b[1]未初始化的情况。
b. High-Order Taint Style Vulnerabilities，没有处理全局变量。
INCRELUX也不跟踪未初始化的堆栈变量传播到后续被使用的全局状态这种情况
其他
中心思想：
INCRELUX is a tool that is flow-sensitive, field-sensitive, context-sensitive, partially path-sensitive, and implements the bottom-up, summary-based Incremental analysis, which is effective across both mainline and stable versions, and provides an effective progressive way to detect bugs with dramatic speed ups compared to today’s expensive whole-kernel analysis that needs to be performed each time a new Linux kernel version is released.
Under-Constraint 的翻译问题：
Under-Constrained Symbolic Execution with Crucible – Galois, Inc.
参考该文章中，对 Under-Constrainted Symbolic Execution的定义，认为是欠约束，即不考虑赋值语句下的符号执行。
