代码迷惑及其语义研究
|
摘要
移动代码是计算机网络和Internet技术中广泛应用的一种计算模式,而且也被应用在许多新的技术中,如移动代理、主动网络等。但是,移动代码也带来了单机环境中不存在的安全威胁。这种威胁来自两个方面:一方面,当移动代码被下载到主机,恶意主机将可能会逆向工程这些代码,从而窃取代码中包含的关键算法或数据。在一些特殊的场合,如在移动代理中,代表计算主体完成计算的移动代理程序及其数据状态对于执行这些程序的主机是开放的。如果该主机是恶意主机,它就有可能对移动代理程序及其数据状态进行篡改,以达到攻击其它主机的目的。另一方面,网络的发展使得我们可以越来越方便地下载并执行一段代码,但是如果这段代码是具有恶意行为的,就有可能会破坏主机系统的资源,威胁到主机机密信息的安全。这两方面问题就称为是恶意主机问题和恶意客户问题。
代码迷惑是为解决恶意主机问题提出的一种自动程序变换技术,在恶意主机问题和恶意客户问题两个方面,代码迷惑扮演着不同的角色,这分别带来了需要研究的问题:
在恶意主机问题中,代码迷惑是一种有效的软件保护机制,但是,代码迷惑以前的研究主要集中在如何构造代码迷惑算法,而对于构造的代码迷惑算法是否有效,这些研究都没有提供严格证明,代码迷惑算法的构造缺乏有效性证明的理论支持。
在恶意客户问题中,代码迷惑被广泛地用来构造恶意软件变体,这给现存的恶意软件判定技术带来了新的问题。采用代码迷惑构造的多态病毒、变体病毒,使得现在已有的恶意软件判定器对主机的保护效果大大降低。
本文研究的思路是建立代码迷惑与语义理论的联系,从而可以利用已有的形式语义方面的研究解决代码迷惑研究中现存的问题。针对上述代码迷惑应用于移动代码安全时分别存在和导致的问题,本文研究分为两个方面:
(1)在恶意主机问题中,代码迷惑是一种保护客户代码的重要的安全性技术,但是目前缺乏代码迷惑作为安全性方法的理论基础。本文研究了从语义角度为代码迷惑建立统一的有效性比较方法:
◇建立代码迷惑有效性比较框架,包括两个部分:形式化代码迷惑空间,形式地定义代码迷惑有效性度量。在该框架中,采用语义信息的变化来刻画有效性,允许定义更加细化的有效性度量,也能将传统的基于语法的有效性度量纳入这个比较系统。
◇压平算法是一种重要的迷惑算法,本文给出了压平算法的形式描述,并基于代码迷惑有效性比较框架证明了其有效性。
我们发现基于偏序的代码迷惑有效性比较框架在表达力方面具有一定的局限性,无法为各种代码迷惑算法都建立有效性比较。
◇本文研究了概率化抽象解释框架,通过建立程序不确定性的量化比较关系,从而达到量化比较代码迷惑有效性的目的。针对目前概率化抽象解释只能适用于有限维状态空间的问题,提出使用紧空间来刻画无限维状态空间的方法,扩展了概率化抽象解释的应用范围。这样,将状态空间提升到可度量的矢量空间上,就可以通过在矢量空间中定义距离来作为迷惑算法的有效性度量。
(2)在恶意客户问题中,代码迷惑技术是一种重要的攻击手段,为构造恶意软件变体提供了一种有效的方法,这使得传统病毒发现技术受到了挑战。本文从语义角度研究了恶意软件的变体判定技术:
◇本文建立了一种新的基于语义的恶意软件判定框架(MOM)。代码迷惑是一种保语义的程序变换技术,可以使用这种程序之间的语义相关性来作为识别一个程序是否是某恶意程序变体的标准。对于属于同一变体的恶意程序,MOM无需更新病毒库就能实现对恶意程序的识别。
◇改进并设计了基于验证的恶意软件判定方法。该方法将恶意软件判定问题转化为证明验证条件正确性问题,并且通过输入迷惑算法规范来指导验证条件的产生和证明。
◇MOM的验证条件产生是采用符号执行技术,因此如何高效地求解符号状态也是需要研究的问题。本文提出了一种不同于传统符号执行的方式,针对传统符号执行中状态替换时效率低下的问题,以静态单赋值形式作为中间表示,以基于支配树作为程序符号状态的收集策略,从而实现了高效地收集符号状态。
◇本文基于编译框架LLVM,实现了一个MOM的原型系统。实验过程说明了基于语义恶意软件判定框架的有效性。
Mobile code is a kind of computing model that is widely used not only in computer network and Internet technique, but also in many new techniques, such as mobile agent and Ad hoc network. However, Mobile code poses threats to security, which had never happened in the stand-alone environment. The threats come from two aspects. In one aspect, when mobile code is downloaded on a host, a malicious host will reverse engineer the code to extract secret data and algorithm from it. In some special situations, such as in mobile agent, the mobile agent program and its data state which work as the computing entity to finish the computation are open to the host. But a malicious host might tamper the agents for the purpose of attacking the mobile code. In the other aspect, the widespread of Internet make it more convenient and easier to download and execute pieces of code. But if the code is malicious, it might ruin resource and security of the host. The two aspects are called as malicious host problem and malicious code problem.
Code obfuscation is a technique of automatic program transformation for solving the malicious host problem. The different roles played by code obfuscation in these two aspects incur respective problems to be dealt with: In mobile host problem, code obfuscation is a useful method to guarantee the security in mobile agent and protect the program from reverse engineering. At present, the interests on code obfuscation mainly focus on the construction of code obfuscation algorithm. None of these algorithms has provided the efficiency proof. In mobile code problem, code obfuscation is a widely-used tool to construct malware variations, which is a hard problem to the research of malware detection. The metaphor and polymorphic virus constructed by code obfuscation have greatly reduced the protecting capability of current malware detectors.
In this dissertation, the relationship is established between the code obfuscation and semantics. Thus, the existing formal semantics theory enlightens the problem which code obfuscation brings up. According to the two problems, our research consists of two parts:
(1) As for malicious host problem, code obfuscation is an important method to protect client code, but the lack of a theoretical background is a major drawback of current research about code obfuscation. This dissertation proposes a general method for measuring the efficiency based on semantic foundation:
The semantic-based comparable framework measuring obfuscation efficiency includes two parts: formalize the space of code obfuscation and formally define the metrics measuring obfuscation efficiency. In the framework, measuring obfuscation efficiency is based on semantic information, more refined metrics can be defined for measuring obfuscation efficiency and the syntax-based metrics also can be involved into it.
The flattening algorithm is a very important code obfuscation method. This dissertation formally defines the flatting algorithm and proves its efficiency in the comparable framework.
We find that the weak expressiveness is the limitation of the partial order based comparable framework. The comparable framework can't compare all obfuscation algorithm based on partial order metrics.
This dissertation studies the Probabilistic Abstract Interpretation (PAI) and establishes the method to measure program uncertainty. The method can be used for quantitatively measuring obfuscation efficiency. This dissertation also presents the Compact Operator space to extend the PAI in finite-dimension state space to infinite-dimension state space. All the obfuscation algorithms can lift the same concrete domain to a measurable vector space. Thus, the distance defined in the vector space can be used as the metrics to measure obfuscation efficiency.
(2) As for malicious code problem, code obfuscation is an important attack tool for effective construction of malware variations, which brings a big challenge to current technique of malware detection. This dissertation studies the semantics-based malware detection.
It presents a new semantics-based malware detector (MOM). Code obfuscation is a program transformation satisfying semantics-equivalence. The semantic relationship is the key to detecting whether a program is variation of a malware. The variations of one malware can be detected by the MOM without updating the virus database.
It designs a malware detection method based on program verification. The method reduces the problem of malware detection into an equivalent problem of judging the validity of the verification conditions (VC). The specification of obfuscation algorithm can be input to guide the generation and proof of VC.
The verification conditions generation of MOM is on the basis of the symbolic execution. So it's a problem to efficiently collect the symbolic state. Different from the traditional symbolic execution, the method proposed in this dissertation tries to solve the low efficiency in state substitution problem, by utilizing the Static Single Assignment (SSA) as the intermediate representation and the dominator tree based symbolic state as collection strategy, and realizes high efficient collection of symbolic state.
It provides a MOM prototype which implemented on the compiling framework LLVM. The experiment shows that the MOM is effective.
代码迷惑是为解决恶意主机问题提出的一种自动程序变换技术,在恶意主机问题和恶意客户问题两个方面,代码迷惑扮演着不同的角色,这分别带来了需要研究的问题:
在恶意主机问题中,代码迷惑是一种有效的软件保护机制,但是,代码迷惑以前的研究主要集中在如何构造代码迷惑算法,而对于构造的代码迷惑算法是否有效,这些研究都没有提供严格证明,代码迷惑算法的构造缺乏有效性证明的理论支持。
在恶意客户问题中,代码迷惑被广泛地用来构造恶意软件变体,这给现存的恶意软件判定技术带来了新的问题。采用代码迷惑构造的多态病毒、变体病毒,使得现在已有的恶意软件判定器对主机的保护效果大大降低。
本文研究的思路是建立代码迷惑与语义理论的联系,从而可以利用已有的形式语义方面的研究解决代码迷惑研究中现存的问题。针对上述代码迷惑应用于移动代码安全时分别存在和导致的问题,本文研究分为两个方面:
(1)在恶意主机问题中,代码迷惑是一种保护客户代码的重要的安全性技术,但是目前缺乏代码迷惑作为安全性方法的理论基础。本文研究了从语义角度为代码迷惑建立统一的有效性比较方法:
◇建立代码迷惑有效性比较框架,包括两个部分:形式化代码迷惑空间,形式地定义代码迷惑有效性度量。在该框架中,采用语义信息的变化来刻画有效性,允许定义更加细化的有效性度量,也能将传统的基于语法的有效性度量纳入这个比较系统。
◇压平算法是一种重要的迷惑算法,本文给出了压平算法的形式描述,并基于代码迷惑有效性比较框架证明了其有效性。
我们发现基于偏序的代码迷惑有效性比较框架在表达力方面具有一定的局限性,无法为各种代码迷惑算法都建立有效性比较。
◇本文研究了概率化抽象解释框架,通过建立程序不确定性的量化比较关系,从而达到量化比较代码迷惑有效性的目的。针对目前概率化抽象解释只能适用于有限维状态空间的问题,提出使用紧空间来刻画无限维状态空间的方法,扩展了概率化抽象解释的应用范围。这样,将状态空间提升到可度量的矢量空间上,就可以通过在矢量空间中定义距离来作为迷惑算法的有效性度量。
(2)在恶意客户问题中,代码迷惑技术是一种重要的攻击手段,为构造恶意软件变体提供了一种有效的方法,这使得传统病毒发现技术受到了挑战。本文从语义角度研究了恶意软件的变体判定技术:
◇本文建立了一种新的基于语义的恶意软件判定框架(MOM)。代码迷惑是一种保语义的程序变换技术,可以使用这种程序之间的语义相关性来作为识别一个程序是否是某恶意程序变体的标准。对于属于同一变体的恶意程序,MOM无需更新病毒库就能实现对恶意程序的识别。
◇改进并设计了基于验证的恶意软件判定方法。该方法将恶意软件判定问题转化为证明验证条件正确性问题,并且通过输入迷惑算法规范来指导验证条件的产生和证明。
◇MOM的验证条件产生是采用符号执行技术,因此如何高效地求解符号状态也是需要研究的问题。本文提出了一种不同于传统符号执行的方式,针对传统符号执行中状态替换时效率低下的问题,以静态单赋值形式作为中间表示,以基于支配树作为程序符号状态的收集策略,从而实现了高效地收集符号状态。
◇本文基于编译框架LLVM,实现了一个MOM的原型系统。实验过程说明了基于语义恶意软件判定框架的有效性。
Mobile code is a kind of computing model that is widely used not only in computer network and Internet technique, but also in many new techniques, such as mobile agent and Ad hoc network. However, Mobile code poses threats to security, which had never happened in the stand-alone environment. The threats come from two aspects. In one aspect, when mobile code is downloaded on a host, a malicious host will reverse engineer the code to extract secret data and algorithm from it. In some special situations, such as in mobile agent, the mobile agent program and its data state which work as the computing entity to finish the computation are open to the host. But a malicious host might tamper the agents for the purpose of attacking the mobile code. In the other aspect, the widespread of Internet make it more convenient and easier to download and execute pieces of code. But if the code is malicious, it might ruin resource and security of the host. The two aspects are called as malicious host problem and malicious code problem.
Code obfuscation is a technique of automatic program transformation for solving the malicious host problem. The different roles played by code obfuscation in these two aspects incur respective problems to be dealt with: In mobile host problem, code obfuscation is a useful method to guarantee the security in mobile agent and protect the program from reverse engineering. At present, the interests on code obfuscation mainly focus on the construction of code obfuscation algorithm. None of these algorithms has provided the efficiency proof. In mobile code problem, code obfuscation is a widely-used tool to construct malware variations, which is a hard problem to the research of malware detection. The metaphor and polymorphic virus constructed by code obfuscation have greatly reduced the protecting capability of current malware detectors.
In this dissertation, the relationship is established between the code obfuscation and semantics. Thus, the existing formal semantics theory enlightens the problem which code obfuscation brings up. According to the two problems, our research consists of two parts:
(1) As for malicious host problem, code obfuscation is an important method to protect client code, but the lack of a theoretical background is a major drawback of current research about code obfuscation. This dissertation proposes a general method for measuring the efficiency based on semantic foundation:
The semantic-based comparable framework measuring obfuscation efficiency includes two parts: formalize the space of code obfuscation and formally define the metrics measuring obfuscation efficiency. In the framework, measuring obfuscation efficiency is based on semantic information, more refined metrics can be defined for measuring obfuscation efficiency and the syntax-based metrics also can be involved into it.
The flattening algorithm is a very important code obfuscation method. This dissertation formally defines the flatting algorithm and proves its efficiency in the comparable framework.
We find that the weak expressiveness is the limitation of the partial order based comparable framework. The comparable framework can't compare all obfuscation algorithm based on partial order metrics.
This dissertation studies the Probabilistic Abstract Interpretation (PAI) and establishes the method to measure program uncertainty. The method can be used for quantitatively measuring obfuscation efficiency. This dissertation also presents the Compact Operator space to extend the PAI in finite-dimension state space to infinite-dimension state space. All the obfuscation algorithms can lift the same concrete domain to a measurable vector space. Thus, the distance defined in the vector space can be used as the metrics to measure obfuscation efficiency.
(2) As for malicious code problem, code obfuscation is an important attack tool for effective construction of malware variations, which brings a big challenge to current technique of malware detection. This dissertation studies the semantics-based malware detection.
It presents a new semantics-based malware detector (MOM). Code obfuscation is a program transformation satisfying semantics-equivalence. The semantic relationship is the key to detecting whether a program is variation of a malware. The variations of one malware can be detected by the MOM without updating the virus database.
It designs a malware detection method based on program verification. The method reduces the problem of malware detection into an equivalent problem of judging the validity of the verification conditions (VC). The specification of obfuscation algorithm can be input to guide the generation and proof of VC.
The verification conditions generation of MOM is on the basis of the symbolic execution. So it's a problem to efficiently collect the symbolic state. Different from the traditional symbolic execution, the method proposed in this dissertation tries to solve the low efficiency in state substitution problem, by utilizing the Static Single Assignment (SSA) as the intermediate representation and the dominator tree based symbolic state as collection strategy, and realizes high efficient collection of symbolic state.
It provides a MOM prototype which implemented on the compiling framework LLVM. The experiment shows that the MOM is effective.
引文
[1]Antonio Carzaniga,Gian Pietro Picco and Giovanni Vigna.Understanding Code Mobility.In IEEE Transactions on Software Engineering 24(5):342-361,1997.
[2]GH.Forman and J.Zahorjan,The Challenges of Mobile Computing,Computer,vol.27,no.4,pages 38-47,1994.
[3]D.Wong,N.Paciorek,Y.Walsh,J.DiCelie,M.Young,and B.Peet.Concordia:An infrastructure for collaborating mobile agents.In First International Workshop of Mobile Agents,MA'97,pages 86-97,1997.
[4]J.Panda,L.Ertaul.Mobile Agent Security,M.Sc.Thesis,California State University,East Bay,2007.
[5]David Kotz.Future directions for mobile agent research.IEEE computer science,2002.
[6]Active Networks Working Group.Architectural Framework for Active Networks Version 1.0.1999.
[7]黄少寅.主动网安全机制若干问题的研究,博士论文,复旦大学,2004.
[8]T.Lindolm and F.Yellin.The Java virtual machine specification.Addison-Wesley,1996.
[9]Fred B.Schneider,Greg Morrisett,Robert Harper.A language-based approach to security.Informatics." 10 Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Heidelberg,pages.86-101,2000.Springer
[10]Peter Lee,George Necula.Research on Proof-Carrying Code for Mobile-Code Security.In Proceedings of the Workshop on Foundations of Mobile Code Security,1997.
[11]From system F to typed assembly language.In ACM Transactions on Programming Languages and Systems,21(3):527-568.1999.
[12]P.Szor.The Art of computer virus research and defense.Addison-Wesley Professional,2005
[13]Cohen F.Computational aspects of computer viruses.Computers & Security,8(4):325-344,1989.
[14]E Filiol,M.Helenius,S.Zanero.Open problems in computer virology.Journal in Computer Virology,1(3):55-66,2006.
[15]Bussiness software Alliance.2007 URL http://w3.bsa.org/china/.
[16]P.C.van Oorschot.Revisiting software protection.In Proceedings of 6th lnternational Information Security Conference(ISC 2003),pages 1-13.Bristol,UK,October 2003.Springer.
[17]Bertrand Anckaert,Bjorn De Sutter and Koen De Bosschere.Software Piracy Prevention through Diversity.In Proceedings of the 4th ACM Workshop on Digital Rights Management,2004.
[18]M.Jakobsson and M.K.Reiter.Discouraging software piracy using software aging,in Proceedings 1st ACM Workshop on Digital Rights Management(DRM 2001),pages 1-12.,2002.Springer.
[19]D.Aucsmith.Tamper resistant software:An implementation.In Proc.1st International Information Hiding Workshop(IHW),pages 317-333,1997.Cambridge,U.K.1997.Springer.
[20]B.Horne and L.Matheson and C.Sheehan and R.Tarjan.Dynamic self-checking techniques for improved tamper resistance.In Proc.1st ACM Workshop on Digital Rights Management (DRM2001),pages 141-159,2002.Springer.
[21]Y.Chen and R.Venkatesan and M.Cary and R.Pang and S.Sinha and.M.Jakubowski.Oblivious hashing:A stealthy software integrity verification primitive.In Proc.5th Information Hiding Workshop(IHW),pages 400-414,Netherlands,October 2002
[22]Trusted Computing Group.2007 URL.http://www.trustedcomputinggroup.org/home.
[23]D.Lie and C.Thekkath and M.Mitchell and P.Lincoln and D.Boneh and J.Mitchell and M.Horowitz.Architectural support for copy and tamper resistant software.In Proc.9th International Conf Architectural Support for Programming Languages and Operating Systems,Nov.2000
[24]R.J.Anderson and M.G.Kuhn.Low cost attacks on tamper-resistant devices.In 5th International Workshop on Security Protocols,pages 125-136.1997.Springer.
[25]Christian Collberg and Clark Thomborson.Software watermarking:Models and dynamic embeddings.In Proceedings of the 26rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL '99),January 1999.
[26]Christian Collberg,Clark Thomborson.Watermarking,Tamper-Proofing,and ObfuscationTools for Software Protection.IEEE Transactions on Software Engineering 28:8,735-746,August 2002.
[27]Christian Collberg,Clark Thomborson,and Douglas Low.Breaking abstractions and unstructuring data structures.In Proceedings of the 1998 International Conference on Computer Languages,page 28-38.IEEE Computer Society,1998.
[28]Cristian Collberg,Clark Thomborson,and Douglas Low.Manufacturing cheap,resilient and stealthy opaque constructs.In Proceedings of the 25rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL '98),pages 184-196,1998.
[29]Cristian Collberg,Clark Thomborson,and Douglas Low.A taxonomy of obfuscating transformations.Department of Computer Science,the University of Auckland.Technical report #148,1997.
[30]L.Ertaul,S.Venkatesh.Novel Obfuscation Algorithms for Software Security,In Proceedings of the 2005 International Conference on Software Engineering Research and Practice,(SERP '05),June,Las Vegas,2005.
[31]Anirban Majumdar,Clark D.Thomborson.Manufacturing opaque predicates in distributed systems for code obfuscation.ACSC 2006,pages 187-196,2006.
[32]William Zhu,Clark D.Thomborson,Fei-Yue Wang:Applications of Homomorphic Functions to Software Obfuscation.WISI:pages 152-153,2006.
[33]M.Weiser.Program slicing.IEEE Transactions on Software Engineering,16(5):498-509,1984.
[34]S.Horwitz,ToReps,and D.Binkley.Interprocedural slicing.In the 20th International Conference on Software Engineering,pages 74-83,1998.
[35]Rakesh Ghiya.Interprocedural analysis in the presence of function pointers.ACAPS Technical Report:62,Dec 28,1992.
[36]N.Jones.An introduction to partial evaluation.ACM Computing Surveys,28(3):480-504,1996.
[37]Cloakware.2007 URL.http://www.cloakware.com/products_services/security_suite/.
[38]S.Venkatesh,L.Ertaul.JHIDE-A Tool Kit for Code Obfuscation,M.Sc.Thesis,California State University,East Bay,2004.
[39]Sandmark.2007 URL.http://sandmark.cs.arizona.edu/.
[40]Gregory Wroblewski.General method of program code obfuscation.PhD thesis,Wroclaw University of Technology,Institute of Engineering Cybernetics,2002.
[41]Wang CX.A security architecture for survivability mechanisms.PhD thesis,University of Virginia,Department of Computer Science,2000.
[42]Lee B,Larry D.Self-protecting mobile agents obfuscation technique evaluation report.Network Associates Laboratories,Report#01-036,2002.
[43]李永祥,陈意云.基于函数指针数组的代码迷惑技术,计算机学报,2004,27(12):1706-1711.
[44]李永祥,陈意云.基于多分支语句的控制流迷惑技术,小型微型计算机系统,2006,27(9):1637-1640.
[45]阳雪林,于勐,陈道蓄,谢立.自动并行编译新技术,软件学报,2000,11(9):1268-1275.
[46]Douglas L.Protecting Java code via code obfuscation,ACM Crossroads,Spring issue 1998.
[47]Josh MacDonald.On Program Security and Obfuscation.Technical Report 9806,University of Virginia,December,1998.
[48]Robert Park.Software Size Measurement:A Framework for Counting Source Statements.Technical Report CMU/SEI-92-TR-020,1992.
[49]McCabe,Charles W.Design Complexity Measurement and Testing.Communications of the ACM 32(12):1415-1425,1989.
[50]McCabe,Thomas J,Arthur H.Software Complexity.Crosstalk,Journal of Defense Software Engineering 7(12):5-9,1994.
[51]E.I.Oviedo.Control flow,data flow and programmers complexity.In Proc.of COMPSAC80,pages 146-152.Chicago,IL,1980.
[52]F.Cohen.Computer viruses.PhD thesis,University of Southern California,1985.
[53]F.Cohen.Computer viruses:Theory and experiments.Computers and Security,6(1):22-35,1987.
[54] N. P. Varnovsky, V. A. Zakharov, N. N. Kuzyurin. Mathematical Problems of Obfuscation.2007 URL. http://www.ispras.ru/news/downloads/obfuscation/obfuscation.pdf
[55] Thomas McCabe. A complexity measure. IEEE Transactions on Software Engineering,2(4):308-320, 1976.
[56] Kelly Heffner and Christian Collberg. The Obfuscation Executive. Information Security Conference, September 27-29, 2004.
[57] Alfred V.Aho, Ravi sethi, Jeffrey D. Ullman. Compiler: Principles, Techniques, and Tools.Pearson Education, Dec, 1986.
[58] T. Ogiso, Y. Sakabe, M. Soshi, and A. Miyaji. Software obfuscation on a theoretical basis and its implementation. IEEE Transaction Fundamentals, E86-A (1), 2003.
[59] S. Chow, Y. Gu, H. Johnson, and V. A. Zakharov. An approach to the obfuscation of control-flow of sequential computer programs. In Proc. 4th International Information Security Conference (ISC'01), volume 2200 of LNCS, pages 144-155,2001.
[60] A. W. Appel. Deobfuscation is in NP. August, 2002.
[61] B.Barak, O.Goldreich, R.Impagliazzo, S.Rudich, A.Sahai, S.P.Vadhan, and K.Yang. On the (im) possibility of obfuscating programs. In Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology. Santa Barbara, California,pages 19-23,2001. Springer.
[62] B. Lynn and M. Prabhakaran and A. Sahai.Positive Results and Techniques for Obfuscation. In Proceedings of EuroCRYPT, Interlaken, Switzerland, pages 20-39,2004.
[63] Symantec Corp. Understanding and managing polymorphic viruses. Technical report, 1996.
[64] C. Nachenberg. Computer virus-antivirus coevolution. Communications of the ACM,40(1):46-51,1997.
[65] Szor P, Ferrie P. Hunting for metamorphic. In Virus Bulletin Conference, 2001.
[66] D.M. Chess and S.R. White. An undetectable computer virus. In Virus Bulletin Conference,2000.
[67] F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 1999.
[68] Plotkin,G.D. Structural operational semantics. Lecture Notes, DAIMI FN-19,1981.
[69] C.Strachey. Towards a Formal Semantics. Formal Language Description Languages for Computer Programming, pages 198-220, North-Holland, Amsterdam, 1966.
[70] R.D.Tennent.The denotational semantics of programming language.Communications of the ACM, 1976, 19(8):437-453.
[71] C. A. R .Hoare.An axiomatic basis for computer programming. Communications of the ACM,1969, 12(10):576-583.
[72] Scott D.S. Domains for denotational semantics. In Procedings of ICALP'82, Lecture Notes in Computer Science vol.140.1982. Springer.
[73] P.Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, 2002, 277(1-2): 47-103.
[74]陈意云,张昱.编译原理.北京:高等教育出版社,2003.
[75]Patrick Cousot.Abstract.Interpretation Based Formal Methods and Future Challenges.Informatics:10 Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Springer-Verlag,Heidelberg,138-156,2000.
[76]J.C.King.Symbolic execution and program testing,Communications of the ACM,19(7),pages 385-394,1976.
[77]Bjarne Steensgaard.Points-to analysis in almost linear time.In Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL'96).Florida,United States,pages 32-41,1996.
[78]Jeffrey S.Foster,Robert Johnson,John Kodumal,and Alex Aiken.Flow-lnsensitive Type Qualifiers.In ACM Transactions on Programming Languages and Systems.28(6):1035-1087,November 2006.
[79]Jeffrey S.Foster,Tachio Terauchi,and Alex Aiken.Flow-sensitive type qualifiers.In ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI'02),pages 1-12,June 2002.
[80]E.M.Clarke,E.A.Emerson and A.P.Sistla.Automatic verification of finite-state concurrent systems using temporal logic specifications.In ACM Transactions on Programming Languages and Systems,8(2):244-263,1986.
[81]E M.Clarke.Progress on the State Explosion Problem in Model Checking.Informatics:10Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Heidelberg,176-196,2000.Springer.
[82]Shuvendu K.Lahiri,Thomas Ball,Byron Cook.Predicate Abstraction via Symbolic Decision Procedures.Technical Report MSR-TR-2005-53,2005.
[83]P.Cousot,R.Cousot.Abstract interpretation:a unified lattice model for static analysis of program by construction or approximation of fixpoints.In proceedings of ACM SIGPLAN-SIGACT on Principles Of Programming Languages(POPL'77),Los Angeles,California,1977,238-252.
[84]P.Cousot and N.Halbwachs.Automatic discovery of linear restraints among variables of a program.In 5th POPL,pages 84-97,Tucson,AZ,1978.ACM Press.
[85]A.Cortesi,G.File,R.Giacobazzi,C.Palamidessi,and F.Ranzato.Complementation in abstract interpretation.In ACM Transaction Programming Language and System.19(1):7-47,1997.
[86]P.Cousot,R.Cousot.Systematic design of program transformation frameworks by abstract interpretation.In Proceedings of ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages(POPL'02),Portland Oregon,2002,178-190.
[87]M.Dalla Preda and R.Giacobazzi.Semantic-based code obfuscation by abstract interpretation.In Proceedings of the ICALP'05,Lisbon,Portugal,2005:1325-1336.
[88]M.Dalla Preda and R.Giacobazzi.Control code obfuscation by abstract interpretation.In Proceedings of the SEFM'05,Koblbenz,Germany,2005:301-310.
[89] Susan Horwitz. Precise Flow-Insensitive May-Alias Analysis is NP-Hard. University of Wisconsin-Madison Technical Report #198,1996.
[90] Anirban Majumdar, Stephen Drape and Clark Thomborson .Metrics-based Evaluation of Slicing Obfuscations. In 2007 International Workshop on Data Hiding for Information and Multimedia Security in conjunction. Manchester, UK, 2007.
[91] N. Saheb-Djahromi. CPO's of measures for nondeterminism. Theoretical Computer Science,12:19-37, 1980.
[92] Richard Blute, Josee Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. In Proceedings Twelth Annual IEEE Symposium on Logic in Computer Science, pages 149-158, Warsaw, Poland, June/July 1997. IEEE Computer Society Press.
[93] Di Pierro, C. Hankin and H. Wiklicky .Probabilistic Lambda-calculus and Quantitative Program Analysis. Journal of Logic and Computation, 15(2): 159-179, 2005.
[94] Di Pierro and H. Wiklicky. Operator Algebras and the Operational Semantics of Probabilistic Languages. Electronic Notes in Theoretical Computer Science. Volume 161,2006.
[95] Di Pierro and H. Wiklicky. Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. In M.Gabbrielli and F.Pfennning, editor. In Proceedings of PPDP'00,Monteeal, Canada. 2000.
[96] Di Pierro and H. Wiklicky. Linear Structure for concurrent programming languages. In M.Gabbrielli and F.Pfennning, editor. In Proceedings of PPDP'00, Monteeal, Canada. 2001.
[97] Edalat, P.Shunderhauf. Computable banach spaces via domain theory. In Theoretical Computer Science 1999,219(1-2), 169-184.
[98] S. S. Muchnick. Advanced compiler design and implementation. Academic Press, Sept. 1997.
[99] R. Jhala, R. Majumdar, R. G. Xu. Structural Invariants. In Proceedings of the 13th International Static Analysis Symposium, pages 71-87,2006.
[100] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02), pages 234-245,2002.
[101] Chris Lattner and Vikram Adve.LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization, Palo Alto, California, Mar. 2004.
[102] A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,LNCS 1384, pages 151-166, 1998.
[103] G. Necula, Translation validation for an optimizing compiler, In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00),pages 83-94, 2000.
[104]Y.Fang.Translation validation of optimizing compilers.PhD thesis.New York University,Department of Computer Science,2005.
[105]C.Mihai,S.Jha,S.A.Seshia,D.Song,and R.E.Bryant.Semantics-aware malware detection.In Proceedings of the 2005 IEEE Symposium on Security and Privacy,pages 32-46,2005.
[106]S.Lerner,T.Millstein,E.Rice,and C.Chambers.Automated soundness proofs for dataflow analyses and transformations via local rules.In Proceedings of the 32rd ACM SIGPLAN-SIGACT Conference on Principles Of Programming Languages(POPL '05),pages 364-377,Jan.2005.
[2]GH.Forman and J.Zahorjan,The Challenges of Mobile Computing,Computer,vol.27,no.4,pages 38-47,1994.
[3]D.Wong,N.Paciorek,Y.Walsh,J.DiCelie,M.Young,and B.Peet.Concordia:An infrastructure for collaborating mobile agents.In First International Workshop of Mobile Agents,MA'97,pages 86-97,1997.
[4]J.Panda,L.Ertaul.Mobile Agent Security,M.Sc.Thesis,California State University,East Bay,2007.
[5]David Kotz.Future directions for mobile agent research.IEEE computer science,2002.
[6]Active Networks Working Group.Architectural Framework for Active Networks Version 1.0.1999.
[7]黄少寅.主动网安全机制若干问题的研究,博士论文,复旦大学,2004.
[8]T.Lindolm and F.Yellin.The Java virtual machine specification.Addison-Wesley,1996.
[9]Fred B.Schneider,Greg Morrisett,Robert Harper.A language-based approach to security.Informatics." 10 Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Heidelberg,pages.86-101,2000.Springer
[10]Peter Lee,George Necula.Research on Proof-Carrying Code for Mobile-Code Security.In Proceedings of the Workshop on Foundations of Mobile Code Security,1997.
[11]From system F to typed assembly language.In ACM Transactions on Programming Languages and Systems,21(3):527-568.1999.
[12]P.Szor.The Art of computer virus research and defense.Addison-Wesley Professional,2005
[13]Cohen F.Computational aspects of computer viruses.Computers & Security,8(4):325-344,1989.
[14]E Filiol,M.Helenius,S.Zanero.Open problems in computer virology.Journal in Computer Virology,1(3):55-66,2006.
[15]Bussiness software Alliance.2007 URL http://w3.bsa.org/china/.
[16]P.C.van Oorschot.Revisiting software protection.In Proceedings of 6th lnternational Information Security Conference(ISC 2003),pages 1-13.Bristol,UK,October 2003.Springer.
[17]Bertrand Anckaert,Bjorn De Sutter and Koen De Bosschere.Software Piracy Prevention through Diversity.In Proceedings of the 4th ACM Workshop on Digital Rights Management,2004.
[18]M.Jakobsson and M.K.Reiter.Discouraging software piracy using software aging,in Proceedings 1st ACM Workshop on Digital Rights Management(DRM 2001),pages 1-12.,2002.Springer.
[19]D.Aucsmith.Tamper resistant software:An implementation.In Proc.1st International Information Hiding Workshop(IHW),pages 317-333,1997.Cambridge,U.K.1997.Springer.
[20]B.Horne and L.Matheson and C.Sheehan and R.Tarjan.Dynamic self-checking techniques for improved tamper resistance.In Proc.1st ACM Workshop on Digital Rights Management (DRM2001),pages 141-159,2002.Springer.
[21]Y.Chen and R.Venkatesan and M.Cary and R.Pang and S.Sinha and.M.Jakubowski.Oblivious hashing:A stealthy software integrity verification primitive.In Proc.5th Information Hiding Workshop(IHW),pages 400-414,Netherlands,October 2002
[22]Trusted Computing Group.2007 URL.http://www.trustedcomputinggroup.org/home.
[23]D.Lie and C.Thekkath and M.Mitchell and P.Lincoln and D.Boneh and J.Mitchell and M.Horowitz.Architectural support for copy and tamper resistant software.In Proc.9th International Conf Architectural Support for Programming Languages and Operating Systems,Nov.2000
[24]R.J.Anderson and M.G.Kuhn.Low cost attacks on tamper-resistant devices.In 5th International Workshop on Security Protocols,pages 125-136.1997.Springer.
[25]Christian Collberg and Clark Thomborson.Software watermarking:Models and dynamic embeddings.In Proceedings of the 26rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL '99),January 1999.
[26]Christian Collberg,Clark Thomborson.Watermarking,Tamper-Proofing,and ObfuscationTools for Software Protection.IEEE Transactions on Software Engineering 28:8,735-746,August 2002.
[27]Christian Collberg,Clark Thomborson,and Douglas Low.Breaking abstractions and unstructuring data structures.In Proceedings of the 1998 International Conference on Computer Languages,page 28-38.IEEE Computer Society,1998.
[28]Cristian Collberg,Clark Thomborson,and Douglas Low.Manufacturing cheap,resilient and stealthy opaque constructs.In Proceedings of the 25rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL '98),pages 184-196,1998.
[29]Cristian Collberg,Clark Thomborson,and Douglas Low.A taxonomy of obfuscating transformations.Department of Computer Science,the University of Auckland.Technical report #148,1997.
[30]L.Ertaul,S.Venkatesh.Novel Obfuscation Algorithms for Software Security,In Proceedings of the 2005 International Conference on Software Engineering Research and Practice,(SERP '05),June,Las Vegas,2005.
[31]Anirban Majumdar,Clark D.Thomborson.Manufacturing opaque predicates in distributed systems for code obfuscation.ACSC 2006,pages 187-196,2006.
[32]William Zhu,Clark D.Thomborson,Fei-Yue Wang:Applications of Homomorphic Functions to Software Obfuscation.WISI:pages 152-153,2006.
[33]M.Weiser.Program slicing.IEEE Transactions on Software Engineering,16(5):498-509,1984.
[34]S.Horwitz,ToReps,and D.Binkley.Interprocedural slicing.In the 20th International Conference on Software Engineering,pages 74-83,1998.
[35]Rakesh Ghiya.Interprocedural analysis in the presence of function pointers.ACAPS Technical Report:62,Dec 28,1992.
[36]N.Jones.An introduction to partial evaluation.ACM Computing Surveys,28(3):480-504,1996.
[37]Cloakware.2007 URL.http://www.cloakware.com/products_services/security_suite/.
[38]S.Venkatesh,L.Ertaul.JHIDE-A Tool Kit for Code Obfuscation,M.Sc.Thesis,California State University,East Bay,2004.
[39]Sandmark.2007 URL.http://sandmark.cs.arizona.edu/.
[40]Gregory Wroblewski.General method of program code obfuscation.PhD thesis,Wroclaw University of Technology,Institute of Engineering Cybernetics,2002.
[41]Wang CX.A security architecture for survivability mechanisms.PhD thesis,University of Virginia,Department of Computer Science,2000.
[42]Lee B,Larry D.Self-protecting mobile agents obfuscation technique evaluation report.Network Associates Laboratories,Report#01-036,2002.
[43]李永祥,陈意云.基于函数指针数组的代码迷惑技术,计算机学报,2004,27(12):1706-1711.
[44]李永祥,陈意云.基于多分支语句的控制流迷惑技术,小型微型计算机系统,2006,27(9):1637-1640.
[45]阳雪林,于勐,陈道蓄,谢立.自动并行编译新技术,软件学报,2000,11(9):1268-1275.
[46]Douglas L.Protecting Java code via code obfuscation,ACM Crossroads,Spring issue 1998.
[47]Josh MacDonald.On Program Security and Obfuscation.Technical Report 9806,University of Virginia,December,1998.
[48]Robert Park.Software Size Measurement:A Framework for Counting Source Statements.Technical Report CMU/SEI-92-TR-020,1992.
[49]McCabe,Charles W.Design Complexity Measurement and Testing.Communications of the ACM 32(12):1415-1425,1989.
[50]McCabe,Thomas J,Arthur H.Software Complexity.Crosstalk,Journal of Defense Software Engineering 7(12):5-9,1994.
[51]E.I.Oviedo.Control flow,data flow and programmers complexity.In Proc.of COMPSAC80,pages 146-152.Chicago,IL,1980.
[52]F.Cohen.Computer viruses.PhD thesis,University of Southern California,1985.
[53]F.Cohen.Computer viruses:Theory and experiments.Computers and Security,6(1):22-35,1987.
[54] N. P. Varnovsky, V. A. Zakharov, N. N. Kuzyurin. Mathematical Problems of Obfuscation.2007 URL. http://www.ispras.ru/news/downloads/obfuscation/obfuscation.pdf
[55] Thomas McCabe. A complexity measure. IEEE Transactions on Software Engineering,2(4):308-320, 1976.
[56] Kelly Heffner and Christian Collberg. The Obfuscation Executive. Information Security Conference, September 27-29, 2004.
[57] Alfred V.Aho, Ravi sethi, Jeffrey D. Ullman. Compiler: Principles, Techniques, and Tools.Pearson Education, Dec, 1986.
[58] T. Ogiso, Y. Sakabe, M. Soshi, and A. Miyaji. Software obfuscation on a theoretical basis and its implementation. IEEE Transaction Fundamentals, E86-A (1), 2003.
[59] S. Chow, Y. Gu, H. Johnson, and V. A. Zakharov. An approach to the obfuscation of control-flow of sequential computer programs. In Proc. 4th International Information Security Conference (ISC'01), volume 2200 of LNCS, pages 144-155,2001.
[60] A. W. Appel. Deobfuscation is in NP. August, 2002.
[61] B.Barak, O.Goldreich, R.Impagliazzo, S.Rudich, A.Sahai, S.P.Vadhan, and K.Yang. On the (im) possibility of obfuscating programs. In Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology. Santa Barbara, California,pages 19-23,2001. Springer.
[62] B. Lynn and M. Prabhakaran and A. Sahai.Positive Results and Techniques for Obfuscation. In Proceedings of EuroCRYPT, Interlaken, Switzerland, pages 20-39,2004.
[63] Symantec Corp. Understanding and managing polymorphic viruses. Technical report, 1996.
[64] C. Nachenberg. Computer virus-antivirus coevolution. Communications of the ACM,40(1):46-51,1997.
[65] Szor P, Ferrie P. Hunting for metamorphic. In Virus Bulletin Conference, 2001.
[66] D.M. Chess and S.R. White. An undetectable computer virus. In Virus Bulletin Conference,2000.
[67] F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 1999.
[68] Plotkin,G.D. Structural operational semantics. Lecture Notes, DAIMI FN-19,1981.
[69] C.Strachey. Towards a Formal Semantics. Formal Language Description Languages for Computer Programming, pages 198-220, North-Holland, Amsterdam, 1966.
[70] R.D.Tennent.The denotational semantics of programming language.Communications of the ACM, 1976, 19(8):437-453.
[71] C. A. R .Hoare.An axiomatic basis for computer programming. Communications of the ACM,1969, 12(10):576-583.
[72] Scott D.S. Domains for denotational semantics. In Procedings of ICALP'82, Lecture Notes in Computer Science vol.140.1982. Springer.
[73] P.Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, 2002, 277(1-2): 47-103.
[74]陈意云,张昱.编译原理.北京:高等教育出版社,2003.
[75]Patrick Cousot.Abstract.Interpretation Based Formal Methods and Future Challenges.Informatics:10 Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Springer-Verlag,Heidelberg,138-156,2000.
[76]J.C.King.Symbolic execution and program testing,Communications of the ACM,19(7),pages 385-394,1976.
[77]Bjarne Steensgaard.Points-to analysis in almost linear time.In Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages(POPL'96).Florida,United States,pages 32-41,1996.
[78]Jeffrey S.Foster,Robert Johnson,John Kodumal,and Alex Aiken.Flow-lnsensitive Type Qualifiers.In ACM Transactions on Programming Languages and Systems.28(6):1035-1087,November 2006.
[79]Jeffrey S.Foster,Tachio Terauchi,and Alex Aiken.Flow-sensitive type qualifiers.In ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI'02),pages 1-12,June 2002.
[80]E.M.Clarke,E.A.Emerson and A.P.Sistla.Automatic verification of finite-state concurrent systems using temporal logic specifications.In ACM Transactions on Programming Languages and Systems,8(2):244-263,1986.
[81]E M.Clarke.Progress on the State Explosion Problem in Model Checking.Informatics:10Years Back,10 Years Ahead,Lecture Notes in Computer Science,Vol.2000,Heidelberg,176-196,2000.Springer.
[82]Shuvendu K.Lahiri,Thomas Ball,Byron Cook.Predicate Abstraction via Symbolic Decision Procedures.Technical Report MSR-TR-2005-53,2005.
[83]P.Cousot,R.Cousot.Abstract interpretation:a unified lattice model for static analysis of program by construction or approximation of fixpoints.In proceedings of ACM SIGPLAN-SIGACT on Principles Of Programming Languages(POPL'77),Los Angeles,California,1977,238-252.
[84]P.Cousot and N.Halbwachs.Automatic discovery of linear restraints among variables of a program.In 5th POPL,pages 84-97,Tucson,AZ,1978.ACM Press.
[85]A.Cortesi,G.File,R.Giacobazzi,C.Palamidessi,and F.Ranzato.Complementation in abstract interpretation.In ACM Transaction Programming Language and System.19(1):7-47,1997.
[86]P.Cousot,R.Cousot.Systematic design of program transformation frameworks by abstract interpretation.In Proceedings of ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages(POPL'02),Portland Oregon,2002,178-190.
[87]M.Dalla Preda and R.Giacobazzi.Semantic-based code obfuscation by abstract interpretation.In Proceedings of the ICALP'05,Lisbon,Portugal,2005:1325-1336.
[88]M.Dalla Preda and R.Giacobazzi.Control code obfuscation by abstract interpretation.In Proceedings of the SEFM'05,Koblbenz,Germany,2005:301-310.
[89] Susan Horwitz. Precise Flow-Insensitive May-Alias Analysis is NP-Hard. University of Wisconsin-Madison Technical Report #198,1996.
[90] Anirban Majumdar, Stephen Drape and Clark Thomborson .Metrics-based Evaluation of Slicing Obfuscations. In 2007 International Workshop on Data Hiding for Information and Multimedia Security in conjunction. Manchester, UK, 2007.
[91] N. Saheb-Djahromi. CPO's of measures for nondeterminism. Theoretical Computer Science,12:19-37, 1980.
[92] Richard Blute, Josee Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. In Proceedings Twelth Annual IEEE Symposium on Logic in Computer Science, pages 149-158, Warsaw, Poland, June/July 1997. IEEE Computer Society Press.
[93] Di Pierro, C. Hankin and H. Wiklicky .Probabilistic Lambda-calculus and Quantitative Program Analysis. Journal of Logic and Computation, 15(2): 159-179, 2005.
[94] Di Pierro and H. Wiklicky. Operator Algebras and the Operational Semantics of Probabilistic Languages. Electronic Notes in Theoretical Computer Science. Volume 161,2006.
[95] Di Pierro and H. Wiklicky. Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. In M.Gabbrielli and F.Pfennning, editor. In Proceedings of PPDP'00,Monteeal, Canada. 2000.
[96] Di Pierro and H. Wiklicky. Linear Structure for concurrent programming languages. In M.Gabbrielli and F.Pfennning, editor. In Proceedings of PPDP'00, Monteeal, Canada. 2001.
[97] Edalat, P.Shunderhauf. Computable banach spaces via domain theory. In Theoretical Computer Science 1999,219(1-2), 169-184.
[98] S. S. Muchnick. Advanced compiler design and implementation. Academic Press, Sept. 1997.
[99] R. Jhala, R. Majumdar, R. G. Xu. Structural Invariants. In Proceedings of the 13th International Static Analysis Symposium, pages 71-87,2006.
[100] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02), pages 234-245,2002.
[101] Chris Lattner and Vikram Adve.LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization, Palo Alto, California, Mar. 2004.
[102] A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,LNCS 1384, pages 151-166, 1998.
[103] G. Necula, Translation validation for an optimizing compiler, In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00),pages 83-94, 2000.
[104]Y.Fang.Translation validation of optimizing compilers.PhD thesis.New York University,Department of Computer Science,2005.
[105]C.Mihai,S.Jha,S.A.Seshia,D.Song,and R.E.Bryant.Semantics-aware malware detection.In Proceedings of the 2005 IEEE Symposium on Security and Privacy,pages 32-46,2005.
[106]S.Lerner,T.Millstein,E.Rice,and C.Chambers.Automated soundness proofs for dataflow analyses and transformations via local rules.In Proceedings of the 32rd ACM SIGPLAN-SIGACT Conference on Principles Of Programming Languages(POPL '05),pages 364-377,Jan.2005.