Vào tháng 6 năm 2016, sự phấn khích dâng cao khi “The DAO”, được xây dựng trên chuỗi khối Ethereum, sắp trở thành quỹ đầu tư phi tập trung, kỹ thuật số hoàn toàn đầu tiên trên thế giới.

Nhưng chỉ trong vài tuần, nó đã trở thành điển hình cho các vụ hack DeFi sau khi những kẻ tấn công đánh cắp số ether trị giá 50 triệu đô la từ nó.

Để bẻ khóa The DAO, kẻ tấn công đã khai thác cái gọi là lỗ hổng reentrancy, một lỗ hổng đồng thời trong đó một phương thức của một hợp đồng thông minh cụ thể được gọi trong khi một phương thức khác vẫn đang thực thi và DAO chỉ là một phần trong quá trình phát triển lâu dài của hợp đồng thông minh đầu tiên mắc phải những lỗi như vậy.

Những kẻ kế nhiệm nổi bật bao gồm Uniswap/Lendf.Me, bị đánh cắp 25 triệu đô la vào năm 2020, CREAM, bị đánh cắp 18 triệu đô la vào năm 2021 và Fei, bị đánh cắp 80 triệu đô la vào năm 2022.

Lý do những lỗi này vẫn tồn tại là vì chúng có thể liên quan đến các tương tác mã không mong muốn nằm rải rác trong hợp đồng thông minh, đôi khi ngay cả trong các hợp đồng thông minh khác nhau, số lượng tương tác mã như vậy có thể rất lớn, khiến con người khó phát hiện và loại bỏ hoàn toàn các hợp đồng thông minh ngoài ý muốn. yêu cầu mã .

Hơn nữa, những tương tác này thường khó kiểm tra một cách tự động và có hệ thống.

TLA+: Kẻ hủy diệt

Nhập Logic hành động tạm thời (TLA+), một ngôn ngữ để chỉ định và xác thực các hệ thống phức tạp TLA+ không chỉ tìm thấy lỗi mà còn xác minh sự tồn tại của chúng.

Bạn hỏi làm thế nào điều này có thể xảy ra? TLA+ đi kèm với một bộ công cụ để xác minh chính thức nhẹ nhàng dưới hình thức được gọi là kiểm tra mô hình. Thông qua việc kiểm tra mô hình, nó khám phá toàn diện tất cả các tương tác đồng thời có thể có của mô hình mã - chính những lĩnh vực khó kiểm tra - và tìm ra lỗi.

Hãy tưởng tượng một người tiêu diệt côn trùng chiếu sáng mọi ngóc ngách để vạch trần và loại bỏ những loài gây hại không mong muốn ẩn náu trong những góc tối thường bị bỏ qua hoặc bỏ qua. Điều quan trọng là sau khi mô hình mã được xây dựng, việc kiểm tra mô hình hầu như không cần con người can thiệp để chạy, khiến việc kiểm tra mô hình này có hiệu quả cao về mặt chi phí.

Để minh họa bằng một số con số bịa đặt: Nếu các phương pháp tiêu chuẩn ngành như kiểm tra và đánh giá bảo mật loại bỏ 80% lỗi và xác minh chính thức "nặng ký" loại bỏ 99%, thì việc sử dụng TLA+ sẽ loại bỏ 90% chỉ với một số ít nỗ lực xác minh nặng nề.

Máy tính TLA+ và Internet

Nhóm kỹ thuật của chúng tôi sử dụng TLA+ để phân tích tất cả các khía cạnh của điện toán Internet, bao gồm các hợp đồng thông minh quan trọng về bảo mật chạy trên nền tảng này. Mặc dù máy tính Ethereum và Internet có mô hình thực thi khác nhau nhưng lỗi đăng nhập lại có thể xuất hiện trong hợp đồng thông minh trên cả hai chuỗi khối.

Trên thực tế, do thông lượng cao, máy tính Internet cho phép nhiều cuộc gọi đồng thời đến một hợp đồng thông minh duy nhất, điều này đòi hỏi các tác giả hợp đồng thông minh phải cẩn thận hơn để loại bỏ các tương tác đồng thời không mong muốn. Vì bảo mật rất quan trọng đối với sự thành công của máy tính trên Internet nên TLA+ được sử dụng trong nhiều hợp đồng thông minh để phát hiện lỗi trong giai đoạn phát triển.

Gần đây, một thùng phân tích TLA+ (hợp đồng thông minh cho máy tính trên internet) đã được tiến hành trên Chain-Key Bitcoin (ckBTC) mới phát hành, kết quả mà tôi sẽ chia sẻ bên dưới.

hợp đồng thông minh ckBTC

