软件安全中由于程序实现过程中程序员的人为因素引入的占比很高。
基于静态分析的程序验证是保障软件安全性和正确性的主要方法，而循环分析是静态分析中面临的最大挑战之一。
问题：在静态分析中，由于循环的迭代次数无法确定，runtime value 使得无法对循环的所有行为分析和检测，从而影响程序验证和高覆盖率测试用例生成的效率。
1.对循环进行建模，分类。 分析循环迭代规律，路径依赖自动机 PDA。 循环多路径间的交错迭代模式。
循环归纳和总结 依赖 多路径的迭代顺序， 以及变量在路径上的可归纳性
分为4类，
多路径整型循环总结， 多路径的交错迭代会增加分析难度。
计算析取式循环总结：对不同类型整型循环进行分类分析，利用变量的可归纳性，对其在PDA 每条path上的多个路径一次归纳总结，得到此变量在这个path上执行后的结果。
如果包括loop, 则对loop进行分析，最终所有的path都进行总结计算得到循环的最终总结。
针对多路径迭代无规律或者变量不可归纳的整型，提出多种策略将其抽象为可总结的循环。
break loop.
多路径字符串循环： 如果在循环中索引变量计算出错，容易造成缓冲区溢出的问题。 在字符串循环迭代中，每条路径遍历字符串中的部分字符，而路径上的字符串条件约束所遍历的字符串子串。
对循环中每条路径，分析索引变量在该路径上的更新值的字符串的范围，并分析路径上的字符串条件生成子串的约束条件。
循环终止性分析：停机问题，分而治之，先分析PDA每条路径的终止性，再基于路径间依赖关系判定整个循环的终止性。
技术问题： 如何解决： 结果如何：
关于 loop analysis的方法有： 1) loop unwinding: 将loop展开固定次数，只能检查部分程序的行为； 2) loop invariant inference：每次迭代中都满足的性质，没有足够强的不变量；ture对任何循环都是不变量，但不够强，无法使用；不变量的生成依赖不停展开循环以计算不动点，消耗大量时间。 3) loop summarization：计算输入和输出的关系，给定一个循环和输入（循环的前置条件）在不执行循环的情况下计算输出结果（后置条件），从而避免不断的迭代循环。
Loop unwinding: 基于抽象解释 53 ， 不停迭代循环直到发现不动点。 引入widening符号，可能会导致结果不准确。 已有的研究 54-57 提出加速循环迭代并减少widening引入的不准确性。
多路径循环：循环内多个if-else分支导致循环具有多种不同的迭代转换为多个单路径循环，并为每一个循环计算不变量。
step 1: 将一个多路径循环转换为多个单路径循环，为每个循环计算不变量。 step 2: 将一个循环分隔为多个阶段，为每个阶段计算不变量。
可能会出现 多路径交错执行出现无限的阶段数或者无限单路径循环。
可以通过动态执行，得到运行时的信息，根据每一个path进行分析，但是这样很耗时。
Comments