摘要:在DevOps持续集成实践中,Web应用的高频代码迭代对传统静态分析工具提出了严峻挑战:全量扫描模式导致计算资源浪费与分析延迟,而现有增量分析技术因对多样化漏洞检测能力的缺失以及精度,效率与一致性的矛盾,难以满足实际需求.对此,本文提出一种面向Web应用漏洞检测的增量静态分析框架AWTaint.该框架具备域敏感,上下文敏感与流敏感能力,其利用函数摘要表征输入输出变量之间的映射关系,产出与各类检测规则相关的污点传播信息.本框架采用了一种细粒度的增量计算方法,首先利用调用图估算保守的增量变化范围,其次利用函数摘要变化感知具体影响范围.从而有效满足工业级Web应用漏洞检测对分析精度,计算效率与结果一致性的三项核心要求.实验表明,在包含10个真实Java Web应用的测试集上,AWTaint可以支持多种Web应用漏洞检测需求,其增量分析模式相较全量分析模式平均加速3.63倍,内存峰值控制在8GB以内,且漏洞检测完全一致性.该框架为安全左移实践提供了工程化解决方案,在保障检测精度的前提下,显著优化了资源利用率与开发迭代效率.

摘要:混成通信顺序进程(Hybrid Communicating Sequential Processes,简称HCSP)是一种广泛应用于混成系统建模的形式化语言.它结合了由逻辑驱动的状态跳转(典型于数字计算)和由微分方程驱动的连续演化(用于刻画物理过程),从而统一刻画了离散与连续行为.这种双重特性使其尤其适用于建模通常具有安全关键性的信息物理系统(Cyber-Physical Systems,简称CPSs).然而,由于混成系统实现复杂、同步行为错综交织,其验证在实际中面临显著挑战.为此,本文提出了一种用于验证从抽象模型到具体实现之间精化关系的逻辑体系——混成精化逻辑(Hybrid Refinement Logic,简称HRL).HRL通过按照系统的结构进行分解,并基于精化构造分层的证明过程,从而提升了验证的可复用性和模块化程度.此外,HRL还支持并行同步进程与顺序进程之间的精化验证,进一步降低了证明复杂性,有效减轻了验证负担.

摘要:传统程序分析方法在处理大规模软件时,常需显式构建依赖图(如系统依赖图、程序依赖图),因程序实体与依赖关系数量随规模呈指数级增长而面临”构图困难”与冗余计算的性能瓶颈.为应对此挑战,本文提出一种基于按需切片计算的并行化程序分析框架.该框架融合了符号化切片与高阶函数摘要技术,其核心思想是：(1)通过将函数调用的影响抽象为可复用的高阶函数式摘要,通过动态函数求值替代显式依赖图存储与遍历,从根本上规避了构图瓶颈;(2)设计了一种针对高阶函数摘要的按需实例化机制,基于用户指定的切片准则(如关键变量),动态地、惰性地实例化摘要,仅计算与分析目标直接相关的依赖,从而大幅削减了计算冗余.该框架通过子分析摘要的独立性和惰性实例化特性,实现了任务的细粒度划分,展现出良好的并行潜力.实验结果表明,该框架下的按需切片计算较符号化切片工具(Sympas)在分析时间上减少了65.3%,内存峰值下降了68.2%;其并行化版本(6线程)时间进一步减少93.8%,并行效率接近90%.为验证该框架在大型程序分析中的实用性与有效性,将该框架应用于访问越界缺陷检测,成功识别了132个真阳性实例,为解决大规模软件分析的性能瓶颈提供了新的形式化解决思路.