Để nói về phân tích TLA+ của ckBTC, hãy bắt đầu với cái nhìn tổng quan cấp cao về ckBTC. ckBTC là mã thông báo gốc của máy tính trên internet được hỗ trợ an toàn bởi Bitcoin (BTC) theo tỷ lệ 1:1.

Sổ cái ckBTC là một hợp đồng thông minh chứa trên chuỗi khối máy tính của Internet để theo dõi số lượng ckBTC mà mỗi người dùng cuối sở hữu. Sổ cái tương tự này cho phép người dùng cuối chuyển ckBTC của họ cho người dùng cuối khác nhanh hơn và rẻ hơn so với chuyển BTC trên mạng Bitcoin.

Để chuyển đổi ckBTC thành BTC và ngược lại, người dùng cuối tương tác với một hợp đồng thông minh khác, công cụ khai thác ckBTC.

Ở mức độ cao, hoạt động chuyển đổi từ BTC sang ckBTC trông như thế này:

Các bước để nhận ckBTC:

1. Trước tiên, người dùng cuối chuyển một số BTC đến địa chỉ gửi Bitcoin cụ thể của người dùng, tất cả các địa chỉ gửi tiền đều được kiểm soát hoàn toàn bằng mã của vùng chứa thông minh minter ckBTC do chữ ký ECDSA của khóa chuỗi, tạo ra một UTXO mới thuộc sở hữu của khoản tiền gửi Địa chỉ;

2. Người dùng cuối thông báo cho hợp đồng thông minh đúc tiền ckBTC về UTXO mới được gửi bằng cách yêu cầu xưởng đúc tiền cập nhật số dư của người dùng;

3. Sau đó, hợp đồng thông minh của máy đào sẽ sử dụng sự tích hợp Bitcoin của máy tính Internet để truy xuất tất cả các UTXO thuộc sở hữu của địa chỉ gửi tiền do người dùng cụ thể kiểm soát. Sau đó, máy đào sẽ chọn các UTXO mới từ mạng Bitcoin bằng cách gửi cho chúng các kiểm tra chéo. danh sách sổ sách kế toán nội bộ của UTXO mà nó đã xử lý;

4. Cuối cùng, máy đào sẽ hướng dẫn sổ cái đúc ckBTC mới cho tất cả các UTXO mới theo tỷ lệ 1:1 và sau khi hoàn thành, nó sẽ thêm các UTXO mới được phát hiện vào danh sách các UTXO đã xử lý.

Tuyên bố miễn trừ trách nhiệm: Quy trình trên bỏ qua quy trình KYT (Biết giao dịch của bạn) để đơn giản hóa.

Hợp đồng thông minh ckBTC đáp ứng TLA+

Bức tranh cấp cao được trình bày ở trên thực sự che giấu một vấn đề tương tranh khó phát hiện và tin tốt là chúng ta có thể phát hiện vấn đề bằng cách sử dụng bộ công cụ TLA+.

Nhưng trước khi TLA+ có thể phát hiện bất cứ điều gì, trước tiên chúng tôi phải cung cấp cho nó hai thứ:

• Tạo mô hình hệ thống của chúng tôi bằng ngôn ngữ TLA+

• Chỉ định các thuộc tính TLA+ mà chúng tôi mong đợi hệ thống triển khai

Mô hình này là một phiên bản đơn giản nhưng vẫn được xác định đầy đủ của hệ thống, trong trường hợp của chúng tôi bao gồm hợp đồng thông minh minter nhưng cũng có tất cả các phần liên quan khác của hệ thống, cụ thể là hợp đồng sổ cái và mạng Bitcoin.

Đối với mỗi thành phần, chúng tôi lập mô hình trạng thái của nó và cách các hành động liên quan mà người dùng cuối có thể thực hiện (tức là chuyển BTC hoặc ckBTC, gửi BTC hoặc gọi các hành động khác nhau do người khai thác đưa ra) sẽ thay đổi trạng thái.

Tất cả các yếu tố này được đơn giản hóa phần nào trong mô hình, với các phần mà phân tích tập trung vào (ví dụ: mã máy đào) được mô hình hóa chi tiết hơn, trong khi các phần khác (ví dụ: mạng Bitcoin) được mô hình hóa ít chi tiết hơn, trên thực tế, là mô hình TLA+ tương tự như đặc tả thiết kế chi tiết của một hệ thống.

Theo trực quan, tính năng chính mà chúng tôi muốn triển khai là đảm bảo rằng ckBTC của chúng tôi được hỗ trợ đầy đủ. Nói cách khác, không người dùng cuối nào có thể “chi tiêu gấp đôi” số BTC đã gửi của họ để nhận được nhiều ckBTC hơn số tiền họ đã gửi.

