检索结果-内蒙古大学图书馆

软件学报 2016年第3期27卷 633-644页

作者：陈鑫黄超张一帆梅一鸣计算机软件新技术国家重点实验室(南京大学) 江苏南京210023 南京大学计算机科学与技术系江苏南京210023

干涉问题是指基础程序和方面之间或者方面之间发生不需要的相互作用,导致最终程序中产生不想要的功能,危害程序的正确性.很难检测和修正在面向方面设计中存在的干涉,已经成为推广面向方面技术的阻碍.受到技术自身可扩展能力的局限,现有... 详细信息

干涉问题是指基础程序和方面之间或者方面之间发生不需要的相互作用,导致最终程序中产生不想要的功能,危害程序的正确性.很难检测和修正在面向方面设计中存在的干涉,已经成为推广面向方面技术的阻碍.受到技术自身可扩展能力的局限,现有的基于模型验证技术的工作不能有效地处理功能干涉问题.设计开发了基于推理验证技术直接检查和去除面向方面设计中功能干涉的工具,它可以根据类和方面的功能规约自动产生确保不发生干涉的条件,并引入交互式证明工具PVS来提高证明过程的自动化程度.证明可以确认设计中无干涉存在或者为修正干涉问题提供线索.

关键词：面向方面的设计功能干涉推理验证设计演算

来源：评论

学校读者我要写书评

暂无评论

BACH:线性混成系统有界可达性模型检验工具

引用

软件学报 2011年第4期22卷 640-658页

作者：卜磊李游王林章李宣东南京大学计算机软件新技术国家重点实验室江苏南京210093 南京大学计算机科学与技术系江苏南京210093

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类——线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规... 详细信息

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类——线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具——BACH(bounded reachability checker),该工具能够沿指定路径(组)对单个线性混成自动机、多个线性混成自动机的组合进行可达性检验,并且在此基础上结合路径遍历技术完成对所有路径的有界可达性检验.实验数据显示,BACH不仅在面向路径可达性检验方面性能优异,可以适用于足够长度的路径,而且在针对所有路径的有界可达性检验时,BACH可以解决的问题规模也远远超过同类工具,已接近工业界应用的要求.

关键词：线性混成系统线性混成自动机有界可达性检验线性规划

来源：评论

学校读者我要写书评

暂无评论

ROP图灵完备的普遍可实现性

引用

软件学报 2017年第10期28卷 2583-2598页

作者：袁平海曾庆凯南京大学计算机科学与技术系江苏南京210023 计算机软件新技术国家重点实验室(南京大学) 江苏南京210023

返回导向编程(return-oriented programming,简称ROP)被广泛用于软件漏洞利用攻击中,用来构造攻击代码.通过更新ROP构造技术,证实了图灵完备的纯ROP攻击代码在软件模块中是普遍可实现的.ROP构造功能代码的难点是实现条件转移逻辑.通过... 详细信息

返回导向编程(return-oriented programming,简称ROP)被广泛用于软件漏洞利用攻击中,用来构造攻击代码.通过更新ROP构造技术,证实了图灵完备的纯ROP攻击代码在软件模块中是普遍可实现的.ROP构造功能代码的难点是实现条件转移逻辑.通过深入分析条件转移机器指令的执行上下文发现,对这些指令的传统认知存在一定的局限性.事实上,在已有代码中存在少量的条件转移指令,它们的两个分支的开始部分都是可复用的代码片段(称为gadgets),而且这两个gadgets会从不同的内存单元中取得下一个gadget的地址,因此,以这些条件转移指令开始的代码片段可以帮助ROP实现条件转移逻辑.把这种代码片段称为if-gadget.在Linux和Windows系统上的实验结果表明,if-gadget普遍存在,即使在代码量很小的日常可执行程序中也存在.在Binutils程序集上的实验结果表明,引入if-gadget后,构造图灵完备的ROP代码要比用传统方法容易得多.在Ubuntu这样的主流操作系统上,由于可执行程序上默认没有实施防御ROP攻击的保护机制,因此,攻击者可以在这些软件模块中构造纯ROP攻击代码来发动攻击.由此可见,ROP对系统安全的威胁比原来认为的严重得多.

