Rust语言安全研究综述 被引量：1

1

作者 胡霜 华保健 +1 位作者 欧阳婉容 樊淇梁 《信息安全学报》 CSCD 2023年第6期64-83,共20页

Rust是为了解决系统编程领域的安全性问题,而设计的一门面向系统编程的兼具类型安全、内存安全和并发安全的新型程序设计语言,强调安全性和高性能,已经在操作系统内核、Web浏览器、网络协议栈、数据库和区块链等底层软件系统的构建中得... Rust是为了解决系统编程领域的安全性问题,而设计的一门面向系统编程的兼具类型安全、内存安全和并发安全的新型程序设计语言,强调安全性和高性能,已经在操作系统内核、Web浏览器、网络协议栈、数据库和区块链等底层软件系统的构建中得到了越来越广泛的应用。现有研究表明,尽管Rust的设计目标是保证安全性,但其自身仍然存在许多安全问题。作为一门系统编程语言,Rust的安全性直接影响到基于Rust开发的软件系统的安全性。随着Rust的广泛应用,对Rust语言安全的研究显得尤为重要。Rust语言安全研究正在成为研究热点,并且在近几年已经取得了较大研究进展。本综述基于该研究领域已经公开发表的46篇研究论文,对该领域的相关研究进行了系统整理、分析和总结:首先,研究分析了Rust的核心安全特性,包括函数式编程范式、强多态类型系统、基于所有权模型的自动内存管理、对非安全代码的显式标记和隔离;其次,提出了Rust语言安全研究领域的分类学,将已有研究分为安全实证研究、漏洞检测研究、安全增强研究和形式化验证研究四个热点方向,并分别对这四个方向上的相关研究进行了综述、深入分析和总结,同时分析了四个研究方向的内在联系;最后,指出了该研究领域的待解决的科学问题,并对未来可能的研究方向进行了展望,提出了四个潜在的研究方向,以期为相关领域的研究者提供有价值的参考。 展开更多

关键词 Rust语言 内存安全 并发安全 漏洞检测与修复

下载PDF 职称材料

融合循环划分的张量指令生成优化

2

作者 梁佳利 华保健 苏少博 《计算机科学》 CSCD 北大核心 2023年第2期374-383,共10页

张量编译器支持将算子的张量描述和计算调度编译为目标硬件的代码。为加速张量运算,深度学习领域专用处理器被设计为包含特殊指令的专有架构,支持多核并行、多级专用内存架构和张量计算,在硬件之上还有与硬件特性紧密相关的张量指令集... 张量编译器支持将算子的张量描述和计算调度编译为目标硬件的代码。为加速张量运算,深度学习领域专用处理器被设计为包含特殊指令的专有架构,支持多核并行、多级专用内存架构和张量计算,在硬件之上还有与硬件特性紧密相关的张量指令集。在这样复杂的架构上,张量指令的使用有着许多约束与限制,并存在以下问题和挑战:首先,因计算任务划分或数据切块等循环分段引入的条件分支增加了模式匹配难度;其次,张量指令有对齐、数据布局等硬件约束。针对上述问题和挑战,提出了一种融合循环划分的张量指令生成优化算法。算法通过划分循环区间,来消除因任务划分或数据切分引入的条件分支;通过补零、等价指令替换和添加额外计算来解决指令和硬件约束;并使用模式匹配的方法生成张量指令。研究并扩展开源深度学习编译器TVM 0.7版本,实现了支持DianNao架构机器学习加速器的张量指令生成的编译器原型系统。为评测算法的有效性,在DianNao架构机器学习加速器硬件平台上,对逐元素二元张量操作算子、原地一元张量操作算子和卷积操作算子3类算子的性能和开发效率进行了测试,实验结果表明3类算子性能平均加速比为125.00%,最大加速比为194.00%,开发效率最高提升了7倍。 展开更多

关键词 深度学习 张量编译器 领域专用处理器 张量化 循环划分

下载PDF 职称材料

面向深度学习算子的循环不变式外提算法

3

作者 梁佳利 华保健 +1 位作者 吕雅帅 苏振宇 《计算机科学与探索》 CSCD 北大核心 2023年第1期127-139,共13页

