张倩颖

作品数：20被引量：89H指数：6
导出分析报告
供职机构：首都师范大学更多>>
发文主题：逻辑命题定理证明器形式化验证逻辑语言机器人更多>>
发文领域：自动化与计算机技术文化科学更多>>
发文期刊：《电子学报》《中国图象图形学报》《通信学报》《小型微型计算机系统》更多>>
所获基金：国家自然科学基金国家重点实验室开放基金国家重点基础研究发展计划中央级公益性科研院所基本科研业务费专项更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
微内核操作系统互斥量模块功能正确性的形式化验证
《软件学报》2024年第9期4179-4192,共14页张林雁 李希萌 施智平 关永 曹钦翔 张倩颖 
国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测...
关键词：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器 
TrustZone中断隔离机制的形式化验证被引量：1
《小型微型计算机系统》2023年第9期2105-2112,共8页付俊仪 张倩颖 王国辉 李希萌 施智平 关永 
国家自然科学基金项目(61802375,61602325,61876111,61877040)资助;北京市教委科技计划一般项目(KM201910028005)资助;中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题项目(CARCH201920)资助;国防科技创新特区项目(18-163-11-ZT-005-038-05)资助;中央支持地方建设-“双一流”建设项目(20531120005)资助.
TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断...
关键词：TRUSTZONE 可信执行环境 中断隔离 信息流安全 形式化验证 
基于函数式语义的循环和递归程序结构通用证明技术
《软件学报》2023年第8期3686-3707,共22页李希萌 王国辉 张倩颖 施智平 关永 
国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)。
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明...
关键词：程序验证 大步操作语义 定理证明 Coq定理证明器 
可信执行环境软件侧信道攻击研究综述被引量：10
《软件学报》2023年第1期381-403,共23页杨帆 张倩颖 施智平 关永 
国家自然科学基金(61802375,61602325,61876111,61877040);北京市教委科技计划一般项目(KM201910028005);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920);交叉科学研究院项目(19530012005)。
为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状...
关键词：可信执行环境(TEE) 隔离架构 ARM TrustZone Intel SGX AMD SEV 软件侧信道攻击 
基于精化的可信执行环境内存隔离机制验证被引量：5
《软件学报》2022年第6期2189-2207,共19页靳翠珍 张倩颖 马雨薇 李希萌 王国辉 施智平 关永 
国家自然科学基金(61802375,61602325,61876111,61877040,62002246);北京市教委科技计划(KM201910028005,KM202010028010);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920);中央支持地方建设-“双一流”建设项目(20531120005)。
可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其...
关键词：TEE 内存隔离机制 形式化验证 精化关系 信息流安全性 
群机器人区域覆盖算法高阶逻辑建模与验证
《小型微型计算机系统》2022年第3期475-482,共8页尹晓娜 王国辉 施智平 关永 张倩颖 张景芝 
国家重点研发计划项目(2019YFB1309900)资助;国家自然科学基金项目(61876111,61877040,62002246)资助;特区项目(18-163-11-ZT-005-038-05)资助;北京市教委科技计划一般项目(KM20190028005)资助;科技创新服务能力建设-基本科研业务费(科研费)项目(00621530290000)资助。
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用...
关键词：群机器人 区域覆盖 高阶逻辑 定理证明 形式化验证 
抗板级物理攻击的持久存储方法研究被引量：2
《计算机工程》2022年第2期132-139,共8页李闽 张倩颖 王国辉 施智平 关永 
国家自然科学基金(61802375,61602325,61876111,61877040);北京市教委科技计划一般项目(KM201910028005);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920);首都师范大学交叉科学研究院项目(19530012005)。
为保护文件系统的安全性,提出一种抗板级物理攻击的持久存储方法。利用ARM TrustZone技术构建持久存储架构,实现内存保护机制和持久存储保护服务,提高文件系统的物理安全性。基于片上内存(OCM)在可信执行环境(TEE)中的内核层建立内存保...
关键词：ARM TrustZone技术 可信执行环境 板级物理攻击 片上内存 持久存储保护 
协作机器人逆运动学形式化建模与验证被引量：2
《小型微型计算机系统》2021年第7期1353-1359,共7页王畅 王国辉 施智平 关永 张倩颖 邵振洲 
国家重点研发计划项目(2019YFB1309900)资助;国家自然科学基金项目(61876111,61877040,62002246)资助;特区项目(18-163-11-ZT-005-038-05)资助;北京市教委科技计划一般项目(KM20190028005)资助;科技创新服务能力建设-基本科研业务费(科研费)项目(006195305000)资助。
在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,...
关键词：机器人逆运动学 旋量 Paden-Kahan子问题 HOL-Light 形式化验证 
以太坊中间语言的可执行语义被引量：5
《软件学报》2021年第6期1717-1732,共16页韩宁 李希萌 张倩颖 王国辉 施智平 关永 
国家自然科学基金(61572331,61602325,61802375,61876111,61877040,62002246);北京市教育委员会科技计划(KM20190028005,KM202010028010);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)。
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以...
关键词：智能合约 Yul语言 Isabelle/HOL 形式化语义 以太坊 
抗电路板级物理攻击的操作系统防御技术研究被引量：3
《软件学报》2020年第10期3120-3146,共27页张倩颖 赵世军 
国家自然科学基金(61802375,61602325,61876111,61877040);北京市教委科技计划一般项目(KM20190028005);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)。
计算设备处理和存储日益增多的敏感信息,如口令和指纹信息等,对安全性提出更高要求.物理攻击技术的发展催生了一种通过攻击电路板级硬件组件来获取操作系统机密信息的攻击方法:电路板级物理攻击.该类攻击具有工具简单、成本低、易流程...
关键词：内存保护 物理攻击 内存加密 内存完整性 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部