科技日报 008｜AI开始给代码写证明，PHP漏洞披露前已遭试探
第 008 期 · 2026-10-23 · SI斗罗
本期范围：北京时间10月22日00:00—10月23日10:00。海外公告保留官网日期；旧项目单独标注为项目观察。
AI写代码越来越快，那谁来证明它写得对？今天的第一条消息，就在尝试回答其中一部分问题。
安全更新也不能漏。昨天说到的PHP漏洞，已有披露前利用尝试的新证据；用Node镜像部署服务的朋友，也有补丁要跟进。
01｜Claude写了1.8亿行证明，验证123个开源库
10月22日 · Anthropic与Theorem公布研究
这次不是让AI看一遍代码，然后说“我觉得没问题”。研究团队让Claude生成数学证明，再交给独立检查器核验。
研究覆盖123个开源库的239个测试入口，生成约1.8亿行Rocq证明。模型负责写，检查器负责验。
证明针对的是特定输入范围内的不崩溃性质。输入须小于64MB，还限定了固定的内存预算。
这批实验使用单线程、静态链接musl的RISC-V/Linux环境，证明不能直接搬到任意x86或ARM服务器上。
它也不代表整个库没有bug，更不保证所有业务逻辑正确。公开仓库目前是25个库、60个入口的子集。
我觉得值得关注的是：AI交付代码时，开始尝试同时交付能被检查的证据。证据覆盖到哪里，仍然要看清楚。
来源：Anthropic研究原文 · 公开证明仓库。
02｜PHP后续：披露前四天，就已有利用尝试
10月22日清晨发布、23日清晨更新 · Amazon威胁情报报告
Amazon回溯MadPot蜜罐数据，发现10月17日已有PHP2Shell利用尝试，比10月21日公开披露早四天。
官方当前正文还表示，已出现广泛的在野利用尝试。这比“补丁已经发了”更值得维护者警惕。
但报告也说，尚不清楚披露前那些尝试能否在真实系统上成功。不能据此写成“大批网站早已被攻破”。
PHP官方仍列出四个修复版本：8.5.12、8.4.27、8.3.36、8.2.35；使用发行版维护包的，要核对其安全公告和回补记录。
更新之后，排查也别只从公开披露当天算起。Amazon建议，PHP2Shell相关调查至少回溯到10月17日。
另外，OpenAI的php2shell-checker今天更新了风险措辞。它依据版本等线索提示“可能受影响”，不能代替实际补丁核验。
来源：AWS安全博客 · PHP安全公告 · php2shell-checker。
03｜Node修复Brotli漏洞，图床用户也要换镜像
10月22日 · 三月图床跟进上游安全更新
CloudFlare-ImgBed（三月图床）发布Docker安全公告，重建官方镜像，跟进Node的Brotli解压漏洞修复。
漏洞编号为CVE-2026-111497，Node官方评级为High；处理不可信压缩数据时，可能导致远程代码执行。
项目作者提醒，Docker版图床在拉取外部资源时，可能遇到这类压缩响应。
Node对应分支修复版本为22.23.4、24.22.1、26.12.1。图床公告确认，新镜像中的Node已升到22.23.4。
用Docker部署的，关键是更新镜像并重建容器。只重启旧容器，或者只升级宿主机上的Node，里面的运行时不会自动变新。
上述图床操作针对Docker版，Pages/Workers托管部署不需执行这套步骤。Node上游补丁已在10月21日发布。
04｜eMudhra退出全球SSL/TLS证书业务，客户需跟进迁移
10月22日 · 公司董事会决定
eMudhra宣布退出全球SSL/TLS证书业务。公司称，这项业务约占总收入的1%，面临成本、合规和近期事件带来的压力。
此前，Mozilla披露8张eMudhra中间证书的私钥受损，存在伪造HTTPS证书的风险。
Firefox和Chrome已在10月17日（UTC）分别屏蔽相关证书或公钥；两者采取的具体屏蔽范围不同。
eMudhra表示，会通过合作方协助受影响客户免费更换证书；撤销与证书状态服务，将维持到既有证书到期或完成替换。
退出业务，不代表所有已签发证书今天同时失效。依赖相关证书的站点，要跟进供应商的迁移通知与信任库更新。
这也提醒做网站的朋友：HTTPS能正常工作，依赖的不只是自己服务器上的那张证书，还包括整条信任链的维护。
来源：eMudhra官方公告 · Mozilla与Chrome根证书项目说明。
05｜微软医疗AI研究登Science，仍需真实临床验证
10月22日 · 微软公布同行评议与扩展评测进展
MAI-DxO模拟多位医生协作，逐轮提问、选择检查，并考虑检查成本。这次研究发表于《Science》。
微软报告，在复杂NEJM病例评测中，系统诊断准确率为83%；医生不查资料、可查资料的结果分别为22%和36%。
在MIMIC-IV-ED急诊病例评测中，系统为80%，医生对照为47%。这些数字来自特定病例与评测设置。
病例基准成绩，不能直接等同真实门诊效果。系统获取信息的方式、医生对照条件，都会影响比较结果。
微软还宣布将与医院开展前瞻研究。接下来要看的，是它在实际诊疗流程里能帮上多少忙。
来源：微软研究介绍 · SDBench项目说明。
06｜Grok扩展企业合作网络，重点是部署与工具集成
10月22日 · x.ai官网发布合作计划
官方推出“SpaceX Super Intelligence Partner Network”，面向使用Grok构建产品、解决方案和服务的企业。
合作伙伴分两类：一类帮助企业部署Grok；另一类开发插件与产品集成，让它接上客户已有的工具。
公告称，早期接入阶段有130多家公司参与，30多家机构的工程师接受了相关认证项目培训。
这些是合作计划的参与规模，不能换算成付费客户数。
我的关注点是，企业AI开始把培训、接入和交付放在一起。模型能力之外，能否接进现有业务同样影响落地。
来源：x.ai合作网络公告。
07｜reylo：直接导入SQL，让TypeScript拿到查询类型
10月23日06:42 · 0.3.0版本发布
reylo让TypeScript直接导入.sql文件，借助开发数据库分析参数和结果类型，减少SQL改了、类型定义忘改的问题。
今晨的0.3.0新增Cloudflare Durable Objects支持，并修正多处空值推断。升级后，有些调用可能需要补null检查。
它采用MIT许可，但工具链要求比较新：Node 24及以上、TypeScript 7.1 Beta，还要配置对应数据库引擎与运行时加载方式。
适合愿意写原生SQL的TS项目。类型检查可以提前发现一些错误，业务逻辑和查询性能仍要自己验证。本期未安装实测。
08｜项目观察：OpenShell给Agent划定访问范围
10月23日观察 · 既有开源项目，不是今日首发
NVIDIA的OpenShell让Agent在隔离环境中运行，用策略限制文件、系统调用和网络访问。
它还管理凭据，只向获准的端点注入相应凭据，适合需要明确Agent权限范围的开发者和平台团队。
项目采用Apache-2.0许可，需要容器或虚拟化环境；Windows支持仍为实验性，Agent和模型也需要自己配置。
它可验证部分策略权限，但检查通过，不等于具体任务绝对安全，也不证明运行时一定正确执行了策略。
给Agent更多能力之前，先把允许它访问什么写清楚。这是这个项目值得研究的地方。本期未安装实测。
来源：OpenShell官方仓库 · 策略验证边界。
