虚拟化软件栈安全研究 被引量：13

1

作者 朱民 涂碧波 孟丹 《计算机学报》 EI CSCD 北大核心 2017年第2期481-504,共24页

随着云计算的兴起,虚拟化技术在IT产业中得到了广泛应用.政府、企业和个人已将自身的大量业务及其敏感数据转移到了云端的虚拟机中.在虚拟化软件栈中,虚拟机监控器具有最高权限和较小的可信计算基,故而能为虚拟化系统提供安全监控和保护... 随着云计算的兴起,虚拟化技术在IT产业中得到了广泛应用.政府、企业和个人已将自身的大量业务及其敏感数据转移到了云端的虚拟机中.在虚拟化软件栈中,虚拟机监控器具有最高权限和较小的可信计算基,故而能为虚拟化系统提供安全监控和保护.但同时也引入了新的软件层,增加了脆弱性,增大了攻击面.另外,多租户模式以及软硬件平台资源共享,更加剧了新软件栈的安全威胁.因此,虚拟机和虚拟机监控器的安全和隐私备受学术界和工业界关注.该文对虚拟化软件栈不同软件层的安全威胁、攻击方式和威胁机理进行了分析,并针对这些安全威胁,以可信基为视角,从基于虚拟机监控器、基于微虚拟机监控器、基于嵌套虚拟化和基于安全硬件等类别分析比较了国内外相关安全方案和技术,并指出了当前仍然存在的安全问题.最后对未来的研究方向进行了探讨和分析,并从软件和硬件两个层面给出了虚拟化软件栈的安全增强方案. 展开更多

关键词 虚拟化软件栈 虚拟机安全 云安全 内存安全 计算机安全体系结构

下载PDF 职称材料

结合模糊测试和动态分析的内存安全漏洞检测

2

作者 马莺姿 陈哲 +1 位作者 殷家乐 毛瑞琪 《计算机科学》 CSCD 北大核心 2024年第2期352-358,共7页

C语言因其在运行速度及内存控制方面的优势而被广泛应用于系统软件和嵌入式软件的开发。指针的强大功能使得它可以直接对内存进行操作,然而C语言并未提供对内存安全性的检测,这就使得指针的使用会导致内存泄露、缓冲区溢出、多次释放等... C语言因其在运行速度及内存控制方面的优势而被广泛应用于系统软件和嵌入式软件的开发。指针的强大功能使得它可以直接对内存进行操作,然而C语言并未提供对内存安全性的检测,这就使得指针的使用会导致内存泄露、缓冲区溢出、多次释放等内存错误,有时这些错误还会造成系统崩溃或内部数据破坏等的致命伤害。当前已存在多种能够对C程序进行内存安全漏洞检测的技术。其中动态分析技术通过插桩源代码来实现对C程序的运行时内存安全检测,但是只有当程序执行到错误所在路径时才能发现错误,因此它依赖于程序的输入;而模糊测试是一种通过向程序提供输入并监视程序运行结果来发现软件漏洞的方法,但是无法检测出没有导致程序崩溃的内存安全性错误,也无法提供错误所在位置等详细信息。除此之外,由于C语言的语法比较复杂,在对一些大型复杂项目进行分析时,动态分析工具经常无法正确处理一些不常见的特定结构,导致插桩失败或者插桩后的程序无法被正确编译。针对上述问题,通过将动态分析技术与模糊测试技术结合,并对已有方法进行改进后,提出了一种能够对包含特定结构的C程序进行内存安全检测的方法。文中进行了可靠性和性能的实验,结果表明,在增加对C语言中特定结构的处理方法之后,能对包含C语言中特定结构的程序进行内存安全检测,并且结合模糊测试技术后具有更强的漏洞检测能力。 展开更多

关键词 内存安全 源代码插桩 动态分析 模糊测试 内存错误

下载PDF 职称材料

多线程C程序内存安全性动态分析方法

3

作者 严瑞 陈哲 《计算机科学》 CSCD 北大核心 2024年第S01期791-796,共6页