关键词：软件漏洞利用返回导向编程图灵完备计算:条件转移逻辑

来源：评论

学校读者我要写书评

暂无评论

面向草图检索的小样本增量有偏学习算法

引用

软件学报 2009年第5期20卷 1301-1312页

作者：梁爽孙正兴南京大学计算机软件新技术国家重点实验室江苏南京210093 南京大学计算机科学与技术系江苏南京210093

为了解决草图检索相关反馈中小样本训练、数据不对称及实时性要求这3个难点问题,提出了一种小样本增量有偏学习算法.该算法将主动式学习、有偏分类和增量学习结合起来,对相关反馈过程中的小样本有偏学习问题进行建模.其中,主动式学习通... 详细信息

为了解决草图检索相关反馈中小样本训练、数据不对称及实时性要求这3个难点问题,提出了一种小样本增量有偏学习算法.该算法将主动式学习、有偏分类和增量学习结合起来,对相关反馈过程中的小样本有偏学习问题进行建模.其中,主动式学习通过不确定性采样,选择最佳的用户标注样本,实现有限训练样本条件下分类器泛化能力的最大化;有偏分类通过构造超球面区别对待正例和反例,准确挖掘用户目标类别;每次反馈循环中新加入的样本则用于分类器的增量学习,在减少分类器训练时间的同时积累样本信息,进一步缓解小样本问题.实验结果表明,该算法可以有效地改善草图检索性能,也适用于图像检索和三维模型检索等应用领域.

关键词：草图检索相关反馈小样本增量有偏学习主动式学习有偏分类增量学习

来源：评论

学校读者我要写书评

暂无评论

测试集有效性评价:问题、进展与挑战

引用

软件学报 2024年第2期35卷 532-580页

作者：路则雨张鹏王洋郭肇强杨已彪周毓明计算机软件新技术国家重点实验室(南京大学) 江苏南京210023 南京大学计算机科学与技术系江苏南京210023

测试用例集的缺陷检测有效性指测试集能够在多大程度上检测出软件中存在的缺陷.如何评价测试集的缺陷检测有效性是一个重要问题.覆盖率和变异得分是两个最重要和最广泛使用的测试集有效性度量.为量化测试集的缺陷检测能力,研究人员对测... 详细信息

测试用例集的缺陷检测有效性指测试集能够在多大程度上检测出软件中存在的缺陷.如何评价测试集的缺陷检测有效性是一个重要问题.覆盖率和变异得分是两个最重要和最广泛使用的测试集有效性度量.为量化测试集的缺陷检测能力,研究人员对测试集有效性评价进行了大量研究并且取得了较大的进展.与此同时,现有研究存在不一致的结论,该领域依然存在一些亟待解决的挑战.对多年来国内外学者在测试集有效性评价领域的研究成果进行系统性的梳理和总结.首先,阐述测试集有效性评价研究中的问题.然后,介绍并分析基于覆盖率和基于变异得分的测试集有效性的评价以及介绍测试集有效性评价在测试集优化中的应用.最后,指出测试集有效性评价研究中面临的挑战并给出建议的研究方向.

关键词：覆盖率变异得分缺陷检测测试集有效性

来源：评论

学校读者我要写书评

暂无评论

攻击网页浏览器:面向脚本代码块的ROP Gadget注入

引用

软件学报 2020年第2期31卷 247-265页

作者：袁平海曾庆凯张云剑刘尧南京大学计算机科学与技术系江苏南京210023 计算机软件新技术国家重点实验室(南京大学) 江苏南京210023

