本文研究的是零知识机器学习（ZKML）电路中的「冗余检查」问题及其可证明安全的去膨胀（debloating）技术。背景是：面向神经网络推理的零知识证明系统会把模型编译成大规模算术约束系统，其中包含大量范围证明、符号查找（sign lookup）、比特分解等约束。作者指出，这些约束中有相当一部分是「冗余检查」——它们所断言的事实在整条电路上已经被其他远处的组件通过一连串推理关系所蕴含，因此单看局部是必要的，但从全局看其约束力是多余的。删除这类冗余约束能显著缩小电路规模、加快证明生成，但删除必须以严格的可靠性（soundness）论证为前提：一旦删得不合理，电路就会变成欠约束（under-constrained），证明者可以构造出原电路本应拒绝的见证，例如谎称某个神经网络产生了它实际上并未计算过的输出。作者强调这不是假设性威胁——已部署的 ZK 系统中出现过的欠约束电路缺陷，曾使攻击者能够伪造交易并完全绕过验证。 核心方法上，作者提出一个自动化框架：对每一个候选删除的约束，工具首先判断「电路其余部分」自身是否仍然能够排除被删约束原本排除的所有取值。为此，工具使用全电路抽象解释（whole-circuit abstract interpretation）来搜索这些替代性论证，并把它们记录在一张溯源图（provenance graph）中；只有当图中存在一条替代路径仍然能够推导出该约束所检查的事实时，才真正删除该约束。这一「先证明替代论证存在、再删除」的流程，从机制上保证去膨胀后的电路不会为敌手开启新的伪造路径，即在不削弱安全性的前提下完成优化。 实验方面，作者在 ezkl 与 zkml 两个生产级框架生成的 MLP、CNN、RNN 与 Transformer 电路上进行评估，电路规模最高达 2530 万条约束。结果显示，工具可移除最高 48.7% 的约束，并把证明者（prover）耗时最多降低 72.8%，同时不削弱安全性。该工作适合零知识证明工程、ZKML 系统开发者、形式化验证与程序分析研究者，以及关注 ZK 电路可靠性漏洞的安全工程师阅读。

本文是第20届编程语言与安全分析研讨会(PLAS 2025)的会议通知。PLAS为学术界和工业界提供了一个探讨如何利用编程语言和程序分析技术来增强软件系统安全性的论坛，覆盖范围从底层编译器到机器学习模型和智能合约等新兴领域。研讨会鼓励提出新颖且富有前瞻性的观点，对新兴威胁和问题进行讨论，并特别欢迎立场论文，以激发关于编程语言与安全交叉领域未来研究方向的深刻讨论。自2007年在圣地亚哥首次举办以来，PLAS已走过20年，成为该领域的重要学术活动。今年的会议将包括两场主旨演讲（分别由Limin Jia和Jan Reineke主讲）以及5篇论文报告。对于安全防御者而言，该研讨会所呈现的研究成果可能推动更先进的静态分析、形式化验证、类型系统、程序修复等技术，从而提升软件供应链安全、智能合约审计以及机器学习模型的可信性。虽然本通知未提供具体技术细节，但其中提及的研究方向对于构建更可靠的漏洞检测工具和开发安全方法具有潜在价值。

本文介绍了一种结合静态与动态程序分析的方法，用于推断和执行服务端 JavaScript 中第三方库的权限。现代软件开发广泛依赖第三方库，但这些库通常未经人工审查，可能引入 bug、漏洞或恶意攻击，最终影响终端用户。作者提出一个以 RWX（读-写-执行）权限系统为核心的分析框架，该权限系统横跨库边界，能够对第三方库的行为进行细粒度约束。在演示中，作者展示了该工具能够检测出注入到流行库中的零日漏洞，而这些漏洞往往被现有先进工具（如 snyk test 和 npm audit）遗漏。该方法通过静态分析提取库的权限需求，并通过动态分析对实际执行行为进行监控与比对，从而发现违规调用或异常行为。主要贡献包括：提出了一个针对第三方库权限建模的统一框架；实现了结合静态和动态分析的原型工具；并通过实验证明了其在检测未知漏洞方面的有效性。适合软件安全研究人员、DevSecOps 工程师以及关注供应链安全的开发者阅读。