随着软件结构越来越复杂以及其要求更高级别的并发量,出现了越来越多的多线程程序,同时C语言程序缺乏检测其内存安全的能力,进而导致C语言实现的程序可能会存在较多的隐藏漏洞,因此对多线程C程序的内存安全检测尤为的重要。较为前沿且... 随着软件结构越来越复杂以及其要求更高级别的并发量,出现了越来越多的多线程程序,同时C语言程序缺乏检测其内存安全的能力,进而导致C语言实现的程序可能会存在较多的隐藏漏洞,因此对多线程C程序的内存安全检测尤为的重要。较为前沿且可靠的检测内存安全的技术主要为动态分析技术,且现在对于多线程C程序内存安全检测的工具不是特别完善,错误检测不完全,性能不是很高。因此提出了基于指针的动态分析技术,同时结合无锁技术、源代码插桩技术实现了工具Movec来对多线程C程序的内存安全性进行检测,并且选取专业测试集来进行实验,验证了本工具对于多线程C程序检测内存安全是有效的,检测的错误更多且性能较为优秀。 展开更多

关键词 多线程 内存安全 动态分析 源代码插桩

下载PDF 职称材料

一种基于数据依赖关系的内存安全性检测方法

4

作者 蒙世满 符祥 《湖北大学学报（自然科学版）》 CAS 2024年第3期402-410,共9页

内存安全问题已成为影响C/C++程序正确性和可靠性的主要因素。一些现有的静态代码检测工具无法识别全局变量+跨函数内存管理的内存泄露和未定义越界访问这两种缺陷,且其他动态代码检测工具,因需要在运行时进行插桩等操作,会增加额外的... 内存安全问题已成为影响C/C++程序正确性和可靠性的主要因素。一些现有的静态代码检测工具无法识别全局变量+跨函数内存管理的内存泄露和未定义越界访问这两种缺陷,且其他动态代码检测工具,因需要在运行时进行插桩等操作,会增加额外的开销导致检测效率慢。为解决这些问题,采用LLVM 15提出一种基于中间语言数据依赖关系的内存安全性检测方法,该方法通过获取并分析LLVM中间语言中指令之间的数据依赖,从而进行判断得出结果。在软件保障参考数据集SARD上的相关测试用例集验证了该方法的有效性,相比现有方法,该方法可以检测这两种内存安全性缺陷。 展开更多

关键词 内存安全 静态检测 LLVM 中间语言 数据依赖

下载PDF 职称材料

Rust语言在Web开发的应用研究

5

作者 顾锡华 《电脑知识与技术》 2024年第5期38-40,共3页

随着互联网技术的飞速发展,Web应用已成为人们日常生活和工作中不可或缺的一部分。但随着Web应用的规模和复杂性的不断增长,传统的开发语言在性能、安全性和并发性方面逐渐面临挑战。Rust作为一种新兴的系统级编程语言,以其高效、安全... 随着互联网技术的飞速发展,Web应用已成为人们日常生活和工作中不可或缺的一部分。但随着Web应用的规模和复杂性的不断增长,传统的开发语言在性能、安全性和并发性方面逐渐面临挑战。Rust作为一种新兴的系统级编程语言,以其高效、安全和并发性强的特点,逐渐在Web开发中得到广泛应用。 展开更多

关键词 RUST WEB开发 异步 并发 内存安全

下载PDF 职称材料

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

6

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

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

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

下载PDF 职称材料

RISC-V技术及生态专题前言 被引量：1

7

作者 邢明杰 宋威 +1 位作者 张科 易秋萍 《计算机系统应用》 2023年第11期1-2,共2页

