软件学报最新期刊目录
面向自动驾驶系统的场景建模及边缘关键场景生成————作者：杜德慧;叶振;郑成行;朱珍珍;李家蕴;
摘要：自动驾驶中极端的场景、无法预测的人类行为等长尾问题逐渐成为制约自动驾驶系统(autonomous driving system, ADS)发展的关键要素,因此有效地生成安全关键场景对于提高自动驾驶系统的安全性至关重要.现有的自动驾驶场景生成主要依赖于大量的路采数据,采用数据驱动式场景生成方法,并结合场景泛化技术生成相应的驾驶场景.该方法耗时耗力,成本高,而且难以有效生成边缘场景.而模型驱动式场景建...
因果时空语义驱动的深度强化学习抽象建模方法————作者：田丽丽;杜德慧;聂基辉;陈逸康;李荥达;
摘要：随着智能信息物理融合系统(intelligent cyber-physical system, ICPS)的快速发展,智能技术在感知、决策、规控等方面的应用日益广泛.其中,深度强化学习因其在处理复杂的动态环境方面的高效性,已被广泛用于ICPS的控制组件中.然而,由于运行环境的开放性和ICPS系统的复杂性,深度强化学习在学习过程中需要对复杂多变的状态空间进行探索,这极易导致决策生成时效率低下和泛化性...
面向智能体路径规划算法的动态随机测试方法————作者：张逍怡;李幸;刘洋;郑征;孙昌爱;
摘要：智能体路径规划算法旨在规划某个智能体的行为轨迹,使其在不碰到障碍物的情况下安全且高效地从起始点到达目标点.目前智能体路径规划算法已经被广泛应用到各种重要的物理信息系统中,因此在实际投入使用前对算法进行测试,以评估其性能是否满足需求就非常重要.然而,作为路径规划算法的输入,任务空间中威胁障碍物的分布形式复杂且多样.此外,路径规划算法在为每个测试用例规划路径时,通常需要较高的运行代价.为了提升路径规划...
基于下推自动机的同步数据流语言可信编译————作者：于涛;王珊珊;徐芊卉;董晓晗;胡代金;罗杰;杨溢龙;吕江花;马殿富;
摘要：同步数据流语言Lustre是安全关键系统开发中常用的开发语言,其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证,对用户也处于黑盒状态.近年来,通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法被证明是成功的.基于下推自动机的编译方法和基于语义一致性的验证方法,提出Lustre语言可信编译方法,能够将Lustre语言转换为C语言并进行形式化验证以保证编译的正...
基于函数间结构特征关联的软件漏洞检测方法————作者：邱少健;程嘉濠;黄梦阳;黄琼;
摘要：漏洞检测是软件系统安全领域的关键技术.近年来,深度学习凭借其代码特征提取的卓越能力,在漏洞检测领域取得了显著进展.然而,当前基于深度学习的方法仅关注于代码实例自身的独立结构特征,而忽视了不同漏洞代码间存在的结构特征相似关联,限制了漏洞检测技术的性能.针对这一问题,提出了一种基于函数间结构特征关联的软件漏洞检测方法 (vulnerability detection method based on c...
单球驱动平衡机器人运动学和动力学形式化验证————作者：张善强;张景芝;施智平;王国辉;关永;
摘要：单球驱动平衡机器人是一种具有全向运动性的机器人,其灵活性能在狭小或复杂环境中得到充分体现,因此受到广泛关注.在该型机器人运动学和动力学设计过程中,保证其模型的正确性至关重要.基于测试和仿真的传统方法难以穷尽系统所有状态,因此可能无法捕捉到某些设计缺陷或潜在的安全风险.为确保单球驱动平衡机器人满足安全攸关机器人的正确性、安全性验证要求,在定理证明器HOL Light中,基于实分析库、矩阵分析库、机器...
面向函数内联场景的二进制到源代码函数相似性检测方法————作者：贾昂;范铭;徐茜;晋武侠;王海军;刘烃;
摘要：二进制到源代码函数相似性检测是软件组成成分分析的基础性工作之一.现有方法主要采用一对一的匹配策略,即使用单一的二进制函数和单一的源代码函数进行比对.然而,由于函数内联的存在,函数之间的映射关系实际上表现为一对多——单一的二进制函数能够关联至多个源代码函数.这一差异导致现有方法在函数内联场景下遭受了30%的性能损失.针对函数内联场景下的二进制到源代码函数匹配需求,提出了一种面向一对多匹配的二进制到源...
结合特征生成与重放的可扩展安全虹膜识别————作者：赵冬冬;宋宝刚;廖虎成;闫江;向剑文;
摘要：随着信息技术的快速发展,安全认证技术成为个人隐私和数据安全的重要保障.其中,虹膜识别技术凭借其出色的准确性和稳定性,被广泛应用于系统访问控制、医疗保健以及司法实践等领域.然而用户的虹膜特征数据泄露,就是永久性丢失,无法进行更改或者撤销.因此,虹膜特征数据的隐私保护尤为重要.随着神经网络技术在图像处理上体现的突出性能,基于神经网络的安全虹膜识别方案被提出,在保护隐私数据的同时保持了识别系统的高性能....
分布式系统动态测试技术研究综述————作者：陈元亮;马福辰;周远航;颜臻;姜宇;孙家广;
摘要：分布式系统是当今计算生态系统的支柱,它使得现代计算更加强大、可靠和灵活,覆盖了从云计算、大数据处理到物联网等多个关键领域.然而,由于系统的复杂性,分布式系统在代码实现过程中总是不可避免地引入一些代码缺陷,从而对系统的可用性、鲁棒性以及安全性造成巨大威胁.因此,分布式系统的测试以及缺陷挖掘工作十分重要.动态测试技术在系统运行中进行实时分析,以挖掘其缺陷,评估其行为和功能,被广泛用于各种系统应用的缺陷...
面向Rust语言的形式化验证方法研究综述————作者：张卓若;常瑞;杨申毅;陈芳;
摘要：Rust作为一种新兴的安全系统级编程语言,以其创新的所有权模型和借用检查机制提供了内存安全和并发安全保证.尽管Rust的设计宗旨在于安全性,但现有研究揭示了其仍面临诸多安全挑战.形式化验证作为一种基于严格数学基础的方法,为Rust安全性提升提供了强有力保障.通过构建精准清晰的语义模型,可以证明遵循Rust检查规则的程序满足安全性要求;借助Rust自动化验证工具能够帮助用户确保其Rust程序的安全性...
基于混成自动机路径过滤与动态选择的CPS系统反例生成————作者：王佳宛;刘熹橦;卜磊;李宣东;
摘要：信息物理融合系统(cyber-physical system, CPS)在安全攸关领域具有广泛的应用,保障其安全性至关重要.形式化验证是证明系统安全性的有效手段,但在现实世界中的复杂CPS系统上应用仍面临挑战.因此,反例生成的方法被提出,旨在通过寻找系统中违背安全规约的反例行为来证明系统的不安全.现有的基于路径的CPS系统反例生成方法采用分治策略,针对系统模型中各条路径上的行为空间分别进行探索,能...
深度学习编译器缺陷实证研究:现状与演化分析————作者：沈庆超;田家硕;陈俊洁;陈翔;陈庆燕;王赞;
摘要：深度学习编译器已被广泛应用于深度学习模型的性能优化和部署.与传统编译器类似,深度学习编译器也存在缺陷.存在缺陷的深度学习编译器会导致编译失败或者产生错误的编译结果,甚至有时会带来灾难性的后果.为了深入理解深度学习编译器缺陷的特性,已有工作针对深度学习编译器早期的603个缺陷进行研究分析.近年来,深度学习编译器在快速迭代更新,伴随着大量新特性的引入和旧特性的弃用.与此同时,一些针对深度学习编译器缺陷...
操作系统内核权能访问控制的形式验证————作者：徐家乐;王淑灵;李黎明;詹博华;吕毅;代艺博;崔舍承;吴鹏;谭宇;张学军;詹乃军;
摘要：操作系统内核是构建安全攸关系统软件的基础.任何计算机系统的正确运行都依赖于底层操作系统实现的正确性,因此,对操作系统内核进行形式验证是很迫切的需求.然而,操作系统中存在的多任务并发、数据共享和竞争等行为,给操作系统内核的验证带来很大的挑战.近年来,基于定理证明的方法广泛用于操作系统各功能模块的形式验证,并取得多个成功应用.微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制,旨在防止未经授权...
动态顺序统计树类结构的函数式建模及其自动化验证————作者：左正康;刘增鑫;柯雨含;游珍;王昌晶;
摘要：动态顺序统计树结构是一类融合了动态集合、顺序统计量以及搜索树结构特性的数据结构,支持高效的数据检索操作,广泛应用于数据库系统、内存管理和文件管理等领域.然而,当前工作侧重讨论结构不变性,如平衡性,而忽略了功能正确性的讨论.且现有研究方法主要针对具体的算法程序进行手工推导或交互式机械化验证,缺乏成熟且可靠的通用验证模式,自动化水平较低.为此,设计动态顺序统计搜索树类结构的Isabelle函数式建模框...
GhostFunc:一种针对Rust操作系统内核的验证方法————作者：何韬;董威;文艳军;
摘要：操作系统是软件的基础平台,操作系统内核的安全性往往影响重大. Rust是逐渐兴起的内存安全语言,具有生命周期、所有权、借用检查、RAⅡ等安全机制,使用Rust语言构建内核逐渐成为当前热门的研究方向.但目前使用Rust构建的系统多包含部分unsafe代码段,无法从根本上保证语言层面的安全性,因而针对unsafe代码段的验证对于保证Rust构建的内核正确可靠尤为重要.以某使用Rust构建的微内核为对象...
干扰惰性序列的连续决策模型模糊测试————作者：吴泊逾;王凯锐;王亚文;王俊杰;
摘要：人工智能技术的应用已经从分类、翻译、问答等相对静态的任务延伸到自动驾驶、机器人控制、博弈等需要和环境进行一系列“交互-行动”才能完成的相对动态的任务.执行这类任务的模型核心是连续决策算法,由于面临更高的环境和交互的不确定性,而且这些任务往往是安全攸关的系统,其测试技术面临极大的挑战.现有的智能算法模型测试技术主要集中在单一模型的可靠性、复杂任务多样性测试场景生成、仿真测试等方向,对连续决策模型的“...
基于代码控制流图的庞氏骗局合约检测————作者：黄静;王梦晓;韩红桂;
摘要：区块链在加密货币投资领域展现出强劲的生命力,吸引了大量投资者的参与.然而,由于区块链的匿名性,导致了许多欺诈行为,其中庞氏骗局智能合约就是一种典型的欺诈性投资活动,给投资者带来了巨大的经济损失.因此,对以太坊上的庞氏骗局合约进行检测变得尤为重要.但是,现有研究大都忽略了庞氏骗局合约源代码中的控制流信息.为提取庞氏骗局合约更丰富的语义信息和结构信息,提出一种基于代码控制流图的庞氏骗局合约检测模型.首...
移动应用GUI测试自动生成技术综述————作者：王博;陈冲;邓明;董震;林友芳;郝丹;
摘要：移动应用是近10年来兴起的新型计算模式,深刻地影响人民的生活方式.移动应用主要以图形用户界面(graphical user interface, GUI)方式交互,而对其进行人工测试需要消耗大量人力和物力.为此,研究者提出针对移动应用GUI的测试自动生成技术以提升测试效率并检测潜在缺陷.收集了145篇相关论文,系统地梳理、分析和总结现有工作.提出了“测试生成器-测试环境”研究框架,将该领域的研究按...
LLM赋能的Datalog代码翻译技术及增量程序分析框架————作者：王熙灶;沈天琪;宾向荣;卜磊;
摘要：Datalog是一种声明式逻辑编程语言,在不同领域得到了广泛应用.近年来,学术界和工业界对Datalog的兴趣高涨,设计并开发了多种Datalog引擎和相应方言.然而,多方言带来的一个问题是以一种Datalog方言实现的代码,一般而言不能在另一种方言的引擎上执行.因此,当采用新Datalog引擎时,需要将现有Datalog代码翻译到新方言上.目前的Datalog代码翻译技术可分为人工重写代码和人工...
软件供应链SBOM关键技术研究————作者：孙泽雨;吴敬征;凌祥;魏怡琳;罗天悦;武延军;
摘要：供应链级别的开源软件及组件复用是当前软件开发的主流模式.该模式避免了重复开发,降低了研发成本,提高了开发效率,但是也不可避免地存在组件的来源未知,成分不清,漏洞不明,许可证违规等问题.为解决上述问题,研究人员提出了软件物料清单(software bill of material, SBOM). SBOM详细列出了构成软件的组件及组件之间的关系,揭示了潜在的和已知的威胁,使软件透明化.自提出以来,国...
