摘要:

摘要:软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.

摘要:覆盖反馈的灰盒Fuzzing已经成为漏洞挖掘最有效的方式之一.广泛使用的边覆盖是一种控制流信息,然而在面向污点风格(taint-style)的漏洞挖掘时,这种反馈信息过于粗糙.大量污点无关的种子被加入队列,污点相关的种子数量又过早收敛,导致Fuzzing失去进化方向,无法高效测试Source和Sink之间的信息流.首先,详细分析了现有反馈机制在检测污点风格漏洞时不够高效的原因;其次,提出了专门用于污点风格漏洞挖掘的模糊器TaintPoint.TaintPoint在控制流轨迹的基础上加入了活跃污点这一数据流信息,形成活跃轨迹(live trace)作为覆盖反馈,并围绕活跃轨迹分别在插桩、种子过滤、选择和变异阶段改进现有方法.在UAFBench上的实验结果表明:TaintPoint检测污点风格漏洞的效率、产出和速度优于业界领先的通用模糊器AFL++及定向模糊器AFLGO;此外,在两个开源项目上发现了4个漏洞并被确认.

摘要:编译器模糊测试,是测试编译器功能性与安全性的常用技术之一.模糊测试器通过产生语法正确的测试用例,对编译器的深层代码展开测试.近来,基于循环神经网络的深度学习模型被引入编译器模糊测试用例生成过程.针对现有方法生成测试用例的语法正确率不足、生成效率低的问题,提出一种基于前馈神经网络的编译器模糊测试用例生成方法,并设计实现了原型工具FAIR.与现有的基于token序列学习的方法不同,FAIR从抽象语法树中提取代码片段,利用基于自注意力的前馈神经网络捕获代码片段之间的语法关联,通过学习程序设计语言的生成式模型,自动生成多样化的测试用例.实验结果表明,FAIR生成测试用例的解析通过率以及生成效率均优于同类型先进方法.该方法显著提升了检测编译器软件缺陷的能力,已成功检测出GCC和LLVM的20处软件缺陷.此外,该方法具有良好的可移植性,简单移植后的FAIR-JS已在JavaScript引擎中检测到两处软件缺陷.

摘要:可信执行环境(trusted execution environment,TEE)是一种应用于隐私计算保护场景的体系结构方案,能为涉及隐私相关的数据和代码提供机密性和完整性的保护,近年来成为机器学习隐私保护、加密数据库、区块链安全等场景的研究热点.主要讨论在新型可信硬件保护下的系统的性能问题:首先对新型可信硬件(Intel SGX2代)进行性能剖析,发现在配置大安全内存的前提下,Intel SGX1代旧有的换页开销不再成为主要矛盾.配置大容量安全内存引起了两个新的问题:首先,普通内存的可用范围被压缩,导致普通应用,尤其是大数据应用的换页开销加剧;其次,安全内存通常处于未被用满阶段,导致整体物理内存的利用率不高.针对以上问题,提出一种全新的轻量级代码迁移方案,将普通应用的代码动态迁入安全内存中,而数据保留在原地不动.迁移后的代码可使用安全内存,避免因磁盘换页导致的剧烈性能下降.实验结果表明:该方法可将普通应用因为磁盘换页导致的性能开销降低73.2%-98.7%,同时不影响安全应用的安全隔离和正常使用.

摘要:引用计数机制是现代软件中一种常见的内存管理技术.引用计数错误往往会导致内存泄露、释放后使用(use after free)等严重的安全问题.现有致力于提高引用计数安全性的工作都依赖于对引用计数的字段进行识别.然而,由于类似于Linux等软件系统的代码十分复杂,在代码中识别出引用计数字段是一项十分困难的工作.传统的基于代码模式匹配的引用计数字段识别方法一方面存在需要专家经验总结规则,人工开销大的问题;另一方面存在总结的模式无法覆盖所有情况,召回率较低等局限.针对这些问题,发现与字段有关的代码行为以及字段的名称可以用来表征这个字段的特征,帮助识别引用计数字段.基于这两个层面的特征,设计了一种基于多模态深度学习的引用计数字段识别方法,并面向Linux内核实现原型系统.测试数据表明:该原型系统的精确率、召回率分别为96.98%和93.54%,而传统的基于代码模式匹配的方法没有识别出任何引用计数字段.此外,在Linux内核上发现61个引用计数字段使用不安全的数据类型,并对其中21个向Linux内核社区提交数据类型转换补丁以提高引用计数字段的安全性,其中6个已经被合并到Linux内核代码主分支.

