期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
5
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
基于函数式语义的循环和递归程序结构通用证明技术
1
作者
李希萌
王国辉
+2 位作者
张倩颖
施智平
关永
《软件学报》
EI
CSCD
北大核心
2023年第8期3686-3707,共22页
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明...
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.
展开更多
关键词
程序验证
大步操作语义
定理证明
Coq定理证明器
下载PDF
职称材料
可信执行环境软件侧信道攻击研究综述
被引量:
2
2
作者
杨帆
张倩颖
+1 位作者
施智平
关永
《软件学报》
EI
CSCD
北大核心
2023年第1期381-403,共23页
为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(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
软件侧信道攻击
下载PDF
职称材料
以太坊中间语言的可执行语义
被引量:
5
3
作者
韩宁
李希萌
+3 位作者
张倩颖
王国辉
施智平
关永
《软件学报》
EI
CSCD
北大核心
2021年第6期1717-1732,共16页
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以...
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
展开更多
关键词
智能合约
Yul语言
Isabelle/HOL
形式化语义
以太坊
下载PDF
职称材料
机器人碰撞检测方法形式化
被引量:
3
4
作者
陈善言
关永
+1 位作者
施智平
王国辉
《软件学报》
EI
CSCD
北大核心
2022年第6期2246-2263,共18页
为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以...
为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.
展开更多
关键词
机器人
碰撞检测
形式化方法
定理证明
HOL-Light
下载PDF
职称材料
基于精化的可信执行环境内存隔离机制验证
被引量:
2
5
作者
靳翠珍
张倩颖
+4 位作者
马雨薇
李希萌
王国辉
施智平
关永
《软件学报》
EI
CSCD
北大核心
2022年第6期2189-2207,共19页
可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其...
可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.
展开更多
关键词
TEE
内存隔离机制
形式化验证
精化关系
信息流安全性
下载PDF
职称材料
题名
基于函数式语义的循环和递归程序结构通用证明技术
1
作者
李希萌
王国辉
张倩颖
施智平
关永
机构
首都师范大学
信息工程学院
电子系统
可靠性
技术
北京市
重点
实验室
(
首都师范大学
)
北京
成像理论与
技术
高精尖创新中心(
首都师范大学
)
出处
《软件学报》
EI
CSCD
北大核心
2023年第8期3686-3707,共22页
基金
国家重点研发计划(2019YFB1309900)
国家自然科学基金(61876111,61877040,62002246)
北京市教育委员会科技计划(KM201910028005,KM202010028010)。
文摘
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.
关键词
程序验证
大步操作语义
定理证明
Coq定理证明器
Keywords
program verification
big-step operational semantics
theorem proving
Coq proof assistant
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
可信执行环境软件侧信道攻击研究综述
被引量:
2
2
作者
杨帆
张倩颖
施智平
关永
机构
首都师范大学
信息工程学院
高
可靠
嵌入式
系统
北京市
工程研究中心(
首都师范大学
)
计算机体系结构国家
重点
实验室
(中国科学院计算
技术
研究所)
电子系统
可靠性
技术
北京市
重点
实验室
(
首都师范大学
)
北京
成像理论与
技术
高精尖创新中心(
首都师范大学
)
出处
《软件学报》
EI
CSCD
北大核心
2023年第1期381-403,共23页
基金
国家自然科学基金(61802375,61602325,61876111,61877040)
北京市教委科技计划一般项目(KM201910028005)
+1 种基金
中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)
交叉科学研究院项目(19530012005)。
文摘
为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(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
软件侧信道攻击
Keywords
trusted execution environment(TEE)
isolation architecture
ARM TrustZone
Intel SGX
AMD SEV
software side-channel attack
分类号
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
以太坊中间语言的可执行语义
被引量:
5
3
作者
韩宁
李希萌
张倩颖
王国辉
施智平
关永
机构
首都师范大学
信息工程学院
电子系统
可靠性
技术
北京市
重点
实验室
(
首都师范大学
)
北京
成像理论与
技术
高精尖创新中心(
首都师范大学
)
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1717-1732,共16页
基金
国家自然科学基金(61572331,61602325,61802375,61876111,61877040,62002246)
北京市教育委员会科技计划(KM20190028005,KM202010028010)
中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)。
文摘
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
关键词
智能合约
Yul语言
Isabelle/HOL
形式化语义
以太坊
Keywords
smart contract
Yul language
Isabelle/HOL
formal semantics
Ethereum
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
机器人碰撞检测方法形式化
被引量:
3
4
作者
陈善言
关永
施智平
王国辉
机构
首都师范大学
信息工程学院
电子系统
可靠性
与数理交叉学科国家国际科技合作示范型基地(
首都师范大学
)
轻型工业机器人与安全验证
北京市
重点
实验室
(
首都师范大学
)
电子系统
可靠性
技术
北京市
重点
实验室
(
首都师范大学
)
高
可靠
嵌入式
系统
北京市
工程研究中心(
首都师范大学
)
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2246-2263,共18页
基金
国家重点研发计划(2019YFB1309900)
国家自然科学基金(61876111,61877040,62002246)
+2 种基金
特区项目(18-163-11-ZT-005-038-05)
北京市教委科技计划(KM201910028005,KM202010028010)
中央支持地方建设——“双一流”建设项目(20531120005)。
文摘
为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.
关键词
机器人
碰撞检测
形式化方法
定理证明
HOL-Light
Keywords
robotics
collision detection
formal method
theorem proving
HOL-Light
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于精化的可信执行环境内存隔离机制验证
被引量:
2
5
作者
靳翠珍
张倩颖
马雨薇
李希萌
王国辉
施智平
关永
机构
首都师范大学
信息工程学院
高
可靠
嵌入式
系统
北京市
工程研究中心(
首都师范大学
)
计算机体系结构国家
重点
实验室
(中国科学院计算
技术
研究所)
电子系统
可靠性
技术
北京市
重点
实验室
(
首都师范大学
)
电子系统
可靠性
与数理交叉学科国家国际科技合作示范型基地(
首都师范大学
)
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2189-2207,共19页
基金
国家自然科学基金(61802375,61602325,61876111,61877040,62002246)
北京市教委科技计划(KM201910028005,KM202010028010)
+1 种基金
中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)
中央支持地方建设-“双一流”建设项目(20531120005)。
文摘
可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.
关键词
TEE
内存隔离机制
形式化验证
精化关系
信息流安全性
Keywords
TEE
memory isolation mechanism
formal verification
refinement relation
information flow security
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
基于函数式语义的循环和递归程序结构通用证明技术
李希萌
王国辉
张倩颖
施智平
关永
《软件学报》
EI
CSCD
北大核心
2023
0
下载PDF
职称材料
2
可信执行环境软件侧信道攻击研究综述
杨帆
张倩颖
施智平
关永
《软件学报》
EI
CSCD
北大核心
2023
2
下载PDF
职称材料
3
以太坊中间语言的可执行语义
韩宁
李希萌
张倩颖
王国辉
施智平
关永
《软件学报》
EI
CSCD
北大核心
2021
5
下载PDF
职称材料
4
机器人碰撞检测方法形式化
陈善言
关永
施智平
王国辉
《软件学报》
EI
CSCD
北大核心
2022
3
下载PDF
职称材料
5
基于精化的可信执行环境内存隔离机制验证
靳翠珍
张倩颖
马雨薇
李希萌
王国辉
施智平
关永
《软件学报》
EI
CSCD
北大核心
2022
2
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部