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

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 project is expected to advance the static analysis methods, techniques and tools for numeric programs, so as to contribute to the dependability assurance of computer software.

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

软件的可信性已成为现代软件质量问题的焦点。计算机软件尤其是嵌入式软件的设计与运行，与系统及环境的数学物理模型密不可分，往往会涉及大量数值运算。因此，计算机软件中的许多可信性质（如输出的有界性）或缺陷（如除零错、算术溢出、数组越界等常见运行时错误）往往和程序中的数值性质密切相关。本项目针对计算机中数值程序的特点，即数值型数据类型值表示范围的有限性、浮点运算的非精确性、输入数据伴随的非确定性等特点，以抽象解释为理论支撑，从源程序级别，面向数值程序的安全性与鲁棒性开展分析与验证技术研究。. 经过三年的研究，项目组依据计划，完成了各项研究内容，达到了预期的研究目标。在面向数值不变式生成的新型数值抽象域的设计与实现、应用相关数值程序安全性的分析、数值程序鲁棒性的分析、数值程序分析工具原型的设计与实现等方面形成了较为系统、深入的研究成果，在基准测试程序和航天工业代码上的应用验证了项目成果的有效性。进展要点如下：. 1) 针对已有数值抽象域在表达能力方面存在的凸性局限性，提出了多种能够表达非凸性质的数值抽象域，包括绝对值八边形抽象域、区间幂集抽象域等；. 2) 针对中断机制在数值运算密集型嵌入式控制软件中广泛使用的特征，提出了面向中断驱动型程序的可靠数值性质分析方法；. 3) 针对浮点计算不精确性导致的程序鲁棒性问题，提出了面向浮点程序的基于自组合的鲁棒性分析方法；. 4) 设计并实现了一个面向C程序的数值程序分析工具原型CAI，支持程序中数值相关运行时错误的检测；. 5) 在基准测试程序以及航天工业代码上开展了实验验证，验证了方法的有效性。. 至2015年，共发表学术论文9篇，其中SCI收录2篇，EI收录5篇。部分论文发表在Science of Computer Programming、SAS 2014、EMSOFT 2015等程序语言与嵌入式软件领域的重要国际期刊会议上，并有一篇论文获得EMSOFT 2015最佳论文提名。目前，发表的论文已被牛津大学、伦敦大学玛丽皇后学院、巴黎高等师范学院、慕尼黑工业大学等大学的同行学者引用。