基于符号执行的注入类安全漏洞的分析技术

doi:10.13209/j.0479-8023.2017.101

北京大学学报自然科学版 ›› 2018, Vol. 54 ›› Issue (1): 1-13.DOI: 10.13209/j.0479-8023.2017.101

基于符号执行的注入类安全漏洞的分析技术

孙基男^1,†, 潘克峰^1,2, 陈雪峰¹, 张君福^1,3

1. 北京大学软件工程国家工程研究中心, 北京 100871
2. 卫士通信息产业股份有限公司北京总部, 北京 100070
3. 北京北大软件工程股份有限公司, 北京 100080

收稿日期:2016-12-05 修回日期:2017-01-17 出版日期:2018-01-20 发布日期:2018-01-20
通讯作者: 孙基男, E-mail: sjn(at)pku.edu.cn

Static Analysis of Injection Security Vulnerabilities Based on Symbolic Execution

SUN Jinan^1,†, PAN Kefeng^1,2, CHEN Xuefeng¹, ZHANG Junfu^1,3

1. National Engineering and Research Center of Software Engineering, Peking University, Beijing 100871
2. Beijing Center of Westone Information Industry Co., Ltd., Beijing 100070
3. Beida Software Engineering Co., Ltd, Beijing 100080

Received:2016-12-05 Revised:2017-01-17 Online:2018-01-20 Published:2018-01-20
Contact: SUN Jinan, E-mail: sjn(at)pku.edu.cn

摘要/Abstract

摘要：

用符号值作为输入, 模拟程序执行, 提取执行路径上相应的约束条件, 即安全约束、攻击约束以及防御约束, 并构成可满足矩阵(SAT)以及不可满足矩阵(UNSAT)两个注入类漏洞安全分析与检测模型, 矩阵模型的求解结果可映射为注入类安全漏洞的安全状态。对Web应用注入类漏洞的检测实验表明, 与目前安全分析主流工具相比, 该分析技术具有降低误报率、漏报率、能自动生成攻击向量等优点。

关键词: 注入类安全漏洞, 符号执行, 程序静态分析, Web应用安全

Abstract:

This research work receives symbols as input variables, simulates the execution of program, extracts the constraints binding with execution paths, such as security constraints, attack constraints and defense constraints, and constructs the SAT judgment matrix and UNSAT judgment matrix as injection vulnerabilities analysis models. According to the logical reduction results of the matrices, the states of injection vulnerabilities are decided. In the controlled experiments, the false positive and false negative ratios are greatly reduced, and the prototype system can generate correct exploits automatically.

Key words: injection vulnerability, symbolic execution, static analysis, web application security

中图分类号:

TP311

孙基男, 潘克峰, 陈雪峰, 张君福. 基于符号执行的注入类安全漏洞的分析技术[J]. 北京大学学报自然科学版, 2018, 54(1): 1-13.

SUN Jinan, PAN Kefeng, CHEN Xuefeng, ZHANG Junfu. Static Analysis of Injection Security Vulnerabilities Based on Symbolic Execution[J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2018, 54(1): 1-13.

导出引用管理器 EndNote|Ris|BibTeX

链接本文: https://xbna.pku.edu.cn/CN/10.13209/j.0479-8023.2017.101

https://xbna.pku.edu.cn/CN/Y2018/V54/I1/1

[1]	沈劲鹏, 王新安. 适用于床垫式生理信号监测系统的信号处理方法[J]. 北京大学学报自然科学版, 2018, 54(5): 921-926.
[2]	王星光, 张瑞洁, 张毅. 基于地理关联度和证据理论的地名消歧方法研究[J]. 北京大学学报自然科学版, 2017, 53(2): 344-352.
[3]	高勇, 姜丹, 刘磊, 林星, 邬伦. 一种地理信息检索的定性模型[J]. 北京大学学报（自然科学版）, 2016, 52(2): 265-273.
[4]	刘磊,高勇,林星,邬伦. 定性地理信息检索方法及其实现[J]. 北京大学学报（自然科学版）, 2013, 49(6): 1017-1024.
[5]	黄健斌,钟翔,孙鹤立,茆婉婷. 基于相似性模块度最大约束标记传播的网络社团发现算法[J]. 北京大学学报（自然科学版）, 2013, 49(3): 389-396.
[6]	仲兆满,刘宗田,李存华. 事件本体模型及事件类排序[J]. 北京大学学报（自然科学版）, 2013, 49(2): 234-240.
[7]	王铁磊,韦韬,邹维. 基于roBDD的细颗粒度动态污点分析[J]. 北京大学学报（自然科学版）, 2011, 47(6): 1003-1008.
[8]	刘钊,黄罡,张颖,梅宏. 一种自动化的资源按需管理方法[J]. 北京大学学报（自然科学版）, 2009, 45(5): 783-790.
[9]	黄雨胡文蕙张世琨. 基于扩展库所网的工作流过程规约和模式描述[J]. 北京大学学报（自然科学版）, 2009, 45(4): 572-578.
[10]	付艳,杨冬青,唐世渭,伍伟,王腾蛟,高军. 基于实体识别的在线主题检测方法[J]. 北京大学学报（自然科学版）, 2009, 45(2): 227-232.
[11]	屈红刚,潘懋,明镜,吴自兴,孙志东. 基于交叉折剖面的高精度三维地质模型快速构建方法研究[J]. 北京大学学报（自然科学版）, 2008, 44(6): 915-920.
[12]	陶有东,童云海,谭少华,唐世渭,杨冬青. 一种实现OLAP数据隐私保护的方法[J]. 北京大学学报（自然科学版）, 2008, 44(5): 705-710.
[13]	屈红刚,潘懋,吕晓俭,刘学清,张永波,于春林. 城市三维地质信息管理与服务系统设计与开发[J]. 北京大学学报（自然科学版）, 2008, 44(5): 781-786.
[14]	韦韬,毛剑,邹维. 反编译中的复合条件分支识别算法[J]. 北京大学学报（自然科学版）, 2008, 44(1): 37-43.
[15]	冯耀东,黄罡,梅宏. 一种自适应软件体系结构建模及其实施方法[J]. 北京大学学报（自然科学版）, 2008, 44(1): 67-76.

基于符号执行的注入类安全漏洞的分析技术

Static Analysis of Injection Security Vulnerabilities Based on Symbolic Execution

RichHTML

PDF

PDF (翻译版)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

留言