嵌入式系统安全保障与形式化检测的研究

结题报告

项目介绍

AI项目解读

基本信息

批准号：
61572279
项目类别：
面上项目
资助金额：
71.0万
负责人：
罗贵明
依托单位：
清华大学
学科分类：
F0206.信息安全
结题年份：
2019
批准年份：
2015
项目状态：
已结题
起止时间：
2016-01-01 至2019-12-31

项目参与者：
张荷花；宋韶旭；万海；周旻；罗建；夏默；张宇来；蒲甫安；赵勃旭；
关键词：
形式化分析自动化验证安全属性验证

项目摘要

With the design complexity increasing of embedded system, how to guarantee the embedded systems security has become an important issue in the computer science and engineering technology. The security of embedded systems is focus in this project. The data of the embedded system security event will be modeled based on the big data method and adaptive approaches. The filtering and optimization are concerned for data model. The causal relationship between events associated with the security of embedded devices will be analyzed. We will investigate that the reason of the equipment faults and security problems are possible generated in the operation stage of an embedded system. The fault location will be fixed and predicted to provide security for an embedded system. The algorithm of safety risk evaluation will be established. Based on the attack graphs technology and the vulnerability database information a safety risk evaluation will be proposed to enhance the ability of the embedded system dealing with all kinds of unexpected attacks. Formal modeling and automatic verification technology will be studied for embedded systems. An automatic verification tool integrated both modeling and model checking is designed and developed. Security and reliability of an embedded system is checked and guaranteed in the design stage. As an application instance, we will model MVB by the formal method. The MVB as well as the train network communication protocol will be modeled by automata. The simulation and formal verification will be executed for the MVB system and protocols. Furthermore, VHDL codes for the hardware are generated automatically, then, the trust MVB will be designed with formal methods.

随着嵌入式系统设计复杂程度的提高，如何保障嵌入式系统安全成为计算机领域和工程界所关注的重要问题。本项目以嵌入式系统安全保障为中心，研究嵌入式系统安全事件建模与优化计算，利用大数据方法和自适应技术给出安全事件的数据建模、滤波和预判；分析嵌入式设备安全事件之间的关联与因果关系，研究系统运行阶段其设备可能产生的故障和安全问题的原因，对故障进行定位和预报，为嵌入系统的安全运行提供保障；研究安全风险评估算法，利用攻击图技术和漏洞库信息建立嵌入式系统安全风险评估系统，提高系统应对各种突发攻击事件的能力；研究嵌入式系统形式化建模与自动检测技术，设计和研发模块建模与模型检测一体化自动检测工具，在设计阶段检查和保障嵌入式系统的安全性和可靠性；以列车网卡MVB为研究案例，用自动机对MVB和列车网络通信协议进行形式化建模，对该嵌入式系统和协议进行仿真和检测，自动生成和优化VHDL代码，完成可信列车网卡的设计

结项摘要

摘要.本项目研究嵌入式系统安全事件建模与优化计算，利用大数据方法和自适应技术给出安全事件的数据建模、滤波和预判；分析嵌入式设备安全事件之间的关联与因果关系，并利用大数据技术分析漏洞之间相关性；研究系统运行阶段其设备可能产生的故障和安全问题的原因，对故障进行定位和预报；研究网络安全建模和网络可靠性路由算法，网络的故障检测理论，提出高效的检测方法；研究语义计算和语义推理，通过图像数据语义分析故障和缺陷；研究嵌入式系统形式化建模与自动检测技术，设计和研发模块建模与模型检测一体化自动检测工具。用自动机对MVB和列车网络通信协议进行形式化建模，对该嵌入式系统和协议进行仿真和检测，自动生成VHDL代码，利用自动机设计列车网卡。