English version · 区块链学习导航 · 上一篇
区块链学习 · 文章 BC068
审计报告或证明结果，只有能关联到所检查系统的一项精确主张时，才真正有用。这种关联需要的不只是徽章，还包括被审查代码产物、覆盖性质、采用假设、未关闭发现，以及当前部署符合该范围的证据。
升级之后，关于旧实现的报告仍然只是关于旧实现。被证明的性质也仍然依赖其形式化陈述和假设。两者都不会自动成为同一网站或合约地址所能触达全部功能的永久保证。
本课评价一份虚构保障材料包及四张部署卡，不为真实审计机构排名，也不认证产品。目标是判断证据支持哪种有限陈述、不支持哪种陈述，以及需要什么额外证据才能填补缺口。
选择适合你的阅读路线
本篇目录
- 1. 先问文件包含哪种证据
- 2. 精确阅读虚构材料包
- 3. 区分被证明性质与更大的承诺
- 4. 部署A卡：所需关联已经给出
- 5. 部署B卡：地址相同，逻辑已变
- 6. 部署C卡：代码身份相同仍不够
- 7. 部署D卡：有徽章，缺少关联
- 8. 把假设当作需要核对的条件
- 9. 如实保留发现状态与证明结果
- 10. 变化带来新问题，不自动带来结论
- 11. 写出经得起仔细阅读的主张
- 12. 练习与答案
- 13. 来源与延伸阅读
- 第1至3节识别文件类型及其主张。
- 第4至7节将材料包与四种部署情况比较。
- 第8至11节讨论假设、发现、变化及可用的主张模板。
- 第12至13节提供练习答案与来源。
1. 先问文件包含哪种证据
代码审查、执行测试和形式化证明承担不同任务。审查可以在范围内识别缺陷并质疑设计；测试观察选定执行；证明则在模型假设下确立指定性质，前提是证明及支持工具可靠。
把三者都称为“已验证”，会隐藏这些区别。评价主张前，应识别方法、对象与结果：审查者检查了哪些文件？回归测试是否实际运行？某项证明义务是否成功完成？另一项是否仍未解决？
Ethereum智能合约安全指导将审计描述为额外独立审查，并明确提醒审计不能发现每个缺陷。本课核对时，页面最后更新于2026年2月26日。这支持认真使用报告，同时避免把它变成万能保障标签。参见智能合约安全指导。
一般数学基础可阅读Proving Software Correct Before It Runs。本课聚焦部署读者的问题：这份具体证据，是否仍适用于当前使用的代码、配置和权限路径？
2. 精确阅读虚构材料包
教学系统是一项目录预约应用。材料包指定源代码修订版R7，以及在特定编译器、设置和依赖集下产生的构建产物B7，并包含实现标识I7。它们只是符号标签，不是真实提交编号或密码学哈希。
代码审查报告覆盖R7的预约逻辑。发现F1记录为已修正，并在R7中经过独立复测。发现F2仍被延期处理，附有解释和负责决定的主体。材料包没有声称所有发现均已关闭。
另一份形式化结果确立性质P：给定模型的所有状态转换中，预约计数始终在零至十之间。模型假设初始状态有效、写入者规则符合描述、确认依赖满足指定条件，并且维护绕行路径未启用。证明不覆盖未来实现变化、任意管理员动作、网站界面或实体目录信息的真实性。
第二项性质Q在工具达到资源限制后仍未解决。材料包将Q标为未知，既没有说Q为假，也没有说Q已经证明。
本练习假设这些文件及所报告结果真实。我们测试的是相关性与范围，不要求你认证真实审计服务提供方。
3. 区分被证明性质与更大的承诺
性质P有实际意义。在其假设和模型转换内，计数边界成立。这比只在几个成功案例中观察计数更强。但它不是“每项预约都会完成”“目录描述现实”或“管理员永远不能改变行为”的证明。
即使容量边界保持，请求仍可能延迟，门户仍可能显示错误信息，外部流程也可能提供误导数据。这些属于不同性质。材料包可能为它们提供其他证据，但不能悄悄扩展P来覆盖它们。
Solidity 0.8.30的SMTChecker文档说明，形式化验证检查形式化规范，而规范本身仍须正确表达预期要求；文档也区分已证明与未证明结果。因此，正确解读需要分析配置和实际性质结果，不能把看似没有内容的输出画面当作证明。参见Solidity SMTChecker文档。
使用证明前，先用普通语言写出结论。如果结论包含P中没有的词，例如可用性、诚实管理或实体准确性，就应问这些词由什么额外证据支持。
4. 部署A卡：所需关联已经给出
A卡识别链C及一个已接受区块H100。在该状态，代理Pxy指向实现I7。材料包提供可靠关联，将I7的部署可执行产物连接到B7，再将B7连接到已审查R7源代码及其声明构建输入。
材料还证明相关配置和可达状态假设符合形式化模型：写入者安排正确，确认依赖满足所述假设，初始状态条件持续保持，维护绕行路径处于禁用状态。
能支持的陈述范围有限：在已识别部署情境及这些假设下，材料包支持被覆盖I7行为的性质P。它同时记录R7的审查状态，包括延期处理的发现。材料没有认证整个服务，也没有消除排除项。
假设升级权限存在，但在H100中尚未改变实现。权限存在，不会自动让旧证明变成错误，却使我们不能把当前关联当作未来所有实现的保证。持续依赖需要证据说明相关条件仍在范围内。
这并不矛盾。一个主张可以在明确范围内很强，同时对运行系统是否持续留在该范围内保持条件性。
5. 部署B卡：地址相同，逻辑已变
B卡独立于A卡结论。在指定区块H120，同一个代理Pxy现在指向由R8源代码构建的I8。材料包没有提供能把R8关联到R7主张的审查或证明。
正确分类是：旧材料包不能确立所请求的当前实现主张。这不是认定I8必然有缺陷，而是说明I7证据尚未连接到I8。
OpenZeppelin代理模式文档解释，代理可以保持为同一个访问入口，而它引用的逻辑实现发生改变。因此，地址未变本身不能证明执行逻辑未变。参见代理升级模式。
团队之后可能提供针对变化的审查、新证明结果，或有依据的等价性证据。需要多少工作，取决于改了什么，以及哪些性质依赖这些变化。本卡没有给出这些材料，读者就应保留缺口，而不是自行补造关联。
有用的问题应具体：“H120中的I8由哪个已审查代码产物及性质证据覆盖？”只问“这个地址审计过吗”，可能得到一个历史上真实的回答，却仍无法解决当前问题。
6. 部署C卡：代码身份相同仍不够
C卡保留实现I7，但改变外围配置。包装合约或模块系统中原先禁用的维护路径被启用，管理员G可以通过它，在P所建模的预约转换之外修改被追踪状态。
原材料明确假设这条绕行路径禁用。I7代码身份比较可能仍通过，但系统已不满足该模型条件。因此，材料包不能确立扩大后的主张，即当前系统所有可达转换都保持P。
题目没有提供G实际使用该路径，或计数已经超过十的证据。技术能力、组织允许的行为和已观察动作是不同事实。权限路径改变本身就足以要求重新评估范围，而不必指控不当行为。
OpenZeppelin访问控制文档区分操作角色与授予、撤销角色的权限。阅读配置时，这一点很有帮助：普通调用限制经过审查，并不自动代表每种管理员可控制的变化都已被评价。参见访问控制文档。
若要恢复有依据的主张，证据需要覆盖已启用路径，或证明相关条件重新满足，或将主张缩小到仍处于旧模型范围内的行为。重复展示旧徽章不能完成这些工作。
7. 部署D卡：有徽章，缺少关联
D卡提供网站徽章及一份报告标题，却没有识别被审查修订版、构建产物、部署实现或配置，也未提供报告实际性质与排除范围。
分类为：证据不足，无法把保障主张连接到当前部署。报告可能存在，也可能有价值，但这张卡没有确立它与眼前系统的相关性。
这不等于证明徽章虚假。缺少证据与存在欺骗证据仍需区分。谨慎做法是索取实际报告和代码产物关联，而不是无依据地认可系统或指控运营者。
即使报告签名真实，也只是根据相应验证假设认证文件，不能自动证明当前系统运行被审查代码。文件真实性与部署对应性是不同问题。
8. 把假设当作需要核对的条件
虚构证明假设了特定确认依赖。如果I7未变，但依赖行为变化，证明对系统的适用性也可能需要重新评估。问题是论证所需假设是否仍成立，而不只是应用自己的文件有没有改。
假设可能涉及初始化、外部调用、允许参与方、算术语义或构建工具。有些由分析确立，有些由配置证据支持，有些仍是受信任条件。有用的材料应明确列出，而不是藏在“已验证”三个字里。
例如，经过认证的确认消息，可能证明哪个组件发送了消息，却不证明真实目录物品一定正确。如果实体准确性在范围之外，将依赖称为“可信”也不会增加一个关于现实真实性的定理。
主张、证据与假设之间的一般关系，可见How Assurance Cases Work。这里的实际阅读任务，是把每项假设对应到具体部署事实，或明确保留的不确定性。
假设记录只有能够被质疑才有用。若只写“所有依赖行为正确”，却不识别依赖及相关行为，就过于模糊，无法解释什么情况会让主张失去依据。
9. 如实保留发现状态与证明结果
F1已在R7中修正并复测，这支持对应关闭记录，但不表示F2也已修正。F2是延期处理，因此“全部发现均已解决”与材料冲突。
负责决定的人可能针对某种情境接受残余问题。这属于治理决定，不等于问题已消除。读者应保留发现状态、理由和范围，而不是把每个不阻止发布的项目都翻译为“已修复”。
Q仍未知，因为分析在资源限制内没有确立结果。未知不等于已证明，也不一定提供了具体反例。这些结果含义不同，应在摘要中保持区别。
简短报告仍可以准确：“P在给定模型下已证明；Q仍未解决；F1已修正并复测；F2延期处理。”这比单个绿色评分更有用，因为它说明哪里有证据支持信心，哪里仍有未回答问题。
严重性标签与发现数量同样需要解释。一个数量不能告诉我们发现是否对应当前版本、被排除组件是否带来重要风险，或审查是否检查了读者真正关心的性质。
10. 变化带来新问题，不自动带来结论
升级不一定摧毁全部旧证据。某个变化可能与特定性质无关，也可能有新论证说明性质保持，但这种关联必须明确建立。
对B卡，变化记录应识别R7到R8的差异、受影响假设和性质，以及用于扩展或替代旧结论的证据。对C卡，则应识别新启用权限路径，并说明性质模型是否包含它的可能动作。
这种区分避免两种相反错误：把每次变化都视为自动不安全，或把旧报告视为自动可迁移。合理立场取决于具体变化及其与主张的关系。
时间也重要。H100状态观察可以确立H100中的关联，不能单独证明H120选择了哪个实现。现在时陈述需要足够当前、关联相关链状态的证据，并理解观察的信任基础。
本课不假设某个公共区块浏览器、标志或界面能够无误提供关联。课堂材料在需要时明确给出可靠证据，实际评价则必须建立自己的来源与核验链。
11. 写出经得起仔细阅读的主张
有用的主张模板应包含代码产物、性质、情境、假设和排除项。对A卡，可以这样写：
“给定材料包确立了R7/B7行为在模型中的计数边界P；这些行为已关联到链C指定H100状态中的I7，并依赖所述写入者、依赖及配置假设。Q仍未解决，F2仍延期处理，未来升级及已启用维护路径不在此主张范围内。”
这句话比“已审计”长，但每项限定都承担作用。删除产物就失去身份，删除P就扩大性质，删除H100就隐藏时间，删除假设就隐藏依赖，删除排除项则容易让读者推断材料从未覆盖的内容。
对B卡，摘要应说明R7材料尚未确立当前I8覆盖；对C卡，应指出“绕行路径禁用”假设已不再成立；对D卡，应说明缺少关联。
目标不是让读者淹没在限制中，而是保留那些会实质改变结论的少数条件。简洁准确的主张，比宽泛承诺加模糊细则更可信。
12. 练习与答案
练习1：同一地址，两种实现
Pxy在H100与H120地址相同，但实现从I7变为I8。仅凭R7材料，能否确立I8的P？
答案：不能。当前实现缺少所需关联与范围证据，但这不证明I8有缺陷。
练习2：代码相同，权限新增
I7未变，但证明排除的维护路径被启用。旧论证哪里无法覆盖扩展后的系统？
答案：绕行路径禁用条件不再成立。旧模型转换结果不能确立所有新可达系统行为。
练习3：延期处理意味着什么？
F1已修正并复测，F2延期处理。摘要能否说全部发现均已修复？
答案：不能。应保留F2状态及决定情境，延期不是修正。
练习4：未知结果
工具达到资源限制，未能确立Q。Q属于已证明、已推翻还是未解决？
答案：未解决。单凭资源限制结果，既没有证明，也没有具体反例。
练习5：文件真实性
报告来源已认证，但没有人把它关联到当前部署实现。部署对应性是否成立？
答案：没有。认证报告与证明部署符合报告范围，是不同证据步骤。
练习6：现实真实性
P约束预约计数，是否证明每件实体目录物品都被正确描述？
答案：不能。实体准确性不属于P，也被材料明确排除。
练习7：未来变化
A卡在H100匹配，系统又存在升级权限。这会自动推翻当前有限证明，还是保证它永远适用？
答案：都不是。当前条件性主张可以有依据，未来改变后的行为则需要各自适用证据。
13. 来源与延伸阅读
来源核对于2026年10月12日。虚构材料包是原创教学例子，不是真实审计或求解器运行结果。
- Ethereum智能合约安全：独立审查与审计局限；页面更新于2026年2月26日。
- Solidity 0.8.30 SMTChecker：形式化规范、假设及分析结果。
- OpenZeppelin代理升级模式：稳定入口背后的实现变化。
- OpenZeppelin访问控制：普通角色与管理权限。
- Proving Software Correct Before It Runs：形式化验证的广泛数学基础。
- How Assurance Cases Work：主张、证据及假设之间可审查的联系。
核心问题很简单：究竟确立了什么，针对哪个代码产物，依赖哪些条件，而这些条件是否仍描述正在讨论的系统？