北大软件马森 - 基于静态分析的程序缺陷自动发现技术

2020-02-27 838浏览

  • 1.北大 软件 打造富有生命力的软件 CREATE THE VITALITY OF SOFTWARE 马森 北京北大软件工程股份有限公司 2017年6月
  • 2.内容提要 2 背景 静态分析技术 相关工具 实现技术及成果
  • 3.背景及必要性 1978年,Hatford体育场倒塌 1985年,Therac-25放射治疗仪 1988年,蠕虫程序 1996年,Ariane火箭 2005年,EDS 儿童资助系统 2006年,熊猫烧香 7000万美元 三人死亡,三人重伤 蔓延互联网 损失5亿美元 损失约5亿多英镑 损失约1亿美元 OWASP历年安全问题Top10多数与程序代码相关 OWASP Top 10 (2004) A1 – 未验证输入 A2 – 失效的访问控制 A3 – 失效的身份认证和会话管理 A4 – 跨站脚本 (XSS) A5 – 缓冲区溢出 A6 – 注入漏洞 A7 – 不正确的错误处理 A8 – 不安全的加密存储 A9 – 拒绝服务 A10 – 不安全的配置管理 OWASP Top 10 (2007) A1 – 跨站脚本 (XSS) A2 – 注入漏洞 A3 – 恶意文件执行 A4 – 不安全的对象直接引用 A5 – 跨站请求伪造 (CSRF) A6 – 信息泄露和不正确错误处理 A7 – 失效的身份认证和会话管理 A8 – 不安全的加密存储 A9 – 不安全的通信 A10 – 没有限制URL访问 OWASP Top 10 (2010) A1 – 注入漏洞 A2 – 跨站脚本 (XSS) A3 – 失效的身份认证和会话管理 A4 – 不安全的对象直接引用 A5 – 跨站请求伪造 (CSRF) A6 – 安全配置错误 A7 – 不安全的加密存储 A8 – 没有限制URL访问 A9 – 传输层保护不足 A10 – 未验证的重定向和转发 OWASP Top 10 (2013) A1 – 注入漏洞 A2 – 失效的身份认证和会话管理 A3 – 跨站脚本 (XSS) A4 – 不安全的对象直接引用 A5 – 安全配置错误 A6 – 敏感信息泄露 A7 – 功能级访问控制缺失 A8 – 跨站请求伪造 (CSRF) A9 – 使用含有已知漏洞的构件 A10 – 未验证的重定向和转发 软件 灾难 只有代码中的安全缺陷得以及时消除, 代码静态分析可以帮助用 代码静态分析工具主要被国外产品 最终形成的软件产品才能具备较高的 户从根源 上减少 30%-70% 所垄断,国内尚无成熟工具,存在 安3 全性,有效降低整体系统安全风险 的软件安全问题 安全隐患,无法做到自主可控
  • 4.自动化漏洞发现比赛-CGC CGC决赛 七支参赛队伍 每支队伍: 1280核 16TB内存 128TB存储空间 • 2016年8月美国DAPRA举办首届CGC挑战赛, 目的是自动挖掘、利用及修复代码中的安 全漏洞。 • 卡耐基梅隆大学Brumley团队的Mayhem夺得 第一名 • MayHem在和人类的PK中处于劣势 在漏洞挖掘领域,机器远未像Alpha Go在智能搜索领域取得的 成绩显著 4
  • 5.自动化漏洞发现比赛-CGC 1st:动态模块 CMU 污点分析 Mayhem 插桩代码 虚拟化执行 静态模块 符号执行 路径选择 利用生成 5 状态保存 2nd:3rd:GrammaTech & Virginia Tech UC-Santa Barbara Xandra MechaPhish 静态漏 洞分析 动态符 模糊测试 号执行 符号执行 漏洞确认引擎 动态分析
  • 6.静态语义检测与动态测试的互补 动态测试 静态语义检测 • 执行单一的路径 • 对关键的功能性测试很有效 6• 对于Corner情况很难 • 执行“符号”分析 • 对于具有缺陷模式的Corner情况非常有效 • 不能进行功能性测试
  • 7.内容提要 7 背景 静态分析技术 相关工具 实现技术及成果
  • 8.未知缺陷自动发现的基本流程 测试 用例 8 源程序 解析 模型构建 AST 程序流图 静态单赋值表示 控制流图 数据流图 编译 抽象解释 符号执行 图可达 抽象方法 程序状态空间 函数调用图 指针指向图 SMT SAT 二进制程序 模糊 测试 执行 缺陷模式 检索 基于缺陷模式的 逻辑表达式 CWE CVE OWASP … 运行行为 动态分析 逻辑表达式求解 检测结果 动态测试用例生成
  • 9.未知缺陷静态检测技术发展历程  移动端安全漏洞的检测  动静结合分析  稀疏值流图、值依赖图技术  切片技术  图可达技术  指向分析技术、SAT  数据流分析技术  符号执行技术  抽象解释技术 1990-2000 1980-1990 2000-2010 2010-今  更多形式化技术融入,Shape Analysis,更完善的指向分析、Bit- 1970-1980 Level符号执行技术、八面体技术等  多种数据流分析技术结合  SMT技术有了很大进展  模型检测技术  并行程序分析(数据竞争、死锁)  指向分析技术+annotation方式的检测  典型工具:法国Astree、美国  典型工具:美国Lint系列工具 Coverity Prevent、韩国Sparrow 9
  • 10.未知缺陷自动发现的基本流程中相关概念 基本分析相关 Control Flow Graph(CFG):控制流图 Call Graph(CFG):函数调用图SSA:静态单赋值 Super Graph:控制流图与调用图的 Mod-effect:修改影响分析,表达指针修改后对其他引用的影响 Dataflow Analysis:包括前后支配分析、到达定值分析、活跃变量分析等 继承关系分析:分析类之间的继承关系 Points-to:指向分析,表达程序中指针的指向关系 建立程序状态空间 • 抽象解释理论是使用一个基于“抽象对象域”上的 符号执行是将程序源代码中变量的值采用抽 较低代价的计算过程来抽象逼近基于“受检程序指 象化符号的形式表示,模拟程序执行目的是 称对象域”上的计算过程,从而使得程序抽象执行 分析程序中变量之间的约束关系,不需制定 的结果能够尽量反映出程序真实运行过程中的部分 具体的输入数据,将变量作为代数中的抽象 信息 符号处理结合程序的约束条件进行推理,结 果是一些描述变量间关系的表达式 图可达性分析根据分析问题的不同 将程序应用一些函数分析技术或者 算法转换为相应的图形,然后利用 上下文无关语言的理论,计算点与 点的可达性 10
  • 11.基于同源分析的已知缺陷发现的基本流程 源代码及二进 制代码数据源 抓取 缺陷数据源 CNNVD NVD 抓取 CAPEC 索引 第三方代码库 (二进制/源码) 待检测软件 (二进制/源码) 搜索 基于文本:代码行特征向量 基于单词:单词特征向量 基于AST:基于单词序列特征向量 索引 基于程序依赖图:子图特征向量 第三方代码漏洞库 使用的第三方代码列表 匹配 基于度量:度量特征向量 确认 11 漏洞报告
  • 12.内容提要 12 背景 静态分析技术 相关工具 实现技术及成果
  • 13.源代码漏洞自动发现工具 工具名称 Coverity Prevent Klocwork Insight HP Fortify FindBugs Clang cpplint Polyspace Astree 13 Sparrow 研发机构 美国Synopsis公司 美国Rogue Wave Software公司 美国HP公司 美国Maryland大学 美国UIUC 美国谷歌 美国MathWorks公 司 法国巴黎LIENS实验 室 韩国首尔国立大学 主要分析技术 符号执行,模式 匹配 符号执行,区间 分析 数据流分析,模 式匹配 模式匹配 符号执行 模式匹配 抽象解释 抽象解释 抽象解释 典型工具 国内工具:  北京大学 CoBOT  基于值依赖图  支持C/C++/Java语言  北京邮电大学 DTS  基于符号执行的实现方式  支持C/C++/Java语言 国外工具  Synopsys Coverity  基于符号执行的实现方式  支持C/C++/Java/C#/Python语言 国内工具要么支持缺陷种类少,要么 误漏报过高运行效率低
  • 14.二进制漏洞自动发现工具 工具名称 研发机构 Veracode 美国Veracode公司 Codesonar 美国GrammaTech公司 Vine 美国加州大学伯克利分校 BAP 美国卡耐基梅隆大学 Codesurfer/x86 美国威斯康辛大学 McVeto 美国威斯康辛大学 Bindead 德国慕尼黑理工大学 Angr 美国加州大学圣芭芭拉分校 Jakstab 德国达姆施塔特理工大学 Valgrind 开源社区(起源于英国剑桥) TEMU 美国加州大学伯克利分校 Triton 法国Quarkslab 14Protecode 美国Synopsys公司 主要分析技术 禁运未知 禁运未知 数据流分析,符号执行 数据流分析,符号执行 值集分析 模型检查 抽象解释 符号执行 符号执行 代码插桩,污点分析 模拟执行,污点分析 动态符号执行 模式匹配 典型工具  Bitblaze  动静结合,基于Vine和 TEMU  效率较低,不支持某些 指令集的解析  Triton  基于动态符号执行的测 试用例生成  难以应用于大型工程  Protecode  基于同源分析检测二进 制代码漏洞  不支持未知漏洞的检测 二进制漏洞检测工具在国内 处于空白状态
  • 15.静态测试工具应用:编码规则、缺陷与漏洞测试 国际标准  MISRA C/C++  由MISRA提出的C语言开发标准。目的在于提高 嵌入式系统的安全性及可移植性  MISRA C 2004,分为21类,共计141项  ISO 17961 安全编码标准,45类  MISRA C++ 2008,分为21类,共计228项 国家标I准SO  GJB 8114-2013  软件C/C++语言安全子集及编程规范  GJB 5369-2005  由航天科工集团公司提出,并结合航天型号软件 特点,经裁减补充而成。分为15类,共计138项 行业标准  921 C-2007  依据GJB 5369,制定了航天“921”工程C语言软件 编程准则和要求。分为15类,共计163项  BACC C-2008  航天某单位C语言编程规范,分为17类,共计134项  CRSC C-2014 15  高铁领域C语言编程规范,分为18类,共计218项 指针缺陷类型\安全等级 内存泄漏 资源泄漏 空指针解引用 释放非堆内存 释放未分配的内存 Critical Severe (1级) (2级) 4 1 16 11 2 使用已释放的内存 44 函数返回局部变量的地址 3 未初始化使用 41 释放不成功 合计 30 11 Error (3级) 1 1 其他缺陷类型\安全等级 Critical (1级) 不可达路径 2 非法计算 库函数(打印) 库函数(网络访问) 库函数(输入输出) 库函数(本地访问) 库函数(宏) 合计 2 Severe (2级) 1 4 10 1 16 CWE缺陷 Error (3级) 4 5 20 22 6 4 61  OWASP中活跃且 严重性等级较高 的漏洞:  缓冲区溢出(27种)  数组越界 (24种)  整数溢出(15种)  浮点数溢出(15种)  SQL注入(10种)
  • 16.静态测试工具应用场景(以库博为例) 开发人员应用 持续集成应用 测试人员应用 采用IDE插件的方式, 与 VC 、 Tornado 、 KMC等开发工具集成 16 每天定时从版本服务器 中更新、检测,第二天 将结果回送 利用管理界面上传不同 工程的代码、随时进行 分析检测
  • 17.测试结果 为了验证编码规则和程序缺陷检测方面的效果,需要进行 三种类型的测试 中等规模开源项目,测试误报率和漏报率 选择SPEC 2000(由标准性能评价组织SPEC开发的用于评测通用型CPU性能的基准程序测试组)中十个开源项目 进行验证分析,项目规模在万行至几十万行之间,主要目标是测试COBOT的误报率和漏报率 较大规模开源项目,测试运行效率及误报率 选择规模在三个百万行以上的大型开源项目,主要目标是测试工具的运行效率及误报率 实际应用项目,综合评估实际运行效果 将工具部署到实际运行环境中,对约数十万行代码进行检测,综合评估实际运行效果。 17
  • 18.航天某单位应用比较:程序缺陷分析 项目 名称 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 总计 18 代码行 4108 3715 1287 331 3641 2744 785 3304 7339 14480 8515 2417 2669 3457 2173 4158 3251 1650 1912 1235 1621 537 14254 89583 CoBOT(库博) 检测 时间 20.2 21.1 10.5 10.8 13.5 14.8 10.8 21.5 16.1 20.7 17.2 20.7 21.9 32.2 22.6 20.5 23.1 13.3 11.1 13.2 10.2 10.8 20.3 397.1 误报数 /总数 0/4 2/5 0/3 0/0 0/0 0/0 0/0 0/1 0/0 0/0 0/2 0/6 0/8 1/9 0/6 0/0 0/0 0/2 0/3 0/0 1/1 0/0 0/1 4/51 Klocwork 检测 时间 48.1 44.4 38.2 28.1 63.2 61.3 31.3 51.4 21.2 31.6 42.6 49.2 45.3 56.4 50.3 45.2 43.5 65.3 43.2 35.5 65.5 35.4 42.8 1039 误报数/ 总数 0/2 0/3 0/3 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/6 0/8 0/8 0/6 0/0 0/0 0/2 0/3 0/0 0/0 0/0 0/0 0/41 合计 2 3 3 0 0 0 0 0 0 0 0 6 8 8 6 0 0 2 3 0 0 0 0 41 相同缺陷 资源 泄漏 2 3 0 0 0 0 0 0 0 0 0 6 8 8 6 0 0 2 3 0 0 0 0 空指针 解引用 0 0 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 38 3 使用释 放内存 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 CoBOT(库博)发现了6个 Klocwork未发现的缺陷:  项目23:空指针解引用 1个;  项目11:资源泄漏 2个;  项目8:资源泄漏 1个;  项目1:资源泄漏 2个 漏报率:CoBOT在10%左右, Klocwork在20%以上 误报率:CoBOT在10%-20% 之间,Klocwork低于10%
  • 19.轨道某单位应用比较:编码规则检测 CoBOT Testbed 漏报率 误报率 漏报率 误报率 1.32% 0.06% 2.60% 0.32% 误 报 率 : 相 比 于 CoBOT , Testbed误报率高出0.26%, 漏报率高出1.28%。可见, 误漏报率均高于CoBOT 19 ID 描述 Testbed漏报 Testbed误报 37S 过程参数只有类型没有标识符 2 0 110S 使用单行注释// 使用了不允许使用的 Included 文 130S 件 331S 字面值需要一个 u 后缀 58S 存在空语句 59S if 语句中没有 else 分支 62D 指针参数应被定义为常量 67S 在模块中使用#define 68S 使用#undef 74S 避免使用联合 87S 用指针进行代数运算 119S 使用嵌套注释 21S …… 总计 34 7 14 18 100 74 38 2 2 16 0 …… 323 0 0 0 0 0 1 0 0 0 0 2 …… 40 CoBOT漏报 0 0 0 67 0 0 6 0 0 0 0 0 …… 164 CoBOT误报 0 0 0 0 4 0 0 0 0 0 0 0 …… 7
  • 20.航空某单位应用比较:编码规则检测  采用GJB 5369编码规则,对襟缝翼系统(代码行数为22051行)进行 了比对测试  比对对象是Testbed Ver7.8.3 Testbed测试较差的条目: 编号 1.2.4 14.1.1 8.1.3 1.1.16 2.1.4 10.2.1 6.1.12 6.1.9 描述 在结构体定义中使用位域 禁止对浮点类型的变量做 相等比较操作 用八进制数 对变量重命名 逻辑上关联的表达式需要 括号 注释中可能包含代码 对有符号类型使用位操作 符号型/无符号型之间没 有使用强制类型转换 Testbed 误报率 100.00% 100.00% Testbed 漏报率 100.00% 100.00% COBOT 误报率 0.00% 0.00% COBOT 漏报率 0.00% 0.00% 100.00% 100.00% 100.00% 100.00% 100.00% 100.00% 0.00% 0.00% 0.00% 0.00% 0.00% 0.00% 35.56% 0.00% 0.00% 57.35% 98.33% 51.60% 1.45% 53.13% 0.00% 0.00% 1.64% 0.00% CoBOT Testbed 漏报率 误报率 漏报率 误报率 1.93% 6.06% 18.91% 25.01% 误 报 率 : 相 比 于 CoBOT , Testbed 误 报 率 高 出 18.95% , 漏报率高出16.98%。可见, 误漏报率均远高于CoBOT 20
  • 21.内容提要 21 背景 静态分析技术 相关工具 实现技术及成果
  • 22.值依赖分析技术 值依赖分析技术是一种符号计算技术,通过值依赖分析构建的值依赖模型:  表达了程序中全部元素,并建立了的6类值 依赖关系及11种值依赖关系  综合利用内存的指向信息、变量的可能取值范围 信息、增强了模型对程序值依赖描述的准确性  通过遍历CFG并利用SSA信息,计算了变量值之间 的约束关系,作为值依赖的守卫表达式 值依赖图是一个有向图,由以下四元组组成:  其中 表达了X的定义点集合  表达了定义点X到其依赖点的映射及值依赖关系 见左图,即  表达了依赖关系所对应的守卫表达式即  表达了 所对应的选择语句集合 22
  • 23.值依赖分析技术 23 相对以符号执行为主的解决方案: 1、检测模型更加简化,以变量值的角度构建模 型而不是以控制流的方式,这样可以省去与值变 化无关的点,使分析效率更高 2、对于精度相对于符号执行,其只能按照符号 执行的逻辑不断计算有可能发生状态爆炸,而值 依赖计算可以根据程序的复杂度设定迭代次数, 是一种主动的折衷方案 3 值依赖模型在由于是跨函数的没有摘要的步骤, 所以对于跨函数的缺陷模式精度更高,函数内精 度相仿
  • 24.值依赖模型与约束求解:空指针解引用 空指针解引用的实例 典型的Infeasible Path程序 值依赖模型及一次迭代求解过程 经过一次迭代,约束表达式由原来的!n3 /\ !n6转 换成了!n3 /\ n3/\ (n5->n6),得到了Unsatisfied结 果,从而消除了误报 24
  • 25.字符串约束求解:SQL注入类漏洞 字符串约束求解实例 1 $username = ‘posted_user’; 2 $newsid = $_POST[‘posted_newsid’]; …… 6 if (!preg_match(‘/[\d]+$/’, $newsid )) { 7 Handle exception… 8 exit; 9} …… 16 $newsid = $DB->query("SELECT * FROM ‘news’ WHERE newsid=".$newsid);Select* FromWherenews newsid : int32 = $newsid 自动生成符号变量$newsid SQL注入攻击向量 0⌒or⌒1=1;#0OR 分析Web应用源代码漏洞,自动生成攻击向量 25newsid : int32 = 0 1 =1
  • 26.基于值依赖分析技术的静态分析工具:库博(COBOT) 工具 支持 自动 检测 程序 模型 基本 分析 编码规则 检测 缺陷模式 约束建立 程序缺陷 检测 区间分析 安全漏洞 检测 程序切 片 测试报告 自动生成 SMT Solver 值依赖分析 SSA 调用关系图CG Pointer Analysis 控制流分析CFG Mod-effect Analysis 数据流分析DFA 预处理 抽象语法树对象封装 抽象语法树AST生成 源程序 编译配置项处理 中间文件 26  COBOT是一款代码静态分析工具  采用基于专利技术分析引擎开发的、 缺 具有自主知识产权程序静态分析框 陷 架,综合运用了多种先进的静态分 模 析技术 式  及时发现代码问题,自动识别程序缺 库 陷、安全漏洞和编码风格问题 :  并可以进行软件度量及规则的定制化 知 分析、质量报表的模板定制 识 库 编码规则检测(10类标准,1000+条规则) 程序缺陷分析(CWE,14类110+种) 安全漏洞扫描(OWASP,8类90+种)
  • 27.相关成果 相关技术成果发表在国际顶级会议和国内刊物上 Safe Memory-Leak Fixing for C Programs, ICSE’15 Fixing Recurring Crash Bugs via Analyzing Q&A Sites, ASE’15 Practical Null Pointer Dereference detection via graph reachability, ISSRE’15 基于值依赖分析的空指针解引用,电子学报 获得软件著作权8项,申请专利2项 2015年,北京市/国家科技创新优秀成果奖 中国唯一一个获得CWE Compatible的安全产品 27
  • 28.√静态测试技术的未来前景  每小时千万行以上的程序静态缺陷扫描技术 - 程序规模不短增大,持续集成要求分析效率与编译速度同一量级,  缺陷模式的全自动总结及挖掘技术 - 如何利用机器学习技术自动挖掘已知的漏洞模式  跨语言分析技术,尤其是对于复杂MVC配置的大型工程 - 大型系统采用MVC框架,通过配置文件确定数据传输处理的程序  动静结合的漏洞自动分析方法的不断完善 - 采用人工智能技术克服静态分析效率问题以产生更多有效的测试用例 28
  • 29.