Nhưng để phân tích một tính chất như vậy, chúng ta phải làm cho trực giác này trở nên thật chính xác bằng cách diễn đạt nó một cách hình thức bằng ngôn ngữ TLA+. Định nghĩa chính thức của chúng tôi là tổng nguồn cung ckBTC (tức là tổng tất cả số dư ckBTC của người dùng cuối, được lưu trữ bởi sổ cái ckBTC) không vượt quá tổng số lượng BTC được kiểm soát bởi vùng đúc tiền (tức là giá trị của tất cả UTXO thuộc sở hữu của địa chỉ gửi tiền).

Phát hiện và giải quyết vấn đề

Khi chúng tôi đã tạo mô hình và thuộc tính, bộ công cụ TLA+ có thể phân tích mô hình. Để chạy phân tích, trước tiên chúng tôi xác định cài đặt để chạy phân tích. Ví dụ: thiết lập của chúng tôi cho ckBTC chỉ bao gồm hai người dùng cuối khác nhau và một lượng nhỏ trong tổng nguồn cung Bitcoin (ví dụ: 5 satoshi).

Mặc dù cài đặt này rất hạn chế nhưng các nghiên cứu thực nghiệm cho thấy rằng phần lớn các vấn đề trong hệ thống máy tính có thể được tìm thấy ở một số ít thực thể. Thiết lập nhỏ cho phép phân tích khám phá một cách có hệ thống tất cả các chuỗi hành động có thể được xác định bởi mô hình và kiểm tra xem các thuộc tính được quy định có tuân theo bất kỳ chuỗi nào như vậy hay không.

Hơn nữa, quá trình phân tích diễn ra hoàn toàn tự động, tức là không yêu cầu bất kỳ thông tin đầu vào nào của con người và nếu các thuộc tính này không được giữ nguyên, nó sẽ cung cấp cho chúng ta chuỗi hoạt động chính xác vi phạm thuộc tính đó.

Ví dụ: phân tích có thể tiết lộ rằng chúng tôi có thể vi phạm thuộc tính "không có ckBTC không bảo đảm" của mình trong tình huống giống như tình huống trong hình bên dưới:

đây:

• Người dùng cuối gửi BTC, giống như trước đây;

• Tuy nhiên, giờ đây, người dùng cuối sẽ hướng dẫn công cụ khai thác ckBTC cập nhật số dư hai lần liên tiếp và trên máy tính internet, những cập nhật này có thể được tương tác đồng thời với các hợp đồng thông minh khác;

• Hai bản cập nhật chạy đồng thời yêu cầu mạng Bitcoin tìm tất cả các UTXO được người dùng cuối gửi và cả hai đều nhận được phản hồi cùng một UTXO đã gửi ở bước 1. Vì UTXO chưa có trong danh sách "đã xử lý" nên cả hai bản cập nhật đều nghĩ UTXO là mới;

• Cả hai bản cập nhật đều hướng dẫn sổ cái đúc số lượng ckBTC tương ứng ở bước 4.

Do đó, ở cuối bước 4, chúng tôi đang ở trạng thái có nguồn cung ckBTC gấp đôi tổng số UTXO trong các địa chỉ gửi tiền, điều này vi phạm thuộc tính "không có ckBTC không được hỗ trợ" của chúng tôi.

Lưu ý rằng lỗi này chỉ xảy ra do các cập nhật đối với số dư của người dùng cuối được thực thi đồng thời - đây thực sự là một lỗi được gửi lại theo cùng kiểu với lỗi đã khiến The DAO bị sập.

Một cách để giải quyết vấn đề này là ngăn các bản cập nhật số dư chạy song song cho cùng một người dùng cuối, chúng ta có thể thực hiện việc này bằng cách yêu cầu công cụ khai thác lưu trữ người dùng cuối trong danh sách người dùng "bị khóa" khi cập nhật số dư bắt đầu và giữ chúng ở đó trong suốt thời gian của danh sách cập nhật để đạt được điều này.

Nếu người dùng cuối cố gắng bắt đầu một bản cập nhật số dư đồng thời khác, bản cập nhật trước tiên sẽ kiểm tra và tìm người dùng cuối cụ thể này trong danh sách người dùng bị khóa, sau đó hủy bỏ.

Lưu ý rằng ở đây chúng tôi đang đơn giản hóa cuộc tấn công một chút: khóa thực sự là một mô hình khá phổ biến đối với các hợp đồng thông minh IC và các thợ đào ckBTC đã triển khai nó ngay từ đầu. Tuy nhiên, việc khóa được thực hiện không đúng cách sẽ mở ra cơ hội cho các cuộc tấn công trên mà TLA+ có thể phát hiện.

