期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
2
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
Petri网的反向展开及其在程序数据竞争检测的应用
被引量:
3
1
作者
郝宗寅
鲁法明
《软件学报》
EI
CSCD
北大核心
2021年第6期1612-1630,共19页
展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的...
展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明:当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,对影响反向展开效率的关键因素做了分析与总结.
展开更多
关键词
PETRI网
可覆盖性判定
反向
展开
启发式优化
数据竞争检测
下载PDF
职称材料
目标导向的多线程程序UAF漏洞预测方法
2
作者
鲁法明
唐梦凡
+2 位作者
包云霞
曾庆田
李彦成
《软件学报》
EI
CSCD
北大核心
2023年第7期3043-3063,共21页
Use-after-free(UAF)漏洞是多线程程序的常见并发缺陷.预测性UAF漏洞检测方法因兼顾误报率和漏报率而备受关注.然而,已有的预测性UAF检测方法未结合待检测目标作针对性优化,当程序规模大或行为复杂时会导致检测效率低下.为了解决上述问...
Use-after-free(UAF)漏洞是多线程程序的常见并发缺陷.预测性UAF漏洞检测方法因兼顾误报率和漏报率而备受关注.然而,已有的预测性UAF检测方法未结合待检测目标作针对性优化,当程序规模大或行为复杂时会导致检测效率低下.为了解决上述问题,提出一种目标导向的多线程程序UAF漏洞检测方法.首先,由程序运行轨迹挖掘程序的Petri网模型;之后,针对每一个潜在可构成UAF漏洞的内存Free/Use操作对,以触发该漏洞为目标导向,在程序的Petri网模型中添加保持操作间因果约束和数据一致性的行为控制结构;在此基础上,设计了一种基于Petri网反向展开的UAF漏洞检测方法.该方法每次只针对1个潜在的UAF漏洞,有针对性地验证其真实性,从而保证检测的效率.与此同时,为了减少待检测的潜在UAF漏洞数量,提出了一种新型向量时钟进行Free操作与Use操作间的因果关系自动识别,据此对潜在的UAF漏洞进行筛选.结合多个程序实例对所提方法进行了实验评估.实验结果表明,所提方法在检测的效率和准确性方面较主流方法有所提高.
展开更多
关键词
软件验证
并发漏洞
PETRI网
UAF漏洞
反向
展开
下载PDF
职称材料
题名
Petri网的反向展开及其在程序数据竞争检测的应用
被引量:
3
1
作者
郝宗寅
鲁法明
机构
山东科技大学计算机科学与工程学院
厦门大学信息学院
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1612-1630,共19页
基金
国家自然科学基金(61602279,61472229)
国家重点研发计划(2016YFC0801406)
+5 种基金
山东省泰山学者工程专项基金(ts20190936)
山东省高等学校青创科技支持计划(2019KJN024)
山东省博士后创新专项基金(201603056)
鲁渝科技协作计划(cstc2020jscx-lyjsAX0008)
国家海洋局海洋遥测工程技术研究中心开放基金(2018002)
山东科技大学领军人才与优秀科研创新团队项目(2015TDJH102)。
文摘
展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明:当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,对影响反向展开效率的关键因素做了分析与总结.
关键词
PETRI网
可覆盖性判定
反向
展开
启发式优化
数据竞争检测
Keywords
Petri net
coverability determination
reverse unfolding
heuristic optimization
data race detection
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
目标导向的多线程程序UAF漏洞预测方法
2
作者
鲁法明
唐梦凡
包云霞
曾庆田
李彦成
机构
山东科技大学计算机科学与工程学院
山东科技大学数学与系统科学学院
百度在线网络技术(北京)有限公司
出处
《软件学报》
EI
CSCD
北大核心
2023年第7期3043-3063,共21页
基金
国家自然科学基金(61602279)
山东省泰山学者工程专项基金(ts20190936)
+2 种基金
山东省高等学校青创科技支持计划(2019KJN024)
山东省自然科学基金智慧计算联合基金(ZR2021LZH004)
青岛市西海岸新区2022年“揭榜挂帅”技术攻关项目。
文摘
Use-after-free(UAF)漏洞是多线程程序的常见并发缺陷.预测性UAF漏洞检测方法因兼顾误报率和漏报率而备受关注.然而,已有的预测性UAF检测方法未结合待检测目标作针对性优化,当程序规模大或行为复杂时会导致检测效率低下.为了解决上述问题,提出一种目标导向的多线程程序UAF漏洞检测方法.首先,由程序运行轨迹挖掘程序的Petri网模型;之后,针对每一个潜在可构成UAF漏洞的内存Free/Use操作对,以触发该漏洞为目标导向,在程序的Petri网模型中添加保持操作间因果约束和数据一致性的行为控制结构;在此基础上,设计了一种基于Petri网反向展开的UAF漏洞检测方法.该方法每次只针对1个潜在的UAF漏洞,有针对性地验证其真实性,从而保证检测的效率.与此同时,为了减少待检测的潜在UAF漏洞数量,提出了一种新型向量时钟进行Free操作与Use操作间的因果关系自动识别,据此对潜在的UAF漏洞进行筛选.结合多个程序实例对所提方法进行了实验评估.实验结果表明,所提方法在检测的效率和准确性方面较主流方法有所提高.
关键词
软件验证
并发漏洞
PETRI网
UAF漏洞
反向
展开
Keywords
software verification
concurrency vulnerability
Petri net
UAF vulnerability
reverse unfolding
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
Petri网的反向展开及其在程序数据竞争检测的应用
郝宗寅
鲁法明
《软件学报》
EI
CSCD
北大核心
2021
3
下载PDF
职称材料
2
目标导向的多线程程序UAF漏洞预测方法
鲁法明
唐梦凡
包云霞
曾庆田
李彦成
《软件学报》
EI
CSCD
北大核心
2023
0
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部