RISC-V作为一个开放的指令集架构标准,已经在产业界和学术界产生广泛影响,被《麻省理工科技评论》评选为2023年“全球十大突破性技术”之一.随着RISC-V技术在高性能、安全、并行计算等领域的进一步发展,必然会迎来新的挑战和机遇.今年... RISC-V作为一个开放的指令集架构标准,已经在产业界和学术界产生广泛影响,被《麻省理工科技评论》评选为2023年“全球十大突破性技术”之一.随着RISC-V技术在高性能、安全、并行计算等领域的进一步发展,必然会迎来新的挑战和机遇.今年的专题采取了自由投稿和定向邀请相结合的方式,共收到9篇稿件,其中8篇通过了形式审查.特约编辑先后邀请了12位相关领域专家参与审稿工作,每篇投稿至少邀请2位专家进行评审.稿件经初审、多轮复审、终审,并在RISC-V技术及生态研讨会上进行报告,最终有4篇论文入选本专题.这些论文涵盖了RISC-V平台的指令追踪、内存安全、操作系统及向量扩展优化等诸多方面的内容. 展开更多

关键词 领域专家 并行计算 操作系统 RISC 特约编辑 科技评论 内存安全 突破性技术

下载PDF 职称材料

密码实现安全形式化验证发展现状与展望

8

作者 宋富 《前瞻科技》 2023年第1期90-105,共16页

密码是保障网络安全和信息安全的核心技术和基础支撑,但密码实现本身面临多种安全威胁,形式化验证是严格证明密码实现安全性的重要技术手段。文章回顾了国内外在密码实现的功能正确性和内存安全性、时间侧信道安全性、功耗侧信道安全性... 密码是保障网络安全和信息安全的核心技术和基础支撑,但密码实现本身面临多种安全威胁,形式化验证是严格证明密码实现安全性的重要技术手段。文章回顾了国内外在密码实现的功能正确性和内存安全性、时间侧信道安全性、功耗侧信道安全性方面的形式化验证技术发展现状和应用情况,分析了当前面向密码实现的形式化验证技术的不足、挑战和发展趋势。鉴于中国密码实现的安全性需求和相应形式化验证技术积累的不足,建议以研制构建高性能、高可信密码库为目标,以国家重大任务为牵引,通过顶层设计,强化自主创新,统一中间表示语言,研制高效率、高精度、自动化的形式化验证平台及安全编译优化工具链,最小化可信计算基,构造高效率、高可信密码实现通用库,促进产学研融合发展,进一步提高国家网络安全和信息安全的发展质量。 展开更多

关键词 密码实现 安全与隐私 形式化验证 功能正确 内存安全 侧信道安全

原文传递

RISC-V架构硬件辅助用户态内存安全防御方案概览

9

作者 解达 欧阳慈俨 宋威 《计算机系统应用》 2023年第11期11-20,共10页

传统的用户态内存安全防御机制基于x86架构和纯软件方式实现,实现内存安全保护的运行时开销很高,难以部署在生产环境中.近年来,随着主流商业处理器开始提供硬件安全扩展,以及RISC-V等开源处理器架构的兴起,内存安全保护方案开始面向x86... 传统的用户态内存安全防御机制基于x86架构和纯软件方式实现,实现内存安全保护的运行时开销很高,难以部署在生产环境中.近年来,随着主流商业处理器开始提供硬件安全扩展,以及RISC-V等开源处理器架构的兴起,内存安全保护方案开始面向x86-64、ARM、RISC-V等多种体系架构和硬件辅助实现方式.我们对RISC-V架构上实现的内存安全防御方案进行了讨论,并对x86-64、ARM、RISC-V等处理器架构在安全方案设计上的特点进行了比较.得益于开放的指令集架构生态,RISC-V架构的内存安全防御方案相较于其他架构有一些优势.一些低成本的安全防御技术有望在RISC-V架构上实现. 展开更多

关键词 RISC-V 内存安全 硬件安全扩展 处理器

下载PDF 职称材料

安全持久性内存存储研究综述 被引量：3

10

作者 杨帆 李飞 舒继武 《计算机研究与发展》 EI CSCD 北大核心 2020年第5期912-927,共16页

