面向数值程序安全性与鲁棒性的抽象解释技术

项目名称： 面向数值程序安全性与鲁棒性的抽象解释技术

项目编号： No.61202120

项目类型： 青年科学基金项目

立项/批准年度： 2013

项目学科： 计算机科学学科

项目作者： 陈立前

作者单位： 中国人民解放军国防科学技术大学

项目金额： 26万元

中文摘要： 计算机软件尤其是嵌入式软件的设计与运行，与系统及环境的数学与物理模型密不可分，往往会涉及大量数值运算。计算机软件的许多可信性质和程序缺陷与程序中的数值性质密切相关。因此，研究数值程序安全性与鲁棒性的分析方法，对提高软件的可信性具有重要意义。本项目针对计算机中数值程序的特点，即数值数据类型值表示范围的有限性、浮点运算的不精确性、输入数据伴随的非确定性等特点，面向数值程序的安全性与鲁棒性，以抽象解释为理论支撑，开展相关静态分析技术研究。拟突破数值不变式生成、数值程序的安全性与鲁棒性分析等关键技术，力求在新型数值抽象域设计、浮点程序分析、命令式程序鲁棒性分析等关键科学问题的研究中获得进展和突破，设计并实现相应的数值程序分析工具原型，针对航空航天等领域典型嵌入式软件的数值相关性质进行示范应用。本项目将形成面向数值程序的静态分析方法、技术和工具，对计算机软件的可信保障具有重要实际应用价值。

中文关键词： 抽象解释；静态分析；数值程序；安全性；鲁棒性

英文摘要： Computer software especially embedded software has a tighten relation with the mathematical and physical model of the system and the environment, and thus often involves a lot of numeric computation. Hence, a variety of dependability properties and software defects are closely related to the numeric properties of programs. This project addresses the safety and robustness issues of numeric programs due to the finite representability of numeric data types, inexactness of floating point computation, and intrinsic uncertainty over input data. The main goal of this project is to develop new methods and tools at the source code level that fit for analyzing the safety and robustness of numeric programs, by exploiting the abstract interpretation theory. This project will explore and strengthen some core techniques, such as numeric invariant generation, safety analysis and robustness analysis of numeric programs, to target several scientific issues including the design of new numeric abstract domains, analysis of floating point programs, robustness analysis of imperative programs, etc. On this basis, this project plans to develop a prototype of static analyzer for numeric programs and apply it to analyze certain numeric related properties of domain-specific software, such as avionics and space embedded software. The proj

英文关键词： abstract interpretation；static analysis；numeric programs；safety；robustness