Trạng Thái Tài Khoản Ethereum: Quy Trình QA cho Token Tối Giản

Bảng điều khiển QA giám sát trạng thái Hợp đồng thông minh 

Bài viết trước đã hướng dẫn qua một triển khai từ đầu đến cuối: một hợp đồng token tối thiểu, tái tạo trạng thái off-chain, và một giao diện React — tất cả từ `mint()` đến MetaMask. Bài viết này tiếp tục từ đó: làm thế nào để QA một thứ như thế này?

Tôi không phải là kỹ sư blockchain (chưa), nhưng các mô hình QA chuyển đổi tốt qua các lĩnh vực, và vay mượn những gì đã hoạt động ở nơi khác là cách tôi học nhanh nhất.

Hợp đồng chỉ làm ba việc: `mint`, `transfer`, và `burn`, nhưng ngay cả điều đó cũng đủ để thực hành toàn bộ chuỗi công cụ QA: phân tích tĩnh, kiểm tra đột biến, phân tích gas, xác minh chính thức.

Mã nguồn nằm trong `egpivo/ethereum-account-state`.

Kim tự tháp QA Blockchain: từ phân tích tĩnh ở cơ sở đến xác minh chính thức ở đỉnh

Những gì chúng tôi bắt đầu với

Trước khi thêm bất cứ điều gì mới, dự án đã có:

• 21 bài kiểm tra đơn vị Foundry bao phủ mỗi chuyển đổi trạng thái (thành công, hoàn nguyên khi đầu vào không hợp lệ, phát ra sự kiện)
• 3 bài kiểm tra bất biến thông qua một `TokenHandler` chạy các chuỗi ngẫu nhiên của `mint`/`transfer`/`burn` trên 10 actor (128k lần gọi mỗi cái)
• Kiểm tra Fuzz kiểm tra `sum(balances) == totalSupply` cho các số lượng ngẫu nhiên
• Kiểm tra miền TypeScript (Vitest) phản ánh máy trạng thái on-chain 
• CI: biên dịch, kiểm tra, lint (Prettier + solhint)

Tất cả các bài kiểm tra đều vượt qua. Độ bao phủ trông ổn. Vậy tại sao phải bận tâm với nhiều hơn?

Bởi vì "tất cả các bài kiểm tra đều vượt qua" không có nghĩa là "tất cả các lỗi đều được phát hiện." 100% độ bao phủ dòng vẫn có thể bỏ lỡ một lỗi thực sự nếu không có xác nhận nào kiểm tra điều đúng.

Giai đoạn 1: Phân tích tĩnh Hợp đồng thông minh và độ bao phủ

Slither

Slither(Trail of Bits) phát hiện các vấn đề không thể nhìn thấy qua kiểm tra: tái nhập, giá trị trả về không được kiểm tra, không khớp giao diện.

./scripts/run-qa.sh slither

Kết quả: 1 phát hiện Trung bình: `erc20-interface`: `transfer()` không trả về `bool`.

Điều này được mong đợi. Hợp đồng cố ý không phải là ERC20 đầy đủ: nó là một máy trạng thái giáo dục. Nhưng phát hiện không phải là học thuật:

Nếu ai đó sau này nhập token này vào một giao thức mong đợi ERC20, sự không khớp giao diện sẽ thất bại im lặng. Slither gắn cờ nó ngay bây giờ để quyết định là có ý thức.

Độ bao phủ

./scripts/run-qa.sh coverageKết quả độ bao phủ.

Một hàm không được bao phủ: `BalanceLib.gt()`. Chúng ta sẽ quay lại điều này.

đầu ra forge coverage: 24 bài kiểm tra vượt qua, bảng độ bao phủ Token.sol 

Ảnh chụp nhanh Gas

./scripts/run-qa.sh gas

Chi phí gas cơ bản cho ba thao tác:

Gas theo các thao tác

