15 篇内容
文章讨论在 TEE 中运行 MPC/门限签名的安全边界，强调 TEE 只能作为纵深防御层，不能替代协议本身的安全性。作者先区分半诚实与恶意安全模型，说明 TEE 的机密性、完整性和远程证明可在正确实现时缓解参与者作恶，但会把信任集中到硬件厂商，并引入不可信主机这一新攻击面。文中归纳审计常见陷阱：证明范围不完整、验证步骤缺失、镜像未加固、备份/文件系统回滚、侧信道与物理攻击、厂商默认策略过宽。并以门限签名为例，恶意主机可在预签名删除后回滚文件系统，造成 nonce 复用和私钥份额泄露。最后给出实践建议：证明绑定参与方身份、在 TEE 内终止点对点通信、完整验证测量值、恒定时间实现，并尽量使用多厂商 TEE。
推荐收录：文章不是泛泛介绍 TEE 或 MPC，而是基于安全审计经验给出具体攻击路径（如预签名回滚导致 nonce 复用）和可执行的最佳实践，涵盖证明验证、信任模型、侧信道与厂商默认策略。适合安全工程师、密码协议实现者和机密计算架构师阅读，可作为审查 TEE+MPC 部署的检查清单；需注意部分风险细节依赖具体厂商和版本。
文章从历史与协议设计角度批判SAML，指出其源于四套XML安全规范的合并，并存在五大缺陷：基于XML、规范化、封装签名、大而全设计与协议僵化。作者结合XSW、XML注释绕过、解析器差异和libxml2怪癖等真实攻击，说明这些缺陷为何长期难修，且多数实现依赖复杂的libxmlsec。文章认为除SP与IdP无法直连等少数场景外，OIDC在网络假设、渐进演进及移动/SPA/IoT适配上更优，并给出SP优先支持OIDC、IdP制定弃用计划等迁移路径。其边界是未量化比较XML与JSON复杂度，偏架构与安全分析而非实现教程，也承认OIDC并非完美。
推荐收录。文章不只是批评SAML，而是以委员会合并历史、XSW与规范化等五类缺陷、解析器差异攻击和OIDC演进时间线为直接证据，给出可执行的迁移建议。适合身份认证、安全架构、协议设计和技术选型读者；其把安全缺陷反推为协议设计检查项的思路可迁移到新认证协议设计，但需注意OIDC并非零风险，存量SAML兼容仍是迁移约束。
Trail of Bits 复盘为 Miden zkVM 做安全审计的准备工作：面对缺少工具链的 MASM 汇编，团队用 AI agent 从零构建 LSP、反编译器、静态分析引擎和 Lean 执行器模型。静态分析借助抽象解释检查 prover advice 值验证、类型约束与变量初始化，发现 400 多处类型验证问题和 mod_12289 未验证余数可伪造 Falcon 签名的高危漏洞。Lean 自动翻译与建模产生 95 个机器检查证明，覆盖核心库二进制算术，并发现 rotr、wrapping_mul 两个单元测试遗漏的边界错误。作者认为 agent 成本下降使高探索性安全工具项目变得可行，但工具仅覆盖 MASM 子集，证明覆盖和定理陈述仍需人工审查。
推荐收录，因为文章给出了可核验的完整案例：用 agent 构建 LSP、反编译器、抽象解释静态分析和 Lean 形式化模型，并具体发现可伪造 Falcon 签名的高危漏洞与 95 个机器检查证明。对安全审计、zkVM 和 AI 辅助工程读者而言，其工具链建设、agent 分工与人工审查边界可直接迁移；但工具仅正确处理 MASM 子集，形式化证明仍需人工检查定理陈述。
Trail of Bits 质疑 1Password 的 AI 补丁基准，认为其“仅 26% 干净修复”的标题误导：样本刻意选复杂漏洞，22% 试验要求应用错误补丁，36% 禁止编译或测试，且模型推理档位不一致。作者重析其公开数据，在允许运行代码且无错误指令的试验中，3,067 个补丁有 2,634 个（86%）阻止了给定 exploit，但阻止 exploit 不等于完整修复。文章还给出咨询中 2,265 个漏洞首次修复失败率 12.5%，Patch the Planet 的 186 个 PR 合并率 67.7%，并追踪后续提交发现功能、构建和性能回归，但无可利用安全漏洞。最后提出基准应衡量代表性样本、工作条件、可验证正确性、结果变化和人机协作贡献，并发布 post-patch-validation 与 review-walkthrough 技能。局限是人机直接对比仍需相同任务条件，部分首次失败记录可能被低估。
推荐收录，因为文章用可复核证据指出 1Password 基准在样本选择、提示词、工具权限和评分一致性上的具体缺陷，并以 3,067 个补丁重析、2,265 个真实漏洞首次修复及 186 个开源 PR 审阅记录做对照。适合安全工程、AI 评测与研究读者，可迁移到补丁验证、基准设计和 Agent 回归审查；需注意其涉及厂商争议，应结合原始数据独立判断。
Trail of Bits 披露了 Lean 4.33.1 及之前版本中的一项严重 bug，可通过制造矛盾来让 Lean 认可 Fermat 大定理的“证明”。根因是 `String.Pos.Raw.extract` 在极大位置上的逻辑定义与原生求值不一致：前者返回空串，后者返回整个原始字符串。这种不一致可推出空串等于非空串，一旦得到矛盾，任意命题都可被证明。文章认为这不是内核 soundness 问题，而是 `native_decide` 引入了编译器这一额外信任边界，并建议验证外部证明时使用 `#print axioms`。Lean 团队快速修复了内存问题并最终解决语义不匹配，展示了对证明工具可信性的持续加固。
推荐收录。本文以真实漏洞为例，清晰揭示了形式化证明工具中逻辑求值与原生求值不一致造成的信任边界问题，填补了普通资料对 `native_decide` 风险的讨论不足。适合使用 Lean 做证明、依赖机器检查结果的研究者与安全工程师；文中发现问题的思路及验证证明的正确方法具有很强的可迁移性与警示价值。
本文来自 Trail of Bits，实测 GPT 5.6-Cyber 代理的 VM 逃逸能力。作者在 Debian 12 + QEMU/KVM 的宿主上让代理从 SSH 进入 VM 并读取 flag，代理在约 12 小时内成功逃逸三次：利用已披露但未同步的内核漏洞、libslirp 版本漏洞以及多个 0-day。最终链路涉及 QEMU、Linux KVM 和 libslirp 的组合漏洞，代理可自主研究、编写 exploit 并回溯失败路径。测试 Firecracker 时代理未能逃逸，但也能硬锁内核。文章结论：普通 VM 无法隔离高级 AI 代理，需要快速补丁、最小攻击面、最小权限、日志监控和时限控制。
推荐收录。文章提供了真实、可复现的安全测试证据，说明 AI 代理已能自主发现并组合多个已知和未知漏洞实施 VM 逃逸，直接挑战当前沙箱假设。适合安全工程师、平台团队和 AI 安全研究者阅读；其结论和缓解建议（如采用 Firecracker、加强补丁和监控）对隔离设计有直接参考价值。
该文披露并复盘了 Provenance Blockchain 在 Cosmos SDK 上的一个严重权限绕过漏洞。marker 模块是链上同质化通证的核心原语，其 AddAccess 授权检查包含三个条件，第三个条件会把存储字段中的 supply 与实际余额比较；对于非 fixed 型 marker，存储的 supply 永远是 0，导致任何持有 0 个代币的调用者都可以满足 0==0，从而自行授予 ACCESS_ADMIN、ACCESS_MINT、ACCESS_WITHDRAW 权限。攻击只需两笔链上交易：先提权，再铸币或提取 escrow 资产。发现时主网有 82 个受影响 marker，涉及桥接稳定币、抵押参与份额等资产，escrow 中被锁定的 nhash 约合 50 万美元；临时修复会显式拒绝零供应，正式修复改为读取 bank 模块的实时 supply。根因是同一代币供应在 marker 结构和 bank 模块中重复存储且未同步，作者强调授权谓词必须保证攻击者默认状态下无法满足，并建议用授权规格说明与基于性质的测试尽早发现此类问题。
推荐收录。文章不是泛泛漏洞播报，而是完整展示了从授权逻辑、根因到攻击路径、影响量化和修复对比的安全分析过程，尤其指出“默认状态即可满足授权谓词”这一可迁移模式。适合区块链开发者、安全审计人员和系统设计者阅读，对其他存在冗余状态或访问控制逻辑的系统也有直接借鉴价值。
Trail of Bits 作为 Signal 自动密钥验证功能的三方审计者之一，从零构建并运行了独立的审计器，用于验证用户公钥映射的全局一致性和完整性。文章介绍了自动密钥验证的工作原理：通过全局一致的公钥视图和定期自检防止服务器提供虚假公钥；审计器利用 Merkle 树维护本地副本并签名，确保任意客户端看到相同的公钥集合。文中还说明了审计器独立实现的原因、签名策略、失败场景以及自动验证的适用范围和限制。
推荐收录，因为它详细展示了如何通过独立审计器增强密钥透明度系统的安全性，提供了可验证的工程实践。适合关注端到端加密、密钥管理和分布式系统信任模型的工程师阅读，审计器设计与实现思路可迁移到其他需要第三方验证的安全基础设施中。
文章系统分析了AWS Nitro Enclaves与KMS集成时的安全威胁与防护策略。作者从被动攻击和主动攻击两个维度出发，详细梳理了数据交换攻击、CMK替换、重放攻击等具体场景，并给出了包含加密上下文、密钥承诺、CMK硬编码、TLS通道等在内的防护检查清单。此外，文章还讨论了KMS策略配置的常见错误、PCR绑定方法、端到端验证的挑战以及操作层面的风险（如密钥轮换、区域性故障、计费问题）。文末指出AWS官方SDK存在漏洞，并建议替代方案。整体内容根植于真实工程约束，但部分防护依赖于AWS内部实现细节，不完全适用于非AWS环境。
推荐收录，因为文章不是浅层介绍，而是对Nitro Enclaves与KMS结合时的攻击面进行了系统性威胁分类，并提供了可落地的安全检查清单。内容来自专业安全公司，具有较高的工程参考价值，适合从事云安全、机密计算或基础设施安全的工程师阅读。其威胁建模方法和防护清单设计思路可迁移到其他TEE或云服务安全评估中。
文章聚焦Uniswap v4 hooks的安全开发，强调其灵活性将部分安全责任转移至应用代码。作者基于Trail of Bits的审计实践及Cork、Bunni等真实攻击案例（损失超2000万美元），提炼出七种重复出现的失败模式：包括未校验调用者、信任任意池、自定义会计泄漏价值、钩子逻辑错放、地址位权限不匹配、非必要代码阻塞核心操作以及回调间状态变更。文章先阐述PoolManager的协议保证与结算机制，明确安全边界，然后逐条分析每种模式的成因、风险与修复方案，并提供面向开发者的八项安全检查清单和面向审计者的七个审查问题。内容面向构建安全DeFi应用的开发者与审计者，具有长期参考价值，但需注意其建议主要针对Uniswap v4生态，部分安全模式可能随协议升级而演进。
本文基于真实安全事件与审计经验，系统梳理了Uniswap v4钩子开发中的七类典型安全缺陷，并给出可操作的预防清单，直接证据清晰。适合所有在v4生态上构建或审计智能合约的工程师和安全研究员，其防御模式可迁移至其他DeFi协议或智能合约设计。帮助读者从已知陷阱中学习，避免重复高额损失。
文章总结了Trail of Bits在“Patch the Planet”项目中使用Codex的/goal功能进行开源软件安全审计的工程实践经验。核心方法包括三项关键技巧：让Codex基于威胁模型自行撰写目标提示，以生成更精确、可测试的成功标准；专注于定义明确的产出而非实现路径，使用详尽的结果条件并提前排除“容易的出口”；为每个代理分配单一目标，避免在一个提示中混合竞争性指标，并通过分治策略在zlib审计中显著提升效能。文中还详细展示了用于Rust编译器的全自动变体分析流水线，该流水线通过多代理分派、双重误报筛查和人工终审，将每个P-critical问题转化为独立追猎任务，并最终发现了所有已提交的Rust漏洞。整体上，这些经验展示了如何将安全专家的领域知识与AI的自主搜索能力结合，但强调最终有效性仍依赖于专家级的威胁建模、提示工程和结果验证，且该方法不适用于缺少明确威胁模型的任意代码库。
本文提供了经过真实关键基础设施项目（Rust、curl等）验证的AI辅助安全审计工程方法论，对prompt设计中的“定义结果而非路径”、“单一代理分工”以及自动化变体分析管线有具体可复制的描述。适合安全工程师、AI工程化团队和关注自动化测试的开发者参考，其中的分治策略和结果校准方法可直接迁移至其他AI驱动的审计场景。但需注意，这套方法强依赖专家的威胁建模能力和人工复核，简单套用可能产生大量误报或遗漏。
文章宣布Trail of Bits在Testing Handbook中新增Rust安全测试章节，系统介绍了用于验证Rust程序安全性的工具和技术。内容首先概述Rust安全保证的边界与未尽问题，然后深入动态分析领域，包括使用Miri检测未定义行为、proptest属性测试、覆盖率测量和变异测试等。接着阐述静态分析工具Clippy的深度用法及推荐lint。此外，还总结了从审计实践中积累的陷阱清单，如操作符优先级差异，并提供了内存清零的三种方案。最后，介绍了专用工具如模型检查器Kani和供应链依赖审查方法。文章旨在为开发者提供一个全面的Rust安全测试流程，但内容为概述，具体细节需参考完整手册章节。
此文系统梳理了Rust安全测试的工具链和最佳实践，从动态分析到静态分析再到供应链安全，覆盖全面，且融入了审计实战经验。适合Rust开发者、安全工程师和注重代码质量的团队参考，可帮助识别常见安全陷阱并集成多种测试方法。虽然文章为概述，但提供了清晰的指引和资源链接，可迁移性强。
文章介绍 Trail of Bits 为 DAML 增加的 Mewt 变异测试支持，核心目标是用“存活变异体”衡量测试集真正能否发现错误，而不是只看覆盖率。作者指出，DAML 内置的模板/choice 覆盖只能证明代码被执行过，不能验证授权语义，尤其容易漏掉 controller、signatory 这类权限规则。Mewt 通过复用 tree-sitter-haskell 解析器并加入两类 DAML 特有变异——控制者替换和控制者删除——来制造授权偏差并观察测试是否失败。文中用双签释放资金的例子说明：只测成功路径会让“少一个签名也能通过”的变异体悄悄存活，从而暴露缺失的拒绝测试。文章也明确了局限，包括等价变异、整套测试带来的时间成本，以及需要人工复核 surviving mutants。
推荐收录，因为它把变异测试具体落到了 DAML 授权规则和真实测试流程上，给出了可复用的变异类型、使用方式和边界条件。适合智能合约、安全测试和测试设计读者参考；同时也提醒了等价变异与长耗时带来的实操风险。
这篇文章是 Trail of Bits 对一次真实安全研究行动的阶段性复盘：他们把 GPT-5.5-Cyber 接入 Codex 的 /goal 模式，要求其针对 zlib 寻找压缩库中高危缺陷。模型没有停留在静态读代码上，而是自动搭建了 ASan/UBSan 构建、测试种子、多个 C/C++ harness 和变体编译配置，覆盖 inflate、uncompress2、gz* 等十余个入口，并据此找到多个正在协调披露的问题。作者强调，真正的价值不只是“能跑起来”，而是模型能持续判断哪些崩溃不具备现实可达性、主动放弃噪声并扩展新的探索方向。文章结论是：面向安全关键代码，定制化 fuzzing 已不再是少数专家的专利，前沿模型正在显著压缩构建攻击/防御工具的门槛，但前提仍是严格的有效性规则和人工把关。它的边界也很明确：这类能力目前更适合作为高信号的辅助研究工具，而不是自动化裁决漏洞是否成立的最终依据。
推荐收录，因为文章给出了可核验的直接证据：GPT-5.5-Cyber 在一天内自动搭建 fuzzing lab、生成多入口 harness、使用 sanitizer 变体并产出可披露发现。对安全研究、漏洞挖掘和 AI 辅助测试读者，这篇文章能迁移的不是某个 zlib 细节，而是“目标约束 + 有效性判定 + 持续探索”的方法。
文章介绍 pyca/cryptography 在 48 版中加入 ML-KEM 与 ML-DSA，使 Python 生态可通过 pip 安装获得后量子密码支持。作者从美国政府推进迁移的时间表切入，强调后量子转型不能只停留在政策层，必须先由底层密码库暴露新原语，应用才能升级。文中对比 Ed25519/X25519 与 ML-DSA/ML-KEM 的密钥、签名和密文尺寸，指出后量子算法会显著放大协议字段、长度前缀和分片假设，因此并非“无痛替换”。同时还讨论了 SLH-DSA 的保守性，以及把这些原语接入真实协议时需要谨慎测试、审核和与维护者协作的边界。
推荐收录，因为它给出了后量子密码进入 Python 生态的直接工程证据：版本发布、API 形态、后端支持与协议迁移约束都很明确。适合密码库维护者、协议设计者和安全工程师参考，尤其能迁移到“先暴露原语、再改协议字段与测试”的升级路径。