摘要:软件形式化验证是通过数学方法和逻辑推理确保软件系统的正确性和可靠性，广泛应用于高安全性要求领域。然而，传统形式化验证技术面临自动化程度低、推理效率不足、规模化困难等挑战，难以满足复杂软件系统快速发展的需求。近年来，大语言模型（LLMs）的快速发展为自然语言处理、代码理解与生成等领域带来了革命性突破，也为形式化验证领域提供了新的自动化解决方案。为了全面梳理和分析大语言模型赋能软件形式化验证领域的研究现状与发展趋势，本文对相关研究成果进行综述。首先，概述软件形式化验证技术的核心流程与方法，以及大语言模型在该领域应用的关键技术。进一步，聚焦LLMs在两大核心场景中的应用：1）自然语言到形式化规约的转换：通过分析LLMs如何将模糊的自然语言形式的需求自动转化为形式规约，降低形式化验证中的模型构造与性质规约转换的门槛；2）在程序验证中辅助推理与证明：探讨LLMs在定理证明器技术中辅助生成证明过程，包括通过代码分析自动提取前/后置条件与不变量等用于辅助性规约的潜力，以及在模型检测中约简状态空间或优化验证策略的可能性。最后，本文总结了大语言模型技术在软件形式化验证中面临的共性挑战与未来可能的发展方向。

摘要:形式化数学是一次数学革命,结合定理证明器的数学定理机器证明,不仅是对数学严谨性的一种新标准,更是发展数学的一种新方式.随着世界范围不断有数学难题在计算机辅助下的成功解决,以及各路专家学者对各种数学形式化项目或工程的发起,形式化数学的影响力与日俱增.国际数学家陶哲轩即于2025年5月发起了一个基于定理证明器Lean的数学分析形式化项目,在数学界与计算机界引起广泛影响.本文介绍一项基于定理证明工具Coq的数学分析形式化系统,该系统以华东师范大学数学系编著的《数学分析》为蓝本,在朴素集合论和初等数论及代数知识体系下进行开发,当前,已经实现其上册中一元微积分相关内容的形式化,包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、不定积分、定积分等内容.我们开发的系统严格对应教材内容,全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过.读者可以跟随代码学习数学,也能够对照数学理解代码,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,实现让读者跟随计算机学习、理解、构建、教育乃至发展现代数学的尝试,提高认识数学、感受数学和欣赏数学的素养.

摘要:在复杂软件系统开发过程中,设计阶段与验证阶段的有效衔接是确保系统可靠性和功能正确性的关键.然而,设计工具与验证工具在建模语言、语义和数据结构上的异构性,易导致模型转换语义不一致、工具链互操作性不足以及验证覆盖不充分.为解决上述挑战,本文提出一种基于统一中间表示的分层转换与多重交叉验证机制.该机制以设计模型为起点,结合系统理论过程分析(STPA)开展危险分析与不安全控制行为识别,提炼安全约束,并与既有的功能、时间和安全属性进行互补校验.随后,构建设计模型到统一中间表示(UIR,Unified Intermediate Representation)的映射,在统一语法与语义域中形式化描述结构、行为、时序与安全约束,并据此给出覆盖上述要素的分层转换规则及其追溯性元数据.基于UIR,派生时序模型、逻辑模型与概率模型等互补的验证模型,并将STPA导出的安全约束系统化映射为可验证属性,开展源-中间-目标模型的一致性检查、时序与逻辑性验证、概率性分析以及安全约束可满足性验证等多视角交叉验证.以自动驾驶汽车控制系统以及多域协同无人机控制系统为例的实际案例结果表明,所提方法提高了验证的覆盖度与准确性,增强了转换与验证过程的可追溯性,为复杂系统的安全驱动开发提供了一条一致且可证的技术路径.