在计算机技术和互联网技术飞速发展的进程中,计算机安全防护和数据机密性保护一直是学术界和工业界关注的焦点.主流的内存安全机制通过提供硬件辅助的机密性与完整性验证,确保选定的代码在运行时的内存可信,达到数据保护、防止泄漏和遭... 在计算机技术和互联网技术飞速发展的进程中,计算机安全防护和数据机密性保护一直是学术界和工业界关注的焦点.主流的内存安全机制通过提供硬件辅助的机密性与完整性验证,确保选定的代码在运行时的内存可信,达到数据保护、防止泄漏和遭篡改的目的.新型持久性内存可像DRAM一样放置在内存总线上,通过处理器load和store指令进行访问,此外,持久性内存能够提供大容量和数据持久性支持,具有高带宽和低延迟的数据访问特性.然而,由于介质特性上的差异,面向DRAM的内存安全机制无法在持久性内存上高效运行,甚至存在可用性问题.因此,构建基于持久性内存的安全内存存储系统将为大数据的安全高效存储带来新的机遇.首先,针对持久性内存的写特性,分析了将面向传统易失内存的安全防护措施应用于持久性内存会引起额外开销的原因,并介绍相关降低开销的研究工作.其次,针对持久性内存的非易失性,分析了为保障持久性内存在其生命周期内的安全性所面临的问题与挑战,并介绍了数据及其安全元数据的一致性管理相关研究工作.最后,总结了构建面向持久性内存的安全存储系统面临的挑战,对相关工作进行综合比较,并提出下一步研究展望. 展开更多

关键词 持久性内存 内存安全 加密 完整性验证 灾后一致性

下载PDF 职称材料

一种用于类C语言环境的安全的类型化内存模型 被引量：3

11

作者 何炎祥 吴伟 +2 位作者 陈勇 李清安 刘健博 《计算机研究与发展》 EI CSCD 北大核心 2012年第11期2440-2449,共10页

使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无... 使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证. 展开更多

关键词 操作语义 形式化验证 内存模型 霍尔逻辑 内存安全

下载PDF 职称材料

姜向前:打造硬核安全能力 夯实网络强国根基

12

作者 本刊编辑部 《互联网天地》 2022年第11期2-6,共5页

安芯网盾是国内内存安全领域的开拓者,公司成立以来,凭借团队十年如一日的深耕和积累,以“保护数字世界的安宁”为使命,致力于为重点关键信息基础设施行业客户,提供新一代高级威胁实时防护解决方案,目前已成长为服务全球用户的内存安全... 安芯网盾是国内内存安全领域的开拓者,公司成立以来,凭借团队十年如一日的深耕和积累,以“保护数字世界的安宁”为使命,致力于为重点关键信息基础设施行业客户,提供新一代高级威胁实时防护解决方案,目前已成长为服务全球用户的内存安全领军企业。安芯网盾创始人、CEO姜向前作为一名网络安全领域的连续创业者,2009年参与创立百锐安全实验室;2012年创立上网快鸟;2019年与姚纪卫先生共同创立了安芯网盾。近期,本刊编辑部与姜向前先生围绕创新技术的发展、网络安全行业发展等问题展开对话。 展开更多

关键词 内存安全 关键信息基础设施 全球用户 硬核 网络安全领域 实时防护 网络强国 安全实验室

原文传递

瞄准靶心 构筑有生命力的内存安全产品——专访安芯网盾(北京)科技有限公司CEO姜向前

13

作者 牟艳霞 姜向前 《信息技术与网络安全》 2021年第4期F0003-F0003,I0001,I0002,共3页

当前,数字经济正成为我国重要的经济增长点。在发展数字经济过程中,以5G网络、大数据中心等为代表的新型基础设施建设成为发展中的热词。随着'新基建的加速推进,人类社会将迈入万物互联时代,新的网络安全问题也不断涌现,给公众人身... 当前,数字经济正成为我国重要的经济增长点。在发展数字经济过程中,以5G网络、大数据中心等为代表的新型基础设施建设成为发展中的热词。随着'新基建的加速推进,人类社会将迈入万物互联时代,新的网络安全问题也不断涌现,给公众人身安全、社会安定甚至是国家安全造成威胁。作为国内内存安全领域的开拓者,安芯网盾主推的内存保护系统,提出了一种全新的思路来帮助客户应对日益增长的安全威胁。 展开更多