TVM是一个深度学习编译器,支持将TVM的领域专用语言即张量表达式定义的算子编译生成目标平台的代码,并在高级中间表示TVM IR上进行一系列优化。张量表达式对算子执行循环变换,产生与循环迭代变量相关的复杂表达式的计算,在多层嵌套循环... TVM是一个深度学习编译器,支持将TVM的领域专用语言即张量表达式定义的算子编译生成目标平台的代码,并在高级中间表示TVM IR上进行一系列优化。张量表达式对算子执行循环变换,产生与循环迭代变量相关的复杂表达式的计算,在多层嵌套循环内这些计算包含了大量的循环不变式。然而,传统的循环不变量外提技术不能判断不变量外提是否能带来额外收益,无法发现操作数顺序不同的循环不变表达式,不能处理嵌套的条件表达式,并且与目标平台编译器优化存在冲突等。由于这些挑战,传统的循环不变量外提算法无法直接用于深度学习编译器的优化,提出了一种融合深度学习代价函数和启发式策略的循环不变量外提算法。该算法基于深度学习编译器的高层中间表示,通过调整操作数顺序和简化嵌套条件表达式等方法规范化表达式。为了衡量优化的收益,在结合TVM IR和目标平台的特点的基础上,提出了一个新的面向深度学习的不变式外提代价指标函数。在开源编译器TVM 0.7版本上,通过新增优化遍的形式,具体实现了所介绍的算法以及代价函数。为评测算法的有效性,在Tesla P4的图形处理器(GPU)平台上对TVM TOPI的测试算子集中27个典型算子不同输入规模的511个测例进行了测试。实验结果表明47.6%的算子性能得到提升,最大加速比大于40.0%。 展开更多

关键词 深度学习编译器 领域专用语言 循环不变量外提 中间表示

下载PDF 职称材料

Android内核钩子的混合检测技术 被引量：2

4

作者 华保健 周艾亭 朱洪军 《计算机应用》 CSCD 北大核心 2014年第11期3336-3339,3343,共5页

针对Android平台上内核级钩子检测的研究,提出了一种结合基于特征模式的静态检测技术和基于行为分析的动态检测技术的Android内核钩子检测技术,这两种技术的结合能够检测基于修改系统调用表项的攻击和基于内联钩子的攻击。为所提技术构... 针对Android平台上内核级钩子检测的研究,提出了一种结合基于特征模式的静态检测技术和基于行为分析的动态检测技术的Android内核钩子检测技术,这两种技术的结合能够检测基于修改系统调用表项的攻击和基于内联钩子的攻击。为所提技术构建了软件原型系统并进行了实验评测,实验结果表明,提出的技术能够针对Android内核钩作出精确检测,并且运行时间开销在7%以内,具有良好运行效率,能够适用于Android内核钩子的混合。 展开更多

关键词 ANDROID LINUX 内核 检测系统 软件原型

下载PDF 职称材料

基于面向对象技术的编译原理课程建设 被引量：2

5

作者 华保健 《计算机教育》 2014年第18期67-70,共4页

面向对象编程语言和技术日益流行,已经成为最重要的编程框架,这一趋势对编译原理课程建设和教学改革实践提出新的挑战。文章根据最新研究趋势和教学需求,对编译原理课程改革和建设进行探讨,以中国科学技术大学软件学院为例,阐述在高等... 面向对象编程语言和技术日益流行,已经成为最重要的编程框架,这一趋势对编译原理课程建设和教学改革实践提出新的挑战。文章根据最新研究趋势和教学需求,对编译原理课程改革和建设进行探讨,以中国科学技术大学软件学院为例,阐述在高等院校计算机相关专业中进行教学改革的实践,为课程改革建设提供新思路。 展开更多

关键词 面向对象技术 编译原理 字节码 垃圾回收 编译优化 虚拟机技术

下载PDF 职称材料

一种命令式风格的面向对象语言语义框架

6

作者 华保健 高鹰 《计算机科学》 CSCD 北大核心 2013年第2期159-162,共4页

面向对象语言在软件工程实践中有着广泛的应用。为面向对象语言定义严格的语义有助于理解面向对象语言的本质特征,对验证软件、提高软件系统可靠性等也具有重要意义。给出了一种新的面向对象语言的语义框架,该框架基于命令式的风格,具... 面向对象语言在软件工程实践中有着广泛的应用。为面向对象语言定义严格的语义有助于理解面向对象语言的本质特征,对验证软件、提高软件系统可靠性等也具有重要意义。给出了一种新的面向对象语言的语义框架,该框架基于命令式的风格,具有操作语义和类型规则;证明了该语义框架的类型安全定理。 展开更多

关键词 面向对象语言 类型系统 操作语义 语义框架

下载PDF 职称材料

安全语言PointerC的设计及形式证明 被引量：8

7

作者 华保健 陈意云 +3 位作者 李兆鹏 王志芳 葛琳 江苏苏州215123 《计算机学报》 EI CSCD 北大核心 2008年第4期556-564,共9页