Ở các lần chạy tiếp theo, `forge snapshot — diff` so sánh với đường cơ sở. Sự hồi quy gas 20% trong `transfer()` là chi phí thực sự cho mỗi người dùng — phát hiện nó trước khi merge là rẻ.

Giai đoạn 2: Kiểm tra đột biến và xác minh chính thức

Kiểm tra đột biến (Gambit)

Đây là nơi mọi thứ trở nên thú vị. Gambit(Certora) tạo ra các đột biến: các bản sao của `Token.sol` với các lỗi nhỏ cố ý (`+=` thành `-=`, `>=` thành `>`, các điều kiện bị phủ định). Pipeline chạy toàn bộ bộ kiểm tra đối với mỗi đột biến. Nếu một đột biến sống sót (tất cả các bài kiểm tra vẫn vượt qua), đó là một khoảng trống kiểm tra cụ thể.

./scripts/run-qa.sh mutation

Kết quả: Điểm đột biến 97.0% — 32 bị tiêu diệt, 1 sống sót trong số 33 đột biến.

Nhật ký đầu ra của Gambit hiển thị mỗi đột biến và những gì nó đã thay đổi. Một vài ví dụ:

Đột biến được tạo #7: BinaryOpMutation — Token.sol:168
totalSupply = totalSupply.add(amountBalance) → totalSupply = totalSupply.sub(amountBalance)
BỊ TIÊU DIỆT bởi test_Mint_Success
Đột biến được tạo #19: RelationalOpMutation — Token.sol:196
if (!fromBalance.gte(amountBalance)) → if (fromBalance.gte(amountBalance))
BỊ TIÊU DIỆT bởi test_Transfer_Success
Đột biến được tạo #28: SwapArgumentsMutation — Token.sol:81
return Balance.unwrap(a) > Balance.unwrap(b) → return Balance.unwrap(b) > Balance.unwrap(a)
SỐNG SÓT ← không có bài kiểm tra nào phát hiện điều nàyKiểm tra đột biến Gambit: 32 bị tiêu diệt, 1 sống sót, điểm đột biến 97.0%

Đột biến sống sót đã hoán đổi `a > b` thành `b > a` trong `BalanceLib.gt()`. Không có bài kiểm tra nào phát hiện nó vì `gt()` là mã chết. Nó không bao giờ được gọi ở bất cứ đâu trong `Token.sol`.

Độ bao phủ gắn cờ 91.67% hàm nhưng không thể giải thích khoảng trống. Kiểm tra đột biến đã làm: `gt()` là mã chết, không có gì gọi nó, và không ai sẽ nhận thấy nếu nó sai.

Mã chết hoặc không được bảo vệ trong Hợp đồng thông minh có tiền lệ thực tế.

Hàm không được dự định là có thể gọi, nhưng không ai kiểm tra giả định đó. `gt()` của chúng ta vô hại khi so sánh, nhưng mô hình giống nhau: mã tồn tại nhưng không bao giờ được thực hiện là mã không ai đang theo dõi.

Xác minh chính thức (Halmos)

Halmos(a16z) suy luận về tất cả các đầu vào có thể một cách tượng trưng. Nơi các bài kiểm tra fuzz lấy mẫu các giá trị ngẫu nhiên và hy vọng chạm các trường hợp biên, Halmos chứng minh các thuộc tính một cách đầy đủ.

./scripts/run-qa.sh halmos

Kết quả: 9/9 bài kiểm tra tượng trưng vượt qua — tất cả các thuộc tính được chứng minh cho tất cả đầu vào.

Các thuộc tính đã xác minh:

Các thuộc tính đã xác minh

Một lưu ý thực tế: Halmos 0.3.3 không hỗ trợ `vm.expectRevert()`, vì vậy tôi không thể viết các bài kiểm tra hoàn nguyên theo cách Foundry bình thường. Giải pháp là một mô hình try/catch — nếu lệnh gọi thành công khi nó nên hoàn nguyên, `assert(false)` làm thất bại chứng minh:

function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // không nên đến đây
} catch {
// hoàn nguyên dự kiến - Halmos chứng minh đường dẫn này luôn được thực hiện
}
}

