Page 20 - 《软件学报》2021年第10期

2992 Journal of Software 软件学报 Vol.32, No.10, October 2021

[15] Sarkar D, Jagannathan M, Thiagarajan J, Venkatapathy R. Flow-insensitive static analysis for detecting integer anomalies in
programs. In: Hasselbring W, ed. Proc. of the 25th Conf. on IASTED Int’l Multi-Conf.: Software Engineering. ACTA, 2007.
334340. [doi: 10.5555/1332044.1332098]
[16] Pereira FMQ, Rodrigues RE, Campos VHS. A fast and low-overhead technique to secure programs against integer overflows. In:
Proc. of the 2013 IEEE/ACM Int’l Symp. on Code Generation and Optimization (CGO). Los Alamitos: IEEE, 2013. 111. [doi:
10.1109/CGO.2013.6494996]
[17] Zhang C, Wang TL, Wei T, Chen Y, Zou W. IntPatch: Automatically fix integer-overflow-to-buffer-overflow vulnerability at
compile-time. In: Gritzalis D, Preneel B, Theoharidou M, eds. Proc. of the 15th European Conf. on Research in Computer Security
(ESORICS). Berlin: Springer-Verlag, 2010. 7186. [doi: 10.1007/978-3-642-15497-3_5]
[18] Sun H, Li HP, Zeng QK. Statically detect and run-time check integer-based vulnerabilities with information flow. Ruan Jian Xue
Bao/Journal of Software, 2013,24(12):27672781 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4385.htm
[doi: 10.3724/SP.J.1001.2013.04385]
[19] Chinchani R, Iyer A, Jayaraman B, Upadhyaya SJ. ARCHERR: Runtime environment driven program safety. In: Samarati P, Ryan
P, Gollmann D, Molva R, eds. Proc. of the 9th European Symp. on Research in Computer Security (ESORICS 2004). Berlin:
Springer-Verlag, 2004. 385406. [doi: 10.1007/978-3-540-30108-0_24]
[20] Brumley D, Song DX, Chiueh T, Johnson R, Lin H. RICH: Automatically protecting against integer-based vulnerabilities. In: Proc.
of the 14th Annual Network and Distributed System Security Symp (NDSS 2007). 2007.
[21] Kroening D, Liang L, Melham T, Schrammel P, Tautschnig M. Effective verification of low-level software with nested interrupts.
In: Nebel W, Atienza D, eds. Proc. of the Design, Automation & Test in Europe Conf. & Exhibition (DATE 2015). CA: EDA
Consortium, 2015. 229234. [doi: 10.7873/DATE.2015.0360]
[22] Schlich B, Noll T, Brauer J, Brutschy L. Reduction of interrupt handler executions for model checking embedded software. In:
Namjoshi K, Zeller A, Ziv A, eds. Proc. of the 5th Int’l Haifa Verification Conf. on Hardware and Software: Verification and
Testing (HVC 2009). Berlin: Springer-Verlag, 2009. 520. [doi: 10.1007/978-3-642-19237-1_5]
[23] Kidd N, Jagannathan S, Vitek J. One stack to run them all: Reducing concurrent analysis to sequential analysis under priority
scheduling. In: van de Pol J, Weber M, eds. Proc. of the 17th Int’l SPIN Conf. on Model Checking Software (SPIN 2010). Berlin:
Springer-Verlag, 2010. 245261. [doi: 10.1007/978-3-642-16164-3_18]
[24] Wu XG, Wen YJ, Chen LQ, Dong W, Wang J. Data race detection for interrupt-driven programs via bounded model checking. In:
Proc. of the 7th Int’l Conf. on Software Security and Reliability Companion (SERE 2013). Los Alamitos: IEEE, 2013. 204210.
[doi: 10.1109/SERE-C.2013.33]

附中文参考文献:
[4] 孙浩,曾庆凯.整数漏洞研究:安全模型、检测方法和实例.软件学报,2015,26(2):413426. http://www.jos.org.cn/1000-9825/4793.
htm [doi:10.13328/j.cnki.jos.004793]
[18] 孙浩,李会朋,曾庆凯.基于信息流的整数漏洞插装和验证.软件学报,2013,24(12):27672781. http://www.jos.org.cn/1000-9825/
4385.htm [doi: 10.3724/SP.J.1001.2013.04385]

高猛(1982－),男,高级工程师,CCF 专业会 王政(1986－),男,博士,高级工程师,主要
员,主要研究领域为软件可靠性,嵌入式软 研究领域为软件形式化建模,分析与验证,
件测试,模型检测. 基于模型的设计.

滕俊元(1985－),男,高级工程师,主要研究
领域为软件形式化验证,嵌入式软件测试.