程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(sid... 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的. 展开更多

关键词 软件安全 语言设计 类型系统 HOARE逻辑 指针逻辑

下载PDF 职称材料

形式化方法类课程设置及教学内容探索

8

作者 华保健 樊淇梁 潘志中 《计算机教育》 2022年第6期213-216,共4页

分析目前计算机和软件工程专业形式化方法类课程的现状,并根据软件工程发展形势的最新要求以及课程体系与ACM/IEEE CS2013计算机科学课程体系规范中知识主体的对应关系,指出现行课程体系的可改进之处,阐述重新构建形式化方法类课程体系... 分析目前计算机和软件工程专业形式化方法类课程的现状,并根据软件工程发展形势的最新要求以及课程体系与ACM/IEEE CS2013计算机科学课程体系规范中知识主体的对应关系,指出现行课程体系的可改进之处,阐述重新构建形式化方法类课程体系的可行途径. 展开更多

关键词 形式化方法 编程语言 软件可靠性

下载PDF 职称材料

一种用于指针程序安全性证明的指针逻辑 被引量：20

9

作者 陈意云 华保健 +1 位作者 葛琳 王志芳 《计算机学报》 EI CSCD 北大核心 2008年第3期372-380,共9页

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,... 在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质. 展开更多

关键词 软件安全 指针逻辑 HOARE逻辑 指针分析 类型系统

下载PDF 职称材料

一种用于指针程序验证的指针逻辑 被引量：6

10

作者 陈意云 李兆鹏 +1 位作者 王志芳 华保健 《软件学报》 EI CSCD 北大核心 2010年第3期415-426,共12页

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便... 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合. 展开更多

关键词 软件安全 HOARE逻辑 指针逻辑 携带证明的代码 出具证明的编译器

下载PDF 职称材料

移动应用代码保护现状与技术研究 被引量：5

11

作者 朱洪军 陈灏 +2 位作者 华保健 刘业 郭宇 《计算机应用与软件》 CSCD 2016年第3期314-319,333,共7页

基于安卓平台应用极易被病毒或恶意软件攻击,除了其平台开源开放等原因外,移动应用自身代码保护强度较弱也是主要因素。针对该问题,以安卓平台应用为研究对象,分析移动应用安全威胁模型及代码安全需求,研究代码混淆、代码隐藏、代码加... 基于安卓平台应用极易被病毒或恶意软件攻击,除了其平台开源开放等原因外,移动应用自身代码保护强度较弱也是主要因素。针对该问题,以安卓平台应用为研究对象,分析移动应用安全威胁模型及代码安全需求,研究代码混淆、代码隐藏、代码加密及代码签名等代码保护技术机制及优缺点;设计并实现了安卓应用代码保护技术分析引擎,对实验数据进行分析和总结。结果表明,不同规模和类型的样本都存在一定比例应用,其代码保护强度较弱;特别地,应用规模越小,代码保护强度越弱,致使该类应用极其容易被恶意攻击。 展开更多

关键词 代码保护 移动应用 安卓 逆向工程

下载PDF 职称材料

汇编代码验证中的形式规范自动生成 被引量：3

12

作者 葛琳 陈意云 +2 位作者 华保健 李兆鹏 刘诚 《小型微型计算机系统》 CSCD 北大核心 2008年第7期1219-1224,共6页

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明... 与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现. 展开更多

关键词 出具证明编译器 汇编代码验证 形式规范Hoare逻辑 前(后)条件

下载PDF 职称材料

一种汇编程序的形式验证框架 被引量：3

13

作者 李兆鹏 陈意云 +1 位作者 葛琳 华保健 《计算机研究与发展》 EI CSCD 北大核心 2008年第5期825-833,共9页

在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关... 在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查. 展开更多

关键词 软件安全 出具证明编译器 指针逻辑 HOARE逻辑 携带证明的汇编程序

下载PDF 职称材料

一种Android应用加固方案 被引量：4

14

作者 朱洪军 陈耀光 +1 位作者 华保健 陈灏 《计算机应用与软件》 CSCD 2016年第11期297-300,320,共5页

Android应用安全问题日益突出,大量Android应用遭受逆向、非法复制及恶意代码注入等攻击。对Android应用安全机制进行研究,在分析静态逆向和动态逆向攻击原理的基础上,提出一种移动应用加固保护方案。方案综合运用加壳、反调试、签名校... Android应用安全问题日益突出,大量Android应用遭受逆向、非法复制及恶意代码注入等攻击。对Android应用安全机制进行研究,在分析静态逆向和动态逆向攻击原理的基础上,提出一种移动应用加固保护方案。方案综合运用加壳、反调试、签名校验及反编译等应用加固技术,对目标应用进行加固;经测试,该加固方案能够很好地对抗常见的静态分析和动态分析等逆向攻击。 展开更多

关键词 加固 反调试 Android安全 加壳

下载PDF 职称材料

移动应用程序内存泄露机制分析与检测方案设计 被引量：3

15

作者 朱洪军 韩洋 +1 位作者 华保健 陈灏 《计算机工程与应用》 CSCD 北大核心 2016年第17期29-34,共6页

Android开发已经成为移动开发热门领域,Android应用程序中内存使用的问题却经常容易被忽视,部分开发者对Java垃圾回收机制认识模糊,使得内存泄漏成为Android应用开发中十分隐秘但又确实存在的应用安全问题,对内存泄漏的危害进行了阐述,... Android开发已经成为移动开发热门领域,Android应用程序中内存使用的问题却经常容易被忽视,部分开发者对Java垃圾回收机制认识模糊,使得内存泄漏成为Android应用开发中十分隐秘但又确实存在的应用安全问题,对内存泄漏的危害进行了阐述,并根据与Activity、Service、Content Provider、Broadcast Receiver等Android组件的相关性归类介绍了一些常见的典型内存泄漏情景,最后分析总结内存泄漏代码特征,并设计一种基于符号执行的内存泄漏静态代码检测方案。 展开更多

关键词 安卓 内存泄漏 符号执行

下载PDF 职称材料

一种汇编语言指针逻辑的设计与实现

16

作者 李兆鹏 陈意云 +2 位作者 华保健 王伟 田波 《小型微型计算机系统》 CSCD 北大核心 2009年第6期1025-1030,共6页

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题... 软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表。 展开更多

关键词 软件安全 指针逻辑 HOARE逻辑 携带证明的汇编程序

下载PDF 职称材料

一个经过证明的类型化汇编语言的类型检查器

17

作者 郭宇 陈意云 +1 位作者 华保健 李兆鹏 《小型微型计算机系统》 CSCD 北大核心 2008年第7期1230-1236,共7页

编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全,内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文... 编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全,内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性. 展开更多

关键词 类型系统 汇编语言 类型检查 软件安全

下载PDF 职称材料

基于语义的恶意软件判定器框架

18

作者 高鹰 陈意云 华保健 《小型微型计算机系统》 CSCD 北大核心 2008年第12期2233-2240,共8页

目前代码迷惑技术已经成为构造恶意软件变体的主要方式,大量出现的病毒变体使得传统基于程序文本特征的病毒排查工具的防护作用大大降低.本文提出一种新的基于语义的恶意软件变体判定框架,为了确定一个程序是否是某种恶意软件的变体:首... 目前代码迷惑技术已经成为构造恶意软件变体的主要方式,大量出现的病毒变体使得传统基于程序文本特征的病毒排查工具的防护作用大大降低.本文提出一种新的基于语义的恶意软件变体判定框架,为了确定一个程序是否是某种恶意软件的变体:首先基于符号执行收集程序语义状态,然后通过证明语义之间是否满足变体关系来确定该程序是否是恶意软件的变体.本框架能够识别经代码迷惑变换后得到的程序是属于变换前程序的变体,从而可以减少对病毒数据库的更新.最后,通过一个实现了该框架的原型系统来说明基于语义的恶意软件判定器框架的可行性. 展开更多

关键词 恶意软件判定 代码迷惑 程序分析 符号执行

下载PDF 职称材料

改进的LS-SVM方法在EMD端点效应问题中的应用 被引量：4

19

作者 徐志军 旷欢 +1 位作者 王如龙 华保健 《计算机工程与应用》 CSCD 北大核心 2015年第3期222-228,共7页

经验模态分解能有效处理非平稳、非线性信号,但在多次采用三次样条插值获取信号上、下包络的过程中容易产生影响分解精度的端点问题。为了抑制经验模态分解中存在的端点效应问题,提出了一种基于最小二乘支持向量机和镜像延拓的端点效应... 经验模态分解能有效处理非平稳、非线性信号,但在多次采用三次样条插值获取信号上、下包络的过程中容易产生影响分解精度的端点问题。为了抑制经验模态分解中存在的端点效应问题,提出了一种基于最小二乘支持向量机和镜像延拓的端点效应抑制方法。该方法采用最小二乘支持向量机对原始信号序列两端分别向左、右各延拓有限个数据点;用镜像延拓对延拓后的信号序列进行对称延拓处理,将其延拓成一个环形信号序列;对这一环形信号序列进行经验模态分解。通过对仿真信号以及真实脑电信号进行实验分析以及与其他延拓方法的对比,结果表明该方法能够有效抑制端点效应问题,并在抑制端点效应问题方面优于传统的支持向量机和最小二乘支持向量机。 展开更多

关键词 经验模态分解 端点效应 最小二乘支持向量机 镜像延拓 支持向量机

下载PDF 职称材料

一个出具证明编译器原型系统的实现 被引量：1

20

作者 刘诚 陈意云 +1 位作者 葛琳 华保健 《计算机工程与应用》 CSCD 北大核心 2007年第21期99-102,114,共5页

出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。

关键词 软件安全 出具证明编译器 验证条件 形式化证明方法 证明生成器

下载PDF 职称材料