摘要:移动终端在飞速发展的同时也带来了安全问题,其中,口令是用户信息的第一道安全防线,因此针对用户口令的窃取攻击是主要的安全威胁之一.利用Android系统中Toast机制设计的缺陷,实现了一种基于Toast重复绘制机制的新型口令攻击.通过分析Android Toast机制的实现原理和功能特点,发现恶意应用可利用Java反射技术定制可获取用户点击事件的Toast钓鱼键盘.虽然Toast会自动定时消亡,但是由于Toast淡入淡出动画效果的设计缺陷,恶意应用可优化Toast绘制策略,通过重复绘制Toast钓鱼键盘使其长时间驻留并覆盖于系统键盘之上,从而实现对用户屏幕输入的隐蔽劫持.最后,攻击者可以通过分析用户点击在Toast钓鱼键盘上的坐标信息,结合实际键盘布局推测出用户输入的口令.在移动终端上实现该攻击并进行了用户实验,验证了该攻击的有效性、准确性和隐蔽性,结果表明:当口令长度为8时,攻击成功率为89%.发现的口令漏洞已在Android最新版本中得到修复.

摘要:软件静态缺陷检测是软件安全领域中的一个研究热点.随着使用C/C++语言编写的软件规模和复杂度的逐渐提高,软件迭代速度的逐渐加快,由于静态软件缺陷检测不需要运行目标代码即可发现其中潜藏的缺陷,因而在工业界和学术界受到了更为广泛的关注.近年来涌现出大量使用软件静态分析技术的检测工具,并在不同领域的软件项目中发挥了不可忽视的作用,但是开发者仍然对静态缺陷检测工具缺乏信心.高误报率是C/C++静态缺陷检测工具难以普及的首要原因.因此,选择现有的较为完善的开源C/C++静态缺陷检测工具,在Juliet基准测试集和37个良好维护的开源软件项目上对特定类型缺陷的检测效果进行了深入研究,结合检测工具的具体实现,归纳了导致静态缺陷检测工具产生误报的关键原因.同时,通过研究静态缺陷检测工具的版本迁移轨迹,总结出了当下静态分析工具的发展方向和未来趋势,有助于未来静态分析技术的优化和发展,从而实现静态缺陷检测工具的普及应用.

摘要:自动生成漏洞利用样本(AEG)已成为评估漏洞的最重要的方式之一,但现有方案在目标系统部署有漏洞缓解机制时受到很大阻碍.当前主流的操作系统默认部署多种漏洞缓解机制,包括数据执行保护(DEP)和地址空间布局随机化(ASLR)等,而现有AEG方案仍无法面对所有漏洞缓解情形.提出了一种自动化方案EoLeak,可以利用堆漏洞实现自动化的信息泄露,进而同时绕过数据执行保护和地址空间布局随机化防御.EoLeak通过动态分析漏洞触发样本(POC)的程序执行迹,对执行迹中的内存布局进行画像并定位敏感数据(如代码指针),进而基于内存画像自动构建泄漏敏感数据的原语,并在条件具备时生成完整的漏洞利用样本.实现了EoLeak原型系统,并在一组夺旗赛(CTF)题目和多个实际应用程序上进行了实验验证.实验结果表明,该系统具有自动化泄露敏感信息和绕过DEP及ASLR缓解机制的能力.

