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

高猛 等:航天嵌入式软件整数溢出的形式化验证方法 2991

5 总 结

在航天嵌入式软件整数溢出检测方面,模型检测技术少有工程应用.一方面,随着程序规模的扩大,存在着
状态空间爆炸问题;另一方面,已有的模型检测技术不能有效支持中断驱动型程序的整数溢出检测.鉴于此,本
文以航天嵌入式软件整数溢出真实案例为基础,系统地分析了整数溢出分布趋势以及溢出特征.在有界模型检
测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术,有效地降低了程序约
束条件 C 的规模.同时,面向中断驱动型程序,提出了基于干扰变量的中断驱动程序顺序化方法,该方法采用抽象
解释、摘要机制对中断函数特征表示,并基于干扰变量分析保证顺序化后的程序包含尽可能少的中断函数.通
过实验,结果表明:本文所提出的方法不仅能够有效地提高分析效率,还使得已有的模型检测技术能够适用于中
断驱动型程序整数溢出检测.由实验分析可知,整数溢出有界模型检测的精度和效率与中断特征抽象程度、干
扰变量个数以及插入中断次数密切相关.因此,结合更精确的中断特征抽象以及程序顺序化优化技术来缩短检
测时间、提升分析精度,将是本文下一步研究的重点.另外,针对带中断的多线程程序整数溢出模型检测,也将是
未来的研究方向.

References:
[1] Sercord RC. Secure Coding in C and C++: Of Strings and Integers. Addison Wesley, 2006. [doi: 10.1109/MSP.2006.22]
[2] Christey S, Martin RA. Vulnerability type distributions in CVE. 2007. https://cve.mitre.org/docs/vuln-trends/vuln-trends.pdf
[3] Christey S, Martin RA, Brown M, Paller A, Kirby D. 2011 CWE/SANS top 25 most dangerous software errors. Technical Report,
MITRE Corporation, 2011. http://cwe.mitre.org/top25
[4] Sun H, Zeng QK. Research on integer-based vulnerabilities: Security model, detecting methods and real-world cases. Ruan Jian
Xue Bao/Journal of Software, 2015,26(2):413426 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4793.htm
[doi: 10.13328/j.cnki.jos.004793]
[5] Dietz W, Li P, Regehr J, Adve VS. Understanding integer overflow in C/C++. In: Proc. of the 34th Int’l Conf. on Software
Engineering (ICSE). Los Alamitos: IEEE, 2012. 760770. [doi: 10.1109/ICSE.2012.6227142]
[6] Wang X, Chen HG, Jia ZH, Zeldovich N, Kaashoek MF. Improving integer security for systems with KINT. In: Proc. of the 10th
USENIX Conf. on Operating Systems Design and Implementation (OSDI). Berkeley: USENIX Association, 2012. 163177.
[7] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs. In: Jensen K, Podelski A, eds. Proc. of the Tools and
Algorithms for the Construction and Analysis of Systems (TACAS 2004). Berlin: Springer-Verlag, 2004. 168176. [doi: 10.1007/
978-3-540-24730-2_15]
[8] Biere A, Cimatti A, Clarke E, Zhu YS. Symbolic model checking without BDDs. In: Cleaveland WR, ed. Proc. of the Tools and
Algorithms for the Construction and Analysis of Systems (TACAS’99). Berlin: Springer-Verlag, 1999. 193207. [doi: 10.1007/3-
540-49059-0_14]
[9] Clarke E, Kroening D, Yorav K. Behavioral consistency of C and verilog programs using bounded model checking. In: Getreu I,
Fix L, Lavagno L, eds. Proc. of the 40th Annual Design Automation Conf. (DAC 2003). New York: ACM, 2003. 368371. [doi:
10.1145/775832.775928]
[10] Cordeiro LC, Fischer B, Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. on
Software Engineering, 2012,38(4):957974. [doi: 10.1109/TSE.2011.59]
[11] de Moura L, Bjørner N. Z3: An efficient SMT solver. In: Ramakrishnan CR, Rehof J, eds. Proc. of the Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2008). Berlin: Springer-Verlag, 2008. 337340. [doi: 10.1007/978-3-540-78800-
3_24]
[12] Wu XG, Chen L, Mine L, Dong W, Wang J. Static analysis of runtime errors in interrupt-driven programs via sequentialization.
ACM Trans. on Embedded Computing Systems (TECS), 2016,15(4):70. [doi: 10.1145/2914789]
[13] Do H, Elbaum SG, Rothermel G. Supporting controlled experimentation with testing techniques: An infrastructure and its potential
impact. Empirical Software Engineering, 2005,10(4):405435. [doi: 10.1007/s10664-005-3861-2]
[14] Sung CH, Kusano M, Wang C. Modular verification of interrupt-driven software. In: Proc. of the 32nd IEEE/ACM Int’l Conf. on
Automated Software Engineering (ASE). Los Alamitos: IEEE, 2017. 206216. [doi: 10.1109/ase.2017.8115634]