Không đẹp nhất, nhưng nó hoạt động — Halmos vẫn chứng minh thuộc tính cho tất cả các đầu vào. Đây là loại điều bạn chỉ tìm ra bằng cách thực sự chạy công cụ.

Để biết bối cảnh về lý do xác minh chính thức quan trọng:

Lỗ hổng nằm trong mã, có thể xem xét bởi bất kỳ ai, nhưng không có công cụ hoặc bài kiểm tra nào phát hiện nó trước khi triển khai. Các công cụ chứng minh tượng trưng như Halmos tồn tại chính xác để đóng khoảng trống đó — chúng không lấy mẫu; chúng kiệt quệ không gian đầu vào.

Đầu ra Halmos: 9 bài kiểm tra vượt qua, 0 thất bại, kết quả kiểm tra tượng trưng 

Tệp kiểm tra là `contracts/test/Token.halmos.t.sol`.

Giai đoạn 3: Kiểm tra thuộc tính cross-layer 

Kiến trúc của bài viết đầu tiên có một lớp miền TypeScript phản ánh máy trạng thái on-chain. Giai đoạn này kiểm tra liệu hai cái có thực sự đồng ý không.

Kiểm tra dựa trên thuộc tính với fast-check

Tôi đã thêm các bài kiểm tra thuộc tính fast-check cho lớp miền TypeScript, phản ánh những gì fuzzer của Foundry làm cho Solidity:

npm test - tests/unit/property.test.ts

Kết quả: 9/9 bài kiểm tra thuộc tính vượt qua sau khi sửa một lỗi thực sự.

Các thuộc tính đã kiểm tra:

• `Balance`: tính giao hoán, tính kết hợp, phần tử đơn vị, phần tử nghịch đảo, tính nhất quán so sánh
• `Token`: bất biến `sum(balances) == totalSupply` dưới các chuỗi thao tác ngẫu nhiên (200 lần chạy, 50 thao tác mỗi lần)
• `Token`: `totalSupply` không âm sau các chuỗi ngẫu nhiên
• `mint` luôn thành công cho các đầu vào hợp lệ
• `transfer` bảo toàn `totalSupply`

Lỗi fast-check tìm thấy

fast-check đã tìm thấy một lỗi tính nhất quán cross-layer thực sự trong `transfer()` của `Token.ts`. Ví dụ phản chứng đã thu nhỏ rõ ràng ngay lập tức:

Thuộc tính thất bại sau 3 bài kiểm tra
Thu nhỏ 2 lần
Ví dụ phản chứng: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (tự chuyển)
→ verifyInvariant() trả về false

Tự chuyển (`from == to`) đã phá vỡ bất biến `sum(balances) == totalSupply`. `toBalance` được đọc trước khi `fromBalance` được cập nhật, vì vậy khi `from == to`, giá trị cũ đã ghi đè phép trừ:

// Trước (lỗi)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← cũ khi from == to
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← ghi đè phép trừ

Sửa: đọc `toBalance` sau khi ghi `fromBalance`, khớp với ngữ nghĩa lưu trữ của Solidity:

// Sau (đã sửa)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← bây giờ đọc giá trị đã cập nhật
this.accounts.set(to.getValue(), toBalance.add(amount));

Hợp đồng Solidity không bị ảnh hưởng: nó đọc lại lưu trữ sau mỗi lần ghi. Nhưng bản phản ánh TypeScript có một sự phụ thuộc thứ tự tinh tế mà không có bài kiểm tra đơn vị hiện có nào bao phủ.

Sự không khớp cross-layer ở quy mô lớn hơn đã rất thảm khốc.

Lỗi tự chuyển của chúng ta sẽ không làm mất tiền của ai, nhưng chế độ thất bại giống nhau về cấu trúc: hai lớp được cho là đồng ý, thì không.

Các cạm bẫy gặp phải trên đường

