Bảo mật & kiểm thử

hax

Xác minh hình thức

hax là một công cụ để dịch với độ đảm bảo cao một tập hợp con lớn của Rust sang các ngôn ngữ hình thức như F* hoặc Rocq.

Tài nguyên liên quan

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM là ngữ nghĩa thực thi K-framework của EVM: hãy trỏ nó vào mã byte khi bạn cần thực thi được kiểm tra sự tuân thủ, khám phá tượng trưng, lập luận về gas hoặc các bằng chứng theo dõi chặt chẽ các quy tắc của Ethereum.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol nâng tầm các bài kiểm thử thuộc tính của Foundry thành các bằng chứng được hỗ trợ bởi KEVM để bạn có thể theo đuổi các đảm bảo hình thức với ít công việc viết đặc tả thủ công hơn so với chỉ dùng KEVM thô.

Act

Act là ngôn ngữ đặc tả khai báo và chuỗi công cụ của Ethereum để mô tả tất cả các hành vi của một chương trình EVM để các bộ giải SMT, trình chứng minh định lý hoặc các công cụ phân tích kinh tế có thể lập luận về tính đúng đắn ở cấp độ mã byte và khả năng tương thích khuyến khích, bao gồm các bằng chứng tinh chỉnh tự động đối với các triển khai cụ thể.

Verifereum

Verifereum kết nối các hợp đồng thông minh Ethereum với việc chứng minh định lý được hỗ trợ bởi HOL4 để bạn có thể nhắm đến các tuyên bố về tính đúng đắn rất mạnh mẽ khi các phương pháp SMT tự động là không đủ.