摘要:近年来,基于大模型的代码生成被广泛应用于软件开发领域.然而,由于大模型生成结果具有一定的随机性,如何保证生成代码的正确性成为重中之重.形式化验证是保障软件正确性的一种有力手段,但验证前需要将代码及相应需求形式化为相关工具的规约语言.Dafny是一种可验证的编程语言,并有相应的自动化验证工具支持.本文旨在探索大模型在将Python代码翻译为Dafny语言方面的能力.为此,本文提出了基于提示词的静态翻译和动态修复的翻译生成方法以及基于程序测试的翻译结果评估方法.静态翻译方法考虑三种渐进的提示词模板(基础模板,Dafny示例模板,对照示例模板),使用大模型一次性生成翻译;动态修复方法多次调用大模型对翻译进行修复,每次将上一轮代码测试的错误信息加入提示词.评估时,在没有现成测试用例集的情况下,利用大模型生成测试用例集;对翻译结果结合测试用例集应用Dafny测试工具进行测试以评估其正确性.我们在GPT-4o和DeepSeek-V3等大模型上使用HumanEval、MBPP和LeetCode等数据集进行了实验.结果表明,使用对照示例模板和动态修复方法能够有效提升大模型在Python到Dafny翻译任务上的表现.此外,本文还基于实验结果分析了影响翻译质量的因素,并对评估方法与标准进行讨论.

摘要:时间自动机的主动学习是一个重要的研究话题.多时钟时间自动机的主动学习是其中一个重要的研究方向.然而,已有的多时钟时间自动机的学习算法的学习速度较慢.在本文中,基于时间观察树提出一种改进的主动学习算法.定义一种名为时间观察树的数据结构,用于存储学习过程中获取的信息.基于时间观察树的特殊结构,可以利用二分搜索技术来分析反例.通过使用该反例分析技术,可以减少成员查询的数量和重置信息查询的数量,从而提高算法的效率.实验结果证明了该方法的有效性.

摘要:深度强化学习虽已在多种复杂任务中取得卓越成果,但其策略在动态高维环境下仍缺乏实时安全保障,因而亟需在部署阶段引入能够实时评估并纠正智能体决策的安全监控机制.现有数据驱动的黑盒监控方法侧重离散或二元决策,难以直接迁移到连续动作空间.针对上述问题,本文提出了模糊映射熵驱动的安全监控框架,仅依赖状态、动作和成本数据即可构建,无需任何环境模型.该方法首先利用高斯混合模型（GMM）对离线收集的安全轨迹进行状态簇硬划分和动作簇软隶属,并提出模糊映射熵在兼顾均衡性与模型复杂度的前提下自适应确定最优动作簇数.随后在?Mamdani?框架下构建模糊逻辑规则,并通过残差网络与对抗判别器联合微调簇中心,使生成动作更贴近真实的安全分布.在线阶段,监控器基于?GMM?后验概率计算每条待执行状态—动作对的簇一致性度量.一旦该度量低于阈值,即通过模糊推理生成平滑的安全替换动作,从而在风险发生之前完成修正.本文在?Safety?Gymnasium?的三个导航任务上,对?PPO?Lag、TRPO?Lag?与?CPPO?PID?策略进行了监控评估.结果显示,该框架在几乎不降低乃至略微提升任务回报的前提下,显著降低累计安全成本,并保持较高的预警覆盖率,验证了该监控框架在连续动作场景中的有效性和实用性.

摘要:相较于初代微内核,第二代微内核L4在性能和灵活性方面显著提升,并在众多领域获得广泛应用.操作系统内核的正确性与可靠性对系统稳定运行起着决定性作用.本研究聚焦于L4微内核的关键机制——线程管理,对其展开形式规约与验证.本文首先构建安全规约以描述安全性质,复用标准的L4 API功能规约明确功能正确性,同时自动生成基于C++源代码的实现规约.为缓和功能规约与实现规约间的巨大差异,本文引入中间规约.其中,前两种规约采用Isabelle/HOL形式化语言编写,后两种则以Python语言表达.通过解释(Interpretation)、建立正向模拟(Forward Simulation)等方法,精化证明各规约间的一致性.在证明过程中,将交互式验证与auto-active验证方法相结合,提升验证自动化能力的同时,减少人工证明工作量.最终发现源代码中存在三个违反正确性和安全性的问题,并针对这些问题提出解决方案.