即时编译机制(just-in-time compilation)改善了网页浏览器执行JavaScript脚本的性能,同时也为攻击者向浏览器进程注入恶意代码提供了便利.借助即时编译器,攻击者可以将脚本中的整型常数放置到动态代码缓存区,以便注入二进制恶意代码片... 详细信息

即时编译机制(just-in-time compilation)改善了网页浏览器执行JavaScript脚本的性能,同时也为攻击者向浏览器进程注入恶意代码提供了便利.借助即时编译器,攻击者可以将脚本中的整型常数放置到动态代码缓存区,以便注入二进制恶意代码片段(称为gadget).通过常数致盲等去毒化处理,基于常数的注入已经得到有效遏制.证实了不使用常数转而通过填充脚本代码块也能实施gadget注入,并实现图灵完备的计算功能.在编译一段给定的脚本代码时,即时编译器生成的动态代码中通常存在着一些固定的机器指令序列.这些指令序列的存在性不受常数致盲和地址空间布局随机化等安全机制的影响,同时,这些指令序列中可能蕴涵着攻击者期望的gadget.在实施攻击时,攻击者可以汇集特定的脚本代码块来构造一个攻击脚本,再借助即时编译器来注入gadget.在x86-64架构上评估了这种注入攻击在Spider Monkey和GoogleV8这两个开源即时编译引擎上的可行性.通过给这两个引擎输入大量的JavaScript脚本,可以得到较为丰富的动态代码块.在这些动态代码块上的统计分析结果表明,这两个引擎生成的动态代码中都存在图灵完备的gadget集合.在实际攻击场景中,攻击者可以利用的脚本集合完全包含且远远多于实验用的脚本.因此,攻击者可以采用该方法注入需要的gadget,以便构造出实现任意功能的ROP(return-oriented programming)代码.

关键词：网页浏览器即时编译机制即时返回导向编程 ROP(return-oriented programming) gadget注入图灵完备计算

来源：评论

学校读者我要写书评

暂无评论

基于MDA的设计模式建模与模型转换

引用

软件学报 2008年第9期19卷 2203-2217页

作者：张天张岩于笑丰王林章李宣东南京大学计算机科学与技术系江苏南京210093 南京大学计算机软件新技术国家重点实验室江苏南京210093

MDA(model driven architecture)的一个重要意图是将模型作为软件开发的基本单元,以进一步提高软件开发的抽象层次.为此,MDA划分了3种抽象级的模型,并通过建立高抽象级的模型和向低抽象级模型及代码的转换来构造可运行的应用程序.在MDA... 详细信息

MDA(model driven architecture)的一个重要意图是将模型作为软件开发的基本单元,以进一步提高软件开发的抽象层次.为此,MDA划分了3种抽象级的模型,并通过建立高抽象级的模型和向低抽象级模型及代码的转换来构造可运行的应用程序.在MDA的框架下,将设计模式作为一种独立的建模和转换单元能够在较高的抽象层次上充分支持复用并提高建模粒度,从而进一步发挥设计模式的优点,提高软件开发效率、降低生产成本.然而,要在MDA的框架下将设计模式作为完整的开发单元来使用,必须解决以模式为单元的建模及转换两个具体问题.针对单元化模式建模的问题,通过扩展MOF(meta object facility)的方式定义了模式单元元模型,并提供了基于此元模型的单元化建模支撑机制,以分离业务模型与模式模型的方式解决了该问题.针对单元化模式模型转换问题,在模式单元元模型的基础上定义了向EJB平台的转换规则.该转换规则使用QVT标准描述,支持单元化的模式模型转换,并具有良好的复用性.

关键词： MDA(model driven architecture)设计模式建模模型转换

来源：评论

学校读者我要写书评

暂无评论

面向危险操作的动态符号执行方法

引用

软件学报 2016年第5期27卷 1230-1245页

作者：王伟光曾庆凯孙浩计算机软件新技术国家重点实验室(南京大学) 江苏南京210046 南京大学计算机科学与技术系江苏南京210046

