基于B方法的智能嵌入式设备安全防护模型研究

With the increasing growth of attacks originated by security threats and vulnerability exploitation, the security of intelligent embedded devices is of strategic importance. It is of great theoretical value and practical significance to carry out security defense research for the discovery of vulnerabilities, the development of security defense technology on intelligent embedded devices, and the maintenance of national information security. The software/hardware isolation environment provides an underlying isolation, which enhances the security of embedded devices. However, the existing problems are as follows: (1) The existing implementation schemes are lack of effective formal analysis and verification, thus the determinacy of the security policies is difficult to guarantee; (2) The majority of formal models are in a high abstract level, and the applications in the real system are difficult. This project focuses on formalized model construction, security analysis and verification, and vulnerability discovery, which are the key issues desiderated to be solved in security defense of intelligent embedded devices. The main contents of this project are formal analysis of system security specification, the design of security defense model based on the B method, security analysis and vulnerability discovery based on the B model, ect. This project will explorer the method of vulnerability discovery in the formal security specifications. It is expected to make some breakthroughs in the key issues such as formal modeling of security defense technology and security analysis of intelligent embedded devices, which will provide theoretical and technical support for the security analysis of embedded devices, the security reinforcement of intelligent hardware, ect.

面对智能嵌入式设备层出不穷的安全威胁和漏洞利用攻击，开展系统安全防护研究对发现设备安全缺陷、推进嵌入式设备安全防护技术的发展和维护国家信息安全具有重要的理论和现实意义。软硬件隔离执行环境为嵌入式设备提供了基于底层隔离的安全防护，但仍存在以下问题：(1)现有的安全防护方案尚缺乏有效的形式化分析与验证，安全策略的确定性难以保证； (2)大部分形式化模型抽象层次较高，缺少在真实系统上的应用。本课题关注智能嵌入式设备安全防护的形式化模型构建、安全性分析与验证、系统脆弱性发现等亟待解决的关键问题。着重对系统安全规约的形式化分析、基于B方法的系统安全防护模型设计、基于B模型的系统安全分析与脆弱性发现等问题展开研究，探索形式化安全规范约束下的系统安全隐患和脆弱点检测方法。期望在智能嵌入式设备安全防护技术的形式化建模与安全性分析方面有所突破，为嵌入式设备安全分析、智能硬件安全加固等领域提供理论和技术支持。

面对智能嵌入式设备层出不穷的安全威胁和漏洞利用攻击，本项目开展系统安全防护研究方面的基础研究，对发现设备安全缺陷、推进嵌入式设备安全防护技术的发展和维护国家信息安全具有重要的理论和现实意义。软硬件隔离执行环境为嵌入式设备提供了基于底层隔离的安全防护，本项目针对以下难点问题展开研究：(1)现有的安全防护方案尚缺乏有效的形式化分析与验证，安全策略的确定性难以保证；(2)大部分形式化模型抽象层次较高，缺少在真实系统上的应用。本课题关注智能嵌入式设备安全防护的形式化模型构建、安全性分析与验证、系统脆弱性发现等亟待解决的关键问题。着重对系统安全规约的形式化分析、基于B方法的系统安全防护模型设计、基于B模型的系统安全分析与脆弱性发现等问题展开研究，探索形式化安全规范约束下的系统安全隐患和脆弱点检测方法。在智能嵌入式设备安全防护技术的形式化建模与安全性分析方面取得了一定的研究成果，有代表性的成果包括以下三个方面。（1）为实现可信执行环境架构下资源的安全管控，提出经过形式化验证的通用可信执行环境框架。并通过386个lemma/theorem形式化验证该框架中定义的原子安全操作满足一致性，且该框架提供的安全功能满足TA隔离、运行时机密性、运行时完整性等安全目标，最终完成该框架的功能正确性和安全性验证。（2）针对可信执行环境中利用内存标签实现的访问控制提出了通用的形式化模型框架，并提出了一种基于模型检测的访问控制安全性分析方法。运用模型检测验证了模型的功能正确性和安全性，自动化遍历了14699098个状态和37834011个状态转移，并模拟了2个具体攻击场景的攻击检测。（3）在系统安全性分析与脆弱性发现方面，针对资源受限的嵌入式设备，研究各类攻击方法和原理，并采用了大量实验验证的方法，基于模型检测的思想，提出用形式化规约来刻画系统正常行为，通过对程序运行过程的建模，在模型上对规约进行验证，从而发现异常并检测出恶意代码，提出并实现了程序运行过程与行为模型相结合的形式化模型，提高了模型检测的准确性。基于上述研究，在本项目支持下发表学术论文8篇均为第一标注，其中SCI期刊6篇（2篇为CCF A类，1篇为CCF B类），中文CCF A类期刊2篇，在发表高水平论文的质量上和数量上均超出预期，取得了有一定影响力的研究成果。