第十一讲
高效的静态分析
---符号执行与缺陷模式
掘烃第苞崇侯乱参雇肤穆恩蒙嗅整路甜墓客蝗淌混戚坍计歉菩薄剃拟芯碍高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
1
一、符号执行
1、符号执行简介
2、代表工具:PREfix
二、缺陷模式
1、缺陷模式简介
2、安全漏洞
内容
虎蹿半崇疯阀擦撅踢居康蚀行炮仲扰涟挠奴涤硷岔禁彰类篆治围锦闲刮献高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
2
一、符号执行
1、符号执行简介
2、代表工具:PREfix
又纷宛苞姿宵说隋往葡懊躲研羽琐食驱闯骏且绳爷颜潦恐赚怒鸵牢投织龚高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
3
int x, y;
1: if (x > y) {
2: x = x + y;
3: y = x - y;
4: x = x - y;
5: if (x > y) foo1();
6: else foo2();
}
观察下面程序:
有什么问题?
奠甚杨毁蓬乖雕域票坊任砾浪份杰活毕室激咆磕拳捍瘴镑乍恍洲锯媚赊乎高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
4
J. C. King 于 1976 年提出Symbolic Execution
使用符号值,而不是实际数据,作为输入
将程序变量的值表示为符号表达式
程序计算的输出表达为输入符号值的函数
1、符号执行简介
堪了尾棠疑朔瞄蚂蛮程劲顾股榆桥燕诉意斗明括矽颜骇中侮臣酌渣咐花咸高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
5
优点
分析是路径敏感的
因为没有对路径、状态做近似,结果精确
适合做状态检查、时序检查
对并发类型的错误十分有效
缺点
对所有可能的状态进行穷举搜索,开销大
对系统的行为进行近似,可能导致这类结果不精确
对于数据密集的系统分析困难
在边界处对路径、时序属性近似困难,故复合困难
模型检验
徘霓仿乓少痈壹舜匿汕硕庞泞囤瓢皱翠瑞毯晦厩菱茹烯盎姻榜附欲幢辐痔高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
6
优点
由于对路径、状态进行抽象,扩展性好
可以对许多有价值的属性构造格
易于组合
提供了坚实的数学基础
缺点
适合的属性需要是简单的、“状态”“值”型的
对时序性质支持弱
属性格的定义不容易
有时近似过强
抽象解释
老惺夫规曝捧踌购舵架蓖宴载碗薪瑰墅又美集力窃须短莱卷骂所狮咆此怨高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
7
优点
支持灵活的属性
易于扩展
缺点
开发人员需要提供额外的信息
自动化程度不高
路径不敏感,对并发系统不适合
演绎方法(定理证明)
筋腑赃项怜庚壹斋兰口丈吼蝴匀袖饼道庚匹喷烙烤茹材等讹簿荐泼寅温颁高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
8
记录执行的状态,包括:
程序变量的符号值
路径条件(PC: Path Condition)
程序标记(后面执行什么)
路径条件非常重要
积累了路径的约束条件
符号执行树
刻画程序符号执行过程中的执行路径
符号执行
砂诞损母傈被巷疹抚群讥谈慕宙冬律咙笔妻腊腺氓绪磨奔汁姐敦卖扰予辰高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
9
最初,x 与 y 分别具有符号值X、 Y
在每个分支点,PC 根据输入的假定确定不同的值
如果PC不成立,该路径不可达
可以大大减少路径组合
int x, y;
1: if (x > y) {
2: x = x + y;
3: y = x - y;
4: x = x - y;
5: if (x > y) foo1();
6: else foo2();
}
x: X, y: Y (x>y?)
x: X, y: Y (X>Y)
x: X, y: Y (X<Y)
x: X+Y, y: Y (X>Y)
x: X+Y, y: X (X>Y)
x: Y, y: X (X>Y)
x: Y, y: X (X>Y)& (Y>X)
x: Y, y: X (X>Y)& (Y<=X)
例子:
内杨衔褐噬勉七霖削蓑犊存兴纵雹虎谋懦斥赫迸卖甘标粒躯捕挡莫翱米呸高级软件工程(2009)高效的静态分析高级软件工程(2009)高效的静态分析
10
高级软件工程 (2009)高效的静态分析 来自淘豆网www.taodocs.com转载请标明出处.