关键词 大数据中心 内存保护 内存安全 安全威胁 经济增长点 万物互联 网络安全问题 基础设施建设

下载PDF 职称材料

跨平台内存安全测试集设计

14

作者 沈思豪 解达 宋威 《计算机系统应用》 2022年第9期39-49,共11页

内存安全性是一项非常重要的性质,但它很容易被攻击者利用.过去针对内存安全问题提出的许多防御方案,由于性能代价高昂,很少能够部署在生产环境中.最近,随着RISC-V等开源处理器架构的兴起,安全领域迎来了设计新的处理器硬件安全拓展的热... 内存安全性是一项非常重要的性质,但它很容易被攻击者利用.过去针对内存安全问题提出的许多防御方案,由于性能代价高昂,很少能够部署在生产环境中.最近,随着RISC-V等开源处理器架构的兴起,安全领域迎来了设计新的处理器硬件安全拓展的热潮,硬件辅助防御方案的性能代价降低,变得可以接受.为了更好地支持内存安全处理器拓展的设计,以及更好地评估处理器内存安全性能,我们设计了一款兼具综合性、可移植性内存安全测试框架,并开源了一个160测例大小的初始版本测试集,覆盖了内存时空安全性、访问控制、指针和控制流完整性等方面,并在x86-64和RISC-V64两种指令集架构的平台上进行了测试. 展开更多

关键词 RISC-V 内存安全 测试集

下载PDF 职称材料

基于定理证明的内存安全性动态检测算法的正确性研究 被引量：1

15

作者 孙小祥 陈哲 《计算机科学》 CSCD 北大核心 2021年第1期268-272,共5页

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程... 随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。 展开更多

关键词 运行时验证 源代码插桩 内存安全 定理证明 COQ

下载PDF 职称材料

基于内存的漏洞缓解关键技术研究

16

作者 贺滢睿 史记 +1 位作者 张涛 文伟平 《信息网络安全》 2014年第12期76-82,共7页

随着漏洞挖掘技术日渐成熟,每年新增漏洞数量逐步增加。从操作系统以及编译器层面来说,为了提高内存保护的安全性,对抗漏洞利用的缓解措施也在不断完善。文章介绍了近年来比较成熟的基于内存的漏洞关键缓解技术,包括GS编译选项技术、SE... 随着漏洞挖掘技术日渐成熟,每年新增漏洞数量逐步增加。从操作系统以及编译器层面来说,为了提高内存保护的安全性,对抗漏洞利用的缓解措施也在不断完善。文章介绍了近年来比较成熟的基于内存的漏洞关键缓解技术,包括GS编译选项技术、SEH安全校验机制、堆数据保护机制、DEP技术以及ASLR技术。GS编译选项技术和SEH安全校验机制能够有效遏制针对栈数据的攻击;堆数据保护机制为堆溢出增加了更多限制;DEP技术能够对内存执行额外检查以防止恶意代码在系统中执行;ASLR技术通过对关键地址的随机化使一些堆栈溢出手段失效。文章还指出了这些防护措施所存在的不足,并据此从攻击者的角度介绍了针对这几种缓解措施的攻击思路。针对漏洞缓解技术,文章指出未来必须考虑的是如何弥补在抵御复合向量攻击方面的不足,如何完善旁路保护。 展开更多

关键词 内存安全 漏洞缓解 绕过

下载PDF 职称材料

基于TXL的源代码插桩技术研究

17

作者 张琦 仵俊 《现代信息科技》 2021年第21期82-85,89,共5页

