指令诱发型硬件木马检测技术研究
|
摘要
当前，信息安全的重要性不言而喻，但信息安全的现状却不尽人意，针对信息安全的攻击技术和手段层出不穷，硬件木马的出现更是给信息安全带来了新的威胁。相对于软件恶意代码，硬件木马与系统底层密切相关，具有更强的隐蔽性和更严重的破坏性，开展硬件木马检测技术的研究对于全面保障信息系统的安全至关重要，具有重要的现实意义和理论意义。
本文以指令诱发型硬件木马为研究对象，主要内容和创新点如下：
1.构建一种指令诱发型硬件木马模型。在分析硬件木马特性的基础上，根据Thimbleby木马模型，提出基于Thimbleby方法的硬件木马模型；在此模型的基础上，结合指令诱发型硬件木马的特点，构建指令诱发型硬件木马模型。
2.提出并实现指令诱发型硬件木马的检测技术。根据指令诱发型硬件木马模型，提出基于指令序列覆盖的指令诱发型硬件木马检测思想和相应算法；在深入分析模型检验方法的基础上，提出基于模型检验的指令诱发型硬件木马检测技术，并给出模型生成算法和待验证性质提取方法。实验结果表明，指令诱发型硬件木马检测技术能够有效检测硬件木马。
3.提出基于抽象解释的二进制代码变量区间分析方法。基于抽象解释理论，结合固件二进制代码变量的特点，扩展区间抽象域，定义字级数据区间抽象域和位级数据区间抽象域；分别给出两种区间抽象域上的区间运算方法；提出不同变量区间抽象域间的转换算法；在转换过程中引入区间集的概念，保证运算的精度。实验结果表明基于抽象解释的二进制代码变量区间分析方法相对于传统依次运算方法在效率上有数量级倍数的提高；引入区间集的区间分析方法的运算精度高于不引入区间集的分析方法。
4.提出基于敏感位置识别的状态缩减技术。为有效缓解硬件木马检测过程中的状态爆炸问题，结合固件代码的特点定义了敏感变量和敏感位置，给出敏感位置识别技术；在敏感位置识别过程中，为了提高识别效率，提出结合子过程摘要信息的敏感位置识别算法。实验结果表明，本文所提方法能够有效缩减状态规模，状态规模优化率最大为91.5%，有效缓解了状态爆炸问题。
In the current information age, the information security is of great importance. However, thepresent situation of information security is unsatisfactory, and the attacking technologies emergein an endless stream. Especially hardware Trojan has become a new serious threat to informationsecurity. Being different from traditional malware, hardware Trojan closely depends on systeminfrastructure, which has stronger concealment and destructiveness. Thus, it is critical to carryout the research on detection techniques of hardware Trojan horse. The research on detectiontechniques of hardware Trojan horse has great significance in both theory and practice.
With the study object of instruction-triggered hardware Trojan horse, the main works andcreations are as follows:
1. Instruction-triggered hardware Trojan model is constructed. On the basis of classicalThimbleby Trojan model, hardware Trojan model is constructed combined with characteristics ofhardware Trojan. The analysis of instruction-triggered hardware Trojan is emphasized in thisdissertation. Then based on hardware Trojan model, the model of instruction-triggered hardwareTrojan is proposed.
2. An instruction-triggered hardware Trojan detection technology is proposed. According toinstruction-triggered hardware Trojan model, the instruction-triggered hardware Trojan detectiontechnology based on instruction sequence covering is proposed. By traversing every instructionof firmware and having real-time monitoring on circuit behaviors, whether there is a hardwareTrojan or not could be judged. Model checking traverses all system states in order to find out theillegal behavior, which is in accordance with the thought of hardware Trojan detection based oninstruction sequence covering, and is suitable for the detection on instruction-triggered hardwareTrojan horse. Therefore, the instruction-triggered hardware Trojan detection technology based onmodel checking is proposed. The model generation algorithm and the method to extractproperties which will be validated are presented. Experimental results show thatinstruction-triggered hardware Trojan could be effectively found by the detection technologyproposed in this dissertation.
3. The binary variable interval analysis method based on abstract interpretation is proposed.Combined with characteristics of firmware binary code, the binary variable interval abstractdomain is defined based on the theory of abstract interpretation, which is divided into word-leveldata interval domain and bit-level data interval domain. Interval arithmetic methods under thetwo kinds of interval abstract domain are presented. Conversion algorithms between the two kinds of variable interval domain are proposed. It is demonstrated by experiments that the binaryinterval analysis method based on abstract interpretation can effectively and accuratelydetermine the interval scope of binary variables.
4. The state reduction technology based on sensitive location identification is proposed. Inthe process of detection using model checking, the state explosion is inevitable. In order toovercome this problem, the sensitive variable and the sensitive location are defined based oncharacteristics of firmware. The state reduction technology based on recognition of sensitivelocation is proposed. To improve the recognition efficiency, the sensitive location recognitionmethod combined with the subprocess abstract information is presented. The experimentalresults indicate that this technology can effectively reduce the state scale and relief the stateexplosion problem.
本文以指令诱发型硬件木马为研究对象，主要内容和创新点如下：
1.构建一种指令诱发型硬件木马模型。在分析硬件木马特性的基础上，根据Thimbleby木马模型，提出基于Thimbleby方法的硬件木马模型；在此模型的基础上，结合指令诱发型硬件木马的特点，构建指令诱发型硬件木马模型。
2.提出并实现指令诱发型硬件木马的检测技术。根据指令诱发型硬件木马模型，提出基于指令序列覆盖的指令诱发型硬件木马检测思想和相应算法；在深入分析模型检验方法的基础上，提出基于模型检验的指令诱发型硬件木马检测技术，并给出模型生成算法和待验证性质提取方法。实验结果表明，指令诱发型硬件木马检测技术能够有效检测硬件木马。
3.提出基于抽象解释的二进制代码变量区间分析方法。基于抽象解释理论，结合固件二进制代码变量的特点，扩展区间抽象域，定义字级数据区间抽象域和位级数据区间抽象域；分别给出两种区间抽象域上的区间运算方法；提出不同变量区间抽象域间的转换算法；在转换过程中引入区间集的概念，保证运算的精度。实验结果表明基于抽象解释的二进制代码变量区间分析方法相对于传统依次运算方法在效率上有数量级倍数的提高；引入区间集的区间分析方法的运算精度高于不引入区间集的分析方法。
4.提出基于敏感位置识别的状态缩减技术。为有效缓解硬件木马检测过程中的状态爆炸问题，结合固件代码的特点定义了敏感变量和敏感位置，给出敏感位置识别技术；在敏感位置识别过程中，为了提高识别效率，提出结合子过程摘要信息的敏感位置识别算法。实验结果表明，本文所提方法能够有效缩减状态规模，状态规模优化率最大为91.5%，有效缓解了状态爆炸问题。
In the current information age, the information security is of great importance. However, thepresent situation of information security is unsatisfactory, and the attacking technologies emergein an endless stream. Especially hardware Trojan has become a new serious threat to informationsecurity. Being different from traditional malware, hardware Trojan closely depends on systeminfrastructure, which has stronger concealment and destructiveness. Thus, it is critical to carryout the research on detection techniques of hardware Trojan horse. The research on detectiontechniques of hardware Trojan horse has great significance in both theory and practice.
With the study object of instruction-triggered hardware Trojan horse, the main works andcreations are as follows:
1. Instruction-triggered hardware Trojan model is constructed. On the basis of classicalThimbleby Trojan model, hardware Trojan model is constructed combined with characteristics ofhardware Trojan. The analysis of instruction-triggered hardware Trojan is emphasized in thisdissertation. Then based on hardware Trojan model, the model of instruction-triggered hardwareTrojan is proposed.
2. An instruction-triggered hardware Trojan detection technology is proposed. According toinstruction-triggered hardware Trojan model, the instruction-triggered hardware Trojan detectiontechnology based on instruction sequence covering is proposed. By traversing every instructionof firmware and having real-time monitoring on circuit behaviors, whether there is a hardwareTrojan or not could be judged. Model checking traverses all system states in order to find out theillegal behavior, which is in accordance with the thought of hardware Trojan detection based oninstruction sequence covering, and is suitable for the detection on instruction-triggered hardwareTrojan horse. Therefore, the instruction-triggered hardware Trojan detection technology based onmodel checking is proposed. The model generation algorithm and the method to extractproperties which will be validated are presented. Experimental results show thatinstruction-triggered hardware Trojan could be effectively found by the detection technologyproposed in this dissertation.
3. The binary variable interval analysis method based on abstract interpretation is proposed.Combined with characteristics of firmware binary code, the binary variable interval abstractdomain is defined based on the theory of abstract interpretation, which is divided into word-leveldata interval domain and bit-level data interval domain. Interval arithmetic methods under thetwo kinds of interval abstract domain are presented. Conversion algorithms between the two kinds of variable interval domain are proposed. It is demonstrated by experiments that the binaryinterval analysis method based on abstract interpretation can effectively and accuratelydetermine the interval scope of binary variables.
4. The state reduction technology based on sensitive location identification is proposed. Inthe process of detection using model checking, the state explosion is inevitable. In order toovercome this problem, the sensitive variable and the sensitive location are defined based oncharacteristics of firmware. The state reduction technology based on recognition of sensitivelocation is proposed. To improve the recognition efficiency, the sensitive location recognitionmethod combined with the subprocess abstract information is presented. The experimentalresults indicate that this technology can effectively reduce the state scale and relief the stateexplosion problem.
引文
[1] Chen Z., Ji C. An Information-Theoretic View of Network-Aware Malware Attacks [J]. IEEETransactions on Information Forensics and Securtiy,2009,4(3):530-541.
[2] Ramachandran K., Sikdar B. Dynamics of Malware Spread in Decentralized Peer-to-Peer Networks [J].IEEE Transactions on Dependable and Secure Computing,2011,8(4):617-623.
[3]陈培.基于行为分析的恶意代码识别系统研究与实现[D].成都:电子科技大学,2010.
[4] Lance W. FBI Kills DNSChanger network, but how many will be affected?[EB/OL].:http://news.cnet.com/8301-1009_3-57468436-83/fbi-kills-dnschanger-network-but-how-many-will-be-affected,2012.07.09.
[5] Steve H. Hackers Strike Back: Team GhostShell Claims Massive Data Leak of CIA, Wall Street Info
[EB/OL].: http://betabeat.com/2012/08/hackers-strike-back-team-ghostshell-claims-massive-data-leak-of-cia-wall-street-info,2012.08.28.
[6]张一弛.程序恶意行为识别及其恶意性判定研究[D].郑州:解放军信息工程大学,2012.
[7] Christodorescu M., Jha S. Static analysis of executables to detect malicious patterns [A]. In:Proceedings of the12thUSENIX Security Symposium [C], San Antonio, Argentina,2003:169-186.
[8] Murat Fiskiran A., Ruby B. L. Runtime Execution Monitoring (REM) to Detect and Prevent MaliciousCode Execution [A]. In: Proceedings of the IEEE International Conference on Computer Design [C],Los Alamitos: IEEE Computer Society Press,2004:452-457.
[9] Heng Y., Dawn S., Manuel E., et al. Panorama: caputing system-wide information flow for malwaredetection and analysis [A]. In: Proceedings of the14thACM Conference on Computer andCommunication Security [C], Alexandria, Virginia, USA,2007:116-127.
[10] Willems C., Holz T., Freiling F. Toward Automated Dynamic Malware Analysis Using CWSandbox [J].IEEE Security&Privacy,2007,5(2):32-39.
[11] Porras P. Directions in Network-Based Security Monitoring [J]. IEEE Security&Privacy,2009,7(1):82-85.
[12] Johannes K., Stefan K., Christian S., Helmut V. Proactive Detection of Computer Worms Using ModelChecking [J]. IEEE Transactions on Dependable and Secure Computing,2010,7(4):424-438.
[13] Hungmin S., Hsun W., Kinghang W., Chienming C. A Native APIs Protection Mechanism in the KernelMode against Malicious Code [J]. IEEE Transactions on Computers,2011,60(6):813-823.
[14] Domagoj B., Daniel R., Dawn S. Recognizing malicious software behaviors with tree automatainference [J]. Formal Methods in System Design,2012,41(1):107-128.
[15] Madhu K. S., Subbu R., Ram S. M., Srinivas M. Malware detection using assembly and API callsequences [J]. Journal in Computer Virology,2011,7(2):107-119.
[16]孔德光.结合语义的统计机器学习方法在代码安全中应用研究[D].合肥:中国科学技术大学,2010.
[17] Mojtaba E., Sattar H. ECFGM: enriched control flow graph miner for unknown vicious infected codedetection [J]. Journal in Computer Virology,2012,8(3):99-108.
[18]张波云.计算机病毒智能检测技术研究[D].长沙:国防科技大学,2007.
[19] Brezo F., Sanz B., Laorden C., et al. Using opcode sequences in single-calss learning to detect unknownmalware [J]. Information Seurity, IET,2011,5(4):220-227.
[20]刘豫.基于动态污点传播的恶意代码分析研究[D].北京:中国科学院研究生院,2011.
[21] Domagoj B., Daniel R., Dawn S. Recognizing malicious software behaviors with tree automatainference [J]. Formal Methods in System Design,2012,41(1):107-128.
[22]郑纬民.云计算的挑战与机遇[J].中国计算机学会通讯,2010,7(1):18-22.
[23]刘功申,张月国,孟魁.恶意代码防范[M].北京:高等教育出版社,2010:100-130.
[24] Dawn S., Elaine S., Ian F., Umesh S. Cloud Data Protection for the Masses [J]. IEEE Computer,2012,45(1):39-45.
[25] Sdrjphb.2012年3月最新杀毒软件病毒扫描测试成绩统计[EB/OL].: http://www.shaduruanjian8.com/avtest-2012-03,2012.04.25.
[26] O’Kane P., Sezer S., Mclaughlin K. Obfuscation: The Hidden Malware [J]. IEEE Security&Privacy,2011,9(5):41-47.
[27] Dube Thomas E., Birrer Bobby D., Raines Richard A., et al. Hidering Reverse Engineering: ThinkingOutside the Box [J]. IEEE Security&Privacy,2008,6(2):58-65.
[28] Baliga A., Ganaphaty V., Iftode L. Detecting Kernal-Level Rootkits using Data Structure Invariants [J].IEEE Transactions on Dependable and Secure Computing,2011,8(5):670-684.
[29] Greg H., James B. ROOTKITS: SUBVERING THE WINDOWS KERNEL [M]. New Jersey:Addison-Wesley,2006:147-169.
[30] Hongbo G., Qingbao L., Yu Z., et al. Research on the Working Mechanism of Bootkit [A]. In:Proceedings of8th International Conference on Information Science and Digital Content Technology
[C], Hyatt Regency Jeju, Korea,2012:476-479.
[31]朱瑜,刘胜利,陈嘉勇,高洪博.针对插入攻击型Bootkit的分析及检测[J].小型微型计算机系统,2012,33(7):1462-1467.
[32] Adam W., Simha S. Silencing Hardware Backdoors [A]. In: Proceedings of32ndIEEE Symposium onSecurity and Privacy [C], Berkeley, California, USA,2011:49-63.
[33] Yun S., Qingbao L., Hongbo G., Ping Z. Towards Hardware Trojan: Problem Analysis and TrojanSimulation [A]. In: Proceedings of2ndInternational Conference on Information Engineering andComputer Science [C], Wuhan, China,2010:1-4.
[34] Karri R., Rajendran J., Rosenfeld K., Tehranipoor M. Trustworthy Hardware: Identifying andClassifying Hardware Trojans [J]. Computer,2010,43(10):39-46.
[35] Narasimhan S., Yueh W., Xinmu W., et al. Improving IC Security against Trojan Attacks ThroughIntegration of Security Monitors [J]. IEEE Design&Test of Computers,2012,29(5):37-46.
[36] Tehranipoor M., Farinaz K. A Survey of Hardware Trojan Taxonomy and Detection [J]. IEEE Design&Test of Computers,2010,27(1):10-25.
[37] Salmani H., Teharanipoor M., Plusquelllic J. A Novel Technique for Improving Hardware TrojanDetection and Reducing Trojan Activation Time [J]. IEEE Transactions on Very Large Scale Integration(VLSI) Systems,2012,20(1):112-125.
[38] Tehranipoor M., Salmani H., Xuehui Z., et al. Trustworthy Hardware: Trojan Detection andDesign-for-Trust Challenges [J]. Computer,2011,44(7):66-74.
[39] Love E., Jin Y., Makris Y. Enhancing security via provably trustworthy hardware intellectual property
[A]. In: Proceedings of2011IEEE International Symposium on Hardware-Oriented Security and Trust(HOST)[C], San Diego California, USA,2011:12-17.
[40] Reece Trey R., Limbrick Daniel B., Robinson William H. Design Comparison to Identify MaliciousHardware in External Intellectual Property [A]. In: Proceedings of2011IEEE10thInternationalConference on Trust, Security and Privacy in Computing and Communications [C], Changsha, China,2011:639-646.
[41] Sunar B. Rise of the hardware Trojans [A]. In: Proceedings of2011IEEE17thInternational On-LineTesting Symposium [C], Athens, Greece,2011:138.
[42] Xuehui Z., Tehranipoor M. Case study: Detecting hardware Trojans in third-party digital IP cores [A]. In:Proceedings of2011IEEE International Symposium on Hardware-Oriented Security and Trust (HOST)
[C], San Diego California, USA,2011:67-70.
[43]蒋平,李冬静.信息对抗[M].北京:清华大学出版社,中国人民公安大学出版社,2007:8-11.
[44] Lawrence K. H. Semiconductor Technology and U.S.National Security[R]. Carlisle: U.S. Army WarCollege,2010.
[45] Thomas R. At the Abyss: An Insider’s History of the Cold War [M]. New York: Presidio Press,2005:30-50.
[46] Clarke Edmund M., Khaira manpreet S., Xudong Z. Word level model checking-avoiding the PentiumFDIV error [A]. In: Proceedings of33rdDesign Automation Conference [C], Las Vegas, NV, USA,1996:645-648,.
[47] Graizer V., Naccache D. Alien vs. Quine [J]. IEEE Security&Privacy,2007,5(2):26-31.
[48] Sally A. The Hunt for the Kill Switch [J]. IEEE Spectrum,2008,45(5):34-39.
[49]张洪波.核心芯片安全缺陷仿真平台的研究与实现[D].郑州:解放军信息工程大学,2010.
[50] John H. Implementing and Detecting a PCI Rootkit [A]. In: Proceedings of BlackHat’07[C],Washington D.C., USA,2007.
[51]谢晓东.基于模型检验的固件恶意代码检测技术研究[D].郑州:解放军信息工程大学,2012.
[52] Sergei S., Christopher W. Breakthrough Silicon Discovers Backdoor in Military Chip [A]. In:Proceedings of14thInternational Workshop on Cryptographic Hardware and Embedded Systems [C],Leuven, Belgium,2012:23-40.
[53] Agrawal D., Baktir S., D. Karakoyunlu, et al. Trojan Detection using IC Fingerprinting [A]. In:Proceedings of IEEE Symposium on Security and Privacy [C], Oakland, California, USA,2007:296-310.
[54] King S. T., Tucek J., Cozzie A., et al. Designing and implementing malicious hardware [A]. In:Proceedings of First USENIX Workshop on Large-Scale Exploits and Emergent Threats [C], SanFrancisco, CA, USA,2008.
[55] Matthew H., Murph F., Samuel T. K. Overcoming an Untrusted Computing Base: Detecting andRemoving Malicious Hardware Automatically [A]. In: Proceedings of2010IEEE Symposium onSecurity and Privacy [C], Oakland, CA, USA,2010:159-172.
[56] Jia D., Smith S. A hardware threat modeling concept for trustable integrated circuits [A]. In:Proceedings of IEEE Region5Technical Conference [C], Fayetteville, Arkansas, USA,2007:354-357.
[57] Abhishek D., Gokhan M., Joseph Z., Choudhary A. Detecting/Preventing Information Leakage on theMemory Bus due to Malicious Hardware [A]. In: Proceedings of2010Design, Automation&Test inEurope Conference&Exhibition [C], Dresden, Germany,2010:861-866.
[58] Jin Y., Kupp N., Makris Y. Experiences in Hardware Trojan Design and Implementation [A]. In:Proceedings of IEEE International Workshop on Hardware-Oriented Security and Trust [C], SanFrancisco, California, USA,2009:50-57.
[59] Santos J., Carlos M., Yunsi F. Designing and implementing a Malicious8051processor [A]. In:Proceedings of2012IEEE International Symposium on Defect and Fault Tolerance in VLSI andNanotechnology Systems [C], Austin, TX,2012:63-66.
[60] Sturton C., Hicks M., Wagner D. A., King S. T. Defeating UCI: Building Stealthy and maliciousHardware [A]. In: Proceedings of2011IEEE Symposium on Security and Privacy [C], Berkeley, CA,USA,2011:64-77.
[61] Yier J., Makris Y. Hardware Trojans in Wireless Cryptographic ICs [J]. IEEE Design&Test ofComputers,2010,27(1):26-35.
[62]涂皓.基于旁路分析的硬件木马设计实现[D].长沙:国防科技大学,2010.
[63]邹程,张鹏,邓高明,吴恒旭.基于功率旁路泄露的硬件木马设计[J].计算机工程,2011,37(11):135-137.
[64]刘华锋.基于FPGA的硬件木马测试与检测[D].广州：华南理工大学,2011.
[65]纪曼.中国集成电路产业国际竞争力研究[D].北京：中国人民大学,2010.
[66]中国集成电路产业知识产权年度报告(2012版)[EB/OL]. http://www.csia.net.cn/Article/ShowInfo.asp?InfoID=27466,2012.06.28.
[67] Wang X., Tehranipoor M., Plusquellic J. Detecting Malicious Inclusions in Secure Hardware:Challenges and Solutions [A]. In: Proceedings of IEEE International Workshop Hardware-OrientedSecurity and Trust [C], Anaheim, California, USA,2008:15-19.
[68]任立儒.新情况下的特殊武器——硬件木马[J].中国电子科学研究院学报,2011,6(2):140-142.
[69]郑朝霞,韩玲,李阳，邹雪城.一种木马电路的实现与特征分析[J].微电子学与计算机,2012,29(10):78-80.
[70] Mark R. B., Bradley D. H., Tristan N. SAFER PATH: Security architecture using fragmented executionand replication for protection against trojaned hardware [A]. In: Proceedings of Design, Automation andTest in Europe Conference [C], Dresden, Germany,2012:1000-1005.
[71] Tehranipoor M., Wang C. Introduction to Hardware Security and Trust [M]. New York: Springer-Verlag,2011.
[72] Berk S. Rise of the hardware Trojans [A]. In: Proceedings of IEEE International On-Line TestingSymposium [C],2011:138
[73] Wolff F., Papachristou C. A., et al. Towards Trojan Free Trusted ICs: Problem Analysis and DetectionScheme [A]. In: Proceedings of Design, Automation and Test in Europe Conference [C], Munich,Germany,2008:1362-1365.
[74] Chakraborty R. S., Seetharam N., Swarup B. Hardware Trojan: Threats and emerging solutions [A]. In:Proceedings of the14thIEEE International High Level Design Validation and Test Workshop [C], SanFrancisco, California, USA,2009:166-171.
[75] Hongbo G., Yu Z., Qingbao L., Yu N. The Concept and Taxonomy of Hardware Trojan Horse [A]. In:Proceedings of20103rdInternational Conference on Computer and Electrical Engineering [C],Chengdu, China,2010.
[76] Salmani H., Tehranipoor M. Layout-Aware Switching Activity Localization to Enhance HardwareTrojan Detection [J]. IEEE Transactions on Information Forensics and Security,2012,7(1):76-87.
[77] Sheng W., Kai L., Farinaze K., Potkonjak M. Hardware Trojan horse benchmark via optimal creationand placement of malicious circuitry [A]. In: Proceedings of201249thACM/EDAC/IEEE DesignAutomation Conference [C], San Francisco, CA, USA,2012:90-95.
[78] Chakraborty R., Bhunia S. Security Against Hardware Trojan Attacks Using Key-based DesignObfuscation [J]. Journal of Electronic Testing and Test Application,2011,27(6):767-785.
[79] John V.钟琳译.硬件黑客[J].环球科学,2010,9:18-23.
[80] Chakraborty R. S., Swarup B. Security against Hardware Trojan through a Novel Application of DesignObfuscation [A]. In: Proceedings of2009International Conference on Computer Aided Design [C], SanJose, California, USA,2009.
[81] Lok-Won K., John D. V. A System-on-Chip Bus Architecture for Thwarting Integrated Circuit TrojanHorses [J].IEEE Transactions on Very Large Scale Integration Systems,2011,19(10):1921-1926.
[82] Abramovici M., Bradley P. Integrated Circuit Security–New Threats and Solutions [A]. In:Proceedings of2009Cyber Security and Information Intelligence Research Workshop, Oak Ridge, TN,USA,2009.
[83] Moore T.D., Jarvis J.L. Failure analysis and stress simulation in small multichip BGAs [J]. IEEETransactions on Advanced Packaging,2001,24(5):216-223.
[84]罗宏伟.集成电路芯片安全隐患检测技术[J].半导体技术,2007,32(12):1094-1097.
[85] Sergei S., Anderson R. Optical Fault Induction Attacks [A]. In: Proceedings of4thInternationalWorkshop on Cryptographic Hardware and Embedded Systems [C], Redwood Shores, CA, USA,2002:2-12.
[86] Chakraborty R. S., Wolff F., et al. MERO: A Statistical Approach for Hardware Trojan Detection [A]. In:Proceedings of Workshop on Cryptographic Hardware and Embedded Systems [C], Lausanne,Switzerland,2009,5727:396-410
[87] Chang K.H., Markov I. L., Bertacco V. Fixing Design Errors with Counter-Examples and Resynthesis[J]. IEEE Transactions on Computer-Aided Design,2008,27(1):184-188.
[88] Jha S., Jha S. K. Randomization based probabilistic approach to detect Trojan circuits [A]. In:Proceedings of the11th IEEE High Assurance Systems Engineering Symposium [C], Nanjing, China,2008:117–124.
[89] Pomeranz I., Reddy S. M. A measure of quality for n-detection test sets. IEEE Transactions onComputer,2004,53(11):1497–1503.
[90] Chakraborty R. S., Paul S., Bhunia S. On-demand transparency for improving hardware Trojandetectability [A]. In: Proceedings of the IEEE International Workshop on Hardware-Oriented Securityand Trust [C], Anaheim, California, USA,2008:48–50.
[91] Min L., Davoodi A., Tehranipoor M. A sensor-assisted self-authentication framework for hardwareTrojan detection [A]. In: Proceedings of Design, Automation&Test in Europe Conference&Exhibition
[C], Dresden, Germany,2012:1331-1336.
[92] Narasimhan S., Xinmu W., Dongdong D., et al. TeSR: A robust Temporal Self-Referencing approach forHardware Trojan detection [A]. In: Proceedings of2011IEEE International Symposium onHardware-Oriented Security and Trust [C], San Diego, CA, USA,2011:71-74.
[93] Salmani H., Tehranipoor M., Plusquellic J. A Novel Technique for Improving Hardware TrojanDetection and Reducing Trojan Activation Time [J]. IEEE Transactions on Very Large Scale Integration(VLSI) Systems,2012,20(1):112-125.
[94] Narasimhan S., Dongdong D., Chakraborty R., et al. Multiple-Parameter Side-Channel Analysis: ANon-Invasive Hardware Trojan Detection Approach [A]. In: Proceedings of2010IEEE InternationalSymposium on Hardware-Oriented Security and Trust [C], Anaheim, CA, USA,2010:13-18.
[95] Xiaoxiao W., Salmani H., Tehranipoor M. Plusquellic J. Hardware Trojan Detection and Isolation UsingCurrent Integration and Localized Current Analysis [A]. In: Proceedings of IEEE InternationalSymposium on Defect and Fault Tolerance of VLSI System [C], Boston,MA, USA,2008:87-95.
[96] Rad Reza M. P., Plusquellic J., Tehranipoor M. A Sensitivity Analysis of Power Signal Methods forDetecting Hardware Trojans under Real Process and Environmental Conditions [J]. IEEE Transactionson Very Large Scale Integration (VLSI) Systems,2010,18(12):1735-1744.
[97] Wei S., Potkonjak M. Integrated circuit security techniques using variable supply voltage [A]. In:Proceedings of Design Automation Conference [C], San Diego, CA, USA,2011:248-253.
[98] Lamech C., Rad Reza M. P., Tehranipoor M., Plusquellic J. An Experimental Analysis of Power andDelay Signal-to-Noise Requirements for Detecting Trojans and Methods for Achieving the RequiredDetection Sensitivities [J]. IEEE Transactions on Information Forensics and Security,2011,6(3):1170-1179.
[99] Rad Reza M. P., Xiaoxiao W., Tehranipoor M., et al. Power supply signal calibration techniques forimproving detection resolution to hardware Trojans [A]. In: Proceedings of IEEE/ACM InternationalConference on Computer-Aided Design [C], San Jose, CA, USA,2008:632-639.
[100] Banga M., Hsiao M. A region based approach for the identification of hardware Trojans [A]. In:Proceedings of2008IEEE International Workshop on Hardware-Oriented Security and Trust [C],Anaheim, CA, USA,2008:40-47.
[101] Li J., Lach J．At-speed delay characterization for IC authentication and Trojan horse detection [A]. In:Proceedings of2008IEEE International Workshop on Hardware-Oriented Security and Trust [C],Anaheim，CA, USA,2008:8-14.
[102] Wenchao L., Wasson Z., Seshia Sanjit A. Reverse engineering circuits using behavioral pattern mining
[A]. In: Proceedings of2012IEEE International Symposium on Hardwware-Oriented Security andTrust, San Francisco, CA, USA,2012:83-88.
[103] Shrestha G., Hsiao M. S. Ensuring trust of third-party hardware design with constrained sequentialequivalence checking [A]. In: Proceedings of2012IEEE Conference on Technologies for HomelandSecurity, Waltham, MA, USA2012:7-12.
[104] Smith Scott C., Jia D. Detecting Malicious Logic through Structural Checking [A]. In: Proceedings of2007IEEE Region5Technical Conference [C], Fayetteville, AR, USA,2007:217-222.
[105]李晓维,吕涛,李华伟,李光辉著.数字集成电路设计验证[M].北京:科学出版社,2010:7-10.
[106] William K.L. Hardware Design Verification: Simulation and Formal Method-Based Approaches [M].Englewood Cliffs: Prentice Hall,2005.
[107] Lucas P. Symbolic Diagnosis and its Formalisation [J]. The Knowledge Engineering Review,1997,12(2):109-146.
[108] Forbus K.D., Kleer J. Building Problem Solvers [M]. Massachusetts: The MIT Press,1993:74-98.
[109]黄杰.分布构件系统故障诊断技术研究[D].长沙:国防科技大学,2005.
[110] Raymond R. A Theory of diagnosis from first principles [J]. Artificial Intelligence,1987,32(1):57-95.
[111] Cristina C. Reverse Compilation Techniques [D]. Queensland: Queensland University of Technology,1994.
[112] Benjamin S., Saumya D., Gregory A. Disassembly of executable code revisited [A]. In: Proceedings ofWorking Conference on Reverse Engineering [C], Richmond, Virginia, USA,2002:45-54.
[113] Bastian S. Model checking of software for microcontrollers [D]. Aachen: RWTH Aachen University,2008.
[114] Cooprider N. Data-flow analysis for interrupt-driven microeontroller software [D]. Salt Lake City: theUniversity of Utah,2008.
[115]霍玮,于洪涛,冯晓兵,张兆庆.静态检测中断驱动程序的数据竞争[J].计算机研究与发展,2011,48(12):2290-2299.
[116] Kinder J., Zuleger F., Veith H. An Abstract Interpretation-Based Framework for Control FlowReconstruction from Binaries [A]. In: Proceedings of10thInternational Conference on Verification,Model Checking, and Abstract Interpretation [C], Savannah, GA, USA,2009:214-228.
[117] Bardin S., Herrmann P., V′edrine F. Refinement-based CFG Reconstruction from UnstructuredPrograms [A]. In: Proceedings of12thInternational Conference on Verification, Model Checking, andAbstract Interpretation [C], Austin, Texas, USA,2011:54-69.
[118] Thomas R., J rg B. Precise control flow reconstruction using boolean logic [A]. In: Proceedings of the11thInternational Conference/Workshop on Embedded Software [C], Taipei, Taiwan, China,2011:117-126.
[119]胡刚.固件代码逆向分析关键技术研究[D].郑州：解放军信息工程大学,2011.
[120] Cohen F. Computer viruses: theory and experiments [J]. Computers&Security,1987,6(1):22-35.
[121] Cohen F. Computational Aspects of Computer Viruses [J]. Computers&Security,1989,8(4):325-344.
[122] Adleman L. M. An Abstract Theory of Computer Viruses [A]. In: Proceedings of InternationalCryptology Conference [C], Santa Barbara, California, USA,1988,354-374.
[123] Thimbleby H., Anderson S., Cairns P. A framework for modelling trojans and computer virus infection[J]. The Computer Journal,1998,41(7):444-458.
[124]张新宇,卿斯汉,马恒太,张楠,孙淑华,蒋建春.特洛伊木马隐藏技术研究,通信学报,2004,25(7):153-159.
[125] Hongbo G., Qingbao L., Yu Z., et al. Code-controlled hardware Trojan horse [A]. In: Proceedings of the3th International Conference on Information Computing and Applications [C], Chengde, China,2012:171-178.
[126] Hongbo G., Qingbao L., Wei W., Yu Z. Research on Detection Technique for C2HTH Based on ModelChecking [J]. International Journal of Advancements in Computing Technology,2012,4(23):814-820.
[127] Baier C., Katoen J.P. Principles of Model Checking [M]. Cambridge: The MIT Press,2008.
[128] Michael H., Mark R. Logic in Computer Science: Modelling and Reasoning about Systems, SecondEdition [M]. Cambridge: Cambridge University Press,2004:193-232.
[129] Edmund M. C., Orna G., Doron A. P. Model Checking [M]. Cambridge: The MIT Press,2000.
[130]林梦香,吴国仕.程序模型检查器综述[J].计算机科学,2009,36(4):12-15.
[131] Bastian S., Stefan K. Model checking C source code for embedded systems [J]. International Journal onSoftware Tools for Technology Transfer,2009,11(3):187-202.
[132]刘万伟.扩展时序逻辑的推理及符号化模型检验技术[D].长沙:国防科技大学,2009.
[133]张振方.基于模型检验的软件分析方法研究[D].武汉:华中师范大学,2009.
[134] Alessandro C., Edmund Clarke C., et al. NUSMV: a new symbolic model checker [J]. InternationalJournal on Software Tools for Technology Transfer (STTT),2000,2(3):410-425.
[135] Gogul B. WYSINWYX: what you see is not what you execute [J].ACM Transactions on ProgrammingLanguages and Systems (TOPLAS),2010,32(6):1-84.
[136] Thomas W.R., Junghee L., Aditya V.T., et al. There’s Plenty of Room at the Bottom: Analyzing andVerifying Machine Code [A]. In: Proceedings of the22nd International Conference on Computer AidedVerification [C], Edinburgh, UK,2010:41-56.
[137] Bastian S. Model checking of software for microcontrollers [J]. ACM Transactions on EmbeddedComputing Systems (TECS).2010,9(4):1-27.
[138] MacKenzie I. S. The8051Microcontroller, Third Edition [M]. Englewood Cliffs: Prentice Hall,1998:19-21.
[139] Muhammad A. M., Janice Gillispie M., Mckinlay R. D. The8051Microcontroller and EmbeddedSystems: Using Assembly and C, Second Edition [M]. Englewood Cliffs: Pearson/Prentice Hall,2006.
[140] Bastian S., Jorg B., Stefan K. Application of static analyses for state-space reduction to themicrocontroller binary code [J]. Science of Computer Programming,2011,76(2):100-118.
[141] Alfred V. A., Monica S. L., Ravi S., Jeffrey D. Compilers-Principles, Techniques, and Tools, SecondEdition [M]. New Jersey: Addison-Wesley,2007.
[142] Ramon E. M., Baker Kearfott R., Michael J. Introduction to interval analysis [M]. Philadelphia: Societyfor Industrial and Applied Mathematics,2009:7-49.
[143] Dongrui W., Mendel J. M., Coupland S. Enhanced interval approach for encoding words into intervaltype-2fuzzy sets and its convergence analysis [J]. IEEE Transactions on Fuzzy Systems,2012,20(3):499-513.
[144]王雅文,姚欣洪,宫云战,杨朝红.一种基于代码静态分析的缓冲区溢出检测算法[J].计算机研究与发展,2012,49(4):839-845.
[145] Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis [M]. Berlin: Springer-Verlag,1999,200-300.
[146] Cousot P. Abstract interpretation based formal methods and future challenges [A]. In: Proceeding ofInformatics-10Years Back,10Years Ahead, London,2001:138-156.
[147]姬孟洛,王怀民,李梦君,董威,齐治昌.一种基于抽象解释和通用单调数据流框架的值范围分析方法[J].计算机研究与发展,2006,43(11):2020-2026.
[148]王雅文,宫云战,肖庆,杨朝红.基于抽象解释的变量值范围分析及应用[J].电子学报,2011,39(2):296-303.
[149] Cousot P., Cousot R. Abstract Interpretation: A unified lattice model for static analysis of programs byconstruction or approximation of fixpoints [A]. In: Proceedings of the4th ACM SIGACT-SIGPLANSymposium on Principles of Programming Languages, New York,1977:238-252.
[150]李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术[J].软件学报,2008,19(1):17-26.
[151] Patrick C., Radhia C., Laurent M.. Theories, solvers and static analysis by abstract interpretation [J].Journal of the ACM,2012,59(6):31.
[152] Julien B., Patrick C., Radhia C., et al. Static analysis by abstract interpretation of embedded criticalsoftware [J]. ACM SIGSOFT Software Engineering Notes,2011,36(1):1-8.
[153] Agostino C., Matteo Z. Widening and narrowing operators for abstract interpretation [J]. ComputerLanguages, Systems&Structures,2011,37(1):24-42.
[154] Thomas R., Jorg B., Martin H., et al. Past time LTL runtime verification for microcontroller binary code
[A]. In: Proceedings of the16thInternational Conference on Formal Methods for Industrial CriticalSystems [C], Trento, Italy,2011:37-51.
[155] Thomas N., Bastian S. Delayed nondeterminism in model checking embedded systems assembly code
[A]. In: Proceedings of the3rdInternational Haifa Verification Conference on Hardware and software:Verification and Testing [C], Haifa, Israel,2008:185-201.
[156] Bruce W., John C., Wolfgang R. Comprehensive Functional Verification: The Complete Industry Cycle
[M]. San Francisco: Morgan Kaufmann Publishers,2005.
[157]贾仰理,李舟军,邢建英,等.基于模型检验的构件验证技术研究进展[J].计算机研究与发展,2011,48(6):913-922.
[158] Nocco S., Quer S. A Novel SAT-Based Approach to the Task Graph Cost-Optimal Scheduling Problem[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2010,29(12):2027-2040.
[159] Iyer S., Sahoo D., Emerson E.A., Jain J. On partitioning and symbolic model checking [J]. IEEETransactios on Computer-Aided Design of Integrated Circuits and Systems,2006,25(5):780-788.
[160] Alessandro C., Alberto G. Software model checking via IC3[A]. In: Proceedings of the24thInternational Conference on Computer Aided Verification, Berkeley, CA, USA,2012:277-293.
[161]虞蕾,赵宗涛. PSL的有界模型检验[J].电子学报，2009,37(3)：614-621.
[162] Cordeiro L., Fischer B., Marques Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-CSoftware [J]. IEEE Transactions on Software Engineering,2012,38(4):957-974.
[163] Cormac F., Patrice G. Dynamic partial-order reduction for model checking software [A]. In:Proceedingsof the32ndACM SIGPLAN-SIGACT symposium on Principles of programming languages [C], LongBeach, California, USA,2005:110-121.
[164] Gerard J. H. On-The-Fly Model Checking [J]. ACM Computing Surveys,1996,28(4):120.
[165] Roberto S., Stefano T., et al. Symbolic system, explicit properties: on hybrid approaches for LTLsymbolic model checking [J]. International Journal on Software Tools for Technology Transfer (STTT),2010,13(4):319-335.
[166]李兴锋,张新常,杨美红,等.基于SPIN的模块化模型检测方法研究[J].电子与信息学报,2011,33(4):902-907.
[167] Karen Y., Orna G. Static analysis for state-space reductions preserving temporal logics [J]. FormalMethods in System Design,2004,25(1):67-96.
[168] Moonzoo K., Yunho K., Hotae K. A comparative study of software model checkers as unit testing tools:an industrial case study [J]. IEEE Transactions on Software Engineering,2011,37(2):146-160.
[169]崔宝江,梁晓兵,王禹,王建新.基于回溯与引导的关键代码区域覆盖的二进制程序测试技术研究[J].电子与信息学报,2012,34(1):108-114.
[170] Weiser M. Program Slicing [J], IEEE Transations on Software Engineering,1984,10(4):352-357.
[171]李必信.程序切片技术及其应用[M].北京:科学出版社,2006.
[172] John H., Matthew B. D., Hongjun Z. Slicing software for model construction [J]. Higher-Order andSymbolic Computation,2000,13(4):315-353.
[173] Sen A., Garg V. K. Formal Verification of Simulation Traces Using Computation Slicing [J]. IEEETransactions on Computers,2007,56(4):511-527.
[174] Mittal N., Sen A., Garg V. K. Solving Computation Slicing Using Predicate Detection [J]. IEEETransactions on Parallel and Distributed Systems,2007,18(12):1700-1713.
[2] Ramachandran K., Sikdar B. Dynamics of Malware Spread in Decentralized Peer-to-Peer Networks [J].IEEE Transactions on Dependable and Secure Computing,2011,8(4):617-623.
[3]陈培.基于行为分析的恶意代码识别系统研究与实现[D].成都:电子科技大学,2010.
[4] Lance W. FBI Kills DNSChanger network, but how many will be affected?[EB/OL].:http://news.cnet.com/8301-1009_3-57468436-83/fbi-kills-dnschanger-network-but-how-many-will-be-affected,2012.07.09.
[5] Steve H. Hackers Strike Back: Team GhostShell Claims Massive Data Leak of CIA, Wall Street Info
[EB/OL].: http://betabeat.com/2012/08/hackers-strike-back-team-ghostshell-claims-massive-data-leak-of-cia-wall-street-info,2012.08.28.
[6]张一弛.程序恶意行为识别及其恶意性判定研究[D].郑州:解放军信息工程大学,2012.
[7] Christodorescu M., Jha S. Static analysis of executables to detect malicious patterns [A]. In:Proceedings of the12thUSENIX Security Symposium [C], San Antonio, Argentina,2003:169-186.
[8] Murat Fiskiran A., Ruby B. L. Runtime Execution Monitoring (REM) to Detect and Prevent MaliciousCode Execution [A]. In: Proceedings of the IEEE International Conference on Computer Design [C],Los Alamitos: IEEE Computer Society Press,2004:452-457.
[9] Heng Y., Dawn S., Manuel E., et al. Panorama: caputing system-wide information flow for malwaredetection and analysis [A]. In: Proceedings of the14thACM Conference on Computer andCommunication Security [C], Alexandria, Virginia, USA,2007:116-127.
[10] Willems C., Holz T., Freiling F. Toward Automated Dynamic Malware Analysis Using CWSandbox [J].IEEE Security&Privacy,2007,5(2):32-39.
[11] Porras P. Directions in Network-Based Security Monitoring [J]. IEEE Security&Privacy,2009,7(1):82-85.
[12] Johannes K., Stefan K., Christian S., Helmut V. Proactive Detection of Computer Worms Using ModelChecking [J]. IEEE Transactions on Dependable and Secure Computing,2010,7(4):424-438.
[13] Hungmin S., Hsun W., Kinghang W., Chienming C. A Native APIs Protection Mechanism in the KernelMode against Malicious Code [J]. IEEE Transactions on Computers,2011,60(6):813-823.
[14] Domagoj B., Daniel R., Dawn S. Recognizing malicious software behaviors with tree automatainference [J]. Formal Methods in System Design,2012,41(1):107-128.
[15] Madhu K. S., Subbu R., Ram S. M., Srinivas M. Malware detection using assembly and API callsequences [J]. Journal in Computer Virology,2011,7(2):107-119.
[16]孔德光.结合语义的统计机器学习方法在代码安全中应用研究[D].合肥:中国科学技术大学,2010.
[17] Mojtaba E., Sattar H. ECFGM: enriched control flow graph miner for unknown vicious infected codedetection [J]. Journal in Computer Virology,2012,8(3):99-108.
[18]张波云.计算机病毒智能检测技术研究[D].长沙:国防科技大学,2007.
[19] Brezo F., Sanz B., Laorden C., et al. Using opcode sequences in single-calss learning to detect unknownmalware [J]. Information Seurity, IET,2011,5(4):220-227.
[20]刘豫.基于动态污点传播的恶意代码分析研究[D].北京:中国科学院研究生院,2011.
[21] Domagoj B., Daniel R., Dawn S. Recognizing malicious software behaviors with tree automatainference [J]. Formal Methods in System Design,2012,41(1):107-128.
[22]郑纬民.云计算的挑战与机遇[J].中国计算机学会通讯,2010,7(1):18-22.
[23]刘功申,张月国,孟魁.恶意代码防范[M].北京:高等教育出版社,2010:100-130.
[24] Dawn S., Elaine S., Ian F., Umesh S. Cloud Data Protection for the Masses [J]. IEEE Computer,2012,45(1):39-45.
[25] Sdrjphb.2012年3月最新杀毒软件病毒扫描测试成绩统计[EB/OL].: http://www.shaduruanjian8.com/avtest-2012-03,2012.04.25.
[26] O’Kane P., Sezer S., Mclaughlin K. Obfuscation: The Hidden Malware [J]. IEEE Security&Privacy,2011,9(5):41-47.
[27] Dube Thomas E., Birrer Bobby D., Raines Richard A., et al. Hidering Reverse Engineering: ThinkingOutside the Box [J]. IEEE Security&Privacy,2008,6(2):58-65.
[28] Baliga A., Ganaphaty V., Iftode L. Detecting Kernal-Level Rootkits using Data Structure Invariants [J].IEEE Transactions on Dependable and Secure Computing,2011,8(5):670-684.
[29] Greg H., James B. ROOTKITS: SUBVERING THE WINDOWS KERNEL [M]. New Jersey:Addison-Wesley,2006:147-169.
[30] Hongbo G., Qingbao L., Yu Z., et al. Research on the Working Mechanism of Bootkit [A]. In:Proceedings of8th International Conference on Information Science and Digital Content Technology
[C], Hyatt Regency Jeju, Korea,2012:476-479.
[31]朱瑜,刘胜利,陈嘉勇,高洪博.针对插入攻击型Bootkit的分析及检测[J].小型微型计算机系统,2012,33(7):1462-1467.
[32] Adam W., Simha S. Silencing Hardware Backdoors [A]. In: Proceedings of32ndIEEE Symposium onSecurity and Privacy [C], Berkeley, California, USA,2011:49-63.
[33] Yun S., Qingbao L., Hongbo G., Ping Z. Towards Hardware Trojan: Problem Analysis and TrojanSimulation [A]. In: Proceedings of2ndInternational Conference on Information Engineering andComputer Science [C], Wuhan, China,2010:1-4.
[34] Karri R., Rajendran J., Rosenfeld K., Tehranipoor M. Trustworthy Hardware: Identifying andClassifying Hardware Trojans [J]. Computer,2010,43(10):39-46.
[35] Narasimhan S., Yueh W., Xinmu W., et al. Improving IC Security against Trojan Attacks ThroughIntegration of Security Monitors [J]. IEEE Design&Test of Computers,2012,29(5):37-46.
[36] Tehranipoor M., Farinaz K. A Survey of Hardware Trojan Taxonomy and Detection [J]. IEEE Design&Test of Computers,2010,27(1):10-25.
[37] Salmani H., Teharanipoor M., Plusquelllic J. A Novel Technique for Improving Hardware TrojanDetection and Reducing Trojan Activation Time [J]. IEEE Transactions on Very Large Scale Integration(VLSI) Systems,2012,20(1):112-125.
[38] Tehranipoor M., Salmani H., Xuehui Z., et al. Trustworthy Hardware: Trojan Detection andDesign-for-Trust Challenges [J]. Computer,2011,44(7):66-74.
[39] Love E., Jin Y., Makris Y. Enhancing security via provably trustworthy hardware intellectual property
[A]. In: Proceedings of2011IEEE International Symposium on Hardware-Oriented Security and Trust(HOST)[C], San Diego California, USA,2011:12-17.
[40] Reece Trey R., Limbrick Daniel B., Robinson William H. Design Comparison to Identify MaliciousHardware in External Intellectual Property [A]. In: Proceedings of2011IEEE10thInternationalConference on Trust, Security and Privacy in Computing and Communications [C], Changsha, China,2011:639-646.
[41] Sunar B. Rise of the hardware Trojans [A]. In: Proceedings of2011IEEE17thInternational On-LineTesting Symposium [C], Athens, Greece,2011:138.
[42] Xuehui Z., Tehranipoor M. Case study: Detecting hardware Trojans in third-party digital IP cores [A]. In:Proceedings of2011IEEE International Symposium on Hardware-Oriented Security and Trust (HOST)
[C], San Diego California, USA,2011:67-70.
[43]蒋平,李冬静.信息对抗[M].北京:清华大学出版社,中国人民公安大学出版社,2007:8-11.
[44] Lawrence K. H. Semiconductor Technology and U.S.National Security[R]. Carlisle: U.S. Army WarCollege,2010.
[45] Thomas R. At the Abyss: An Insider’s History of the Cold War [M]. New York: Presidio Press,2005:30-50.
[46] Clarke Edmund M., Khaira manpreet S., Xudong Z. Word level model checking-avoiding the PentiumFDIV error [A]. In: Proceedings of33rdDesign Automation Conference [C], Las Vegas, NV, USA,1996:645-648,.
[47] Graizer V., Naccache D. Alien vs. Quine [J]. IEEE Security&Privacy,2007,5(2):26-31.
[48] Sally A. The Hunt for the Kill Switch [J]. IEEE Spectrum,2008,45(5):34-39.
[49]张洪波.核心芯片安全缺陷仿真平台的研究与实现[D].郑州:解放军信息工程大学,2010.
[50] John H. Implementing and Detecting a PCI Rootkit [A]. In: Proceedings of BlackHat’07[C],Washington D.C., USA,2007.
[51]谢晓东.基于模型检验的固件恶意代码检测技术研究[D].郑州:解放军信息工程大学,2012.
[52] Sergei S., Christopher W. Breakthrough Silicon Discovers Backdoor in Military Chip [A]. In:Proceedings of14thInternational Workshop on Cryptographic Hardware and Embedded Systems [C],Leuven, Belgium,2012:23-40.
[53] Agrawal D., Baktir S., D. Karakoyunlu, et al. Trojan Detection using IC Fingerprinting [A]. In:Proceedings of IEEE Symposium on Security and Privacy [C], Oakland, California, USA,2007:296-310.
[54] King S. T., Tucek J., Cozzie A., et al. Designing and implementing malicious hardware [A]. In:Proceedings of First USENIX Workshop on Large-Scale Exploits and Emergent Threats [C], SanFrancisco, CA, USA,2008.
[55] Matthew H., Murph F., Samuel T. K. Overcoming an Untrusted Computing Base: Detecting andRemoving Malicious Hardware Automatically [A]. In: Proceedings of2010IEEE Symposium onSecurity and Privacy [C], Oakland, CA, USA,2010:159-172.
[56] Jia D., Smith S. A hardware threat modeling concept for trustable integrated circuits [A]. In:Proceedings of IEEE Region5Technical Conference [C], Fayetteville, Arkansas, USA,2007:354-357.
[57] Abhishek D., Gokhan M., Joseph Z., Choudhary A. Detecting/Preventing Information Leakage on theMemory Bus due to Malicious Hardware [A]. In: Proceedings of2010Design, Automation&Test inEurope Conference&Exhibition [C], Dresden, Germany,2010:861-866.
[58] Jin Y., Kupp N., Makris Y. Experiences in Hardware Trojan Design and Implementation [A]. In:Proceedings of IEEE International Workshop on Hardware-Oriented Security and Trust [C], SanFrancisco, California, USA,2009:50-57.
[59] Santos J., Carlos M., Yunsi F. Designing and implementing a Malicious8051processor [A]. In:Proceedings of2012IEEE International Symposium on Defect and Fault Tolerance in VLSI andNanotechnology Systems [C], Austin, TX,2012:63-66.
[60] Sturton C., Hicks M., Wagner D. A., King S. T. Defeating UCI: Building Stealthy and maliciousHardware [A]. In: Proceedings of2011IEEE Symposium on Security and Privacy [C], Berkeley, CA,USA,2011:64-77.
[61] Yier J., Makris Y. Hardware Trojans in Wireless Cryptographic ICs [J]. IEEE Design&Test ofComputers,2010,27(1):26-35.
[62]涂皓.基于旁路分析的硬件木马设计实现[D].长沙:国防科技大学,2010.
[63]邹程,张鹏,邓高明,吴恒旭.基于功率旁路泄露的硬件木马设计[J].计算机工程,2011,37(11):135-137.
[64]刘华锋.基于FPGA的硬件木马测试与检测[D].广州：华南理工大学,2011.
[65]纪曼.中国集成电路产业国际竞争力研究[D].北京：中国人民大学,2010.
[66]中国集成电路产业知识产权年度报告(2012版)[EB/OL]. http://www.csia.net.cn/Article/ShowInfo.asp?InfoID=27466,2012.06.28.
[67] Wang X., Tehranipoor M., Plusquellic J. Detecting Malicious Inclusions in Secure Hardware:Challenges and Solutions [A]. In: Proceedings of IEEE International Workshop Hardware-OrientedSecurity and Trust [C], Anaheim, California, USA,2008:15-19.
[68]任立儒.新情况下的特殊武器——硬件木马[J].中国电子科学研究院学报,2011,6(2):140-142.
[69]郑朝霞,韩玲,李阳，邹雪城.一种木马电路的实现与特征分析[J].微电子学与计算机,2012,29(10):78-80.
[70] Mark R. B., Bradley D. H., Tristan N. SAFER PATH: Security architecture using fragmented executionand replication for protection against trojaned hardware [A]. In: Proceedings of Design, Automation andTest in Europe Conference [C], Dresden, Germany,2012:1000-1005.
[71] Tehranipoor M., Wang C. Introduction to Hardware Security and Trust [M]. New York: Springer-Verlag,2011.
[72] Berk S. Rise of the hardware Trojans [A]. In: Proceedings of IEEE International On-Line TestingSymposium [C],2011:138
[73] Wolff F., Papachristou C. A., et al. Towards Trojan Free Trusted ICs: Problem Analysis and DetectionScheme [A]. In: Proceedings of Design, Automation and Test in Europe Conference [C], Munich,Germany,2008:1362-1365.
[74] Chakraborty R. S., Seetharam N., Swarup B. Hardware Trojan: Threats and emerging solutions [A]. In:Proceedings of the14thIEEE International High Level Design Validation and Test Workshop [C], SanFrancisco, California, USA,2009:166-171.
[75] Hongbo G., Yu Z., Qingbao L., Yu N. The Concept and Taxonomy of Hardware Trojan Horse [A]. In:Proceedings of20103rdInternational Conference on Computer and Electrical Engineering [C],Chengdu, China,2010.
[76] Salmani H., Tehranipoor M. Layout-Aware Switching Activity Localization to Enhance HardwareTrojan Detection [J]. IEEE Transactions on Information Forensics and Security,2012,7(1):76-87.
[77] Sheng W., Kai L., Farinaze K., Potkonjak M. Hardware Trojan horse benchmark via optimal creationand placement of malicious circuitry [A]. In: Proceedings of201249thACM/EDAC/IEEE DesignAutomation Conference [C], San Francisco, CA, USA,2012:90-95.
[78] Chakraborty R., Bhunia S. Security Against Hardware Trojan Attacks Using Key-based DesignObfuscation [J]. Journal of Electronic Testing and Test Application,2011,27(6):767-785.
[79] John V.钟琳译.硬件黑客[J].环球科学,2010,9:18-23.
[80] Chakraborty R. S., Swarup B. Security against Hardware Trojan through a Novel Application of DesignObfuscation [A]. In: Proceedings of2009International Conference on Computer Aided Design [C], SanJose, California, USA,2009.
[81] Lok-Won K., John D. V. A System-on-Chip Bus Architecture for Thwarting Integrated Circuit TrojanHorses [J].IEEE Transactions on Very Large Scale Integration Systems,2011,19(10):1921-1926.
[82] Abramovici M., Bradley P. Integrated Circuit Security–New Threats and Solutions [A]. In:Proceedings of2009Cyber Security and Information Intelligence Research Workshop, Oak Ridge, TN,USA,2009.
[83] Moore T.D., Jarvis J.L. Failure analysis and stress simulation in small multichip BGAs [J]. IEEETransactions on Advanced Packaging,2001,24(5):216-223.
[84]罗宏伟.集成电路芯片安全隐患检测技术[J].半导体技术,2007,32(12):1094-1097.
[85] Sergei S., Anderson R. Optical Fault Induction Attacks [A]. In: Proceedings of4thInternationalWorkshop on Cryptographic Hardware and Embedded Systems [C], Redwood Shores, CA, USA,2002:2-12.
[86] Chakraborty R. S., Wolff F., et al. MERO: A Statistical Approach for Hardware Trojan Detection [A]. In:Proceedings of Workshop on Cryptographic Hardware and Embedded Systems [C], Lausanne,Switzerland,2009,5727:396-410
[87] Chang K.H., Markov I. L., Bertacco V. Fixing Design Errors with Counter-Examples and Resynthesis[J]. IEEE Transactions on Computer-Aided Design,2008,27(1):184-188.
[88] Jha S., Jha S. K. Randomization based probabilistic approach to detect Trojan circuits [A]. In:Proceedings of the11th IEEE High Assurance Systems Engineering Symposium [C], Nanjing, China,2008:117–124.
[89] Pomeranz I., Reddy S. M. A measure of quality for n-detection test sets. IEEE Transactions onComputer,2004,53(11):1497–1503.
[90] Chakraborty R. S., Paul S., Bhunia S. On-demand transparency for improving hardware Trojandetectability [A]. In: Proceedings of the IEEE International Workshop on Hardware-Oriented Securityand Trust [C], Anaheim, California, USA,2008:48–50.
[91] Min L., Davoodi A., Tehranipoor M. A sensor-assisted self-authentication framework for hardwareTrojan detection [A]. In: Proceedings of Design, Automation&Test in Europe Conference&Exhibition
[C], Dresden, Germany,2012:1331-1336.
[92] Narasimhan S., Xinmu W., Dongdong D., et al. TeSR: A robust Temporal Self-Referencing approach forHardware Trojan detection [A]. In: Proceedings of2011IEEE International Symposium onHardware-Oriented Security and Trust [C], San Diego, CA, USA,2011:71-74.
[93] Salmani H., Tehranipoor M., Plusquellic J. A Novel Technique for Improving Hardware TrojanDetection and Reducing Trojan Activation Time [J]. IEEE Transactions on Very Large Scale Integration(VLSI) Systems,2012,20(1):112-125.
[94] Narasimhan S., Dongdong D., Chakraborty R., et al. Multiple-Parameter Side-Channel Analysis: ANon-Invasive Hardware Trojan Detection Approach [A]. In: Proceedings of2010IEEE InternationalSymposium on Hardware-Oriented Security and Trust [C], Anaheim, CA, USA,2010:13-18.
[95] Xiaoxiao W., Salmani H., Tehranipoor M. Plusquellic J. Hardware Trojan Detection and Isolation UsingCurrent Integration and Localized Current Analysis [A]. In: Proceedings of IEEE InternationalSymposium on Defect and Fault Tolerance of VLSI System [C], Boston,MA, USA,2008:87-95.
[96] Rad Reza M. P., Plusquellic J., Tehranipoor M. A Sensitivity Analysis of Power Signal Methods forDetecting Hardware Trojans under Real Process and Environmental Conditions [J]. IEEE Transactionson Very Large Scale Integration (VLSI) Systems,2010,18(12):1735-1744.
[97] Wei S., Potkonjak M. Integrated circuit security techniques using variable supply voltage [A]. In:Proceedings of Design Automation Conference [C], San Diego, CA, USA,2011:248-253.
[98] Lamech C., Rad Reza M. P., Tehranipoor M., Plusquellic J. An Experimental Analysis of Power andDelay Signal-to-Noise Requirements for Detecting Trojans and Methods for Achieving the RequiredDetection Sensitivities [J]. IEEE Transactions on Information Forensics and Security,2011,6(3):1170-1179.
[99] Rad Reza M. P., Xiaoxiao W., Tehranipoor M., et al. Power supply signal calibration techniques forimproving detection resolution to hardware Trojans [A]. In: Proceedings of IEEE/ACM InternationalConference on Computer-Aided Design [C], San Jose, CA, USA,2008:632-639.
[100] Banga M., Hsiao M. A region based approach for the identification of hardware Trojans [A]. In:Proceedings of2008IEEE International Workshop on Hardware-Oriented Security and Trust [C],Anaheim, CA, USA,2008:40-47.
[101] Li J., Lach J．At-speed delay characterization for IC authentication and Trojan horse detection [A]. In:Proceedings of2008IEEE International Workshop on Hardware-Oriented Security and Trust [C],Anaheim，CA, USA,2008:8-14.
[102] Wenchao L., Wasson Z., Seshia Sanjit A. Reverse engineering circuits using behavioral pattern mining
[A]. In: Proceedings of2012IEEE International Symposium on Hardwware-Oriented Security andTrust, San Francisco, CA, USA,2012:83-88.
[103] Shrestha G., Hsiao M. S. Ensuring trust of third-party hardware design with constrained sequentialequivalence checking [A]. In: Proceedings of2012IEEE Conference on Technologies for HomelandSecurity, Waltham, MA, USA2012:7-12.
[104] Smith Scott C., Jia D. Detecting Malicious Logic through Structural Checking [A]. In: Proceedings of2007IEEE Region5Technical Conference [C], Fayetteville, AR, USA,2007:217-222.
[105]李晓维,吕涛,李华伟,李光辉著.数字集成电路设计验证[M].北京:科学出版社,2010:7-10.
[106] William K.L. Hardware Design Verification: Simulation and Formal Method-Based Approaches [M].Englewood Cliffs: Prentice Hall,2005.
[107] Lucas P. Symbolic Diagnosis and its Formalisation [J]. The Knowledge Engineering Review,1997,12(2):109-146.
[108] Forbus K.D., Kleer J. Building Problem Solvers [M]. Massachusetts: The MIT Press,1993:74-98.
[109]黄杰.分布构件系统故障诊断技术研究[D].长沙:国防科技大学,2005.
[110] Raymond R. A Theory of diagnosis from first principles [J]. Artificial Intelligence,1987,32(1):57-95.
[111] Cristina C. Reverse Compilation Techniques [D]. Queensland: Queensland University of Technology,1994.
[112] Benjamin S., Saumya D., Gregory A. Disassembly of executable code revisited [A]. In: Proceedings ofWorking Conference on Reverse Engineering [C], Richmond, Virginia, USA,2002:45-54.
[113] Bastian S. Model checking of software for microcontrollers [D]. Aachen: RWTH Aachen University,2008.
[114] Cooprider N. Data-flow analysis for interrupt-driven microeontroller software [D]. Salt Lake City: theUniversity of Utah,2008.
[115]霍玮,于洪涛,冯晓兵,张兆庆.静态检测中断驱动程序的数据竞争[J].计算机研究与发展,2011,48(12):2290-2299.
[116] Kinder J., Zuleger F., Veith H. An Abstract Interpretation-Based Framework for Control FlowReconstruction from Binaries [A]. In: Proceedings of10thInternational Conference on Verification,Model Checking, and Abstract Interpretation [C], Savannah, GA, USA,2009:214-228.
[117] Bardin S., Herrmann P., V′edrine F. Refinement-based CFG Reconstruction from UnstructuredPrograms [A]. In: Proceedings of12thInternational Conference on Verification, Model Checking, andAbstract Interpretation [C], Austin, Texas, USA,2011:54-69.
[118] Thomas R., J rg B. Precise control flow reconstruction using boolean logic [A]. In: Proceedings of the11thInternational Conference/Workshop on Embedded Software [C], Taipei, Taiwan, China,2011:117-126.
[119]胡刚.固件代码逆向分析关键技术研究[D].郑州：解放军信息工程大学,2011.
[120] Cohen F. Computer viruses: theory and experiments [J]. Computers&Security,1987,6(1):22-35.
[121] Cohen F. Computational Aspects of Computer Viruses [J]. Computers&Security,1989,8(4):325-344.
[122] Adleman L. M. An Abstract Theory of Computer Viruses [A]. In: Proceedings of InternationalCryptology Conference [C], Santa Barbara, California, USA,1988,354-374.
[123] Thimbleby H., Anderson S., Cairns P. A framework for modelling trojans and computer virus infection[J]. The Computer Journal,1998,41(7):444-458.
[124]张新宇,卿斯汉,马恒太,张楠,孙淑华,蒋建春.特洛伊木马隐藏技术研究,通信学报,2004,25(7):153-159.
[125] Hongbo G., Qingbao L., Yu Z., et al. Code-controlled hardware Trojan horse [A]. In: Proceedings of the3th International Conference on Information Computing and Applications [C], Chengde, China,2012:171-178.
[126] Hongbo G., Qingbao L., Wei W., Yu Z. Research on Detection Technique for C2HTH Based on ModelChecking [J]. International Journal of Advancements in Computing Technology,2012,4(23):814-820.
[127] Baier C., Katoen J.P. Principles of Model Checking [M]. Cambridge: The MIT Press,2008.
[128] Michael H., Mark R. Logic in Computer Science: Modelling and Reasoning about Systems, SecondEdition [M]. Cambridge: Cambridge University Press,2004:193-232.
[129] Edmund M. C., Orna G., Doron A. P. Model Checking [M]. Cambridge: The MIT Press,2000.
[130]林梦香,吴国仕.程序模型检查器综述[J].计算机科学,2009,36(4):12-15.
[131] Bastian S., Stefan K. Model checking C source code for embedded systems [J]. International Journal onSoftware Tools for Technology Transfer,2009,11(3):187-202.
[132]刘万伟.扩展时序逻辑的推理及符号化模型检验技术[D].长沙:国防科技大学,2009.
[133]张振方.基于模型检验的软件分析方法研究[D].武汉:华中师范大学,2009.
[134] Alessandro C., Edmund Clarke C., et al. NUSMV: a new symbolic model checker [J]. InternationalJournal on Software Tools for Technology Transfer (STTT),2000,2(3):410-425.
[135] Gogul B. WYSINWYX: what you see is not what you execute [J].ACM Transactions on ProgrammingLanguages and Systems (TOPLAS),2010,32(6):1-84.
[136] Thomas W.R., Junghee L., Aditya V.T., et al. There’s Plenty of Room at the Bottom: Analyzing andVerifying Machine Code [A]. In: Proceedings of the22nd International Conference on Computer AidedVerification [C], Edinburgh, UK,2010:41-56.
[137] Bastian S. Model checking of software for microcontrollers [J]. ACM Transactions on EmbeddedComputing Systems (TECS).2010,9(4):1-27.
[138] MacKenzie I. S. The8051Microcontroller, Third Edition [M]. Englewood Cliffs: Prentice Hall,1998:19-21.
[139] Muhammad A. M., Janice Gillispie M., Mckinlay R. D. The8051Microcontroller and EmbeddedSystems: Using Assembly and C, Second Edition [M]. Englewood Cliffs: Pearson/Prentice Hall,2006.
[140] Bastian S., Jorg B., Stefan K. Application of static analyses for state-space reduction to themicrocontroller binary code [J]. Science of Computer Programming,2011,76(2):100-118.
[141] Alfred V. A., Monica S. L., Ravi S., Jeffrey D. Compilers-Principles, Techniques, and Tools, SecondEdition [M]. New Jersey: Addison-Wesley,2007.
[142] Ramon E. M., Baker Kearfott R., Michael J. Introduction to interval analysis [M]. Philadelphia: Societyfor Industrial and Applied Mathematics,2009:7-49.
[143] Dongrui W., Mendel J. M., Coupland S. Enhanced interval approach for encoding words into intervaltype-2fuzzy sets and its convergence analysis [J]. IEEE Transactions on Fuzzy Systems,2012,20(3):499-513.
[144]王雅文,姚欣洪,宫云战,杨朝红.一种基于代码静态分析的缓冲区溢出检测算法[J].计算机研究与发展,2012,49(4):839-845.
[145] Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis [M]. Berlin: Springer-Verlag,1999,200-300.
[146] Cousot P. Abstract interpretation based formal methods and future challenges [A]. In: Proceeding ofInformatics-10Years Back,10Years Ahead, London,2001:138-156.
[147]姬孟洛,王怀民,李梦君,董威,齐治昌.一种基于抽象解释和通用单调数据流框架的值范围分析方法[J].计算机研究与发展,2006,43(11):2020-2026.
[148]王雅文,宫云战,肖庆,杨朝红.基于抽象解释的变量值范围分析及应用[J].电子学报,2011,39(2):296-303.
[149] Cousot P., Cousot R. Abstract Interpretation: A unified lattice model for static analysis of programs byconstruction or approximation of fixpoints [A]. In: Proceedings of the4th ACM SIGACT-SIGPLANSymposium on Principles of Programming Languages, New York,1977:238-252.
[150]李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术[J].软件学报,2008,19(1):17-26.
[151] Patrick C., Radhia C., Laurent M.. Theories, solvers and static analysis by abstract interpretation [J].Journal of the ACM,2012,59(6):31.
[152] Julien B., Patrick C., Radhia C., et al. Static analysis by abstract interpretation of embedded criticalsoftware [J]. ACM SIGSOFT Software Engineering Notes,2011,36(1):1-8.
[153] Agostino C., Matteo Z. Widening and narrowing operators for abstract interpretation [J]. ComputerLanguages, Systems&Structures,2011,37(1):24-42.
[154] Thomas R., Jorg B., Martin H., et al. Past time LTL runtime verification for microcontroller binary code
[A]. In: Proceedings of the16thInternational Conference on Formal Methods for Industrial CriticalSystems [C], Trento, Italy,2011:37-51.
[155] Thomas N., Bastian S. Delayed nondeterminism in model checking embedded systems assembly code
[A]. In: Proceedings of the3rdInternational Haifa Verification Conference on Hardware and software:Verification and Testing [C], Haifa, Israel,2008:185-201.
[156] Bruce W., John C., Wolfgang R. Comprehensive Functional Verification: The Complete Industry Cycle
[M]. San Francisco: Morgan Kaufmann Publishers,2005.
[157]贾仰理,李舟军,邢建英,等.基于模型检验的构件验证技术研究进展[J].计算机研究与发展,2011,48(6):913-922.
[158] Nocco S., Quer S. A Novel SAT-Based Approach to the Task Graph Cost-Optimal Scheduling Problem[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2010,29(12):2027-2040.
[159] Iyer S., Sahoo D., Emerson E.A., Jain J. On partitioning and symbolic model checking [J]. IEEETransactios on Computer-Aided Design of Integrated Circuits and Systems,2006,25(5):780-788.
[160] Alessandro C., Alberto G. Software model checking via IC3[A]. In: Proceedings of the24thInternational Conference on Computer Aided Verification, Berkeley, CA, USA,2012:277-293.
[161]虞蕾,赵宗涛. PSL的有界模型检验[J].电子学报，2009,37(3)：614-621.
[162] Cordeiro L., Fischer B., Marques Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-CSoftware [J]. IEEE Transactions on Software Engineering,2012,38(4):957-974.
[163] Cormac F., Patrice G. Dynamic partial-order reduction for model checking software [A]. In:Proceedingsof the32ndACM SIGPLAN-SIGACT symposium on Principles of programming languages [C], LongBeach, California, USA,2005:110-121.
[164] Gerard J. H. On-The-Fly Model Checking [J]. ACM Computing Surveys,1996,28(4):120.
[165] Roberto S., Stefano T., et al. Symbolic system, explicit properties: on hybrid approaches for LTLsymbolic model checking [J]. International Journal on Software Tools for Technology Transfer (STTT),2010,13(4):319-335.
[166]李兴锋,张新常,杨美红,等.基于SPIN的模块化模型检测方法研究[J].电子与信息学报,2011,33(4):902-907.
[167] Karen Y., Orna G. Static analysis for state-space reductions preserving temporal logics [J]. FormalMethods in System Design,2004,25(1):67-96.
[168] Moonzoo K., Yunho K., Hotae K. A comparative study of software model checkers as unit testing tools:an industrial case study [J]. IEEE Transactions on Software Engineering,2011,37(2):146-160.
[169]崔宝江,梁晓兵,王禹,王建新.基于回溯与引导的关键代码区域覆盖的二进制程序测试技术研究[J].电子与信息学报,2012,34(1):108-114.
[170] Weiser M. Program Slicing [J], IEEE Transations on Software Engineering,1984,10(4):352-357.
[171]李必信.程序切片技术及其应用[M].北京:科学出版社,2006.
[172] John H., Matthew B. D., Hongjun Z. Slicing software for model construction [J]. Higher-Order andSymbolic Computation,2000,13(4):315-353.
[173] Sen A., Garg V. K. Formal Verification of Simulation Traces Using Computation Slicing [J]. IEEETransactions on Computers,2007,56(4):511-527.
[174] Mittal N., Sen A., Garg V. K. Solving Computation Slicing Using Predicate Detection [J]. IEEETransactions on Parallel and Distributed Systems,2007,18(12):1700-1713.