16
Anthropic 联合 Theorem 发布研究,展示利用 Claude 在汇编语言层面(RISC-V)为 123 个真实开源软件库生成形式化证明。据 Anthropic 称,Claude 能在单线程静态二进制、固定内存预算及小于 64 MB 输入等前提假设下,通过 Rocq 证明检查器验证程序不会发生内存安全错误或断言崩溃,并在推导证明过程中自主发现并修补了传统模糊测试难以触发的复杂深层漏洞。目前该验证仍存在限制,其建立在特定的 RISC-V 与 Linux 抽象模型之上,尚未完全覆盖 x86/ARM 架构、多线程以及动态链接等实际生产环境。
为什么重要传统形式化验证因需投入大量专家人力而仅局限于航空、微内核等极少数高安全场景;该研究表明大语言模型有望将形式化数学证明推向常规开源组件,显著降低高可靠性软件的安全验证门槛。
必要背景形式化验证通过将代码转化为数学模型并证明其符合安全规范来保证无特定错误,但编写证明工作量极大。例如文中指出,seL4 微内核实现仅需 2 个人年,而形式化验证却耗费了 20 个人年。
证据状态仅有当前来源,尚未独立核实。上述技术成果、测试数据及漏洞发现案例均来自 Anthropic 与合作方 Theorem 的官方研究主张;模型代码与证明子集已由厂商公开,但其在工业化全流程中的可复现性与准确度仍待社区与学术界独立验证。
AI 编程 · Anthropic · 形式化验证 · 软件工程
17
数字信任服务商 eMudhra 宣布,其董事会已决定主动退出全球 SSL/TLS 证书业务。官方表示,此前涉及全球 SSL/TLS 证书的安全事件已在发现后 14 小时内吊销受影响 CA,未签发终端证书且基础设施未受破坏,但该业务仅占公司全球营收约 1%,在面临高昂合规成本、免费证书竞争以及过度审查压力下,投资回报已大幅降低。在过渡期内,其 G1 RSA 根证书将继续运行,官方将通过合作伙伴为客户免费替换证书,而企业 PKI 及数字签名等核心业务不受影响。
为什么重要对于使用 eMudhra SSL/TLS 证书的站点和企业,需在过渡期内配合完成免费证书轮换与替代部署;该事件也反映出在免费 CA 普及和浏览器根证书计划日益严格的监管下,小型商业公共 CA 面临着巨大的合规与运营压力。
证据状态eMudhra 宣布自愿退出全球 SSL/TLS 证书业务的消息已由《经济时报》(The Economic Times)等媒体报道证实。此前引发争议的 8 个中级 CA 私钥泄露事件,已获得 Google Chrome 安全团队和 Mozilla Bugzilla 记录的独立确认。关于“受影响 CA 未签发任何最终实体证书、基础设施未受损”以及“该业务仅占总收入约 1%”的说法,据 eMudhra 官方声明称,目前尚无独立第三方审计报告完全证实。
网络技术 · 网络安全 · SSL/TLS · Web PKI · 证书颁发机构
18
NVIDIA 开源了面向自主 AI 智能体集群的私有安全运行时 OpenShell,并推出 0.1.x 版本。该项目通过内核级沙箱机制限制智能体的文件访问、系统调用与出站网络,并对真实凭据实施拦截注入,避免智能体直接接触敏感密钥;同时引入形式化验证机制,在策略变更涉及高危权限(如新增带凭据的主机访问或 API 调用)时拦截并交由人工审查。OpenShell 支持 Linux、Apple Silicon 架构的 macOS 以及基于 WSL 2 的 Windows 环境,并提供了 Python、TypeScript、Go 和 Rust 语言的 SDK 支持。
为什么重要针对自主 AI 智能体执行代码、访问网络和调用外部服务时的安全风险,OpenShell 提供了系统级沙箱隔离与凭据托管方案,有助于降低企业批量部署自动化智能体时的越权与泄密隐患。
证据状态OpenShell 属于 NVIDIA 官方开源项目,其代码仓库与发布信息已由 GitHub 及官方新闻稿确认 。关于该项目具备的内核级策略拦截、形式化验证及凭据隔离等技术特性与安全效果,目前均据 NVIDIA 官方文档及代码库主张,尚未见独立第三方安全审计或评测机构核实。
AI Agent · NVIDIA · 沙箱环境 · 安全运行时 · 开发工具
19
非营利性公共 DNS 服务商 Quad9 宣布,因法国法院在一项涉及转播版权侵权的诉讼中作出不利判决,要求其针对法国境内用户阻断特定域名的递归 DNS 解析,Quad9 决定自 11 月 24 日起停止向法国用户提供解析服务。法院虽将每日罚金从 58 万欧元降至 1,000 欧元,但 Quad9 表示作为不记录用户身份和地理信息的公益服务,无法在技术上仅对法国用户实施定向阻断,且拒绝通过全球阻断扩大管辖范围或违背 DNS 中立性原则。Quad9 称法国境内还有约 20 起类似阻断诉讼正在进行,机构无法承受持续的法律诉讼与罚款风险,目前正针对该裁决提起上诉。
为什么重要该事件凸显了版权方利用司法判决将内容过滤责任转嫁给递归 DNS 等网络基础设施中间人时引发的治理冲突。法国本地的公共机构、关键基础设施和普通用户将在 11 月 24 日后失去 Quad9 提供的威胁防护解析,同时可能促使更多公共解析服务商审视在欧盟成员国面临的合规与运营风险。
必要背景本案由体育转播商 beIN 提起,指控相关网站侵犯其赛事转播版权并要求解析服务商实施封锁。Quad9 是一家总部位于瑞士的公益基金会,主要提供带有恶意软件和网络钓鱼防护的免费递归 DNS 解析服务,主张递归解析属于中立被动的基础设施,不应承担内容审查功能。
证据状态退出法国及自 11 月 24 日停止服务的信息来自 Quad9 官方发布的公告,其关于无法在保护隐私前提下定向屏蔽及面临约 20 起类似诉讼的表述属于机构自述。外部媒体报道确认了 beIN 诉 Quad9 等 DNS 解析服务商要求屏蔽侵权域名的案件背景与相关司法裁决争议。
Quad9 · DNS · 网络技术 · 网络监管 · 网络安全
20
开源隐私支付项目 NGI TALER 宣布在德国波鸿设立新实体 Taler Operations AG,作为卢森堡 Taler Systems SA 的子公司推进欧元区合规落地。该实体计划向德国联邦金融监管局(BaFin)申请电子货币机构(EMI)牌照,以直接运营面向欧元的 GNU Taler 支付系统。此前原定承担发行方角色的 GLS Bank 已于 2026 年 1 月放弃该职能并转为支持角色,目前该运营实体正在筹集监管合规所需的资本,正式上线时间取决于 BaFin 的审批进度。
为什么重要这标志着倡导买方隐私与商户透明纳税的自由软件支付协议迈向合规金融基础设施运营的关键一步,若牌照获批,将使欧洲用户能够直接以欧元进行合规的数字现金支付。
必要背景GNU Taler 并非独立货币,其通过发行具有等值面额的无记名代币来实现支付,因此在欧盟法规下属于电子货币范畴,必须由持牌银行或取得许可的电子货币机构运营。GNU Taler 协议套件及其参考实现本身仍保持自由开源软件属性不变。
证据状态关于成立 Taler Operations AG 以及向德国联邦金融监管局(BaFin)申请电子货币机构牌照的计划,据 GNU Taler 官方公告称。目前网络检索除项目官方渠道及社区聚合转载外,仅有当前来源,尚未独立核实;相关牌照能否获批及实际商用落地时间,仍需等待监管机构后续审查结果。
GNU Taler · 隐私支付 · 开源软件 · 网络金融