本文是关于第18届编程语言与安全分析研讨会（PLAS）的会议介绍。PLAS 是一个专注于探索和评估编程语言与程序分析技术在安全领域应用的学术论坛，覆盖范围广泛，从编译器、机器学习模型到智能合约等各类软件系统。研讨会鼓励提出新颖的、探索性的想法，评估新技术或已有技术在实际环境中的效果，并讨论新兴威胁与问题。此外，PLAS 还欢迎立场论文，这些论文通常具有前瞻性和激进性，旨在引发富有洞察力的讨论，从而影响编程语言与安全交叉领域的未来研究方向。本届研讨会是该系列的第18届，首届于2007年在圣地亚哥举行。会议预计将呈现精彩的项目和丰富的讨论。

本文提出一种名为 VetSC 的新型自动化安全审查技术，针对去中心化应用（DApps）中的智能合约。由于 DApps 的业务逻辑通常由链上合约与链下界面共同组成，传统静态分析难以直接从合约代码中提取高层业务语义，也无法自动确定需要验证的安全属性，导致安全审查高度依赖人工。VetSC 采用界面驱动（UI-driven）的程序分析引导的模型检测方法：首先从合约代码中提取业务模型图（business model graphs），以捕获其内在的业务和安全逻辑；随后，从 DApp 的用户界面中检索文本语义，自动推理出应检查的安全规范（safety specifications）。为了防止不可信的界面文本误导分析，VetSC 还会校验界面与合约逻辑的一致性，检测二者之间的偏差。作者实现了 VetSC 原型，并将其应用于 34 个真实 DApp。实验表明，VetSC 能够准确解释智能合约代码、实现自主安全审查，并在真实 DApp 中发现安全风险。利用该工具，作者在真实场景中发现了 19 个新的安全风险，例如过期的彩票仍可兑奖、同一用户重复投票等问题。该技术的主要贡献在于将自然语言界面信息与合约代码分析结合，实现了安全属性的自动推导，显著降低了 DApps 安全审查的人工门槛。适合区块链安全研究人员、智能合约审计人员以及 DApp 开发者阅读。

该论文针对Android恶意软件检测问题，指出现有方法基于表面信号（如学习特征或代码片段）进行检测，容易产生误报和漏报，因为偏离代理信号并不等同于恶意。作者提出行为导向的检测方法，并实现系统Praxis。Praxis采用假设-确认-判断流水线：首先从粗粒度静态信号假设候选行为，然后通过程序分析验证代码证据来确认行为，最后在上下文中判断确认的行为是否真正恶意（考虑用户意识、应用功能上下文以及它们如何组合成攻击）。对于恶意应用，Praxis返回判决和支持的行为。实验在三个挑战性场景下与七种基线方法对比，整体F1达到87.4%，比基线提高18.6-34.8个百分点；在高权限良性应用上，误报率降至13.0%，比基线降低41.1-67.0个百分点；在细粒度恶意行为恢复上，F1达到87.3%，比先前行为级方法提高56.5-73.4个百分点。消融实验证明各阶段均有贡献。

该论文提出了一种名为JUNID的方法，旨在提升静态分析中处理不完整句子交集问题的渐近最优性。静态分析是软件安全中的重要技术，用于在不执行程序的情况下检测潜在漏洞。然而，当分析涉及不完整的程序片段或部分代码时，现有交集算法的效率可能下降。JUNID通过理论优化，实现了在渐近意义下最优的交集计算，从而更高效地处理不完整句子。该方法可能适用于符号执行、抽象解释等场景，能够提高静态分析工具的精度和速度。由于仅提供摘要，具体算法细节和实验验证需参考全文。该研究为静态分析领域提供了理论贡献，尤其对需要处理部分代码的漏洞检测场景具有潜在价值。