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

项目名称： 嵌入式软件可组合信息流安全验证机制研究

项目编号： No.61303033

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

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 孙聪

作者单位： 西安电子科技大学

项目金额： 23万元

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

中文关键词： 信息流安全；嵌入式软件；组件；可组合性；程序验证

英文摘要： 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.

英文关键词： information flow security；embedded software；component；compositionality；program verification