缓冲区溢出漏洞的静态检测方法研究
|
摘要
程序运行时的缓冲区溢出将导致程序行为异常。恶意用户可以利用服务程序中的缓冲区溢出漏洞,攻击目标计算机系统,窃取或破坏其中的敏感信息,甚至控制该系统向其它主机发动攻击。在每年数十万的网络攻击事件中,大约50%与缓冲区溢出漏洞有关,每年给计算机用户造成的经济损失超过100亿美元。缓冲区溢出漏洞已经成为一种最危险和最常见的软件安全漏洞。
静态检测方法通过分析程序源码,发现其中的缓冲区溢出漏洞,可以从根本上提高软件的安全性。和动态检测方法相比,静态检测方法具有不降低程序执行效率、无兼容性问题、可在软件开发早期应用等优点。缓冲区溢出漏洞的静态检测正在成为信息安全领域的一个研究热点。
本文的目标是研究不依赖用户注释,同时具有高检测精度和高检测效率的缓冲区溢出漏洞静态检测技术。在已有的静态检测方法中,数据流分析和约束分析方法具有不依赖用户注释和高效的特点。数据流分析沿控制流传播约束变量的范围,当传播达到不动点时得到分析的结果。由于数据流分析不能跟踪控制条件,特别是传统的加宽/收窄技术不考虑循环控制条件中约束变量之间的数据依赖关系,导致采用数据流分析的缓冲区溢出漏洞检测方法的精度不高。约束分析通过约束状态的建立和求解发现程序性质。如果循环定义的约束变量之间存在相互依赖的关系,那么包含这些依赖关系的约束状态将无解。此外,基于约束分析的已有静态检测系统忽略指令执行条件的传播和求解,这也降低了它们的检测精度。
本文从提高缓冲区溢出漏洞静态检测的精度和效率入手,针对上述问题展开深入研究,主要研究工作和创新包括:
(1)针对已有数据流分析方法不能精确分析循环的问题,提出一种基于反向路径的循环分析方法。缓冲区溢出和循环有着密切的联系。使用加宽/收窄操作能够快速建立循环的近似解,但是已有方法在分析循环控制条件时不考虑约束变量之间的数据依赖关系,分析精度不高。本文提出一个基于反向路径的循环分析框架和一组双向数据流方程,以及一个基于此框架和数据流方程的循环分析算法。对于循环内可能改进分析结果的控制转移节点,该算法首先进行后向数据流分析,并沿反向路径传播节点的控制条件,再进行前向数据流分析,改进控制转移节点的数据流状态,提高循环分析的精度。
(2)针对穷尽约束产生方法建立的约束状态中存在大量冗余约束条件的问题,提出一种需求驱动的约束产生方法。传统的穷尽约束产生方法计算每条语句的约束信息。由于程序中的许多指令是与内存访问无关的,所以这种方法产生了许多冗余的约束条件。本文提出的需求驱动约束产生方法仅为内存访问指令维护约束状态,并且仅考虑那些与缓冲区溢出漏洞检测有关的约束信息,从而减少了需要建立的约束状态和约束条件的数量,提高了约束产生的效率。
(3)针对已有约束状态安全检查方法求解精度不高的问题,提出一种范围约束和控制约束相互改进的约束状态检查方法。该方法通过一个“求解一检查一改进”的迭代过程,不断缩小约束变量在范围约束和控制约束下的取值范围,逐步提高溢出表达式的计算精度。由于迭代过程充分利用了控制约束,所以本方法能够获得比以往方法更精确的检测结果。同时,迭代可以在求解结果足以确定指令安全性时停止,避免不必要的改进。如果程序中存在循环或递归,那么本文的约束状态安全检查算法还通过打破范围依赖环路的方法,消除使得约束状态无解的约束条件,其效率明显高于使用IIS的传统方法。
(4)针对单一静态分析方法不能同时获得高检测精度和高检测效率的问题,本文提出一种基于反例的溢出漏洞静态检测方法。该方法是一种层次式检测方法,先通过流敏感和上下文敏感的快速检测,发现可能的缓冲区溢出漏洞,再在快速检测结果的指导下,进行路径敏感和上下文敏感的精确检测,消除快速检测引入的误报,建立可导致缓冲区溢出的具体反例。由于反例的建立是在快速检测结果的指导下完成的,因而这种方法比传统的精确检测方法更高效,又不会降低检测的精度。为了消除数据流分析或约束分析各自在检测缓冲区溢出漏洞时的不足,该方法还将数据流分析建立的循环分析结果和约束分析建立的约束状态合并,组成统一的约束状态。
(5)根据本文提出的分析算法,我们实现了一个缓冲区溢出漏洞静态检测的原型系统,并对它的总体和各个部分进行了性能讦测。实验结果表明,本原型系统具有非常高的检测精度和检测效率,总体性能优于已有的典型缓冲区溢出漏洞静态检测系统。
综上所述,本文针对缓冲区溢出漏洞静态检测的几个关键问题进行了探索,取得了一定的研究成果。对于提高溢出漏洞静态检测的精度和效率具有重要的理论意义和应用价值。
Buffer overflows at run-time can lead to non-deterministic program behavior, which may be used by malicious attackers to compromise a computer, such as to access or corrupt sensitive information, and even worse, to control the computer to attack others. Every year, hundreds of thousands of network attacks happen, about fifty percent of which are related to buffer overflow vulnerabilities. And the economic waste caused by this kind of attacks is more than 10 billion dollars. Buffer overflow has become the most dangerous and most common software security vulnerability.
Static analysis can be used to detect vulnerability by analying source codes. It helps developers in eliminating buffer overflows before software is deployed and improve software security essentially. Compared with dynamic analysis, static analysis methods have such advantages as not slowing down program execution, not leading to compatibility problems and being processed at early stage of software development. Static detection for buffer overflow (SDBO) is becoming a hot topic in the area of information security.
The goal of the thesis is to present very high precise and efficient static analysis methods for buffer overflow detection without depending on user annotations. Among the existing static analysis methods, data flow analysis and constraint analysis don't depend on user annotations, and are very efficient at the same tiime. Data flow analysis propagates ranges of constraint variables along control flow, and gains solutions when fixed point is arrived. But data flow analysis method does not trace control conditions. Especially, the traditional widening/narrowing method does not consider data dependence between constraint variables of loop control conditions. Therefore, the precision of existing data flow analysis is poor. Constraint analysis finds program characteristics by building and solving constraint states of the program. If there are co-dependent relations among constraint variables defined in a loop, the constraint states including these relations are infeasible. In addition, the existing constraint-based static detection systems ignore the propagation and solution of execution conditions of instructions, which makes the detection precision very low.
To improve the precision and efficience of static analysis methods for buffer overflow vulnerabilities, detailed researches have been done. The main contributions are as follows:
(1) To improve the precision of data flow loop analysis, a loop analysis method based on reverse paths is proposed. Buffer overflows are usually related to loops. With the widening/narrowing operator, traditional loop analysis methods can obtain approximate solutions of loops fast, but these methods ignore data dependence between constraint variables, and leads to poor imprecise. In this dissertation, a framework based on bidirectional data flow analysis and the corresponding bidirection dataflow equations are established. On the basis of the framework and the equations, a loop analysis algorithm is proposed. For control nodes that may improve the result of loop analysis, the algorithm first propagates control conditions along reverse paths, and then makes a forward data flow analysis to improve their data flow state. By this way, the precision of the loop analysis is improved.
(2) To avoid the redundant constraint conditions that are generated by exhaustive constraint analysis, a demand-driven constraint generating method is proposed. Traditional constraint analysis methods compute constraint information for every instruction. Because many instructions are not related to memory access, the exhaustive method should generate many redundant constraints for buffer overflow detection. Our demand-driven constraint generation approach only maintains constraint states for memory access instructions, and only considers constraint information that is related to buffer overflow detection. Therefor, the number of constraint states and constraint conditions is decreased and the efficiency of constraint generation is improved.
(3) To improve the solution precision of constraint state computing, a constraint state computing algorithm which mutually refines the solution of range constraints and control constraints is proposed. Through an iteration of "resolution - check - refinement", the algorithm reduces ranges of constraint variables with range constraints and control constraints, and improves resolution precision of overflow expression step by step. It is more precise than existing ones benefit from control constraints. At the same time, it stops the iteration as soon as the memory access is decided to be safe, avoiding unnecessary computation. To eliminate constraint conditions that make range constraints infeasible, this algorithm builds range dependency graph of the range constraints and breaks loops in the graph, which is more efficient than the tradition methods of using IIS.
(4) To overcome the shortcoming of single static analysis mode that cannot gain both high precision and high efficiency, a hierarchy analysis algorithm based on counter-example is proposed. As a hierarchy analysis approach, it first makes a fast detection with flow sensitive and context sensitive analysis to find possible buffer overflow vulnerabilities, then makes a precision detection with path and context sensitive analysis guided by the former result to reduce false positives and identifying the concrete path of inducing buffer overflow. Since the counter examples are constructed under the guide of the fast analysis, the algorithm is more efficient than traditional path-sensitive algorithms, and don't sacrifice precision at the same time. To eliminate the imprecision of buffer overflow static detection with data flow analysis and constraint analysis, the algorithm forms the analysis state of memory access instructions by combining the result of data flow loop analysis and the constraint state of constraint state of constraint analysis.
(5) A prototype system is designed and implemented with technologies described above. The experiment results show that the prototype system can detect buffer overflow vulnerabilities automatically with high precision and high efficiency. In the mass, the capability of the prototype system is better than existing classical systems.
To sum up, in this dissertation, several key problems of SDBO have been studied and some contributions have been achieved. Our contributions listed above are helpful for enhancing the performance of SDBO in both theory and practice.
静态检测方法通过分析程序源码,发现其中的缓冲区溢出漏洞,可以从根本上提高软件的安全性。和动态检测方法相比,静态检测方法具有不降低程序执行效率、无兼容性问题、可在软件开发早期应用等优点。缓冲区溢出漏洞的静态检测正在成为信息安全领域的一个研究热点。
本文的目标是研究不依赖用户注释,同时具有高检测精度和高检测效率的缓冲区溢出漏洞静态检测技术。在已有的静态检测方法中,数据流分析和约束分析方法具有不依赖用户注释和高效的特点。数据流分析沿控制流传播约束变量的范围,当传播达到不动点时得到分析的结果。由于数据流分析不能跟踪控制条件,特别是传统的加宽/收窄技术不考虑循环控制条件中约束变量之间的数据依赖关系,导致采用数据流分析的缓冲区溢出漏洞检测方法的精度不高。约束分析通过约束状态的建立和求解发现程序性质。如果循环定义的约束变量之间存在相互依赖的关系,那么包含这些依赖关系的约束状态将无解。此外,基于约束分析的已有静态检测系统忽略指令执行条件的传播和求解,这也降低了它们的检测精度。
本文从提高缓冲区溢出漏洞静态检测的精度和效率入手,针对上述问题展开深入研究,主要研究工作和创新包括:
(1)针对已有数据流分析方法不能精确分析循环的问题,提出一种基于反向路径的循环分析方法。缓冲区溢出和循环有着密切的联系。使用加宽/收窄操作能够快速建立循环的近似解,但是已有方法在分析循环控制条件时不考虑约束变量之间的数据依赖关系,分析精度不高。本文提出一个基于反向路径的循环分析框架和一组双向数据流方程,以及一个基于此框架和数据流方程的循环分析算法。对于循环内可能改进分析结果的控制转移节点,该算法首先进行后向数据流分析,并沿反向路径传播节点的控制条件,再进行前向数据流分析,改进控制转移节点的数据流状态,提高循环分析的精度。
(2)针对穷尽约束产生方法建立的约束状态中存在大量冗余约束条件的问题,提出一种需求驱动的约束产生方法。传统的穷尽约束产生方法计算每条语句的约束信息。由于程序中的许多指令是与内存访问无关的,所以这种方法产生了许多冗余的约束条件。本文提出的需求驱动约束产生方法仅为内存访问指令维护约束状态,并且仅考虑那些与缓冲区溢出漏洞检测有关的约束信息,从而减少了需要建立的约束状态和约束条件的数量,提高了约束产生的效率。
(3)针对已有约束状态安全检查方法求解精度不高的问题,提出一种范围约束和控制约束相互改进的约束状态检查方法。该方法通过一个“求解一检查一改进”的迭代过程,不断缩小约束变量在范围约束和控制约束下的取值范围,逐步提高溢出表达式的计算精度。由于迭代过程充分利用了控制约束,所以本方法能够获得比以往方法更精确的检测结果。同时,迭代可以在求解结果足以确定指令安全性时停止,避免不必要的改进。如果程序中存在循环或递归,那么本文的约束状态安全检查算法还通过打破范围依赖环路的方法,消除使得约束状态无解的约束条件,其效率明显高于使用IIS的传统方法。
(4)针对单一静态分析方法不能同时获得高检测精度和高检测效率的问题,本文提出一种基于反例的溢出漏洞静态检测方法。该方法是一种层次式检测方法,先通过流敏感和上下文敏感的快速检测,发现可能的缓冲区溢出漏洞,再在快速检测结果的指导下,进行路径敏感和上下文敏感的精确检测,消除快速检测引入的误报,建立可导致缓冲区溢出的具体反例。由于反例的建立是在快速检测结果的指导下完成的,因而这种方法比传统的精确检测方法更高效,又不会降低检测的精度。为了消除数据流分析或约束分析各自在检测缓冲区溢出漏洞时的不足,该方法还将数据流分析建立的循环分析结果和约束分析建立的约束状态合并,组成统一的约束状态。
(5)根据本文提出的分析算法,我们实现了一个缓冲区溢出漏洞静态检测的原型系统,并对它的总体和各个部分进行了性能讦测。实验结果表明,本原型系统具有非常高的检测精度和检测效率,总体性能优于已有的典型缓冲区溢出漏洞静态检测系统。
综上所述,本文针对缓冲区溢出漏洞静态检测的几个关键问题进行了探索,取得了一定的研究成果。对于提高溢出漏洞静态检测的精度和效率具有重要的理论意义和应用价值。
Buffer overflows at run-time can lead to non-deterministic program behavior, which may be used by malicious attackers to compromise a computer, such as to access or corrupt sensitive information, and even worse, to control the computer to attack others. Every year, hundreds of thousands of network attacks happen, about fifty percent of which are related to buffer overflow vulnerabilities. And the economic waste caused by this kind of attacks is more than 10 billion dollars. Buffer overflow has become the most dangerous and most common software security vulnerability.
Static analysis can be used to detect vulnerability by analying source codes. It helps developers in eliminating buffer overflows before software is deployed and improve software security essentially. Compared with dynamic analysis, static analysis methods have such advantages as not slowing down program execution, not leading to compatibility problems and being processed at early stage of software development. Static detection for buffer overflow (SDBO) is becoming a hot topic in the area of information security.
The goal of the thesis is to present very high precise and efficient static analysis methods for buffer overflow detection without depending on user annotations. Among the existing static analysis methods, data flow analysis and constraint analysis don't depend on user annotations, and are very efficient at the same tiime. Data flow analysis propagates ranges of constraint variables along control flow, and gains solutions when fixed point is arrived. But data flow analysis method does not trace control conditions. Especially, the traditional widening/narrowing method does not consider data dependence between constraint variables of loop control conditions. Therefore, the precision of existing data flow analysis is poor. Constraint analysis finds program characteristics by building and solving constraint states of the program. If there are co-dependent relations among constraint variables defined in a loop, the constraint states including these relations are infeasible. In addition, the existing constraint-based static detection systems ignore the propagation and solution of execution conditions of instructions, which makes the detection precision very low.
To improve the precision and efficience of static analysis methods for buffer overflow vulnerabilities, detailed researches have been done. The main contributions are as follows:
(1) To improve the precision of data flow loop analysis, a loop analysis method based on reverse paths is proposed. Buffer overflows are usually related to loops. With the widening/narrowing operator, traditional loop analysis methods can obtain approximate solutions of loops fast, but these methods ignore data dependence between constraint variables, and leads to poor imprecise. In this dissertation, a framework based on bidirectional data flow analysis and the corresponding bidirection dataflow equations are established. On the basis of the framework and the equations, a loop analysis algorithm is proposed. For control nodes that may improve the result of loop analysis, the algorithm first propagates control conditions along reverse paths, and then makes a forward data flow analysis to improve their data flow state. By this way, the precision of the loop analysis is improved.
(2) To avoid the redundant constraint conditions that are generated by exhaustive constraint analysis, a demand-driven constraint generating method is proposed. Traditional constraint analysis methods compute constraint information for every instruction. Because many instructions are not related to memory access, the exhaustive method should generate many redundant constraints for buffer overflow detection. Our demand-driven constraint generation approach only maintains constraint states for memory access instructions, and only considers constraint information that is related to buffer overflow detection. Therefor, the number of constraint states and constraint conditions is decreased and the efficiency of constraint generation is improved.
(3) To improve the solution precision of constraint state computing, a constraint state computing algorithm which mutually refines the solution of range constraints and control constraints is proposed. Through an iteration of "resolution - check - refinement", the algorithm reduces ranges of constraint variables with range constraints and control constraints, and improves resolution precision of overflow expression step by step. It is more precise than existing ones benefit from control constraints. At the same time, it stops the iteration as soon as the memory access is decided to be safe, avoiding unnecessary computation. To eliminate constraint conditions that make range constraints infeasible, this algorithm builds range dependency graph of the range constraints and breaks loops in the graph, which is more efficient than the tradition methods of using IIS.
(4) To overcome the shortcoming of single static analysis mode that cannot gain both high precision and high efficiency, a hierarchy analysis algorithm based on counter-example is proposed. As a hierarchy analysis approach, it first makes a fast detection with flow sensitive and context sensitive analysis to find possible buffer overflow vulnerabilities, then makes a precision detection with path and context sensitive analysis guided by the former result to reduce false positives and identifying the concrete path of inducing buffer overflow. Since the counter examples are constructed under the guide of the fast analysis, the algorithm is more efficient than traditional path-sensitive algorithms, and don't sacrifice precision at the same time. To eliminate the imprecision of buffer overflow static detection with data flow analysis and constraint analysis, the algorithm forms the analysis state of memory access instructions by combining the result of data flow loop analysis and the constraint state of constraint state of constraint analysis.
(5) A prototype system is designed and implemented with technologies described above. The experiment results show that the prototype system can detect buffer overflow vulnerabilities automatically with high precision and high efficiency. In the mass, the capability of the prototype system is better than existing classical systems.
To sum up, in this dissertation, several key problems of SDBO have been studied and some contributions have been achieved. Our contributions listed above are helpful for enhancing the performance of SDBO in both theory and practice.
引文
[1]Xie Yichen,Chou Andy,E D.ARCHER:Using symbolic,path-sensitive analysis to detect memory access errors.In:European software engineering conference.Helsinki,Finland:2003.
[2]Buffer Overflows-What Are They and What Can I Do About Them.http://www.cert.org/homeusers/buffer_overflow.html.2001.
[3]Internet Worm Resource:HomePage.http://worm.ccert.edu.cn/wiki/index.cgi?HomePage.2007.
[4]The 10 Most Destructive PC Viruses of All Time.http://www.informationweek.com/news/showArticle.jhtml?articleID=190300173.2006.
[5]Mitchell J.Network worms:attacks and defenses.Technical Stanford University,2006.
[6]CERT/CC Advisories.http://www.cert.org/advisories/.2006.
[7]David Wagner,Jeffrey S.Foste,Eric A.Brewer A.A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities.In:Network and Distributed System Security.San Diego,CA,USA:2000.
[8]Olatunji Ruwase M S L.A Practical Dynamic Buffer Overflow Detector.In:the 11th Annual Network and Distributed System Security Symposium.San Diego,California,USA:2004.
[9]Mitchell J.Control Hijacking Attacks.Technical Stanford University.
[10]CNCERT/CC.http://www.cert.org.cn/upload/2005CNCERTCCAnnualReport_Chinese.pdf.2005.
[11]David Larochelle D E.Statically Detecting Likely Buffer Overflow Vulnerabilities.In:USENIX Security Symposium.Washington D C,USA:2001.
[12][美]dorothyEdenning 著,吴汉平等译.信息战与信息安全.电子工业出版社,2003.
[13]Crispin Cowan,Perry Wagle,Calton Pu,Steve Beattie A J W.Buffer Overflows:Attacks and Defenses for the Vulnerability of the Decade.In:DARPA Information Survivability Conference and Expo(DISCEX).2000.
[14]S.Non-executable stack patch.2006.http://www.openwall.com/linux.
[15]Changes to Functionality in Microsoft Windows XP Service Pack 2,Part 3:Memory Protection Technologies.http://www.microsoft.com/technet/prodtechnol/winxppro/maintain/sp2mempr.msp x.2004.
[16]NX bit may provide more comfort than security.http://www.geek.com/news/geeknews/2005Aug/bch20050801031613.htm.2005.
[17]Documentation for the PaX project,http://pax.grsecurity.net/docs/.2003.
[18]Vendicator.Stack Shield.2001.http://www.angelfire.com/sk/stackshield/.
[19]C.Cowan,C.Pu,D.Maier,J.Walpole,P.Bakke,S.Beattie,A.Grier,P.Wagle H H.Stack-Guard:Automatic adaptive detection and prevention of buffer-overflow attacks.In:USENIX Security Conference.San Antonio,Texas,USA:1998.
[20]GCC extension for protecting applications from stack-smashing attacks.http://www.trl.ibm,com/projects/security/ssp.2000.
[21]陈志强,严晓浪.CPU微结构中侦测和防止缓冲区溢出的实现.固体电子学研究与进展.2006(2).
[22] Libsafe: protecting critical elements of stacks.http://www.research.avayalabs.com/project/libsafe. 1990.
[23] A. Baratloo, N. Singh T T. Transparent Run-Time Defense against Stack Smashing Attacks. In: USENIX Technical Conference.San Diego, California, USA: 2000.
[24] Crispin Cowan, Matt Barringer, Steve Beattie G K. FormatGuard: Automatic Protection From printf Format String Vulnerabilities. In: USENIX Security Symposium.Washington, USA: 2001.
[25] Richard W M, Jones P H J K. Backwards-compatible bounds checking for arrays and pointers in C programs. In: International Workshop on Automated and Algorithmic Debugging.Linkping, Sweden: 1997.
[26] Kyung suk, Lhee S J C. Type-Assisted Dynamic Buffer Overflow Detection. In:USENIX Security Symposium.San Francisco, California, USA: 2002.
[27] Cowan C, Beattie S J J. Pointguard: Protecting pointers from buffer overflow vulnerabilities. In: USENIX Security Symposium.Washington DC, USA: 2003.
[28] Bhatkar, Duvarney S. Address Obfuscation: an Efficient Approach to Combat a Broad Range of Memory Error Exploits. In: USENIX Security Symposium.Washington, DC, USA: 2003.
[29] Vladimir Kiriansky, Derek Bruening S A. Secure Execution via Program Shepherding. In: USENIX Security Symposium.San Francisco, USA: 2002.
[30] Bypassing StackGuard and StackShield. http://www.phrack.org/show.php?P=56&a=5.2002.
[31] Pincus J. Graceless Degradation, Measurement, and Other Challenges in Security and Privacy. Technical Microsoft Research, 2004.
[32] Sites R L. Proving that computer programs terminate cleanly. Ph. D., Stanford,1974.
[33] Johnson S C. Lint, a C Program Checker. Technical AT&T Bell Laboratories,1978.
[34] Dawson Engler, Ted Kremenek, Ken Ashcraft J Y. Correlation Exploitation in Error Ranking. In: ACM SIGSOFT twelfth international symposium on Foundations of software engineering.Newport Beach, CA, USA: 2004.
[35] Kwangkeun Yi, Yungbum Jung, Jaehwang Kim J S. Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience. In:BUGS 2005 Workshop on the Evaluation of Software Defect Detection Tools.Chicago, Illinois, USA: 2005.
[36] 田鹏,李明,李祥和.二进制扫描的缓冲区溢出漏洞探测技术.微计算机信息.2007, 3.
[37] yan feiZheng, huiLi, ke feiChen. Buffer Overflow Detection on Binary Code.Journal of Shanghai Jiaotong University (Science). 2006(6): 224-229.
[38] P. Cousot, R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoits. In: ACM symposium on principles of programming languages.Los Angeles, California,USA: 1977.
[39] Notes on abstrct interpretation.www.eecs.umich.edu/～bchandra/courses/papers/Salcianu_AbstractI nterpretation.pdf.2001.
[40] Aiken A. Introduction to set constraint-based program analysis. In science of computer programming. 1999, 35(2): 79-111.
[41] Jeffrey D. Ullman Alfred V. Aho R S. 编译原理.机械工业出版社, 2003.
[42] Flemming Nielson, Hanne R N A C H. Principles of Program Analysis. Berlin Heidelberg: Springer-Verlag, 1999.
[43] Umesh Shankar, Kunal Talwar, Jeffrey S. Foster D W. Detecting Format String Vulnerabilities with Type Qualifiers. In: USENIX Security Symposium.Washington, D.C., USA: 2001.
[44]林惠民,张文辉.模型检测:理论、方法和应用.电子学报.2002(12):1907-1912.
[45] L E M C D E. Model checking and abstraction. ACM Transactions on Programming Languages and System. 1994,15(5): 1512—1542.
[46] Hao Chen, D W. MOPS: an Infrastructure for Examining Security Properties of software. In: ACM Conference on Computer and Communications Security.Washington, DC, USA: 2002.
[47] G H. UNO: Static source code checking for user-defined properties. Technical Bell Labs, 2002.
[48] Detlefs D L, Leino K R M, Nelson G S J B. Extended Static Checking. Technical Palo Alto, USA: Compaq System Research Center, 1998.
[49] Rustan K, L M. Extended static checking:a ten-year perspective. In: Lecture Notes in Computer Science.New York: Springer, 2001.
[50] Dor N, rodeh M S M. CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C. In: ACM Conference on Programming Language Design and Implementation.San Diego, California, USA: 2003.
[51] B. V. Chess. Improving Computer Security using Extended Static Checking. In:IEEE Symposium on Security and Privacy.Oakland, California, USA: 2002.
[52] Welcome to RATS - Rough Auditing Tool for Security.http://www.fortifysoftware.com/security-resources/rats.jsp.2007.
[53] J. Viega, J. T. Bloch, Y. Kohno G M. ITS4: A static vulnerability scanner for C and C++ code. ACM Transactions on Information and System Security. 2002,5(2).
[54] Flawfinder. http://www.dwheeler.com/flawfinder/.
[55] V. Markstein, J. Cocke P M. Optimization of Range Checking. In: Symposium on Compiler Construction.Boston, Massachusetts, USA: 1982.
[56] Gupta R. A fresh look at optimizing array bound checking. In: ACM Conference on Programming Language Design and Implementation.New York, USA: 1990.
[57] Gupta R. Optimizing array bound checks using flow analysis. 1993
[58] Hongwei Xi, F P. Eliminating array bound checking through dependent types. In:ACM Conference on Programming Language Design and Implementation.Montreal, Canada: 1998.
[59] Bodik R. ABCD: Eliminating array bounds checks on demand. In: ACM Conference on Programming Language Design and Implementation.Vancouver,British Columbia, Canada: 2000.
[60] George C. Necula, Scott Mcpeak W W. CCured: type-safe retrofitting of legacy code. In: ACM Conference on Programming Language Design and Implementation.Berlin, Germany: 2002.
[61] Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney Y W.Cyclone: A Safe Dialect of C. In: USENIX Annual Technical Conference.Monterey, CA, USA: 2002.
[62] Schmidt D A. Data flow analysis is model checking of abstract interpretations. In:ACM Conference on Symposium on Principles of Programming Languages.San Diego, California, USA: 1998.
[63] Shankar N. Combining Theorem Proving and Model Checking through Symbolic Analysis. In: ACM conference on Concurrency Theory.London, UK: 2000.
[64] P. Cousot, R C. Refining model checking by abstract interpretation. Automated Software Engineering. 1999(6): 69-95.
[65] P. Cousot, R C. Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. In: Program Analysis by Abstract Interpretation.La Jolla, California, USA: 1995.
[66] 王兵山,王长英,周贤林.离散数学.长沙:国防科技大学出版社,1986.
[67] Muchnick S S. 高级编译器设计与实现.机械工业出版社, 2003.
[68] Westley Weimer, George C. Necula, Scott Mcpeak S P R. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In:International Conference on Compiler Construction.Grenoble, France: 2002.
[69] BANE: Analysis Programmer. Interface.http://www.cs.berkeley.edu/Research/Aiken/#0.
[70] Wagner D. Static analysis and computer security: New techniques for software assurance. PH. D., Berkley: University of California, 2001.
[71] Vinod Ganapathy, Somesh Jha, David Chandler, David Melski D V. Buffer Overrun Detection using Linear Programming and Static Analysis. In: ACM Conference on Computer and Communications Security.Washington, DC, USA:2003.
[72] Evans D, L D. Improving security using extensible lightweight static analysis.IEEE Software. 2002(1): 42-51.
[73] Livshits V B, Lam M S. Tracking Pointers with Path and Context Sensitivity for Bug Detection in C Programs. In: European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering.Helsinki,Finland: 2003.
[74] Venet A, V A. Precise and efficient static array bound checking for large embedded C programs. In: ACM Conference on Programming Language Design and Implementation.Washington, DC, USA: 2004.
[75] PolySpace C Verifier: Product Leaflet.www.cert.fr/francais/deri/seguin/SEE/00.05.25/CLeaflet.pdf.2000.
[76] Blanchet B. A Static Analyzer for Large Safety Critical software. In: ACM Conference on Programming Language Design and Implementation.San Diego,California, USA: 2003.
[77] AIRAC: Static Analzyer for Automatic Verification of Array Index Ranges in C Programs. http://ropas.snu.ac.kr/airac.2005.
[78] Kwangkeun Yi, Yungbum Jung, Jaehwang Kim J S. Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience. In:BUGS 2005 Workshop on the Evaluation of Software Defect Detection Tools.Chicago, Illinois, USA: 2005.
[79] Detlefs D, Nelson G, Saxe J B. Simplify: A Theorem Prover for Program Checking.Technical HP Labs, 2003.
[80] Palsberg J. Type-based analysis and applications. In: Workshop on Program Analysis for Software Tools and Engineering.Snowbird, Utah, USA: ACM Press,2001.
[81] Johnson R, W D. Finding User/Kernel Pointer Bugs With Type Inference. USENIX Security Symposium.San Diego, CA, USA: 2004.
[82] Dawson Engler, Madanlal Musuvathi. Static analysis versus software model checking for bug finding. Proc. of the 5th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004). LNCS 2937,Springer-Verlag, 2004. 191-210.
[83] Visser W, Havelund K, Brat G, Park S L F. Model Checking Programs. Automated Software Engineering Jounal. 2003,10(2): 203-232.
[84] Madanlal Musuvathi, David Park, Andy Chou, Dawson R. CMC: A Pragmatic Approach to Model Checking Real Code. In: The Fifth Symposium on Operating Systems Design and Implementation.Boston, Massachusetts, USA: 2002.
[85] P G. Model Checking for Programming Languages using VeriSoft. In: ACM Symposium on Principles of Programming Languages.Paris, France: 1997.
[86] Henzinger T A, Jhala R, majumdar R E A. Software Verification with Blast. In:SPIN Workshop on Model Checking Software.Springer-Verlag, 2003. 235—239.
[87] Ball T, R S K. The SLAM Project: Debugging System Software via Static Analysis. In: ACM Conference on Symposium on Principles of Programming Languages.Portland, OR, USA: 2002.
[88] SUIF. http://suif.stanford.edu.
[89] William Blume, R E. Symbolic Range Propagation. In: the 9th International Parallel Processing Symposium.Cancun, Mexico, USA: 1994.
[90] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman F K Z.Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems. 1991,13(4):451-490.
[91] Yuri Gurevich, JKH. The Semantics of the C Programming Language. In: Workshop on Computer Science Logic.Berne, Switzerland: 1992.
[92] Papaspyrou N. A formal semantics for the C programming language. Ph. D.,National Technical University of Athens, 1998.
[93] Fahringer T. Efficient symbolic analysis for parallelizing compilers and performance estimators. The Journal of Supercomputing. 1998, 12(3): 1-29.
[94] Radu Rugina, M R. Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions. In: ACM Conference on Programming Language Design and Implementation.Vancouver B.C., Canada: 2000.
[95] Vaserstein L N. Introduction to Linear Programming. 机械工业出版社, 2005.
[96] SoPlex.www.zib.de/Optimization/Software/Soplex/.2007.
[97] CPLEX. http://www.cplex.com.2007.
[98] FortMP Manual. http://www.unicom.co.uk/FortMP/ManFrame.htm.
[99] CLP. http://opensource.org/licenses/cpl.php.
[100] GLPK - GNU Project - Free Software Foundation(FSF).www.gnu.org/software/glpk/.
[101] LPSOLVE. http://www.statslab.cam.ac.uk/～rrwl/opt/lp_solve/.
[102] The LLVM Compiler Infrastructure. http://www.llvm.org.
[103] SUIF. http://suif.stanford.edu.
[104] Lengauer, thomasRobertETarjan. A fast algorithm for finding dominators in a flowgraph. ACM Transactions on Programming Languages and System. 1979,1(1): 121-141.
[105] Steensgaard B. Points-to analysis in almost linear time. In: ACM SIGPLAN-SIGACT symposium on Principles of programming languages.St.Petersburg Beach, Florida, USA: ACM Press, 1996.
[106] Andersen. Program Analysis and Specialization for the C Programming Language. PH. D., DIKU, University of Copenhagen, 1994.
[107] Manuvir Das, Ben Liblit, Manuel Fahndrich J R. Estimating the Impact of Scalable Pointer Analysis on Optimization. In: Static Analysis Symposium.Paris,France: 2001.
[108]Lattner C.Macroscopic Data Structure Analysis and Optimization.Ph.D.,University of Illinois at Urbana-Champaign,2005.
[2]Buffer Overflows-What Are They and What Can I Do About Them.http://www.cert.org/homeusers/buffer_overflow.html.2001.
[3]Internet Worm Resource:HomePage.http://worm.ccert.edu.cn/wiki/index.cgi?HomePage.2007.
[4]The 10 Most Destructive PC Viruses of All Time.http://www.informationweek.com/news/showArticle.jhtml?articleID=190300173.2006.
[5]Mitchell J.Network worms:attacks and defenses.Technical Stanford University,2006.
[6]CERT/CC Advisories.http://www.cert.org/advisories/.2006.
[7]David Wagner,Jeffrey S.Foste,Eric A.Brewer A.A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities.In:Network and Distributed System Security.San Diego,CA,USA:2000.
[8]Olatunji Ruwase M S L.A Practical Dynamic Buffer Overflow Detector.In:the 11th Annual Network and Distributed System Security Symposium.San Diego,California,USA:2004.
[9]Mitchell J.Control Hijacking Attacks.Technical Stanford University.
[10]CNCERT/CC.http://www.cert.org.cn/upload/2005CNCERTCCAnnualReport_Chinese.pdf.2005.
[11]David Larochelle D E.Statically Detecting Likely Buffer Overflow Vulnerabilities.In:USENIX Security Symposium.Washington D C,USA:2001.
[12][美]dorothyEdenning 著,吴汉平等译.信息战与信息安全.电子工业出版社,2003.
[13]Crispin Cowan,Perry Wagle,Calton Pu,Steve Beattie A J W.Buffer Overflows:Attacks and Defenses for the Vulnerability of the Decade.In:DARPA Information Survivability Conference and Expo(DISCEX).2000.
[14]S.Non-executable stack patch.2006.http://www.openwall.com/linux.
[15]Changes to Functionality in Microsoft Windows XP Service Pack 2,Part 3:Memory Protection Technologies.http://www.microsoft.com/technet/prodtechnol/winxppro/maintain/sp2mempr.msp x.2004.
[16]NX bit may provide more comfort than security.http://www.geek.com/news/geeknews/2005Aug/bch20050801031613.htm.2005.
[17]Documentation for the PaX project,http://pax.grsecurity.net/docs/.2003.
[18]Vendicator.Stack Shield.2001.http://www.angelfire.com/sk/stackshield/.
[19]C.Cowan,C.Pu,D.Maier,J.Walpole,P.Bakke,S.Beattie,A.Grier,P.Wagle H H.Stack-Guard:Automatic adaptive detection and prevention of buffer-overflow attacks.In:USENIX Security Conference.San Antonio,Texas,USA:1998.
[20]GCC extension for protecting applications from stack-smashing attacks.http://www.trl.ibm,com/projects/security/ssp.2000.
[21]陈志强,严晓浪.CPU微结构中侦测和防止缓冲区溢出的实现.固体电子学研究与进展.2006(2).
[22] Libsafe: protecting critical elements of stacks.http://www.research.avayalabs.com/project/libsafe. 1990.
[23] A. Baratloo, N. Singh T T. Transparent Run-Time Defense against Stack Smashing Attacks. In: USENIX Technical Conference.San Diego, California, USA: 2000.
[24] Crispin Cowan, Matt Barringer, Steve Beattie G K. FormatGuard: Automatic Protection From printf Format String Vulnerabilities. In: USENIX Security Symposium.Washington, USA: 2001.
[25] Richard W M, Jones P H J K. Backwards-compatible bounds checking for arrays and pointers in C programs. In: International Workshop on Automated and Algorithmic Debugging.Linkping, Sweden: 1997.
[26] Kyung suk, Lhee S J C. Type-Assisted Dynamic Buffer Overflow Detection. In:USENIX Security Symposium.San Francisco, California, USA: 2002.
[27] Cowan C, Beattie S J J. Pointguard: Protecting pointers from buffer overflow vulnerabilities. In: USENIX Security Symposium.Washington DC, USA: 2003.
[28] Bhatkar, Duvarney S. Address Obfuscation: an Efficient Approach to Combat a Broad Range of Memory Error Exploits. In: USENIX Security Symposium.Washington, DC, USA: 2003.
[29] Vladimir Kiriansky, Derek Bruening S A. Secure Execution via Program Shepherding. In: USENIX Security Symposium.San Francisco, USA: 2002.
[30] Bypassing StackGuard and StackShield. http://www.phrack.org/show.php?P=56&a=5.2002.
[31] Pincus J. Graceless Degradation, Measurement, and Other Challenges in Security and Privacy. Technical Microsoft Research, 2004.
[32] Sites R L. Proving that computer programs terminate cleanly. Ph. D., Stanford,1974.
[33] Johnson S C. Lint, a C Program Checker. Technical AT&T Bell Laboratories,1978.
[34] Dawson Engler, Ted Kremenek, Ken Ashcraft J Y. Correlation Exploitation in Error Ranking. In: ACM SIGSOFT twelfth international symposium on Foundations of software engineering.Newport Beach, CA, USA: 2004.
[35] Kwangkeun Yi, Yungbum Jung, Jaehwang Kim J S. Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience. In:BUGS 2005 Workshop on the Evaluation of Software Defect Detection Tools.Chicago, Illinois, USA: 2005.
[36] 田鹏,李明,李祥和.二进制扫描的缓冲区溢出漏洞探测技术.微计算机信息.2007, 3.
[37] yan feiZheng, huiLi, ke feiChen. Buffer Overflow Detection on Binary Code.Journal of Shanghai Jiaotong University (Science). 2006(6): 224-229.
[38] P. Cousot, R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoits. In: ACM symposium on principles of programming languages.Los Angeles, California,USA: 1977.
[39] Notes on abstrct interpretation.www.eecs.umich.edu/～bchandra/courses/papers/Salcianu_AbstractI nterpretation.pdf.2001.
[40] Aiken A. Introduction to set constraint-based program analysis. In science of computer programming. 1999, 35(2): 79-111.
[41] Jeffrey D. Ullman Alfred V. Aho R S. 编译原理.机械工业出版社, 2003.
[42] Flemming Nielson, Hanne R N A C H. Principles of Program Analysis. Berlin Heidelberg: Springer-Verlag, 1999.
[43] Umesh Shankar, Kunal Talwar, Jeffrey S. Foster D W. Detecting Format String Vulnerabilities with Type Qualifiers. In: USENIX Security Symposium.Washington, D.C., USA: 2001.
[44]林惠民,张文辉.模型检测:理论、方法和应用.电子学报.2002(12):1907-1912.
[45] L E M C D E. Model checking and abstraction. ACM Transactions on Programming Languages and System. 1994,15(5): 1512—1542.
[46] Hao Chen, D W. MOPS: an Infrastructure for Examining Security Properties of software. In: ACM Conference on Computer and Communications Security.Washington, DC, USA: 2002.
[47] G H. UNO: Static source code checking for user-defined properties. Technical Bell Labs, 2002.
[48] Detlefs D L, Leino K R M, Nelson G S J B. Extended Static Checking. Technical Palo Alto, USA: Compaq System Research Center, 1998.
[49] Rustan K, L M. Extended static checking:a ten-year perspective. In: Lecture Notes in Computer Science.New York: Springer, 2001.
[50] Dor N, rodeh M S M. CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C. In: ACM Conference on Programming Language Design and Implementation.San Diego, California, USA: 2003.
[51] B. V. Chess. Improving Computer Security using Extended Static Checking. In:IEEE Symposium on Security and Privacy.Oakland, California, USA: 2002.
[52] Welcome to RATS - Rough Auditing Tool for Security.http://www.fortifysoftware.com/security-resources/rats.jsp.2007.
[53] J. Viega, J. T. Bloch, Y. Kohno G M. ITS4: A static vulnerability scanner for C and C++ code. ACM Transactions on Information and System Security. 2002,5(2).
[54] Flawfinder. http://www.dwheeler.com/flawfinder/.
[55] V. Markstein, J. Cocke P M. Optimization of Range Checking. In: Symposium on Compiler Construction.Boston, Massachusetts, USA: 1982.
[56] Gupta R. A fresh look at optimizing array bound checking. In: ACM Conference on Programming Language Design and Implementation.New York, USA: 1990.
[57] Gupta R. Optimizing array bound checks using flow analysis. 1993
[58] Hongwei Xi, F P. Eliminating array bound checking through dependent types. In:ACM Conference on Programming Language Design and Implementation.Montreal, Canada: 1998.
[59] Bodik R. ABCD: Eliminating array bounds checks on demand. In: ACM Conference on Programming Language Design and Implementation.Vancouver,British Columbia, Canada: 2000.
[60] George C. Necula, Scott Mcpeak W W. CCured: type-safe retrofitting of legacy code. In: ACM Conference on Programming Language Design and Implementation.Berlin, Germany: 2002.
[61] Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney Y W.Cyclone: A Safe Dialect of C. In: USENIX Annual Technical Conference.Monterey, CA, USA: 2002.
[62] Schmidt D A. Data flow analysis is model checking of abstract interpretations. In:ACM Conference on Symposium on Principles of Programming Languages.San Diego, California, USA: 1998.
[63] Shankar N. Combining Theorem Proving and Model Checking through Symbolic Analysis. In: ACM conference on Concurrency Theory.London, UK: 2000.
[64] P. Cousot, R C. Refining model checking by abstract interpretation. Automated Software Engineering. 1999(6): 69-95.
[65] P. Cousot, R C. Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. In: Program Analysis by Abstract Interpretation.La Jolla, California, USA: 1995.
[66] 王兵山,王长英,周贤林.离散数学.长沙:国防科技大学出版社,1986.
[67] Muchnick S S. 高级编译器设计与实现.机械工业出版社, 2003.
[68] Westley Weimer, George C. Necula, Scott Mcpeak S P R. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In:International Conference on Compiler Construction.Grenoble, France: 2002.
[69] BANE: Analysis Programmer. Interface.http://www.cs.berkeley.edu/Research/Aiken/#0.
[70] Wagner D. Static analysis and computer security: New techniques for software assurance. PH. D., Berkley: University of California, 2001.
[71] Vinod Ganapathy, Somesh Jha, David Chandler, David Melski D V. Buffer Overrun Detection using Linear Programming and Static Analysis. In: ACM Conference on Computer and Communications Security.Washington, DC, USA:2003.
[72] Evans D, L D. Improving security using extensible lightweight static analysis.IEEE Software. 2002(1): 42-51.
[73] Livshits V B, Lam M S. Tracking Pointers with Path and Context Sensitivity for Bug Detection in C Programs. In: European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering.Helsinki,Finland: 2003.
[74] Venet A, V A. Precise and efficient static array bound checking for large embedded C programs. In: ACM Conference on Programming Language Design and Implementation.Washington, DC, USA: 2004.
[75] PolySpace C Verifier: Product Leaflet.www.cert.fr/francais/deri/seguin/SEE/00.05.25/CLeaflet.pdf.2000.
[76] Blanchet B. A Static Analyzer for Large Safety Critical software. In: ACM Conference on Programming Language Design and Implementation.San Diego,California, USA: 2003.
[77] AIRAC: Static Analzyer for Automatic Verification of Array Index Ranges in C Programs. http://ropas.snu.ac.kr/airac.2005.
[78] Kwangkeun Yi, Yungbum Jung, Jaehwang Kim J S. Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience. In:BUGS 2005 Workshop on the Evaluation of Software Defect Detection Tools.Chicago, Illinois, USA: 2005.
[79] Detlefs D, Nelson G, Saxe J B. Simplify: A Theorem Prover for Program Checking.Technical HP Labs, 2003.
[80] Palsberg J. Type-based analysis and applications. In: Workshop on Program Analysis for Software Tools and Engineering.Snowbird, Utah, USA: ACM Press,2001.
[81] Johnson R, W D. Finding User/Kernel Pointer Bugs With Type Inference. USENIX Security Symposium.San Diego, CA, USA: 2004.
[82] Dawson Engler, Madanlal Musuvathi. Static analysis versus software model checking for bug finding. Proc. of the 5th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004). LNCS 2937,Springer-Verlag, 2004. 191-210.
[83] Visser W, Havelund K, Brat G, Park S L F. Model Checking Programs. Automated Software Engineering Jounal. 2003,10(2): 203-232.
[84] Madanlal Musuvathi, David Park, Andy Chou, Dawson R. CMC: A Pragmatic Approach to Model Checking Real Code. In: The Fifth Symposium on Operating Systems Design and Implementation.Boston, Massachusetts, USA: 2002.
[85] P G. Model Checking for Programming Languages using VeriSoft. In: ACM Symposium on Principles of Programming Languages.Paris, France: 1997.
[86] Henzinger T A, Jhala R, majumdar R E A. Software Verification with Blast. In:SPIN Workshop on Model Checking Software.Springer-Verlag, 2003. 235—239.
[87] Ball T, R S K. The SLAM Project: Debugging System Software via Static Analysis. In: ACM Conference on Symposium on Principles of Programming Languages.Portland, OR, USA: 2002.
[88] SUIF. http://suif.stanford.edu.
[89] William Blume, R E. Symbolic Range Propagation. In: the 9th International Parallel Processing Symposium.Cancun, Mexico, USA: 1994.
[90] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman F K Z.Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems. 1991,13(4):451-490.
[91] Yuri Gurevich, JKH. The Semantics of the C Programming Language. In: Workshop on Computer Science Logic.Berne, Switzerland: 1992.
[92] Papaspyrou N. A formal semantics for the C programming language. Ph. D.,National Technical University of Athens, 1998.
[93] Fahringer T. Efficient symbolic analysis for parallelizing compilers and performance estimators. The Journal of Supercomputing. 1998, 12(3): 1-29.
[94] Radu Rugina, M R. Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions. In: ACM Conference on Programming Language Design and Implementation.Vancouver B.C., Canada: 2000.
[95] Vaserstein L N. Introduction to Linear Programming. 机械工业出版社, 2005.
[96] SoPlex.www.zib.de/Optimization/Software/Soplex/.2007.
[97] CPLEX. http://www.cplex.com.2007.
[98] FortMP Manual. http://www.unicom.co.uk/FortMP/ManFrame.htm.
[99] CLP. http://opensource.org/licenses/cpl.php.
[100] GLPK - GNU Project - Free Software Foundation(FSF).www.gnu.org/software/glpk/.
[101] LPSOLVE. http://www.statslab.cam.ac.uk/～rrwl/opt/lp_solve/.
[102] The LLVM Compiler Infrastructure. http://www.llvm.org.
[103] SUIF. http://suif.stanford.edu.
[104] Lengauer, thomasRobertETarjan. A fast algorithm for finding dominators in a flowgraph. ACM Transactions on Programming Languages and System. 1979,1(1): 121-141.
[105] Steensgaard B. Points-to analysis in almost linear time. In: ACM SIGPLAN-SIGACT symposium on Principles of programming languages.St.Petersburg Beach, Florida, USA: ACM Press, 1996.
[106] Andersen. Program Analysis and Specialization for the C Programming Language. PH. D., DIKU, University of Copenhagen, 1994.
[107] Manuvir Das, Ben Liblit, Manuel Fahndrich J R. Estimating the Impact of Scalable Pointer Analysis on Optimization. In: Static Analysis Symposium.Paris,France: 2001.
[108]Lattner C.Macroscopic Data Structure Analysis and Optimization.Ph.D.,University of Illinois at Urbana-Champaign,2005.