Chạy các công cụ QA trên một dự án hiện có không bao giờ chỉ là "cài đặt và chạy." Một vài điều bị hỏng trước khi chúng hoạt động:

• 0% độ bao phủ vì `foundry.toml` không có đường dẫn kiểm tra: Lần chạy `forge coverage` đầu tiên trả về 0% trên toàn bộ. Hóa ra `foundry.toml` không chỉ định `test = "contracts/test"` hoặc `script = "contracts/script"`, vì vậy Forge không khám phá bất kỳ bài kiểm tra nào. Lệnh độ bao phủ thành công im lặng — nó chỉ không có gì để bao phủ. Đây là thất bại gây hiểu lầm nhất: một lần chạy xanh không có đầu ra hữu ích.
• Import `InvariantTest` không còn trong forge-std v1.14.0: `Invariant.t.sol` đã nhập `InvariantTest` từ `forge-std`, đã bị xóa trong một bản phát hành gần đây. Biên dịch thất bại với lỗi "symbol not found" mơ hồ. Cách sửa là bỏ import — `Test` một mình là đủ cho kiểm tra bất biến của Foundry bây giờ.
• `uint256(token.totalSupply())` so với `Balance.unwrap()`: Các bài kiểm tra đang sử dụng một ép kiểu rõ ràng để trích xuất `uint256` cơ bản từ kiểu `Balance` do người dùng định nghĩa. Nó biên dịch, nhưng đó là thành ngữ sai — `Balance.unwrap(token.totalSupply())` là những gì hệ thống UDVT được thiết kế cho. Áp dụng trên `Token.t.sol`, `Invariant.t.sol`, và `DeploySepolia.s.sol`.

Thiết kế Pipeline

Mọi thứ chạy qua hai script:

• scripts/setup-qa-tools.sh`: cài đặt Slither, Halmos, Gambit (idempotent)
• `scripts/run-qa.sh`: chạy kiểm tra, lưu kết quả có dấu thời gian vào `qa-results/`

./scripts/run-qa.sh slither gas # chỉ phân tích tĩnh + gas
./scripts/run-qa.sh mutation # chỉ kiểm tra đột biến
./scripts/run-qa.sh all # mọi thứ

Không phải mọi kiểm tra đều nhanh. Slither và độ bao phủ chạy trên mỗi commit. Kiểm tra đột biến và Halmos chậm hơn — phù hợp hơn cho các lần chạy hàng tuần hoặc trước phát hành.

Tóm tắt

Chuỗi công cụ QA Blockchain: những gì mỗi lớp phát hiện — từ phân tích tĩnh đến kiểm tra thuộc tính cross-layer 

Năm lớp QA, mỗi lớp phát hiện một lớp vấn đề khác nhau.

Giải thích lớp

Gambit và fast-check đưa ra kết quả có thể hành động nhất trong vòng này.

Pipeline CI

Các kiểm tra QA hiện đã được kết nối vào GitHub Actions như một pipeline sáu giai đoạn:

CI Pipeline: Build & Lint mở rộng đến các giai đoạn Test, Coverage, Gas, Slither, và Audit 

Pipeline GitHub Actions: Build & Lint kiểm soát tất cả các giai đoạn downstream.

Giải thích giai đoạn

Tài liệu tham khảo

• Nguồn Ethereum Account State: [github.com/egpivo/ethereum-account-state](https://github.com/egpivo/ethereum-account-state)
• Bài viết trước: Ethereum Account State
• Slither: github.com/crytic/slither
• Gambit: github.com/Certora/gambit
• Halmos: github.com/a16z/halmos
• fast-check: github.com/dubzzz/fast-check
• Foundry: getfoundry.sh

Ghi chú

• Bài viết này được chuyển thể từ bài đăng blog gốc của tôi.

---

Ethereum Account State: QA Pipeline for a Minimal Token ban đầu được xuất bản trong Coinmonks trên Medium, nơi mọi người đang tiếp tục cuộc trò chuyện bằng cách làm nổi bật và phản hồi câu chuyện này.