WEB程序污点分析的形式化定义和验证研究

Recently, one of the hottest research fields on Web security is finding potential injecttion vulnerability by taint analysis, which enumerates all the possible data flows from tainted external inputs to program output statements. .The goal of the project is a sound taint analysis framework for web security of J2EE programs, which includes:.1) formal description of the static taint analylsis based on dependent relation and combined with points-to analysis and program slicing. Formally defining tainted information domain and the semantics of tainted inforamtion propagation on JIMPLE language and proving the soundness of the analysis in the monotone framework..2)formally defining a dynamic taint analysis instrumenting tainted java objects,extending JIMPLE program execution contexts and operational semantics so as to dynamically record the changes of taitned information, verifying the correctness of the analysis with prototype implementation on SOOT platform..3) an algorithm on computing the symbolized summary of tainted information for a java method based on abstract interpretion, stuyding the abstract domain to represent tainted information, studying the formal definition of statemnt-level transformers on JIMPLE statements, studing the combining algorithm of statement-level transformers under the framework of condtional micro- transformers..The analysis framework would be used to precisely locate the security holes of large scale J2EE programs.

污点分析寻找所有从污点(Tainted)输入数据到WEB程序输出的污点数据流传播路径，可有效发现WEB程序漏洞。研究一套面向J2EE程序的可靠污点分析框架，包括：1）形式化定义基于依赖关系并结合指针分析和程序切片的静态污点分析，以JIMPLE为目标语言定义污点信息空间和污点传播语义，在单调性框架内验证分析的可靠性。2）形式化定义对象级跟踪动态污点分析方法，扩展JIMPLE程序执行上下文和JIMPLE语言的操作语义来动态跟踪污点信息变化,在SOOT平台进行实验验证。3）结合抽象解释理论，研究污点信息在方法摘要中的抽象域表示、针对JIMPLE语言的语句级转换器的形式化定义、以及基于条件化微转换器框架的转换器合并算法。期待应用该框架实现对大规模J2EE程序安全漏洞的精确定位。

污点分析技术通过分析污点输入与程序输出之间的关系，可有效发现程序的安全漏洞，研究污点分析的理论和实现技术对提升WEB程序安全有着重要意义。. 项目主要研究了计划中的前两项内容，一是基于依赖的静态污点分析方法，二是支持对象和流跟踪的动态污点分析方法。围绕污点分析技术，目前取得了四个方面的研究进展。1)设计实现一种基于依赖的静态污点分析方法并给出了其形式化描述，对不同方法参数的依赖关系以及域变量和参数的依赖关系进行形式化定义，提出了一种迭代求精的多阶段分析方法对数据依赖图进行遍历，可以有效分析1万7千行规模的WEB程序。2) 提出了一种面向Trace的半自动分析方法，在设计实现一种基于Trace的上下文敏感和域敏感的污点分析方法基础上，形式化定义Jimple指令的污点传播语义并使其满足污点传播的一致性约束，结合程序插桩、活变量分析和程序变换方法，能够高效可靠地验证针对1万行规模的Android代码的静态污点分析结果的正确性。3)设计实现了一种面向用户意图的SQLIAD检测方法，定义了SQLIDL语言来描述程序的SQL操作并产生自动机模型，通过动态检测用户提交的数据库操作是否属于自动机模型的语言，可以实时防御SQLIA攻击。4)设计实现了一种基于混合特征的恶意代码检测方法，将静态污点分析产生的污点传播路径进行抽象和降维后作为代码的语义特征，与经典语法特征相结合并应用机器学习算法进行分类，相比现有检测方案精确度更高。. 项目总共发表核心期刊论文7篇，会议论文1篇，1篇待发表核心期刊论文已在知网刊出，授权国内发明专利2项，登记软件著作权2项。