Ngoài ra, chúng tôi đã phát hiện một số trường hợp nghiêm trọng vi phạm "không có ckBTC không được hỗ trợ" và các thuộc tính quan trọng khác và sau khi chúng tôi áp dụng tất cả các bản sửa lỗi, TLA+ có thể xác minh và xác nhận rằng không còn vi phạm thuộc tính nào nữa trong thiết lập đã xác định của chúng tôi.

Bạn có nên sử dụng TLA+ cho hợp đồng thông minh của mình không?

Tuyệt đối! Được rồi, được rồi, có lẽ tôi nên đưa ra câu trả lời chi tiết hơn mà nhóm R&D của chúng tôi sử dụng cho các hợp đồng thông minh quan trọng trên máy tính Internet bất cứ khi nào có sự đồng thời không tầm thường.

Ví dụ: phân tích TLA+ đã phát hiện ra các lỗi đồng thời tinh vi trong Quản trị máy tính Internet và Bộ chứa sổ cái đã bị bỏ qua trong các đánh giá bảo mật thủ công trước đó và có thể dẫn đến các vấn đề, trường hợp và điểm quan trọng — TLA+ là công cụ giúp phát hiện ra những vấn đề hóc búa như vậy. Một vụ nổ tuyệt đối.

Tất nhiên, sẽ phải trả giá khi có được bí quyết và sau đó xây dựng mô hình, nhưng về mặt thực nghiệm thì mức giá này là hợp lý, đặc biệt là với tính chất rủi ro cao của bảo mật blockchain.

Người ta không nên bị chính ngôn ngữ TLA+ đe dọa, mặc dù cái tên đáng sợ nhưng việc truy cập các tính năng mạnh mẽ của nó khá đơn giản. Trên thực tế, một bảng tóm tắt TLA+ mô tả hầu hết tất cả các tính năng của TLA+ có thể vừa vặn trên một trang:

• mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html

Hơn nữa, nỗ lực cần thiết để xây dựng mô hình có thể so sánh với việc đánh giá bảo mật thủ công tiêu chuẩn. Ví dụ: đối với một máy khai thác ckBTC, sẽ mất tổng cộng khoảng 3 tuần để 1 người hiểu được thiết kế, tạo mô hình ban đầu và các thuộc tính.

Mô hình TLA+ thu được đơn giản hơn nhiều so với việc triển khai, vì nó đơn giản hơn mã và vì tính chất cấp cao của TLA+. Mô hình cho công cụ khai thác ckBTC yêu cầu khoảng 250 dòng mã so với hàng nghìn dòng triển khai Rust. Có lẽ đáng ngạc nhiên là một trong những phần khó khăn nhất về mặt nỗ lực là chỉ định các thuộc tính cần thiết, vì người ta thường tìm thấy những lỗ hổng trong các thông số kỹ thuật trực quan.

Khi mô hình hoàn tất, quá trình phân tích (kiểm tra mô hình) sẽ tự động được hoàn thành. Quá trình phân tích có thể mất nhiều thời gian – ví dụ: đối với ckBTC, phải mất hơn 20 giờ để hoàn thành. Cuối cùng, một lợi ích khác của TLA là việc lập mô hình và phân tích có thể được thực hiện trong giai đoạn thiết kế trước khi triển khai mã, giúp loại bỏ các lần tái cấu trúc lớn do lỗi thiết kế sau này.

Trường hợp TLA+ vô dụng

Về mặt tiêu cực, TLA+ ít hữu ích hơn đối với các chương trình tuần tự phức tạp, trái ngược với các chương trình đồng thời, và nó cũng không tốt trong việc xử lý các giao thức mật mã phức tạp, trong đó có các công cụ khác (ví dụ: Tamarin) hữu ích hơn.

Cuối cùng, có vấn đề về việc giữ đồng bộ hóa mô hình TLA+ và quá trình triển khai thực tế, vì mã triển khai phát triển theo thời gian, nó có thể không còn phù hợp với mô hình nữa, điều này có thể khó nắm bắt nếu không có công cụ hỗ trợ.

Trên thực tế, nhóm R&D của chúng tôi đang cố gắng giải quyết vấn đề này – tôi hy vọng chúng tôi có thể sớm chia sẻ một số công cụ với bạn!

Tôi hy vọng phần tổng quan này đã thu hút sự quan tâm của bạn đến việc sử dụng TLA+ cho các hợp đồng thông minh quan trọng của riêng bạn và nếu vậy, hãy chú ý theo dõi - bài đăng tiếp theo có hướng dẫn sâu hơn về cách sử dụng TLA+ cho hợp đồng thông minh sẽ sớm ra mắt, và Đính kèm là mô hình TLA+ thực tế được phát triển bởi nhóm R&D của chúng tôi.

Nội dung IC bạn quan tâm

Tiến độ Công nghệ Thông tin Dự án |

Thu thập và theo dõi Kênh IC Binance

Luôn cập nhật những thông tin mới nhất