嵌入式软件可组合信息流安全验证机制研究

Information flow security is a critical problem to the security of embedded softwares. In this project, we investigate the information flow security problems brought by the component-based design of embedded softwares. With an emphasis on the precision, scalability and soundness of verification, we propose to give a formal definition of the security property and to develop a precise verification to enforce compositional information flow security on heterogeneous component-based embedded softwares. Under the given component model framework, we plan to implement a layered low-overlapping verification mechanism by using the techniques of model abstraction and transformation, automated program verification, and contract-based reasoning. We also explain the preciseness, soundness and compositionality of this verification mechanism. The overall result is a highly precise, sound and scalable verification framework for the information flow security of heterogeneous component-based embedded softwares. This project will provide important promotion and supports to the development of verification for security properties of complicated embedded softwares on both theory and technique aspects.

信息流安全是嵌入式软件安全性研究需要考虑的重要问题。本项目针对嵌入式软件组件化设计过程所引入的信息流安全问题，以验证机制的精确性、可扩展性、可靠性为侧重点，研究异构组件化嵌入式软件的可组合信息流安全属性的形式化定义和精确验证。在具体组件模型框架下，通过运用模型抽象与变换技术、自动程序验证技术和基于契约的推理技术，实现分层低耦合的信息流安全属性验证机制，并说明该验证机制的精确性、可靠性和可组合性，最终提供一种高精确性、高可靠性、可扩展性良好的信息流安全验证框架。项目将对复杂嵌入式软件安全性验证理论和技术的发展提供重要的推动和支持。

本项目针对嵌入式软件组件化设计过程所引入的信息流安全问题，研究异构组件化嵌入式软件的可组合信息流安全属性的形式化定义和精确验证。项目主要贡献如下：.1）提出新的信息流安全属性（Relaxed Release with Reference Points, R3P），提出“条件持久性”这一新的谨慎性原则，使用下推系统可达性分析验证程序的R3P属性，并通过“存储-匹配”模式的模型变换提高验证效率。.2）提出将可组合的信息流安全验证应用于模型驱动的嵌入式软件开发过程中，对SysML建模语言的IBD图进行自动抽象，转化为安全相关的接口自动机，在此基础上给出了组件安全属性定义、组合系统安全条件，并实现了相应的判定算法。.3）提出广义安全接口结构，并在广义安全结构上定义了支持任意有限格模型的基于安全多执行的无干扰属性，针对单个组件的安全属性验证给出了判定过程算法，针对组合系统的安全，给出了可组合定理证明及其判定算法，并将可组合验证应用于控制系统安全协议等场景。.4）给出了BIP组件模型的可组合信息流安全验证方法，将BIP模型抽象为广义安全接口结构，用于嵌入式组件化系统（以双余度飞行控制系统为例）的信息流安全验证。.5）针对服务云环境下的信息流安全控制问题，提出相应的信息流安全模型和组合验证算法，并提出了针对智能传感器网络中信息流安全验证的分布式验证算法。.本项目对组件化软件模型可组合信息流安全验证机制的研究成果和工具成果，可用于保证领域特定的嵌入式软件数据访问、数据传递的机密性，弥补目前航空、工业控制等领域嵌入式软件安全性验证中缺乏信息流安全属性形式化验证理论、技术和工具的不足，对复杂嵌入式软件安全性验证理论和技术的发展提供推动和支持。