针对缺陷检测的需求,提出了面向危险操作的动态符号执行方法.依据所关注的缺陷类型,定义危险操作及危险操作相关路径,通过计算覆盖不同上下文中危险操作的能力,协助动态符号执行选择高效初始输入,并利用危险操作相关信息引导测试流程.... 详细信息

针对缺陷检测的需求,提出了面向危险操作的动态符号执行方法.依据所关注的缺陷类型,定义危险操作及危险操作相关路径,通过计算覆盖不同上下文中危险操作的能力,协助动态符号执行选择高效初始输入,并利用危险操作相关信息引导测试流程.缺陷检测成为定位待测程序内危险操作以及对危险操作相关路径进行检测的过程.实现了面向Linux平台二进制可执行程序的原型系统Crash Finder,实验结果表明,该方法能够更快地发现更多缺陷.

关键词：危险操作动态符号执行污点分析路径选择缺陷检测

来源：评论

学校读者我要写书评

暂无评论

网格环境下清空型调度策略应用研究

引用

计算机工程 2005年第21期31卷 28-30页

作者：刘奇志张剡毛奇正南京大学软件新技术国家重点实验室南京大学计算机科学与技术系南京210093

在网格计算中,资源的调度优化特别是请求的调度优化是一个关键技术问题,引入离散事件动态系统中的水箱型混合动态系统模型,对网格上的资源和请求进行一体化建模。清空型调度策略是混合动态系统中一类重要的调度策略,研究了它在网格环境... 详细信息

在网格计算中,资源的调度优化特别是请求的调度优化是一个关键技术问题,引入离散事件动态系统中的水箱型混合动态系统模型,对网格上的资源和请求进行一体化建模。清空型调度策略是混合动态系统中一类重要的调度策略,研究了它在网格环境下的应用性能,提出一种推广形式。重点研究系统模型的建立和调度策略的稳定性分析,给出稳定性证明的理论推导过程和仿真实验结果。为下一代网络中的数据管理提供了一种新思路。

关键词：网格计算水箱型HDS CAF型调度策略

来源：评论

学校读者我要写书评

暂无评论

Pobe:一种基于生成式模型的分布外文本检测方法

引用

软件学报 2024年第9期35卷 4365-4376页

作者：欧阳亚文高源宗石鲍宇戴新宇计算机软件新技术国家重点实验室(南京大学) 江苏南京210023 南京大学计算机科学与技术系江苏南京210023

对于安全可靠的机器学习系统,具备检测训练集分布外(out-of-distribution,OOD)样本的能力十分必要.基于似然的生成式模型由于训练时不需要样本标签,是一类非常受欢迎的OOD检测方法.然而,近期研究表明通过似然来检测OOD样本往往会失效,... 详细信息

对于安全可靠的机器学习系统,具备检测训练集分布外(out-of-distribution,OOD)样本的能力十分必要.基于似然的生成式模型由于训练时不需要样本标签,是一类非常受欢迎的OOD检测方法.然而,近期研究表明通过似然来检测OOD样本往往会失效,并且失效原因与解决方案的探究仍较少,尤其是对于文本数据.从模型层面和数据层面分析文本上失效的原因:生成式模型的泛化性不足和文本先验概率的偏差.在此基础上,提出一种新的OOD文本检测方法Pobe.针对生成式模型泛化性不足的问题,引入KNN检索的方式,来提升模型的泛化性.针对文本先验概率偏差的问题,设计一种偏差校准策略,借助预训练语言模型改善概率偏差对OOD检测的影响,并通过贝叶斯定理证明策略的合理性.通过在广泛的数据集上进行实验,证明所提方法的有效性,其中,在8个数据集上的平均AUROC值超过99%,FPR95值低于1%.

关键词：机器学习分布外检测生成式模型文本检索预训练语言模型

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：