检索结果-内蒙古大学图书馆

软件学报 2023年第1期34卷 381-403页

作者：杨帆张倩颖施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048 计算机体系结构国家重点实验室(中国科学院计算技术研究所) 北京100190 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048

为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状... 详细信息

为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状态就能通过软件方式获取机密信息的访问模式,从而进一步推测出机密信息.TEE架构仅提供隔离机制,无法抵抗这类新出现的软件侧信道攻击.深入调研了ARM TrustZone、Intel SGX和AMD SEV这3种TEE架构的软件侧信道攻击及相应防御措施,并探讨其攻击和防御机制的发展趋势.首先,介绍了ARM TrustZone、Intel SGX和AMD SEV的基本原理,并详细阐述了软件侧信道攻击的定义以及缓存侧信道攻击的分类、方法和步骤;之后从处理器指令执行的角度,提出一种TEE攻击面分类方法,利用该方法对TEE软件侧信道攻击进行分类,并阐述了软件侧信道攻击与其他攻击相结合的组合攻击;然后详细讨论TEE软件侧信道攻击的威胁模型;最后全面总结业界对TEE软件侧信道攻击的防御措施,并从攻击和防御两方面探讨TEE软件侧信道攻击未来的研究趋势.

关键词：可信执行环境(TEE) 隔离架构 ARM TrustZone Intel SGX AMD SEV 软件侧信道攻击

来源：评论

学校读者我要写书评

暂无评论

机器人碰撞检测方法形式化

引用

软件学报 2022年第6期33卷 2246-2263页

作者：陈善言关永施智平王国辉首都师范大学信息工程学院北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048 轻型工业机器人与安全验证北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以... 详细信息

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

关键词：机器人碰撞检测形式化方法定理证明 HOL-Light

来源：评论

学校读者我要写书评

暂无评论

基于精化的可信执行环境内存隔离机制验证

引用

软件学报 2022年第6期33卷 2189-2207页

作者：靳翠珍张倩颖马雨薇李希萌王国辉施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048 计算机体系结构国家重点实验室(中国科学院计算技术研究所) 北京100190 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其... 详细信息

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

关键词： TEE 内存隔离机制形式化验证精化关系信息流安全性

来源：评论

学校读者我要写书评

暂无评论

TrustZone中断隔离机制的形式化验证

引用

小型微型计算机系统 2023年第9期44卷 2105-2112页

作者：付俊仪张倩颖王国辉李希萌施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心北京100048 中国科学院计算技术研究所计算机体系结构国家重点实验室北京100190 电子系统可靠性技术北京市重点实验室北京100048 北京成像理论与技术高精尖创新中心北京100048

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断... 详细信息

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.

关键词： TrustZone 可信执行环境中断隔离信息流安全形式化验证

来源：评论

学校读者我要写书评

暂无评论

CAN网络层次化动态调度策略设计与实现

引用

小型微型计算机系统 2022年第6期43卷 1141-1146页

作者：邵椿与李晓娟史涤霏张笑搏王瑞关永首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室北京100048 首都师范大学燕都学院北京100048

CAN总线是一种基于消息的事件触发通信服务,主要应用于汽车、机器人等实时通信系统.CAN总线上有多个节点互相独立工作,当多个节点访问总线时出现消息碰撞,由于CAN总线采用按位仲裁算法决定节点访问总线的优先级,导致低优先级节点访问失... 详细信息