摘要:跨项目缺陷预测(cross-project defect prediction,CPDP)已经成为软件工程数据挖掘领域的一个重要研究方向,它利用其他项目的缺陷代码来建立预测模型,解决了模型构建过程中的数据不足问题.然而源项目和目标项目的代码文件之间存在着数据分布的差异,导致跨项目预测效果不佳.基于生成式对抗网络(generative adversarial network,GAN)中的对抗学习思想,在鉴别器的作用下,通过改变目标项目特征的分布,使其接近于源项目特征的分布,从而提升跨项目缺陷预测的性能.具体来说,提出的抽象连续生成式对抗网络(abstract continuous generative adversarial network,AC-GAN)方法包括数据处理和模型构建两个阶段:(1)首先将源项目和目标项目的代码转换为抽象语法树(abstract syntax tree,AST)的形式,然后以深度优先方式遍历抽象语法树得出节点序列,再使用连续词袋模型(continuous bag-of-words model,CBOW)生成词向量,依据词向量表将节点序列转化为数值向量;(2)处理后的数值向量被送入基于GAN网络结构的模型进行特征提取和数据迁移,然后使用二分类器来判断目标项目代码文件是否有缺陷.AC-GAN方法在15组源-目标项目对上进行了对比实验,实验结果表明了该方法的有效性.

关键

摘要:

摘要:迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.

摘要:霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.

摘要:飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

摘要:定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

摘要:可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

摘要:实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.

摘要:矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.

摘要:为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

摘要:云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

摘要:软件缺陷在软件的开发和维护过程中是不可避免的,软件缺陷报告是软件维护过程中重要的缺陷描述文档,高质量的软件缺陷报告可以有效提高软件缺陷修复的效率.然而,由于存在许多开发人员、测试人员和用户与缺陷跟踪系统交互并提交软件缺陷报告,同一个软件缺陷可能被不同的人员报告,导致了大量重复的软件缺陷报告.重复的软件缺陷报告势必加重人工检测重复缺陷报告的工作量,并造成人力物力的浪费,降低了软件缺陷修复的效率.以系统文献调研的方式,对近年来国内外学者在重复软件缺陷报告检测领域的研究工作进行了系统的分析.主要从研究方法、数据集的选取、性能评价等方面具体分析总结,并提出该领域在后续研究中存在的问题、挑战以及建议.

摘要:安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

摘要:实体解析是数据集成的关键方面,也是大数据分析与挖掘的必要预处理步骤.大数据时代,随着查询驱动的数据应用需求的不断增长,查询式实体解析成为热点问题.为了提升查询-解析效率,研究了面向实体缓存的多属性数据索引技术.涉及两个核心问题:(1)如何设计多属性数据索引?设计了基于R-树的多属性索引结构.为了满足实体缓存在线生成需求,提出了基于空间聚类的在线索引构建方法.提出了基于“过滤-验证”的多维查询方法,利用多属性索引有效地过滤掉不可能命中的记录,然后采用相似性函数或距离函数逐一验证候选记录.(2)如何将不同的字符串属性插入到树形索引中?解决思路是,将字符串映射到数值空间.针对Jaccard相似性和编辑相似性,提出了基于q-gram的映射方法,并提出了基于向量降维的优化和基于z-order的优化,实现高质量的“字符串®数值”映射.最后,在两个数据集上进行实验评估,验证多属性索引的有效性,并测试其各个方面.

摘要:基于中心化/本地化差分隐私的直方图发布已得到了研究者的广泛关注.用户的隐私需求与收集者的分析精度之间的矛盾直接制约着直方图发布的可用性.针对现有直方图发布方法难以有效同时兼顾用户隐私与收集者分析精度的不足,提出了一种基于混洗差分隐私的直方图发布算法HP-SDP (histogram publication with shuffled differential privacy).该算法结合本地哈希编码技术所设计的混洗应答机制SRR (shuffled randomized response),能够以线性分解的方式扰动用户数据以及摆脱数据值域大小的影响.结合SRR机制产生的用户消息,设计了一种基于堆排列技术的用户消息均匀随机排列算法MRS (message random shuffling),混洗方利用MRS对所有用户的消息进行随机排列.由于经过MRS混洗后的消息满足中心化差分隐私,使得恶意收集者无法通过消息与用户之间的链接对目标用户进行身份甄别.此外,HP-SDP利用基于二次规划技术的后置处理算法POP (post-processing)对混洗后的直方图进行求精处理.HP-SDP算法与现有的7种直方图发布算法在4种数据集上所做实验结果表明,其发布精度优于同类算法.