常见的运行时验证技术的插桩方式包括中间代码插桩、二进制代码插桩和源代码插桩。前两种插桩方式的插桩结果通常依赖于平台,而且不同的优化等级也会带来不同的结果,会使得部分错误被忽略。TXL是一种函数和规则混合的语言,提供源代码到... 常见的运行时验证技术的插桩方式包括中间代码插桩、二进制代码插桩和源代码插桩。前两种插桩方式的插桩结果通常依赖于平台,而且不同的优化等级也会带来不同的结果,会使得部分错误被忽略。TXL是一种函数和规则混合的语言,提供源代码到源代码的转换。文章使用TXL作为插桩工具,提出一套完整的源代码插桩算法,实现了基于指针技术的C语言运行时验证工具。实验表明,该算法可以有效实现对C程序的插桩。 展开更多

关键词 运行时验证 源代码插桩 TXL 内存安全

下载PDF 职称材料

一种面向大规模C程序的内存错误调试方法

18

作者 仵俊 《现代信息科技》 2021年第21期152-154,共3页

为了实现极致的性能,C语言将操纵内存的权限以指针的方式暴露给开发人员。但是C语言编译器GCC和Clang都不提供内存安全检测,导致开发人员使用C语言编写的项目可能含有潜在的内存安全性漏洞。可以先使用检测工具定位错误,然后执行GDB来... 为了实现极致的性能,C语言将操纵内存的权限以指针的方式暴露给开发人员。但是C语言编译器GCC和Clang都不提供内存安全检测,导致开发人员使用C语言编写的项目可能含有潜在的内存安全性漏洞。可以先使用检测工具定位错误,然后执行GDB来验证。文章介绍了GDB调试C程序时所采用的方法和技巧,并使用GDB验证了内存检测工具AddressSanitizer和Movec在大规模测试集SPEC上检测的有效性。 展开更多

关键词 调试 GDB 内存安全 大规模C程序

下载PDF 职称材料

C程序内存安全的运行时检测方法研究和实现 被引量：6

19

作者 严俊琦 陈哲 黄志球 《小型微型计算机系统》 CSCD 北大核心 2017年第10期2358-2362,共5页

随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.然而由于C语言自身缺乏边界检测的机制,使得它不能确保软件的可靠性与安全性.当前的检测方法都或多或少存在问题,如不兼容、不完整等.设计了... 随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.然而由于C语言自身缺乏边界检测的机制,使得它不能确保软件的可靠性与安全性.当前的检测方法都或多或少存在问题,如不兼容、不完整等.设计了一种完整的C程序内存安全的运行时检测方法,能确保C程序的时间内存安全和空间内存安全.本文是采用基于指针方法,并且借助开源编译器clang实现了确保C程序内存安全的运行时验证工具TASSafe.通过实验证明我们的工具是有效并且是高效的. 展开更多

关键词 运行时验证 缓冲区溢出 时间内存安全 空间内存安全 基于指针

下载PDF 职称材料

基于分离逻辑的程序验证研究综述 被引量：7

20

作者 秦胜潮 许智武 明仲 《软件学报》 EI CSCD 北大核心 2017年第8期2010-2025,共16页

自20世纪60年代以来,虽然有Floyd-Hoare逻辑的出现,但使用形式化工具对命令式程序的正确性和可靠性进行自动验证,一直被认为是极具挑战性、神圣不可及的工作.20世纪末,由于更多科研的投入,特别是微软、IBM等大型公司研发部门的大量人力... 自20世纪60年代以来,虽然有Floyd-Hoare逻辑的出现,但使用形式化工具对命令式程序的正确性和可靠性进行自动验证,一直被认为是极具挑战性、神圣不可及的工作.20世纪末,由于更多科研的投入,特别是微软、IBM等大型公司研发部门的大量人力、物力的投入,程序验证方面在21世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRéE工具、用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆(heap):ASTRéE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上,很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序(heap-manipulating programs)进行自动验证仍然是一个难题.2001年~2002年,分离逻辑(separation logic)提出后,其分离(separation)思想和相应的框(frame)规则使得局部推理(local reasoning)可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如Space Invader/Abductor,Slayer,HIP/SLEEK,CSL等工作.着重对这方面的部分重要工作进行阐述. 展开更多

关键词 分离逻辑 程序分析 程序验证 内存安全性 功能正确性

下载PDF 职称材料