CAN总线是一种基于消息的事件触发通信服务,主要应用于汽车、机器人等实时通信系统.CAN总线上有多个节点互相独立工作,当多个节点访问总线时出现消息碰撞,由于CAN总线采用按位仲裁算法决定节点访问总线的优先级,导致低优先级节点访问失败,而高优先级节点继续传输消息,这种方式导致低优先级节点饥饿现象而丢失消息,因此CAN总线调度算法随之被提出.目前调度策略已从静态发展到动态,但是随着节点的增多,系统维护和调度难度增加,单条总线调度策略难以维持系统性能需要.因此本文考虑将系统中的节点挂载到多条CAN总线上构成CAN网络,针对CAN网络提出了一种层次化的动态调度算法,将节点优先级仲裁分为:单条总线本地优先级仲裁和系统全局优先级仲裁,确定系统优先级最高的节点,使其进行数据传输.利用MATLAB中的Stateflow工具,建立分层动态调度模型,依据CAN总线数据传输机制和仲裁机制,设计实现了节点模块、总线模块、函数模块等,在总线模块实现了两级调度.实验结果表明,本算法在增加了节点总数目的基础上,满足高优先级节点传输且避免了低优先级节点的饿死现象.

关键词： CAN总线两级仲裁层次化动态调度 Stateflow建模

来源：评论

学校读者我要写书评

暂无评论

抗板级物理攻击的持久存储方法研究

引用

计算机工程 2022年第2期48卷 132-139页

作者：李闽张倩颖王国辉施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心北京100048 中国科学院计算技术研究所计算机体系结构国家重点实验室北京100190 电子系统可靠性技术北京市重点实验室北京100048 北京成像理论与技术高精尖创新中心北京100048

为保护文件系统的安全性,提出一种抗板级物理攻击的持久存储方法。利用ARM TrustZone技术构建持久存储架构,实现内存保护机制和持久存储保护服务,提高文件系统的物理安全性。基于片上内存(OCM)在可信执行环境(TEE)中的内核层建立内存保... 详细信息

为保护文件系统的安全性,提出一种抗板级物理攻击的持久存储方法。利用ARM TrustZone技术构建持久存储架构,实现内存保护机制和持久存储保护服务,提高文件系统的物理安全性。基于片上内存(OCM)在可信执行环境(TEE)中的内核层建立内存保护机制,保证TEE的可信应用能够抵抗板级物理攻击。基于TEE的内存保护机制实现保护文件系统中敏感数据的持久存储保护服务,确保文件系统的机密性和完整性。在物理开发板上实现持久存储架构的原型系统,使用基准测试工具对原型系统进行性能评估,并分析性能损耗的原因。测试结果表明,内存保护机制在保护TEE系统物理安全性时引入的时间开销会随着OCM的增大而减小,持久存储保护服务在保护数据量较小的敏感数据时产生的时间开销在用户可接受范围内。

关键词： ARM TrustZone技术可信执行环境板级物理攻击片上内存持久存储保护

来源：评论

学校读者我要写书评

暂无评论

COVID-19医学影像数据集及研究进展

引用

计算机工程与应用 2021年第22期57卷 15-27页

作者：刘锐丁辉尚媛园邵珠宏刘铁首都师范大学信息工程学院北京100048 成像技术北京市高精尖创新中心北京100048 高可靠嵌入式系统技术北京市工程研究中心北京100048 电子系统可靠性技术北京市重点实验室北京100048

由于影像学技术在新型冠状病毒肺炎(COVID-19)的诊断和评估中发挥了重要作用,COVID-19相关数据集陆续被公布,但目前针对相关文献中数据集以及研究进展的整理相对较少。为此,通过COVID-19相关的期刊论文、报告和相关开源数据集网站,对涉... 详细信息

由于影像学技术在新型冠状病毒肺炎(COVID-19)的诊断和评估中发挥了重要作用,COVID-19相关数据集陆续被公布,但目前针对相关文献中数据集以及研究进展的整理相对较少。为此,通过COVID-19相关的期刊论文、报告和相关开源数据集网站,对涉及到的新冠肺炎数据集及深度学习模型进行整理和分析,包括计算机断层扫描(CT)图像数据集和X射线(CXR)图像数据集。对这些数据集呈现的医学影像的特征进行分析;重点论述开源数据集,以及在相关数据集上表现较好的分类和分割模型。最后讨论了肺部影像学技术未来的发展趋势。

