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

   下一篇

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

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

  1. 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 Jinan1,†, PAN Kefeng1,2, CHEN Xuefeng1, ZHANG Junfu1,3   

  1. 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

摘要:

用符号值作为输入, 模拟程序执行, 提取执行路径上相应的约束条件, 即安全约束、攻击约束以及防御约束, 并构成可满足矩阵(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

中图分类号: