高可信嵌入式系统软件的关键技术研究
发布时间：2021-01-11 01:07
为了满足先进工业制造和装备控制智能化的需求,嵌入式系统已成为关键基础设施的核心控制组件,并在工业制造、船舶、交通、国防安全、信息通信等领域起着影响全局系统安全的重要作用。近年来,随着嵌入式应用的广泛普及,以及网络化、智能化的发展趋势,系统运行的可靠性和敏感数据的安全性成为了嵌入式领域亟待解决的关键问题。倘若嵌入式软件系统失效或遭受安全入侵,则可能产生危及到国家政治、经济以及军事安全的重大事故。因此,如何针对此类安全关键的应用场景,设计和开发一种功能正确、满足所需安全（Security）和防危（Safety）属性,并能对所宣称的正确性提供确凿可信证据的嵌入式系统,成为了一个重要的研究课题。针对上述问题,本文全面分析并总结了高可信嵌入式应用对于系统软件的安全要求,提出满足安全隔离和形式化验证的软件体系架构。并针对系统软件中,硬件机制建模、可中断代码验证、不可信组件的安全访问控制以及基于虚拟化的隔离保护等关键问题,分别提出了相应的解决方法。最终,形成了一套可组合、可伸缩的高可信嵌入式系统基础软件开发和形式化验证框架与工具链,并实现了原型系统的开发和实验评估。结果表明,通过采用隔离、硬件保护机...
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：184 页
【学位级别】：博士
【部分图文】：
命令填充及不同类型命令解释时延
第四章 非安全关键驱动的安全运行环境4.7.2 命令解释吞吐量实验比较内核态 AHCI 驱动与相同功能的用户态驱动在被连续调用模块中磁盘读写函数时，单位时间内可以访问磁盘的数据量。为了消除由于进程抢占所导致的抖动，测试时终止除测试进程和 idle 以外的其他进程，并对于用户态驱动而言，测试被代码直接运行于 AHCI 驱动进程中。实验结果如图 4-16 所示，其中横轴表示每次磁盘访问（即发送 FrameInformationStructure，FIS）时 DMA 的数据块大小，单位为 KB，纵轴为每秒可以读取或写入的数据量。随着单次 DMA 数据块大小的增加，磁盘访问效率提升，吞吐量也随之提升，但用户态驱动与内核态驱动在 DMA 数据块大小相同时，吞吐量非常接近。其原因在于用户态执行驱动程序并没有成为磁盘读写的性能瓶颈。
图 4-17 用户态与内核态串口数据发送时延4.7.4 综合吞吐量实验测量在综合环境下，框架对驱动吞吐量产生的影响。实验由两台计算机组成，辅助机向实验机串口中尽可能多地输出数据，通过测量实验验机内核态与用户态串口驱动每秒最大可接收的字符数，获得框架对驱动吞吐量带来的影响。实验结果如图 4-18 所示，试验中串口运行在波特率为 115200，数据位 8，停止位 1，无奇偶校验的状态下，理论最大吞吐量应为 12800char/s（即图中 baseline 一项）。由于串口控制器、中断响应与系统调用等额外负载，内核态驱动最大吞吐量为理论值的 89%，而用户态驱动的吞吐量与内核态相差 1%左右。
【参考文献】：
期刊论文
[1]嵌入式系统安全综述[J]. 赵波,倪明涛,石源,樊佩茹. 武汉大学学报(理学版). 2018(02)
[2]未来网络与工业互联网发展综述[J]. 吴文君,姚海鹏,黄韬,王露瑶,张延华,刘韵洁. 北京工业大学学报. 2017(02)
[3]基于可信计算基的主机可信安全体系结构研究[J]. 黄强,常乐,张德华,汪伦伟. 信息网络安全. 2016(07)
[4]关键基础设施信息安全分析及防护[J]. 刘松,朱钱祥,陈开放. 智慧工厂. 2016(03)
[5]嵌入式操作系统的形式化验证研究[J]. 陈丽蓉,李允,罗蕾. 计算机科学. 2015(08)
[6]设备驱动程序可靠性和正确性保障方法与技术研究进展[J]. 张一帆,黄超,欧建生,汤恩义,陈鑫. 软件学报. 2015(02)
[7]微内核中断机制的形式化设计与验证[J]. 李康杰,钱振江,黄皓. 计算机科学. 2013(03)
[8]操作系统对象语义模型（OSOSM）及形式化验证[J]. 钱振江,刘苇,黄皓. 计算机研究与发展. 2012(12)
[9]网卡驱动程序的用户态移植和优化[J]. 王燕飞,华蓓. 电子技术. 2012(08)
[10]用户态驱动框架的研究与实现[J]. 刘军卫,李曦,陈香兰,徐军. 计算机系统应用. 2011(11)
博士论文
[1]安全操作系统形式化设计与验证方法研究[D]. 钱振江.南京大学 2013
[2]面向目标代码的实时操作系统形式化验证方法研究[D]. 史建琦.华东师范大学 2012
[3]高可信嵌入式操作系统体系架构研究[D]. 杨霞.电子科技大学 2010
[4]基于模型检测的安全操作系统验证方法研究[D]. 程亮.中国科学技术大学 2009
硕士论文
[1]基于AUTOSAR的汽车电子操作系统及其应用的建模与分析[D]. 彭云辉.华东师范大学 2014
本文编号：2969767
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：184 页
【学位级别】：博士
【部分图文】：
命令填充及不同类型命令解释时延
第四章 非安全关键驱动的安全运行环境4.7.2 命令解释吞吐量实验比较内核态 AHCI 驱动与相同功能的用户态驱动在被连续调用模块中磁盘读写函数时，单位时间内可以访问磁盘的数据量。为了消除由于进程抢占所导致的抖动，测试时终止除测试进程和 idle 以外的其他进程，并对于用户态驱动而言，测试被代码直接运行于 AHCI 驱动进程中。实验结果如图 4-16 所示，其中横轴表示每次磁盘访问（即发送 FrameInformationStructure，FIS）时 DMA 的数据块大小，单位为 KB，纵轴为每秒可以读取或写入的数据量。随着单次 DMA 数据块大小的增加，磁盘访问效率提升，吞吐量也随之提升，但用户态驱动与内核态驱动在 DMA 数据块大小相同时，吞吐量非常接近。其原因在于用户态执行驱动程序并没有成为磁盘读写的性能瓶颈。
图 4-17 用户态与内核态串口数据发送时延4.7.4 综合吞吐量实验测量在综合环境下，框架对驱动吞吐量产生的影响。实验由两台计算机组成，辅助机向实验机串口中尽可能多地输出数据，通过测量实验验机内核态与用户态串口驱动每秒最大可接收的字符数，获得框架对驱动吞吐量带来的影响。实验结果如图 4-18 所示，试验中串口运行在波特率为 115200，数据位 8，停止位 1，无奇偶校验的状态下，理论最大吞吐量应为 12800char/s（即图中 baseline 一项）。由于串口控制器、中断响应与系统调用等额外负载，内核态驱动最大吞吐量为理论值的 89%，而用户态驱动的吞吐量与内核态相差 1%左右。
【参考文献】：
期刊论文
[1]嵌入式系统安全综述[J]. 赵波,倪明涛,石源,樊佩茹. 武汉大学学报(理学版). 2018(02)
[2]未来网络与工业互联网发展综述[J]. 吴文君,姚海鹏,黄韬,王露瑶,张延华,刘韵洁. 北京工业大学学报. 2017(02)
[3]基于可信计算基的主机可信安全体系结构研究[J]. 黄强,常乐,张德华,汪伦伟. 信息网络安全. 2016(07)
[4]关键基础设施信息安全分析及防护[J]. 刘松,朱钱祥,陈开放. 智慧工厂. 2016(03)
[5]嵌入式操作系统的形式化验证研究[J]. 陈丽蓉,李允,罗蕾. 计算机科学. 2015(08)
[6]设备驱动程序可靠性和正确性保障方法与技术研究进展[J]. 张一帆,黄超,欧建生,汤恩义,陈鑫. 软件学报. 2015(02)
[7]微内核中断机制的形式化设计与验证[J]. 李康杰,钱振江,黄皓. 计算机科学. 2013(03)
[8]操作系统对象语义模型（OSOSM）及形式化验证[J]. 钱振江,刘苇,黄皓. 计算机研究与发展. 2012(12)
[9]网卡驱动程序的用户态移植和优化[J]. 王燕飞,华蓓. 电子技术. 2012(08)
[10]用户态驱动框架的研究与实现[J]. 刘军卫,李曦,陈香兰,徐军. 计算机系统应用. 2011(11)
博士论文
[1]安全操作系统形式化设计与验证方法研究[D]. 钱振江.南京大学 2013
[2]面向目标代码的实时操作系统形式化验证方法研究[D]. 史建琦.华东师范大学 2012
[3]高可信嵌入式操作系统体系架构研究[D]. 杨霞.电子科技大学 2010
[4]基于模型检测的安全操作系统验证方法研究[D]. 程亮.中国科学技术大学 2009
硕士论文
[1]基于AUTOSAR的汽车电子操作系统及其应用的建模与分析[D]. 彭云辉.华东师范大学 2014
本文编号：2969767
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/2969767.html
