摘要:

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

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

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

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

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

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

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

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

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

摘要:Web 3.0 是以区块链为技术底座的新一代互联网框架, 能够助力数据资产化, 形成可流通的数字资产, 促进数字经济发展. 然而, Web 3.0 在用户生态构建与数字资产流通两方面仍然存在挑战: (1) Web 3.0 用户信任机制多样导致用户数字身份管理难; (2) Web 3.0 数字资产侵权成本低、鉴权粒度粗导致数字资产高效流通难; (3) Web 3.0 开放自治且参与实体多元导致用户生态治理难; (4) Web 3.0 数据公开透明且攻击面多样导致隐私保护与安全监管平衡难. 围绕这4个挑战, 提出面向数据资产化的 Web 3.0 技术架构, 针对数据资产化在身份管理、资产流通、生态治理与安全监管这4个方面的需求, 结合技术自身特点, 对国内外相关的 Web 3.0 技术研究工作进行归纳、分类、分析与总结. 具体包括: (1)分布式数字身份管理机制, 包含数字身份创建、标识鉴别与隐私保护等技术; (2) Web 3.0 数字资产流通机制, 包含数字资产确权、鉴权与流通等技术; (3) Web 3.0 生态治理机制, 包含用户声誉评价与权益激励等技术; (4) Web 3.0 数字资产安全防护与监管技术, 包含主动监管、链上数据监测与应用前端安全分析等技术. 最后, 展望 Web 3.0 技术的未来研究方向.

摘要:遗忘学习在隐私保护、减少污染数据影响和冗余数据处理等方面具有重要应用价值, 但现有的遗忘学习方法多用于神经网络等黑箱模型中, 在可解释的TSK模糊分类系统中实现高效的单类和多类遗忘仍面临挑战. 为此, 提出了一种面向分类的TSK模糊遗忘学习方法(TSK-FUC). 首先, 通过各规则的前件参数在(单类或多类)遗忘数据上的归一化激活强度, 将规则库划分为与遗忘数据高相关的删减规则集、与遗忘数据低相关的保留规则集以及与遗忘数据和保留数据关系较为重叠的更新规则集. 继而采取差异化处理策略: 直接剔除删减规则集, 以消除主要信息残留, 并降低分类系统参数量; 完整保存保留规则集, 以缩小遗忘学习过程的参数调整范围; 对于更新规则集, 通过为每个遗忘类添加噪声, 用以进一步消除规则中关于遗忘数据的信息, 从而实现单类和多类遗忘. 实验结果表明, 在16个真实数据集的已建好的0阶和1阶TSK分类系统上, TSK-FUC能够较为准确地划分规则空间, 并结合差异化的处理展现出良好的单类和多类遗忘效果. 该方法在保持规则库可解释性的同时, 使得遗忘学习后的TSK模糊分类系统在结构上更加轻量化.

摘要:时空逻辑分析是指用逻辑符号准确表达实体间的时空关系. 传统的时空逻辑分析分为封闭域与开放域两种形式. 封闭域方法预先定义了表示时空逻辑的符号体系, 然后将自然语言转换成逻辑语言. 此类方法的优点是对时空关系的表达准确, 但是由于人工定义的局限性, 所定义的体系并不能覆盖复杂的时空关系. 开放域的方法使用自然语言表示时空关系, 也就是将关键词进行抽取. 此类方法的优点是能够覆盖复杂的时空关系, 但是由于自然语言本身存在歧义性, 所表示的逻辑并不精确. 为了将自然语言表达的时空关系转化为逻辑语言, 从而更准确地表达时空信息, 针对如上问题展开研究. 考虑时空关系在语言学范畴主要通过方位词表达, 如果能把方位词的语义用逻辑符号加以定义, 那么既可以解决覆盖不足的问题, 也可以解决表达不精确的问题. 为此, 设计方位词的时空逻辑体系, 定义标注规范, 总结方位词的逻辑表达范围, 给出详细的标注准则; 基于该规范, 在人民日报和CTB两个数据集上手工标注样本6190条, 形成该任务的语料库; 最后基于该语料库, 利用大语言模型对方位词触发的时空逻辑表达式进行推理, 准确率可达到70%以上.

