WongSSH

Build engineer

[WongSSH @wong_ssh]

Yi 发现这个问题后和我进行了讨论，这是一个并不复杂的问题，简单来说就是 ERC4626 金库的奖励分发不应该是突变的，否则攻击者可以在奖励分配前存入资产，然后出触发奖励分配，最后撤回所有资产。我在此前甚至和 ChatGPT 讨论了这个问题。

[Yi @SuplabsYi]

If you’re wrong, own it. If you mishandle a responsible disclosure, take your lumps. @codephobic

I followed USD8’s own security.md, privately submitted a Loss of Funds bug with a working PoC, then watched it get quietly patched with no credit and mocked as spam.

This is exactly how you teach researchers that responsible disclosure is a sucker's game.

I documented the case here:
https://t.co/wePfeHpi6J

cc @openzeppelin @demibrener @holajotola

[Invariant Labs @InvariantBuild]

Formal Verification gets clearer when it moves from textbook examples to real bugs.

Our new Dafny walkthrough starts with Bubble Sort, Quick Sort, and Merge Sort, then shows how specifications, invariants, and proof obligations uncover a stage-accounting vulnerability.

[WongSSH @wong_ssh]

@erik5187 判定某一个 language 是否为 RE 的 pumping lemma 有一个类似表述方法

[WongSSH @wong_ssh]

背后的所有与 codex 的沟通流程可以在 gist 内找到，但是其实没啥用，核心就是让 codex 读 solidity 然后抽象后编写证明不变量的 dafny 代码，最好让 codex 写一份 MODEL.md 文档用于描述目前的抽象情况，方便人工判读，因为抽象不是没有代价的，可能会不小心把核心代码抽象掉
https://t.co/LGOU65XSUt

[WongSSH @wong_ssh]

今天尝试证明了一下 uniswap v4 内的 balance delta 的正确性，核心不变量就是用户的余额变化与 balance delta 变化是一致的，然后把所有涉及到 Balance detla 的 solidity 函数丢给 codex 进行抽象，然后使用 dafny 证明。发现了一个有趣的点，即 self-call 返回 ZERO_DELTA 其实是为了资金安全

[WongSSH @wong_ssh]

当我们尝试干掉 `caller == hook` 的 require 时，我们就可以看到 dafny 的抱怨，其实是因为假如允许 hook 进行 self-call 就会被双重记账，产生没有 balance 支持的 balance delta

[WongSSH @wong_ssh]

听说 Uniswap v4 hook 有火起来了，作为 Uniswap v4 hook 项目开发者并且拿过 Uniswap 审计赞助的我很开心，欢迎大家去读我过去写过的三篇文章。
https://t.co/sPPLxKJhjl
https://t.co/Ow2NSRbRbK
https://t.co/SjgqIwRmFH
虽然我自己的项目 @licredity 至今还没有部署，甚至还有一个漏洞没修

[WongSSH @wong_ssh]

之前还 vibe coding 了一个小工具来辅助抓取某一个核心不变量有关的所有函数片段，过几天可能开源一下，大概只需要十几分钟就可以拿 codex 写出来，底层用的是 slither-analyzer 来解析 solidity 合约

[WongSSH @wong_ssh]

为昨天未完成的博客补充了最后一个案例，并且大概总结了一下如何在 dafny 内证明 solidity 的正确性，这个步骤是我目前认为正确的环节。目前我还没有证明过极其复杂的 solidity 合约机制，我认为 uniswap v3 的区间流动性手续费算法可能算最复杂的合约机制之一，这也是未来我希望证明的机制

[WongSSH @wong_ssh]

博客链接
https://t.co/i1GwjwNWR1

[WongSSH @wong_ssh]

@SphinxPatrick 居然在研究 Dafny 形式化证明前端，感觉杀鸡用牛刀，看了一下基础的模式，感觉和我现在使用 Dafny 证明智能合约用的方法是一致的，把机制抽象成类似状态机的系统，然后证明核心不变量在状态机的每一次状态转移都是正确的

[WongSSH @wong_ssh]

最近手动使用 dafny 证明了几个经典的数组排序算法，从浅入深分别是冒泡排序、快速排序和归并排序，最难证明的应该是快速排序。在写代码过程中，我写了一篇博客。由于我目前实践较少，所以博客内容不太成体系。
除了算法外，博客最后附上了一个智能合约漏洞的证明，明天应该还会再补充另一个案例。

[WongSSH @wong_ssh]

部分内容参考了 The Calculus of Computation 的第六章 Program Correctness: Strategies。
目前来看，使用 dafny 写形式化证明的核心就是复制已知条件进入 loop invariant，毕竟使用的 basic path 方法会丢弃大量上下文。当然，很好的是目前来看，LLM 比我这个初学者厉害，核心性质都可以写出来

[WongSSH @wong_ssh]

博客链接
https://t.co/i1GwjwNWR1

[WongSSH @wong_ssh]

@murage_kibicho z3 is a SMT solver. Some foraml verification likes Dafny use Z3 as default solver. You can verify Quick Sort using Dafny and z3.
https://t.co/1i1Io6Q12i
And SAT/SMT by Example give more examples about how to use smt solver.
https://t.co/OLSHJwsuBG

[WongSSH @wong_ssh]

发现我的 128GB 内存的 MacBook Pro 插电情况下也好卡，看一下活动监控器，发现 z3 内存泄漏了 128GB，太恐怖了。为了保命直接 kill 掉了，感觉应该研究一下内存泄漏的原因，也许这是一个用 Rust 重写 z3 的好理由

[WongSSH @wong_ssh]

@yanbo2004 看上去是因为 vscode 和 dafny 的一些原因炸掉了，感觉应该收集一些信息给开发团队报一下 Bug，但是实在太卡了，直接全部 kill 掉了

[WongSSH @wong_ssh]

而《数学哲学讲义》是真心推荐所有人阅读，内容丰富且有趣，这点可以从课后习题内看到，课后习题的答案其实在前面的文本内都是出现过的。假如有计算机科学背景，建议优先阅读第五章 证明和第六章 可计算性。

[WongSSH @wong_ssh]

最近正在读 2 本与逻辑学有关的书，一本是 The Calculus of Computation，另一本是《面向计算机科学的数理逻辑》(最近出了中文版，但我还是用的影印版)。前者强调 semantics，而后者第一章全是 natural deduction。我没有搞明白两者的异同，但《数学哲学讲义》内证明的哥德尔完备性定理解决了我的疑惑

[WongSSH @wong_ssh]

《面向计算机科学的数理逻辑》的影印版目前应该只能找到二手书了，2005 年出版的，最近出了中文版