关键词： COVID-19数据集深度学习图像分割图像分类

来源：评论

学校读者我要写书评

暂无评论

一种考虑温度和电压的超级电容寿命预测方法

引用

电源技术 2018年第1期42卷 90-92,96页

作者：吴立锋单金生关永王洪民首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室北京100048

介绍了超级电容的退化特征,阐释了影响其寿命衰减的因素,比较了各因素在超级电容退化过程中的作用,重点阐述了退化因素中环境温度和使用电压对超级电容寿命的影响。提出了基于现有的寿命数据或者经验法则,对工作在不同温度和电压下的超... 详细信息

介绍了超级电容的退化特征,阐释了影响其寿命衰减的因素,比较了各因素在超级电容退化过程中的作用,重点阐述了退化因素中环境温度和使用电压对超级电容寿命的影响。提出了基于现有的寿命数据或者经验法则,对工作在不同温度和电压下的超级电容寿命的预测方法,并把这种方法应用于对超级电容退化特征参数的预测,为超级电容的合理使用提供参考依据。

关键词：超级电容退化寿命预测

来源：评论

学校读者我要写书评

暂无评论

Nuttx操作系统进程切换调度实时性的形式化验证

引用

计算机应用与软件 2018年第7期35卷 15-20,51页

作者：郝英华王瑞李晓娟首都师范大学信息工程学院北京100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室北京100048

随着工业机器人的发展,实时性操作系统在工业控制领域的地位越来越重要。实时调度对实时操作系统的实时性有重要影响,是提高系统实时性的关键技术。Nuttx操作系统就是一个实时操作系统,它有三种调度策略:先来先服务、时间片轮转法以及... 详细信息

随着工业机器人的发展,实时性操作系统在工业控制领域的地位越来越重要。实时调度对实时操作系统的实时性有重要影响,是提高系统实时性的关键技术。Nuttx操作系统就是一个实时操作系统,它有三种调度策略:先来先服务、时间片轮转法以及零星调度。首次提出对以上三种调度策略进行切换,使得任务到达时能够根据自身的特点去选择适合自己的调度策略,以便得到更快的响应。对切换策略建立时间自动机模型;用计算树逻辑公式对实时性进行了形式化描述;在模型检测工具时间自动机Uppaal中进行了验证。结果表明该切换策略能够使任务在规定的时间内更好地完成操作,满足了系统的实时性。

关键词：工业机器人实时调度 Nuttx操作系统切换实时性时间自动机Uppaal

来源：评论

学校读者我要写书评

暂无评论

基于排队论的UM-BUS总线性能建模与评估

引用

计算机科学 2017年第S1期44卷 504-509页

作者：张少楠邱柯妮张伟功王晶郑佳欣白瑞英朱晓燕首都师范大学信息工程学院北京100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心北京100048 北京成像技术高精尖创新中心北京100048 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

UM-BUS总线是一种具有动态容错能力和远程穿透式访问能力的高速串行总线,其性能模型对UM-BUS的综合评估和优化设计具有重要意义。针对UM-BUS总线系统,提出基于排队论的性能评估的模型,该模型定性描述了总线上不同节点之间的数据流关系... 详细信息

UM-BUS总线是一种具有动态容错能力和远程穿透式访问能力的高速串行总线,其性能模型对UM-BUS的综合评估和优化设计具有重要意义。针对UM-BUS总线系统,提出基于排队论的性能评估的模型,该模型定性描述了总线上不同节点之间的数据流关系、数据包到达节点的特征以及在节点处等待处理的特性;定量分析了不同数据包在总线信道传输的最大延迟、最小延迟以及平均延迟。在MATLAB平台上测试了数据包在总线上的等待时间和传输时间。实验结果可以帮助设计者快速分析总线在实际应用系统中的特性并对其进行优化配置,提高总线的使用效率。

关键词： UM-BUS总线排队论性能建模传输延迟

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：