摘要:时序图是一类节点之间交互时带有时间戳的图结构, 其比静态图具有更多的建模优势, 比如可以发现在一定时间区间内的洗钱、刷单、股权关系、金融欺诈、循环担保等行为. 环路是对时序图中的路径组成回路的行为建模. 现有的时序环路检测或挖掘方法大多数关注时间非递减的完全环路检测, 忽略了时间处于一定区间内的近似环路分析与发现, 发现此类近似环路可以检测出一些作弊手段更强的欺诈行为. 针对处于一定时间区间内, 事实上已经出现环路, 但在单一源数据上未完全展示出环路的近似环路发现问题, 提出一种基于深度优先搜索的近似环路检测方法, 简称基线方法(Baseline). 首先在每个窗口内挖掘时间维度上满足非递减顺序的边组成的完全环路, 接着将其中符合一定特征的节点分别作为近似环路的起止点, 并在后续窗口中挖掘处于一定时间区间内的边组成的路径, 即时间区间近似环路. 针对基线方法存在的问题, 提出一种优化的近似环路检测方法, 简称优化方法(Improved). 首先利用节点的活跃度来提升起止点的可能性, 接着使用活跃路径和热点来优化索引的特征, 最后运用起止点到热点的双向搜索与连接来加快检测速度. 在真实数据和人工数据上进行的大量实验证明了所提方法的高效性与有效性.

摘要:随着5G技术的快速发展, 5G-AKA协议作为5G技术的核心安全机制, 受到广泛关注. 5G-AKA协议的部署推动了通信网络的高速互联, 但也带来了用户对隐私泄露的担忧. 运营商在协议交互过程将收集大量数据, 这些数据一旦泄露, 将给用户造成严重的威胁. 因此, 提出基于SM2的匿名认证与密钥协商协议, 实现用户认证过程的隐私增强, 达到用户信息的最小揭露. 扩展了国密SM2数字签名算法实现对多消息的签名, 结合ElGamal算法对用户的身份进行加密并利用零知识证明技术保证用户证书的匿名性, 有效实现对用户身份的匿名认证. 协议保护合法用户在网络活动中的身份隐私, 并有效阻断对用户信息的非法获取. 此外, 协议还具备对恶意用户的可追责性, 其允许经授权的监管机构在合法流程下还原出用户身份. 最后, 开展协议实验测评, 基于Windows及Raspberry Pi 4B平台上进行部署和实现. 测评结果显示, 匿名认证与密钥协商过程耗时均为毫秒级, 充分展示了所提协议的高效性与实用性.

摘要:随着深度学习和计算机视觉的快速发展, 灰度图像着色研究已从传统手工特征设计转向数据驱动的深度神经网络范式. 然而, 现有的灰度图像着色模型评估体系面临双重挑战: 其一, 由于评价指标的局限性以及着色任务的高度病态性本质, 传统评价指标(如PSNR、SSIM和FID等)难以准确量化着色模型性能; 其二, 开展大规模主观实验进行定性分析耗时费力且可行性差. 针对上述问题, 提出了基于难样本挖掘的灰度图像着色模型评估方法. 该方法旨在通过多维度差异化(包括图像质量、美学表现和颜色差异)比较, 高效地挖掘用于比较着色模型的代表性样本; 随后开展可控小规模主观实验, 可靠地比较不同模型的性能, 并指出不同模型的优势和不足. 实验结果表明: 提出的方法能够高效、准确地找到模型的难样本, 在极大幅度地减小主观实验规模的同时, 揭示模型的优缺点, 为灰度图像着色模型评估提供了新范式, 并为模型优化指明方向.