XÁC THỰC FORMAL CỦA HỢP ĐỒNG THÔNG MINH
Hợp đồng thông minhđang làm cho việc tạo ra ứng dụng phi tín nhiệm, phi tập trung và mạnh mẽ trở nên khả thi, giới thiệu các trường hợp sử dụng mới và mở khóa giá trị cho người dùng. Bởi vì hợp đồng thông minh xử lý một lượng lớn giá trị, an ninh là một yếu tố quan trọng đối với các nhà phát triển.
Xác minh hình thức là một trong các kỹ thuật được khuyến nghị để cải thiện an toàn hợp đồng thông minh. Xác minh hình thức, sử dụng phương pháp hình thức
được sử dụng từ nhiều năm để xác định, thiết kế và xác minh các chương trình, để đảm bảo tính chính xác của các hệ thống phần cứng và phần mềm quan trọng.
Khi được triển khai trong các hợp đồng thông minh, xác minh hình thức có thể chứng minh logic kinh doanh của một hợp đồng đáp ứng một số quy định cụ thể. So với các phương pháp khác để đánh giá tính đúng đắn của mã hợp đồng, chẳng hạn như kiểm thử, xác minh hình thức đưa ra các cam kết mạnh mẽ hơn rằng một hợp đồng thông minh là chính xác về mặt chức năng.
FORMAL VERIFICATION LÀ GÌ?
Xác minh hình thức đề cập đến quá trình đánh giá tính chính xác của hệ thống so với một đặc tả hình thức. Nói một cách đơn giản, xác minh hình thức cho phép chúng ta kiểm tra xem hành vi của hệ thống có đáp ứng một số yêu cầu hay không (tức là, nó hoạt động theo như chúng ta mong muốn).
Các hành vi dự kiến của hệ thống (một hợp đồng thông minh trong trường hợp này) được mô tả bằng mô hình hình thức, trong khi ngôn ngữ đặc tả cho phép tạo ra các thuộc tính hình thức. Các kỹ thuật xác minh hình thức sau đó có thể xác minh rằng việc triển khai của một hợp đồng tuân thủ với đặc tả của nó và rút ra chứng minh toán học về tính đúng đắn của hợp đồng đó. Khi một hợp đồng đáp ứng đặc tả của nó, nó được mô tả là “chính xác về chức năng”, “chính xác theo thiết kế”, hoặc “chính xác theo công trình”.
Mô hình hình thức là gì?
Trong khoa học máy tính, một mô hình chính thức
là mô tả toán học của một quy trình tính toán. Các chương trình được trừu tượng hóa thành các hàm toán học (phương trình), với mô hình mô tả cách tính các đầu ra cho các hàm được tính toán với một đầu vào.
Mô hình hình thức cung cấp một mức độ trừu tượng mà qua đó phân tích hành vi của chương trình có thể được đánh giá. Sự tồn tại của mô hình hình thức cho phép tạo ra một đặc tả hình thức, mô tả các thuộc tính mong muốn của mô hình cụ thể.
Các kỹ thuật khác nhau được sử dụng để mô hình hóa hợp đồng thông minh để xác minh hình thức. Ví dụ, một số mô hình được sử dụng để suy luận về hành vi cấp cao của một hợp đồng thông minh. Các kỹ thuật mô hình hóa này áp dụng một quan điểm hộp đen cho các hợp đồng thông minh, xem chúng như các hệ thống chấp nhận đầu vào và thực thi tính toán dựa trên các đầu vào đó.
Các mô hình cấp cao tập trung vào mối quan hệ giữa hợp đồng thông minh và các tác nhân bên ngoài, như tài khoản sở hữu bên ngoài (EOAs), tài khoản hợp đồng và môi trường blockchain. Những mô hình như vậy hữu ích để xác định các thuộc tính mô tả cách mà một hợp đồng nên hoạt động khi phản ứng với một số tương tác của người dùng nhất định.
Ngược lại, mô hình hình thức khác tập trung vào hành vi cấp thấp của một hợp đồng thông minh. Trong khi mô hình cấp cao có thể giúp trong việc suy luận về chức năng của một hợp đồng, chúng có thể không thể nắm bắt được chi tiết về cách hoạt động bên trong của việc triển khai. Các mô hình cấp thấp áp dụng quan điểm hộp trắng cho phân tích chương trình và phụ thuộc vào các biểu diễn cấp thấp hơn của các ứng dụng hợp đồng thông minh, như dấu vết chương trình và đồ thị luồng điều khiển
, để suy luận về các thuộc tính liên quan đến việc thực hiện hợp đồng.
Mô hình cấp thấp được coi là lý tưởng vì chúng đại diện cho việc thực thi thực tế của một hợp đồng thông minh trong môi trường thực thi của Ethereum (tức là,EVMCác kỹ thuật mô hình hóa cấp thấp đặc biệt hữu ích trong việc xác định các thuộc tính an toàn quan trọng trong hợp đồng thông minh và phát hiện các lỗ hổng tiềm năng.
Formal specification là gì?
Một đặc tả đơn giản chỉ là yêu cầu kỹ thuật mà một hệ thống cụ thể phải đáp ứng. Trong lập trình, các đặc tả đại diện cho các ý tưởng chung về việc thực hiện chương trình (tức là, chương trình nên làm gì).
Trong ngữ cảnh của hợp đồng thông minh, các đặc tả hình thức đề cập đến các thuộc tính—mô tả hình thức của các yêu cầu mà một hợp đồng phải thỏa mãn. Các thuộc tính như vậy được mô tả là “bất biến” và đại diện cho những khẳng định logic về việc thực thi của một hợp đồng mà phải luôn đúng trong mọi trường hợp có thể xảy ra, mà không có bất kỳ ngoại lệ nào.
Do đó, chúng ta có thể coi một đặc tả hình thức là một tập hợp các câu lệnh được viết bằng một ngôn ngữ hình thức mô tả việc thực thi dự định của một hợp đồng thông minh. Đặc tả bao gồm các thuộc tính của một hợp đồng và xác định cách mà hợp đồng nên hoạt động trong các hoàn cảnh khác nhau. Mục đích của việc xác minh hình thức là để xác định xem một hợp đồng thông minh có sở hữu những thuộc tính này (các không đổi) và rằng những thuộc tính này không bị vi phạm trong quá trình thực thi.
Các đặc tả chính thức rất quan trọng trong việc phát triển các triển khai an toàn của hợp đồng thông minh. Các hợp đồng mà không thực hiện được những biến invariants hoặc có các thuộc tính của họ bị vi phạm trong quá trình thực thi có thể dễ bị tổn thương chức năng hoặc gây ra lỗ hổng độc hại.
CÁC LOẠI ĐỊNH DẠNG FORMAL CHO HỢP ĐỒNG THÔNG MINH
Các đặc tả chính thức cho phép lập luận toán học về tính đúng đắn của việc thực thi chương trình. Giống như các mô hình chính thức, các đặc tả chính thức có thể bắt kịp các thuộc tính ở mức cao hoặc hành vi ở mức thấp của việc thực thi hợp đồng.
Các thông số chính thức được tạo ra bằng cách sử dụng các yếu tố củalogic chương trình
, cho phép lý luận hình thức về các tính chất của một chương trình. Một logic chương trình có các quy tắc hình thức biểu diễn (bằng ngôn ngữ toán học) hành vi dự kiến của một chương trình. Các logic chương trình khác nhau được sử dụng trong việc tạo ra các thông số kỹ thuật hình thức, bao gồm lô-gic khả năng tiếp cận
và Hoare logic
Các đặc tả chính thức cho hợp đồng thông minh có thể được phân loại rộng rãi là đặc tả cấp cao hoặc đặc tả cấp thấp. Bất kể đặc tả thuộc loại nào, nó phải mô tả đầy đủ và không gây hiểu lầm về thuộc tính của hệ thống đang được phân tích.
Đặc tả cấp cao
Như tên cho thấy, một đặc tả cấp cao (còn được gọi là "đặc tả hướng mô hình") mô tả hành vi cấp cao của một chương trình. Thông số kỹ thuật cấp cao mô hình hợp đồng thông minh dưới dạng máy trạng thái hữu hạn
(FSM), mà có thể chuyển tiếp giữa các trạng thái bằng cách thực hiện các hoạt động, với logic thời gian được sử dụng để xác định các tính chất hình thức cho mô hình FSM.
là “các quy tắc để suy luận về các mệnh đề được xác định theo thời gian (ví dụ, “Tôi luôn đói” hoặc “Cuối cùng tôi sẽ đói”).” Khi áp dụng vào xác minh hình thức, logic thời gian được sử dụng để nêu các khẳng định về hành vi chính xác của các hệ thống được mô hình hóa như các máy trạng thái. Cụ thể, logic thời gian mô tả các trạng thái tương lai mà một hợp đồng thông minh có thể ở và cách nó chuyển đổi giữa các trạng thái.
Các đặc tả cấp cao thường bao gồm hai tính chất thời gian quan trọng cho hợp đồng thông minh: an toàn và sống động. Các tính chất an toàn đại diện cho ý tưởng rằng “không bao giờ xảy ra điều xấu” và thường biểu diễn tính không biến đổi. Một tính chất an toàn có thể định nghĩa các yêu cầu phần mềm chung, chẳng hạn như sự tự do khỏideadlock
, hoặc biểu diễn các tính chất cụ thể cho hợp đồng (ví dụ, điều kiện không thay đổi về kiểm soát truy cập cho các chức năng, các giá trị cho phép của biến trạng thái, hoặc điều kiện cho việc chuyển token).
Ví dụ, yêu cầu an toàn này bao gồm các điều kiện sử dụng transfer() hoặc transferFrom() trong các hợp đồng token ERC-20: “Số dư của người gửi không bao giờ thấp hơn số lượng token được yêu cầu gửi đi.”. Mô tả ngôn ngữ tự nhiên này về một hằng số hợp đồng có thể được dịch thành một đặc tả (toán học) chính thức, sau đó có thể được kiểm tra một cách nghiêm ngặt để xác thực.
Thuộc tính liveness khẳng định rằng “cuối cùng sẽ xảy ra điều tốt” và liên quan đến khả năng của hợp đồng để tiến triển qua các trạng thái khác nhau. Một ví dụ về thuộc tính liveness là “thuận lợi về thanh khoản”, đề cập đến khả năng của một hợp đồng để chuyển số dư của mình cho người dùng khi được yêu cầu. Nếu thuộc tính này bị vi phạm, người dùng sẽ không thể rút ra tài sản được lưu trữ trong hợp đồng, giống như điều đã xảy ra với Sự cố ví Parity
.
Thông số cấp thấp
Các đặc tả cấp cao lấy mô hình trạng thái hữu hạn của hợp đồng làm điểm khởi đầu và xác định các thuộc tính mong muốn của mô hình này. Ngược lại, các đặc tả cấp thấp (còn được gọi là 'đặc tả hướng thuộc tính') thường mô hình các chương trình (hợp đồng thông minh) như các hệ thống bao gồm một bộ sưu tập các hàm toán học và mô tả hành vi chính xác của các hệ thống đó.
Nói một cách đơn giản hơn, các thông số kỹ thuật cấp thấp phân tích dấu vết chương trình và cố gắng xác định các thuộc tính của hợp đồng thông minh trên các dấu vết này. Dấu vết đề cập đến chuỗi thực thi chức năng làm thay đổi trạng thái của hợp đồng thông minh; Do đó, các thông số kỹ thuật cấp thấp giúp xác định các yêu cầu đối với việc thực hiện nội bộ của hợp đồng.
Các đặc tả hình thức cấp thấp có thể được xác định dưới dạng các thuộc tính kiểu Hoare hoặc các điều kiện không đổi trên đường đi thực thi.
Các tính chất theo phong cách Hoare
cung cấp một bộ quy tắc hình thức để suy luận về tính chính xác của các chương trình, bao gồm các hợp đồng thông minh. Một thuộc tính kiểu Hoare được biểu diễn bằng một ba Hoare {P}c{Q}, trong đó c là một chương trình và P và Q là các mệnh đề về trạng thái của c (tức là chương trình), được mô tả một cách hình thức như các điều kiện tiên quyết và điều kiện hậu quả, tương ứng.
Một điều kiện tiên điều là một mệnh đề mô tả các điều kiện cần thiết cho việc thực thi đúng của một hàm; người dùng gọi vào hợp đồng phải đáp ứng yêu cầu này. Một điều kiện hậu điều là một mệnh đề mô tả điều kiện mà một hàm thiết lập nếu được thực thi đúng; người dùng có thể mong đợi điều kiện này là đúng sau khi gọi vào hàm. Một biến không đổi trong logic Hoare là một mệnh đề được bảo tồn bởi việc thực thi của một hàm (tức là, nó không thay đổi).
Các thông số kiểu Hoare có thể đảm bảo tính đúng đắn một phần hoặc hoàn toàn. Việc triển khai của một hàm hợp đồng được coi là "một phần đúng" nếu điều kiện tiên quyết đúng trước khi hàm được thực thi, và nếu thực thi kết thúc, điều kiện hậu quả cũng đúng. Chứng minh tính đúng đắn hoàn toàn được đạt được nếu điều kiện tiên quyết đúng trước khi hàm thực thi, thực thi được đảm bảo kết thúc và khi thực thi kết thúc, điều kiện hậu quả cũng đúng.
Việc chứng minh tính đúng đắn hoàn toàn khó khăn vì một số thực thi có thể trì hoãn trước khi kết thúc, hoặc thậm chí không bao giờ kết thúc. Tuy nhiên, việc thực thi có kết thúc hay không có thể coi là vấn đề không đáng kể khi cơ chế gas của Ethereum ngăn chặn vòng lặp chương trình vô hạn (thực thi kết thúc thành công hoặc kết thúc do lỗi 'hết gas').
Các đặc tả hợp đồng thông minh được tạo ra bằng logic Hoare sẽ có các tiền điều kiện, hậu điều kiện và không biến được xác định cho việc thực thi các hàm và vòng lặp trong một hợp đồng. Tiền điều kiện thường bao gồm khả năng nhập không chính xác vào một hàm, trong khi hậu điều kiện mô tả phản hồi dự kiến cho các đầu vào đó (ví dụ, ném một ngoại lệ cụ thể). Theo cách này, các thuộc tính theo phong cách Hoare là hiệu quả để đảm bảo tính chính xác của việc triển khai hợp đồng.
Nhiều khung xác minh chính thức sử dụng các thông số kỹ thuật kiểu Hoare để chứng minh tính đúng đắn ngữ nghĩa của các hàm. Cũng có thể thêm các thuộc tính kiểu Hoare (dưới dạng khẳng định) trực tiếp vào mã hợp đồng bằng cách sử dụng các câu lệnh require và assert trong Solidity.
Các câu lệnh yêu cầu biểu thị một điều kiện tiên quyết hoặc bất biến và thường được sử dụng để xác minh đầu vào của người dùng, trong khi assert ghi lại một hậu điều kiện cần thiết cho an toàn. Ví dụ, kiểm soát truy cập đúng đắn cho các chức năng (một ví dụ về thuộc tính an toàn) có thể được đạt được bằng cách sử dụng require như một kiểm tra tiên quyết về danh tính của tài khoản gọi. Tương tự, một bất biến về các giá trị cho phép của biến trạng thái trong một hợp đồng (ví dụ, tổng số token trong lưu thông) có thể được bảo vệ khỏi vi phạm bằng cách sử dụng assert để xác nhận trạng thái của hợp đồng sau khi thực thi chức năng.
Thuộc tính cấp Trace
Các mô tả dựa trên dấu vết mô tả các hoạt động chuyển đổi hợp đồng giữa các trạng thái khác nhau và mối quan hệ giữa các hoạt động này. Như đã giải thích trước đó, các dấu vết là chuỗi các hoạt động thay đổi trạng thái của một hợp đồng theo cách cụ thể.
Phương pháp này phụ thuộc vào mô hình hợp đồng thông minh như các hệ thống chuyển trạng thái với một số trạng thái được xác định trước (mô tả bởi biến trạng thái) cùng với một tập hợp các chuyển trạng thái được xác định trước (mô tả bởi các chức năng hợp đồng). Hơn nữa, một biểu đồ luồng điều khiển
(CFG), đây là biểu diễn đồ họa của luồng thực thi chương trình, thường được sử dụng để mô tả ngữ nghĩa vận hành của một hợp đồng. Ở đây, mỗi dấu vết được biểu diễn dưới dạng một đường đi trên đồ thị luồng điều khiển.
Đầu tiên, các thông số cấp độ theo dõi được sử dụng để suy luận về các mẫu thực thi nội bộ trong hợp đồng thông minh. Bằng cách tạo các thông số cấp độ theo dõi, chúng ta khẳng định các đường đi thực thi cho phép (tức là, các chuyển đổi trạng thái) cho một hợp đồng thông minh. Sử dụng các kỹ thuật, như thực thi tượng trưng, chúng ta có thể xác minh hình thức rằng thực thi không bao giờ đi theo một đường không được xác định trong mô hình hình thức.
Hãy sử dụng một ví dụ về một DAOhợp đồng có một số chức năng có thể truy cập công khai để mô tả các thuộc tính cấp độ theo dõi. Ở đây, chúng ta giả định hợp đồng DAO cho phép người dùng thực hiện các hoạt động sau:
- Nạp tiền
- Bỏ phiếu cho một đề xuất sau khi gửi tiền
- Yêu cầu hoàn tiền nếu họ không bỏ phiếu cho một đề xuất
Các thuộc tính cấp độ theo dõi ví dụ có thể là “người dùng không nạp tiền không thể bỏ phiếu cho một đề xuất” hoặc “người dùng không bỏ phiếu cho một đề xuất luôn luôn có thể yêu cầu hoàn tiền”. Cả hai thuộc tính này khẳng định các chuỗi thực thi ưa thích (việc bỏ phiếu không thể xảy ra trước khi nạp tiền và việc yêu cầu hoàn tiền không thể xảy ra sau khi bỏ phiếu cho một đề xuất).
CÁC KỸ THUẬT CHO VIỆC XÁC MINH FORMAL CỦA HỢP ĐỒNG THÔNG MINH
Kiểm tra mô hình
Kiểm tra mô hình là một kỹ thuật xác minh hình thức trong đó một thuật toán kiểm tra một mô hình hình thức của một hợp đồng thông minh đối với đặc tả của nó. Trong kiểm tra mô hình, các hợp đồng thông minh thường được biểu diễn dưới dạng hệ thống chuyển trạng thái, trong khi các thuộc tính trên các trạng thái hợp đồng cho phép được xác định bằng logic thời gian.
Kiểm tra mô hình đòi hỏi tạo ra một biểu diễn toán học trừu tượng của một hệ thống (tức là một hợp đồng) và diễn đạt các tính chất của hệ thống này bằng các công thức gốc trong logic hồi quy
Điều này giúp đơn giản hóa công việc của thuật toán kiểm tra mô hình, cụ thể là chứng minh rằng một mô hình toán học thỏa mãn một công thức logic đã cho.
Kiểm tra mô hình trong xác minh hình thức chủ yếu được sử dụng để đánh giá các thuộc tính thời gian mô tả hành vi của một hợp đồng theo thời gian. Các thuộc tính thời gian cho hợp đồng thông minh bao gồm an toàn và sự sống còn, mà chúng tôi đã giải thích trước đó.
Ví dụ, một thuộc tính bảo mật liên quan đến kiểm soát truy cập (ví dụ, chỉ chủ sở hữu hợp đồng mới có thể gọi hàm selfdestruct) có thể được viết bằng logic hình thức. Sau đó, thuật toán kiểm tra mô hình có thể xác minh xem hợp đồng có đáp ứng đặc tả hình thức này hay không.
Kiểm tra mô hình sử dụng việc khám phá không gian trạng thái, bao gồm việc xây dựng tất cả các trạng thái có thể của một hợp đồng thông minh và cố gắng tìm ra các trạng thái có thể đạt được dẫn đến vi phạm thuộc tính. Tuy nhiên, điều này có thể dẫn đến một số lượng trạng thái vô hạn (được biết đến như vấn đề “nổ trạng thái”), do đó các bộ kiểm tra mô hình phụ thuộc vào các kỹ thuật trừu tượng để làm cho việc phân tích hiệu quả của hợp đồng thông minh trở nên khả thi.
Chứng minh định lý
Chứng minh định lý là một phương pháp suy luận toán học về tính chính xác của các chương trình, bao gồm cả hợp đồng thông minh. Nó liên quan đến việc chuyển đổi mô hình của hệ thống hợp đồng và các đặc tả của nó thành công thức toán học (câu lệnh logic).
Mục tiêu của việc chứng minh định lý là xác minh sự tương đương logic giữa những câu lệnh này. “Sự tương đương logic” (còn được gọi là “song hành logic”) là một loại mối quan hệ giữa hai câu lệnh sao cho câu lệnh đầu tiên đúng nếu và chỉ nếu câu lệnh thứ hai đúng.
Mối quan hệ cần thiết (tương đương logic) giữa các tuyên bố về mô hình hợp đồng và tính chất của nó được xác định dưới dạng một tuyên bố có thể chứng minh (được gọi là một định lý). Sử dụng hệ thống suy luận hình thức, phần mềm chứng minh định lý tự động có thể xác minh tính hợp lệ của định lý. Nói cách khác, một trình chứng minh định lý có thể chứng minh một cách rõ ràng rằng mô hình của một hợp đồng thông minh khớp hoàn toàn với các thông số của nó.
Trong khi các mô hình kiểm tra mô hình hợp đồng như các hệ thống chuyển tiếp với trạng thái hữu hạn, chứng minh định lý có thể xử lý phân tích các hệ trạng thái vô hạn. Tuy nhiên, điều này có nghĩa là một người chứng minh định lý tự động không phải lúc nào cũng biết liệu một vấn đề logic có thể "quyết định" hay không.
Do đó, thường cần sự hỗ trợ của con người để hướng dẫn trình chứng minh định lý trong việc suy luận về tính chính xác. Việc sử dụng sự cố gắng của con người trong việc chứng minh định lý làm cho nó đắt đỏ hơn việc kiểm tra mô hình, mà hoàn toàn tự động.
Ký hiệu thực thi
Biểu diễn tượng trạng là một phương pháp phân tích hợp đồng thông minh bằng cách thực thi các chức năng bằng các giá trị tượng trưng (ví dụ, x > 5) thay vì giá trị cụ thể (ví dụ, x == 5). Là một kỹ thuật xác minh hình thức, biểu diễn tượng trạng được sử dụng để lập luận một cách hình thức về các thuộc tính cấp dấu vết trong mã của một hợp đồng.
Biểu diễn thực thi biểu thị một dãy thực thi như một công thức toán học trên các giá trị đầu vào biểu tượng, còn được gọi là mệnh đề đường đi. Một Trình giải SMT
được sử dụng để kiểm tra xem một path predicate có “thỏa mãn” không (tức là, có tồn tại một giá trị có thể thỏa mãn công thức). Nếu một path có lỗ hổng là thỏa mãn, trình giải SMT sẽ tạo ra một giá trị cụ thể kích hoạt việc thực thi hướng tới path đó.
Giả sử một hàm của hợp đồng thông minh nhận giá trị uint (x) làm đầu vào và quay lại khi x lớn hơn 5 và cũng nhỏ hơn 10. Tìm một giá trị cho x gây ra lỗi bằng quy trình kiểm thử thông thường sẽ đòi hỏi chạy qua hàng chục trường hợp kiểm thử (hoặc nhiều hơn) mà không có đảm bảo thực sự tìm thấy đầu vào gây ra lỗi.
Ngược lại, một công cụ thực hiện biểu tượng sẽ thực thi hàm với giá trị biểu tượng: X > 5 ∧ X < 10 (tức là x lớn hơn 5 VÀ x nhỏ hơn 10). Câu điều kiện đường đường đi kèm X > 5 ∧ X < 10 sau đó sẽ được đưa cho bộ giải quyết SMT để giải quyết. Nếu một giá trị cụ thể thỏa mãn công thức x = X > 5 ∧ X < 10, bộ giải quyết SMT sẽ tính toán nó - ví dụ, bộ giải quyết có thể tạo ra giá trị 7 cho x.
Vì biểu tượng thực thi phụ thuộc vào đầu vào của chương trình, và tập hợp các đầu vào để khám phá tất cả các trạng thái có thể đạt được là vô hạn, nó vẫn là một dạng kiểm thử. Tuy nhiên, như đã thấy trong ví dụ, biểu tượng thực thi hiệu quả hơn so với kiểm thử thông thường để tìm ra các đầu vào kích hoạt vi phạm tính chất.
Ngoài ra, việc thực hiện biểu tượng tạo ra ít dương tính giả mạo hơn các kỹ thuật dựa trên thuộc tính khác (ví dụ, fuzzing) mà tạo ngẫu nhiên các đầu vào cho một hàm. Nếu trạng thái lỗi được kích hoạt trong quá trình thực hiện biểu tượng, thì có thể tạo ra một giá trị cụ thể kích hoạt lỗi và tái tạo vấn đề.
Việc thực thi biểu tượng cũng có thể cung cấp một số mức độ chứng minh toán học về tính đúng đắn. Xem xét ví dụ sau về một hàm hợp đồng có bảo vệ tràn số: 
Một dãy truy vết thực thi dẫn đến tràn số nguyên sẽ cần phải thỏa mãn công thức: z = x + y VÀ (z >= x) VÀ (z=>y) VÀ (z < x HOẶC z < y) Một công thức như vậy khó có thể giải quyết, do đó nó chứng minh toán học rằng hàm safe_add không bao giờ tràn số.
Tại sao sử dụng xác minh hình thức cho các hợp đồng thông minh?
Nhu cầu về đáng tin cậy
Xác minh hình thức được sử dụng để đánh giá tính chính xác của các hệ thống yêu cầu an toàn mà sự cố có thể có hậu quả tàn khốc, như cái chết, thương tích hoặc tàn phá tài chính. Các hợp đồng thông minh là các ứng dụng có giá trị cao kiểm soát số lượng lớn giá trị, và các lỗi đơn giản trong thiết kế có thể dẫn đếncác khoản thiệt hại không thể khôi phục được cho người dùng
Việc xác minh một hợp đồng một cách chính thức trước khi triển khai, tuy nhiên, có thể tăng cường đảm bảo rằng nó sẽ hoạt động như dự kiến khi chạy trên blockchain.
Đáng tin cậy là một chất lượng rất mong muốn trong bất kỳ hợp đồng thông minh nào, đặc biệt vì mã được triển khai trong Máy Ảo Ethereum (EVM) thường là bất biến. Với việc nâng cấp sau khi ra mắt không dễ dàng tiếp cận, nhu cầu đảm bảo tính đáng tin cậy của các hợp đồng là cần thiết, điều này khiến cho việc xác minh hình thức trở nên cần thiết. Xác minh hình thức có thể phát hiện các vấn đề khó chịu, chẳng hạn như tràn và tràn số nguyên, việc gọi lại, và tối ưu hóa gas kém, các vấn đề này có thể trượt qua các nhà kiểm toán và người kiểm tra.
Chứng minh tính đúng đắn chức năng
Kiểm thử chương trình là phương pháp phổ biến nhất để chứng minh rằng một hợp đồng thông minh đáp ứng một số yêu cầu. Điều này bao gồm việc thực thi một hợp đồng với một mẫu dữ liệu mà nó dự kiến xử lý và phân tích hành vi của nó. Nếu hợp đồng trả về kết quả mong đợi cho dữ liệu mẫu, thì nhà phát triển có bằng chứng khách quan về tính đúng đắn của nó.
Tuy nhiên, phương pháp này không thể chứng minh việc thực thi chính xác cho các giá trị đầu vào không phải là một phần của mẫu. Do đó, việc kiểm thử hợp đồng có thể giúp phát hiện lỗi (tức là nếu một số lối đi mã không trả về kết quả mong muốn trong quá trình thực thi), nhưng không thể chứng minh một cách khách quan sự vắng mặt của lỗi.
Ngược lại, xác minh hình thức có thể chứng minh một cách hình thức rằng một hợp đồng thông minh đáp ứng yêu cầu cho một loạt thực thi vô hạn mà không chạy hợp đồng nào cả. Điều này đòi hỏi tạo ra một đặc tả hình thức mà mô tả chính xác các hành vi hợp đồng đúng và phát triển một mô hình hình thức (toán học) của hệ thống hợp đồng. Sau đó, chúng ta có thể tuân theo một quy trình chứng minh hình thức để kiểm tra tính nhất quán giữa mô hình hợp đồng và đặc tả của nó.
Với xác minh hình thức, vấn đề xác minh xem logic kinh doanh của một hợp đồng có đáp ứng yêu cầu hay không là một mệnh đề toán học có thể được chứng minh hoặc bác bỏ. Bằng cách chứng minh một mệnh đề một cách hình thức, chúng ta có thể xác minh một số lượng vô hạn các trường hợp kiểm tra bằng một số bước hữu hạn. Theo cách này, xác minh hình thức có triển vọng tốt hơn trong việc chứng minh một hợp đồng là chính xác về mặt chức năng so với một đặc tả.
Mục tiêu xác minh lý tưởng
Một mục tiêu xác minh mô tả hệ thống cần được xác minh một cách hình thức. Xác minh hình thức được sử dụng tốt nhất trong “hệ thống nhúng” (những phần mềm nhỏ, đơn giản là một phần của hệ thống lớn hơn). Chúng cũng lý tưởng cho các lĩnh vực chuyên biệt có ít quy tắc, vì điều này làm cho việc sửa đổi công cụ để xác minh các thuộc tính cụ thể của lĩnh vực dễ dàng hơn.
Hợp đồng thông minh — ít nhất là một phần — thỏa mãn cả hai yêu cầu. Ví dụ, kích thước nhỏ của các hợp đồng Ethereum làm cho chúng dễ kiểm tra chính xác. Tương tự, EVM tuân theo các quy tắc đơn giản, điều này làm cho việc chỉ định và xác minh các thuộc tính ngữ nghĩa cho các chương trình chạy trên EVM dễ dàng hơn.
Chu kỳ phát triển nhanh hơn
Các kỹ thuật xác minh hình thức, như kiểm tra mô hình và thực thi biểu tượng, thường hiệu quả hơn so với phân tích thông thường của mã hợp đồng thông minh (thực hiện trong quá trình kiểm thử hoặc kiểm toán). Điều này bởi vì xác minh hình thức dựa vào các giá trị biểu tượng để kiểm tra các khẳng định (''thử xem người dùng có thử rút n ether không?'') khác với kiểm thử sử dụng các giá trị cụ thể (''thử xem người dùng có thử rút 5 ether không?'').
Các biến đầu vào tượng trưng có thể bao gồm nhiều lớp giá trị cụ thể, vì vậy các phương pháp xác minh hình thức hứa hẹn việc phủ sóng mã hơn trong khoảng thời gian ngắn hơn. Khi sử dụng một cách hiệu quả, xác minh hình thức có thể tăng tốc chu kỳ phát triển cho các nhà phát triển.
Xác minh chính thức cũng cải thiện quy trình xây dựng ứng dụng phi tập trung (dapps) bằng cách giảm thiểu các lỗi thiết kế đắt tiền. Nâng cấp các hợp đồng (nếu có thể) để sửa các lỗ hổng đòi hỏi việc viết lại mã nguồn một cách mở rộng và tốn nhiều công sức hơn trong quá trình phát triển. Xác minh chính thức có thể phát hiện nhiều lỗi trong việc triển khai hợp đồng mà có thể trượt qua các bài kiểm tra và kiểm toán viên và cung cấp cơ hội đáng kể để sửa chữa những vấn đề đó trước khi triển khai một hợp đồng.
NHƯỢC ĐIỂM CỦA XÁC MINH FORMAL
Chi phí lao động thủ công
Xác minh chính thức, đặc biệt là xác minh bán tự động trong đó con người hướng dẫn bằng chứng để suy luận chính xác, đòi hỏi một lượng lao động thủ công đáng kể. Hơn nữa, việc tạo ra đặc tả chính thức là một hoạt động phức tạp đòi hỏi một mức độ kỹ năng cao.
Những yếu tố này (cố gắng và kỹ năng) làm cho xác minh hình thức trở nên đòi hỏi và đắt đỏ hơn so với các phương pháp thông thường để đánh giá tính chính xác trong các hợp đồng, chẳng hạn như kiểm thử và kiểm toán. Tuy nhiên, việc trả giá cho một cuộc kiểm toán xác minh đầy đủ là hợp lý, xét đến chi phí của lỗi trong việc triển khai hợp đồng thông minh.
Kết quả âm
Xác minh chính thức chỉ có thể kiểm tra xem việc thực thi của hợp đồng thông minh có khớp với đặc tả chính thức hay không. Do đó, quan trọng là đảm bảo rằng đặc tả mô tả đúng các hành vi dự kiến của một hợp đồng thông minh.
Nếu các đặc tả được viết kém, vi phạm các thuộc tính—điều chỉ ra các thực thi dễ bị tổn thương—không thể được phát hiện bởi cuộc kiểm tra xác thực hình thức. Trong trường hợp này, một nhà phát triển có thể vô tình giả định rằng hợp đồng không có lỗi.
Vấn đề hiệu suất
Xác minh hình thức gặp phải một số vấn đề về hiệu suất. Ví dụ, các vấn đề về mở rộng trạng thái và đường dẫn gặp phải trong quá trình kiểm tra mô hình và kiểm tra biểu tượng, có thể ảnh hưởng đến các thủ tục xác minh. Ngoài ra, các công cụ xác minh hình thức thường sử dụng trình giải SMT và các trình giải ràng buộc khác trong lớp cơ bản của họ và các trình giải này dựa vào các thủ tục tính toán mất nhiều công suất tính toán.
Ngoài ra, đôi khi không thể xác định được nếu các bộ xác nhận chương trình có thể xác định xem một thuộc tính (được mô tả dưới dạng một công thức logic) có thể được thỏa mãn hay không (câu lệnhvấn đề quyết định
“) bởi vì một chương trình có thể không bao giờ kết thúc. Do đó, có thể là không thể chứng minh một số thuộc tính cho một hợp đồng ngay cả khi nó được xác định rõ ràng.”
CÔNG CỤ XÁC MINH FORMAL CHO HỢP ĐỒNG THÔNG MINH ETHEREUM
Ngôn ngữ đặc tả để tạo đặc tả hình thức
Act: Act cho phép xác định cập nhật lưu trữ, điều kiện trước/sau và hợp đồng bằng chứng minh. Bộ công cụ của nó cũng có công cụ chứng minh công cộ có thể chứng minh nhiều thuộc tính qua Coq, các bác giải SMT, hoặc hevm.
Scribble - Scribble chuyển đổi các chú thích mã trong ngôn ngữ đặc tả Scribble thành các khẳng định cụ thể kiểm tra đặc tả.
Dafny - Dafny là một ngôn ngữ lập trình sẵn sàng kiểm tra dựa vào các chú thích cấp cao để suy luận và chứng minh tính đúng đắn của mã.
Chương trình kiểm tra viên để kiểm tra tính chính xác
Certora Prover - Certora Prover là một công cụ xác minh hình thức tự động để kiểm tra tính chính xác của mã trong hợp đồng thông minh. Các thông số được viết bằng CVL (Ngôn ngữ Xác minh Certora), với vi phạm tính chất được phát hiện bằng cách kết hợp phân tích tĩnh và giải quyết ràng buộc.
Kiểm tra SMT của Solidity - SMTChecker của Solidity là một công cụ kiểm tra mô hình tích hợp dựa trên SMT (Satisfiability Modulo Theories) và giải quyết Horn. Nó xác nhận nếu mã nguồn hợp đồng khớp với các thông số kỹ thuật trong quá trình biên dịch và kiểm tra tĩnh để phát hiện vi phạm các tính chất an toàn.
solc-verify - solc-verify là một phiên bản mở rộng của trình biên dịch Solidity có thể thực hiện xác minh hình thức tự động trên mã Solidity bằng cách sử dụng chú thích và xác minh chương trình modul.
KEVM - KEVM là một ngữ nghĩa hình thức của Máy Ảo Ethereum (EVM) được viết trong K framework. KEVM có thể thực thi và chứng minh một số tuyên bố liên quan đến tính chất bằng cách sử dụng logic đạt được.
Kerangka logic cho chứng minh định lý
Isabelle - Isabelle/HOL là một trợ lý chứng minh cho phép các công thức toán học được diễn đạt bằng ngôn ngữ hình thức và cung cấp các công cụ để chứng minh những công thức đó. Ứng dụng chính là hình thức hóa chứng minh toán học và đặc biệt là xác minh hình thức, bao gồm chứng minh tính chính xác của phần cứng hoặc phần mềm máy tính và chứng minh các tính chất của ngôn ngữ và giao thức máy tính.
Coq - Coq là một công cụ chứng minh định lý tương tác cho phép bạn xác định các chương trình bằng cách sử dụng các định lý và tương tác để tạo ra các bằng chứng kiểm tra máy tính về tính chính xác.
Công cụ dựa trên thực thi biểu tượng để phát hiện mẫu dễ bị tổn thương trong hợp đồng thông minh
Manticore - Một công cụ để phân tích mã bytecode EVM dựa trên việc thực hiện biểu tượng.
hevm - hevm là một công cụ thực thi biểu tượng và kiểm tra tính tương đương cho bytecode EVM.
Mythril - Một công cụ thực thi tượng trưng để phát hiện lỗ hổng trong các hợp đồng thông minh Ethereum
免責聲明：
- Bài viết này được in lại từ []. Tất cả bản quyền thuộc về tác giả gốc [**]. Nếu có bất kỳ ý kiến phản đối nào về việc tái in này, vui lòng liên hệ với Cổng Họcđội ngũ và họ sẽ xử lý nhanh chóng.
- Tuyên bố từ chối trách nhiệm: Các quan điểm và ý kiến được thể hiện trong bài viết này chỉ là của tác giả và không đại diện cho bất kỳ lời khuyên đầu tư nào.
- Việc dịch bài báo ra các ngôn ngữ khác được thực hiện bởi nhóm Gate Learn. Trừ khi được nêu ra, việc sao chép, phân phối hoặc đạo văn các bài báo dịch là không được phép.
Artikel terkait
MakerDAO: DAPP "điên rồ nhất" của Ethereum
Hướng dẫn cách chuyển mạng trong MetaMask
Ethereum 2.0 là gì? Hiểu sự hợp nhất
XÁC THỰC FORMAL CỦA HỢP ĐỒNG THÔNG MINH
XÁC MINH CHÍNH THỨC LÀ GÌ?
CÁC LOẠI ĐỊNH DẠNG FORMAL CHO HỢP ĐỒNG THÔNG MINH
KỸ THUẬT XÁC THỰC FORMAL CỦA HỢP ĐỒNG THÔNG MINH
NHƯỢC ĐIỂM CỦA XÁC NHẬN FORMAL
CÔNG CỤ XÁC THỰC FORMAL CHO HỢP ĐỒNG THÔNG MINH ETHEREUM
Hợp đồng thông minhđang làm cho việc tạo ra ứng dụng phi tín nhiệm, phi tập trung và mạnh mẽ trở nên khả thi, giới thiệu các trường hợp sử dụng mới và mở khóa giá trị cho người dùng. Bởi vì hợp đồng thông minh xử lý một lượng lớn giá trị, an ninh là một yếu tố quan trọng đối với các nhà phát triển.
Xác minh hình thức là một trong các kỹ thuật được khuyến nghị để cải thiện an toàn hợp đồng thông minh. Xác minh hình thức, sử dụng phương pháp hình thức
được sử dụng từ nhiều năm để xác định, thiết kế và xác minh các chương trình, để đảm bảo tính chính xác của các hệ thống phần cứng và phần mềm quan trọng.
Khi được triển khai trong các hợp đồng thông minh, xác minh hình thức có thể chứng minh logic kinh doanh của một hợp đồng đáp ứng một số quy định cụ thể. So với các phương pháp khác để đánh giá tính đúng đắn của mã hợp đồng, chẳng hạn như kiểm thử, xác minh hình thức đưa ra các cam kết mạnh mẽ hơn rằng một hợp đồng thông minh là chính xác về mặt chức năng.
FORMAL VERIFICATION LÀ GÌ?
Xác minh hình thức đề cập đến quá trình đánh giá tính chính xác của hệ thống so với một đặc tả hình thức. Nói một cách đơn giản, xác minh hình thức cho phép chúng ta kiểm tra xem hành vi của hệ thống có đáp ứng một số yêu cầu hay không (tức là, nó hoạt động theo như chúng ta mong muốn).
Các hành vi dự kiến của hệ thống (một hợp đồng thông minh trong trường hợp này) được mô tả bằng mô hình hình thức, trong khi ngôn ngữ đặc tả cho phép tạo ra các thuộc tính hình thức. Các kỹ thuật xác minh hình thức sau đó có thể xác minh rằng việc triển khai của một hợp đồng tuân thủ với đặc tả của nó và rút ra chứng minh toán học về tính đúng đắn của hợp đồng đó. Khi một hợp đồng đáp ứng đặc tả của nó, nó được mô tả là “chính xác về chức năng”, “chính xác theo thiết kế”, hoặc “chính xác theo công trình”.
Mô hình hình thức là gì?
Trong khoa học máy tính, một mô hình chính thức
là mô tả toán học của một quy trình tính toán. Các chương trình được trừu tượng hóa thành các hàm toán học (phương trình), với mô hình mô tả cách tính các đầu ra cho các hàm được tính toán với một đầu vào.
Mô hình hình thức cung cấp một mức độ trừu tượng mà qua đó phân tích hành vi của chương trình có thể được đánh giá. Sự tồn tại của mô hình hình thức cho phép tạo ra một đặc tả hình thức, mô tả các thuộc tính mong muốn của mô hình cụ thể.
Các kỹ thuật khác nhau được sử dụng để mô hình hóa hợp đồng thông minh để xác minh hình thức. Ví dụ, một số mô hình được sử dụng để suy luận về hành vi cấp cao của một hợp đồng thông minh. Các kỹ thuật mô hình hóa này áp dụng một quan điểm hộp đen cho các hợp đồng thông minh, xem chúng như các hệ thống chấp nhận đầu vào và thực thi tính toán dựa trên các đầu vào đó.
Các mô hình cấp cao tập trung vào mối quan hệ giữa hợp đồng thông minh và các tác nhân bên ngoài, như tài khoản sở hữu bên ngoài (EOAs), tài khoản hợp đồng và môi trường blockchain. Những mô hình như vậy hữu ích để xác định các thuộc tính mô tả cách mà một hợp đồng nên hoạt động khi phản ứng với một số tương tác của người dùng nhất định.
Ngược lại, mô hình hình thức khác tập trung vào hành vi cấp thấp của một hợp đồng thông minh. Trong khi mô hình cấp cao có thể giúp trong việc suy luận về chức năng của một hợp đồng, chúng có thể không thể nắm bắt được chi tiết về cách hoạt động bên trong của việc triển khai. Các mô hình cấp thấp áp dụng quan điểm hộp trắng cho phân tích chương trình và phụ thuộc vào các biểu diễn cấp thấp hơn của các ứng dụng hợp đồng thông minh, như dấu vết chương trình và đồ thị luồng điều khiển
, để suy luận về các thuộc tính liên quan đến việc thực hiện hợp đồng.
Mô hình cấp thấp được coi là lý tưởng vì chúng đại diện cho việc thực thi thực tế của một hợp đồng thông minh trong môi trường thực thi của Ethereum (tức là,EVMCác kỹ thuật mô hình hóa cấp thấp đặc biệt hữu ích trong việc xác định các thuộc tính an toàn quan trọng trong hợp đồng thông minh và phát hiện các lỗ hổng tiềm năng.
Formal specification là gì?
Một đặc tả đơn giản chỉ là yêu cầu kỹ thuật mà một hệ thống cụ thể phải đáp ứng. Trong lập trình, các đặc tả đại diện cho các ý tưởng chung về việc thực hiện chương trình (tức là, chương trình nên làm gì).
Trong ngữ cảnh của hợp đồng thông minh, các đặc tả hình thức đề cập đến các thuộc tính—mô tả hình thức của các yêu cầu mà một hợp đồng phải thỏa mãn. Các thuộc tính như vậy được mô tả là “bất biến” và đại diện cho những khẳng định logic về việc thực thi của một hợp đồng mà phải luôn đúng trong mọi trường hợp có thể xảy ra, mà không có bất kỳ ngoại lệ nào.
Do đó, chúng ta có thể coi một đặc tả hình thức là một tập hợp các câu lệnh được viết bằng một ngôn ngữ hình thức mô tả việc thực thi dự định của một hợp đồng thông minh. Đặc tả bao gồm các thuộc tính của một hợp đồng và xác định cách mà hợp đồng nên hoạt động trong các hoàn cảnh khác nhau. Mục đích của việc xác minh hình thức là để xác định xem một hợp đồng thông minh có sở hữu những thuộc tính này (các không đổi) và rằng những thuộc tính này không bị vi phạm trong quá trình thực thi.
Các đặc tả chính thức rất quan trọng trong việc phát triển các triển khai an toàn của hợp đồng thông minh. Các hợp đồng mà không thực hiện được những biến invariants hoặc có các thuộc tính của họ bị vi phạm trong quá trình thực thi có thể dễ bị tổn thương chức năng hoặc gây ra lỗ hổng độc hại.
CÁC LOẠI ĐỊNH DẠNG FORMAL CHO HỢP ĐỒNG THÔNG MINH
Các đặc tả chính thức cho phép lập luận toán học về tính đúng đắn của việc thực thi chương trình. Giống như các mô hình chính thức, các đặc tả chính thức có thể bắt kịp các thuộc tính ở mức cao hoặc hành vi ở mức thấp của việc thực thi hợp đồng.
Các thông số chính thức được tạo ra bằng cách sử dụng các yếu tố củalogic chương trình
, cho phép lý luận hình thức về các tính chất của một chương trình. Một logic chương trình có các quy tắc hình thức biểu diễn (bằng ngôn ngữ toán học) hành vi dự kiến của một chương trình. Các logic chương trình khác nhau được sử dụng trong việc tạo ra các thông số kỹ thuật hình thức, bao gồm lô-gic khả năng tiếp cận
và Hoare logic
Các đặc tả chính thức cho hợp đồng thông minh có thể được phân loại rộng rãi là đặc tả cấp cao hoặc đặc tả cấp thấp. Bất kể đặc tả thuộc loại nào, nó phải mô tả đầy đủ và không gây hiểu lầm về thuộc tính của hệ thống đang được phân tích.
Đặc tả cấp cao
Như tên cho thấy, một đặc tả cấp cao (còn được gọi là "đặc tả hướng mô hình") mô tả hành vi cấp cao của một chương trình. Thông số kỹ thuật cấp cao mô hình hợp đồng thông minh dưới dạng máy trạng thái hữu hạn
(FSM), mà có thể chuyển tiếp giữa các trạng thái bằng cách thực hiện các hoạt động, với logic thời gian được sử dụng để xác định các tính chất hình thức cho mô hình FSM.
là “các quy tắc để suy luận về các mệnh đề được xác định theo thời gian (ví dụ, “Tôi luôn đói” hoặc “Cuối cùng tôi sẽ đói”).” Khi áp dụng vào xác minh hình thức, logic thời gian được sử dụng để nêu các khẳng định về hành vi chính xác của các hệ thống được mô hình hóa như các máy trạng thái. Cụ thể, logic thời gian mô tả các trạng thái tương lai mà một hợp đồng thông minh có thể ở và cách nó chuyển đổi giữa các trạng thái.
Các đặc tả cấp cao thường bao gồm hai tính chất thời gian quan trọng cho hợp đồng thông minh: an toàn và sống động. Các tính chất an toàn đại diện cho ý tưởng rằng “không bao giờ xảy ra điều xấu” và thường biểu diễn tính không biến đổi. Một tính chất an toàn có thể định nghĩa các yêu cầu phần mềm chung, chẳng hạn như sự tự do khỏideadlock
, hoặc biểu diễn các tính chất cụ thể cho hợp đồng (ví dụ, điều kiện không thay đổi về kiểm soát truy cập cho các chức năng, các giá trị cho phép của biến trạng thái, hoặc điều kiện cho việc chuyển token).
Ví dụ, yêu cầu an toàn này bao gồm các điều kiện sử dụng transfer() hoặc transferFrom() trong các hợp đồng token ERC-20: “Số dư của người gửi không bao giờ thấp hơn số lượng token được yêu cầu gửi đi.”. Mô tả ngôn ngữ tự nhiên này về một hằng số hợp đồng có thể được dịch thành một đặc tả (toán học) chính thức, sau đó có thể được kiểm tra một cách nghiêm ngặt để xác thực.
Thuộc tính liveness khẳng định rằng “cuối cùng sẽ xảy ra điều tốt” và liên quan đến khả năng của hợp đồng để tiến triển qua các trạng thái khác nhau. Một ví dụ về thuộc tính liveness là “thuận lợi về thanh khoản”, đề cập đến khả năng của một hợp đồng để chuyển số dư của mình cho người dùng khi được yêu cầu. Nếu thuộc tính này bị vi phạm, người dùng sẽ không thể rút ra tài sản được lưu trữ trong hợp đồng, giống như điều đã xảy ra với Sự cố ví Parity
.
Thông số cấp thấp
Các đặc tả cấp cao lấy mô hình trạng thái hữu hạn của hợp đồng làm điểm khởi đầu và xác định các thuộc tính mong muốn của mô hình này. Ngược lại, các đặc tả cấp thấp (còn được gọi là 'đặc tả hướng thuộc tính') thường mô hình các chương trình (hợp đồng thông minh) như các hệ thống bao gồm một bộ sưu tập các hàm toán học và mô tả hành vi chính xác của các hệ thống đó.
Nói một cách đơn giản hơn, các thông số kỹ thuật cấp thấp phân tích dấu vết chương trình và cố gắng xác định các thuộc tính của hợp đồng thông minh trên các dấu vết này. Dấu vết đề cập đến chuỗi thực thi chức năng làm thay đổi trạng thái của hợp đồng thông minh; Do đó, các thông số kỹ thuật cấp thấp giúp xác định các yêu cầu đối với việc thực hiện nội bộ của hợp đồng.
Các đặc tả hình thức cấp thấp có thể được xác định dưới dạng các thuộc tính kiểu Hoare hoặc các điều kiện không đổi trên đường đi thực thi.
Các tính chất theo phong cách Hoare
cung cấp một bộ quy tắc hình thức để suy luận về tính chính xác của các chương trình, bao gồm các hợp đồng thông minh. Một thuộc tính kiểu Hoare được biểu diễn bằng một ba Hoare {P}c{Q}, trong đó c là một chương trình và P và Q là các mệnh đề về trạng thái của c (tức là chương trình), được mô tả một cách hình thức như các điều kiện tiên quyết và điều kiện hậu quả, tương ứng.
Một điều kiện tiên điều là một mệnh đề mô tả các điều kiện cần thiết cho việc thực thi đúng của một hàm; người dùng gọi vào hợp đồng phải đáp ứng yêu cầu này. Một điều kiện hậu điều là một mệnh đề mô tả điều kiện mà một hàm thiết lập nếu được thực thi đúng; người dùng có thể mong đợi điều kiện này là đúng sau khi gọi vào hàm. Một biến không đổi trong logic Hoare là một mệnh đề được bảo tồn bởi việc thực thi của một hàm (tức là, nó không thay đổi).
Các thông số kiểu Hoare có thể đảm bảo tính đúng đắn một phần hoặc hoàn toàn. Việc triển khai của một hàm hợp đồng được coi là "một phần đúng" nếu điều kiện tiên quyết đúng trước khi hàm được thực thi, và nếu thực thi kết thúc, điều kiện hậu quả cũng đúng. Chứng minh tính đúng đắn hoàn toàn được đạt được nếu điều kiện tiên quyết đúng trước khi hàm thực thi, thực thi được đảm bảo kết thúc và khi thực thi kết thúc, điều kiện hậu quả cũng đúng.
Việc chứng minh tính đúng đắn hoàn toàn khó khăn vì một số thực thi có thể trì hoãn trước khi kết thúc, hoặc thậm chí không bao giờ kết thúc. Tuy nhiên, việc thực thi có kết thúc hay không có thể coi là vấn đề không đáng kể khi cơ chế gas của Ethereum ngăn chặn vòng lặp chương trình vô hạn (thực thi kết thúc thành công hoặc kết thúc do lỗi 'hết gas').
Các đặc tả hợp đồng thông minh được tạo ra bằng logic Hoare sẽ có các tiền điều kiện, hậu điều kiện và không biến được xác định cho việc thực thi các hàm và vòng lặp trong một hợp đồng. Tiền điều kiện thường bao gồm khả năng nhập không chính xác vào một hàm, trong khi hậu điều kiện mô tả phản hồi dự kiến cho các đầu vào đó (ví dụ, ném một ngoại lệ cụ thể). Theo cách này, các thuộc tính theo phong cách Hoare là hiệu quả để đảm bảo tính chính xác của việc triển khai hợp đồng.
Nhiều khung xác minh chính thức sử dụng các thông số kỹ thuật kiểu Hoare để chứng minh tính đúng đắn ngữ nghĩa của các hàm. Cũng có thể thêm các thuộc tính kiểu Hoare (dưới dạng khẳng định) trực tiếp vào mã hợp đồng bằng cách sử dụng các câu lệnh require và assert trong Solidity.
Các câu lệnh yêu cầu biểu thị một điều kiện tiên quyết hoặc bất biến và thường được sử dụng để xác minh đầu vào của người dùng, trong khi assert ghi lại một hậu điều kiện cần thiết cho an toàn. Ví dụ, kiểm soát truy cập đúng đắn cho các chức năng (một ví dụ về thuộc tính an toàn) có thể được đạt được bằng cách sử dụng require như một kiểm tra tiên quyết về danh tính của tài khoản gọi. Tương tự, một bất biến về các giá trị cho phép của biến trạng thái trong một hợp đồng (ví dụ, tổng số token trong lưu thông) có thể được bảo vệ khỏi vi phạm bằng cách sử dụng assert để xác nhận trạng thái của hợp đồng sau khi thực thi chức năng.
Thuộc tính cấp Trace
Các mô tả dựa trên dấu vết mô tả các hoạt động chuyển đổi hợp đồng giữa các trạng thái khác nhau và mối quan hệ giữa các hoạt động này. Như đã giải thích trước đó, các dấu vết là chuỗi các hoạt động thay đổi trạng thái của một hợp đồng theo cách cụ thể.
Phương pháp này phụ thuộc vào mô hình hợp đồng thông minh như các hệ thống chuyển trạng thái với một số trạng thái được xác định trước (mô tả bởi biến trạng thái) cùng với một tập hợp các chuyển trạng thái được xác định trước (mô tả bởi các chức năng hợp đồng). Hơn nữa, một biểu đồ luồng điều khiển
(CFG), đây là biểu diễn đồ họa của luồng thực thi chương trình, thường được sử dụng để mô tả ngữ nghĩa vận hành của một hợp đồng. Ở đây, mỗi dấu vết được biểu diễn dưới dạng một đường đi trên đồ thị luồng điều khiển.
Đầu tiên, các thông số cấp độ theo dõi được sử dụng để suy luận về các mẫu thực thi nội bộ trong hợp đồng thông minh. Bằng cách tạo các thông số cấp độ theo dõi, chúng ta khẳng định các đường đi thực thi cho phép (tức là, các chuyển đổi trạng thái) cho một hợp đồng thông minh. Sử dụng các kỹ thuật, như thực thi tượng trưng, chúng ta có thể xác minh hình thức rằng thực thi không bao giờ đi theo một đường không được xác định trong mô hình hình thức.
Hãy sử dụng một ví dụ về một DAOhợp đồng có một số chức năng có thể truy cập công khai để mô tả các thuộc tính cấp độ theo dõi. Ở đây, chúng ta giả định hợp đồng DAO cho phép người dùng thực hiện các hoạt động sau:
- Nạp tiền
- Bỏ phiếu cho một đề xuất sau khi gửi tiền
- Yêu cầu hoàn tiền nếu họ không bỏ phiếu cho một đề xuất
Các thuộc tính cấp độ theo dõi ví dụ có thể là “người dùng không nạp tiền không thể bỏ phiếu cho một đề xuất” hoặc “người dùng không bỏ phiếu cho một đề xuất luôn luôn có thể yêu cầu hoàn tiền”. Cả hai thuộc tính này khẳng định các chuỗi thực thi ưa thích (việc bỏ phiếu không thể xảy ra trước khi nạp tiền và việc yêu cầu hoàn tiền không thể xảy ra sau khi bỏ phiếu cho một đề xuất).
CÁC KỸ THUẬT CHO VIỆC XÁC MINH FORMAL CỦA HỢP ĐỒNG THÔNG MINH
Kiểm tra mô hình
Kiểm tra mô hình là một kỹ thuật xác minh hình thức trong đó một thuật toán kiểm tra một mô hình hình thức của một hợp đồng thông minh đối với đặc tả của nó. Trong kiểm tra mô hình, các hợp đồng thông minh thường được biểu diễn dưới dạng hệ thống chuyển trạng thái, trong khi các thuộc tính trên các trạng thái hợp đồng cho phép được xác định bằng logic thời gian.
Kiểm tra mô hình đòi hỏi tạo ra một biểu diễn toán học trừu tượng của một hệ thống (tức là một hợp đồng) và diễn đạt các tính chất của hệ thống này bằng các công thức gốc trong logic hồi quy
Điều này giúp đơn giản hóa công việc của thuật toán kiểm tra mô hình, cụ thể là chứng minh rằng một mô hình toán học thỏa mãn một công thức logic đã cho.
Kiểm tra mô hình trong xác minh hình thức chủ yếu được sử dụng để đánh giá các thuộc tính thời gian mô tả hành vi của một hợp đồng theo thời gian. Các thuộc tính thời gian cho hợp đồng thông minh bao gồm an toàn và sự sống còn, mà chúng tôi đã giải thích trước đó.
Ví dụ, một thuộc tính bảo mật liên quan đến kiểm soát truy cập (ví dụ, chỉ chủ sở hữu hợp đồng mới có thể gọi hàm selfdestruct) có thể được viết bằng logic hình thức. Sau đó, thuật toán kiểm tra mô hình có thể xác minh xem hợp đồng có đáp ứng đặc tả hình thức này hay không.
Kiểm tra mô hình sử dụng việc khám phá không gian trạng thái, bao gồm việc xây dựng tất cả các trạng thái có thể của một hợp đồng thông minh và cố gắng tìm ra các trạng thái có thể đạt được dẫn đến vi phạm thuộc tính. Tuy nhiên, điều này có thể dẫn đến một số lượng trạng thái vô hạn (được biết đến như vấn đề “nổ trạng thái”), do đó các bộ kiểm tra mô hình phụ thuộc vào các kỹ thuật trừu tượng để làm cho việc phân tích hiệu quả của hợp đồng thông minh trở nên khả thi.
Chứng minh định lý
Chứng minh định lý là một phương pháp suy luận toán học về tính chính xác của các chương trình, bao gồm cả hợp đồng thông minh. Nó liên quan đến việc chuyển đổi mô hình của hệ thống hợp đồng và các đặc tả của nó thành công thức toán học (câu lệnh logic).
Mục tiêu của việc chứng minh định lý là xác minh sự tương đương logic giữa những câu lệnh này. “Sự tương đương logic” (còn được gọi là “song hành logic”) là một loại mối quan hệ giữa hai câu lệnh sao cho câu lệnh đầu tiên đúng nếu và chỉ nếu câu lệnh thứ hai đúng.
Mối quan hệ cần thiết (tương đương logic) giữa các tuyên bố về mô hình hợp đồng và tính chất của nó được xác định dưới dạng một tuyên bố có thể chứng minh (được gọi là một định lý). Sử dụng hệ thống suy luận hình thức, phần mềm chứng minh định lý tự động có thể xác minh tính hợp lệ của định lý. Nói cách khác, một trình chứng minh định lý có thể chứng minh một cách rõ ràng rằng mô hình của một hợp đồng thông minh khớp hoàn toàn với các thông số của nó.
Trong khi các mô hình kiểm tra mô hình hợp đồng như các hệ thống chuyển tiếp với trạng thái hữu hạn, chứng minh định lý có thể xử lý phân tích các hệ trạng thái vô hạn. Tuy nhiên, điều này có nghĩa là một người chứng minh định lý tự động không phải lúc nào cũng biết liệu một vấn đề logic có thể "quyết định" hay không.
Do đó, thường cần sự hỗ trợ của con người để hướng dẫn trình chứng minh định lý trong việc suy luận về tính chính xác. Việc sử dụng sự cố gắng của con người trong việc chứng minh định lý làm cho nó đắt đỏ hơn việc kiểm tra mô hình, mà hoàn toàn tự động.
Ký hiệu thực thi
Biểu diễn tượng trạng là một phương pháp phân tích hợp đồng thông minh bằng cách thực thi các chức năng bằng các giá trị tượng trưng (ví dụ, x > 5) thay vì giá trị cụ thể (ví dụ, x == 5). Là một kỹ thuật xác minh hình thức, biểu diễn tượng trạng được sử dụng để lập luận một cách hình thức về các thuộc tính cấp dấu vết trong mã của một hợp đồng.
Biểu diễn thực thi biểu thị một dãy thực thi như một công thức toán học trên các giá trị đầu vào biểu tượng, còn được gọi là mệnh đề đường đi. Một Trình giải SMT
được sử dụng để kiểm tra xem một path predicate có “thỏa mãn” không (tức là, có tồn tại một giá trị có thể thỏa mãn công thức). Nếu một path có lỗ hổng là thỏa mãn, trình giải SMT sẽ tạo ra một giá trị cụ thể kích hoạt việc thực thi hướng tới path đó.
Giả sử một hàm của hợp đồng thông minh nhận giá trị uint (x) làm đầu vào và quay lại khi x lớn hơn 5 và cũng nhỏ hơn 10. Tìm một giá trị cho x gây ra lỗi bằng quy trình kiểm thử thông thường sẽ đòi hỏi chạy qua hàng chục trường hợp kiểm thử (hoặc nhiều hơn) mà không có đảm bảo thực sự tìm thấy đầu vào gây ra lỗi.
Ngược lại, một công cụ thực hiện biểu tượng sẽ thực thi hàm với giá trị biểu tượng: X > 5 ∧ X < 10 (tức là x lớn hơn 5 VÀ x nhỏ hơn 10). Câu điều kiện đường đường đi kèm X > 5 ∧ X < 10 sau đó sẽ được đưa cho bộ giải quyết SMT để giải quyết. Nếu một giá trị cụ thể thỏa mãn công thức x = X > 5 ∧ X < 10, bộ giải quyết SMT sẽ tính toán nó - ví dụ, bộ giải quyết có thể tạo ra giá trị 7 cho x.
Vì biểu tượng thực thi phụ thuộc vào đầu vào của chương trình, và tập hợp các đầu vào để khám phá tất cả các trạng thái có thể đạt được là vô hạn, nó vẫn là một dạng kiểm thử. Tuy nhiên, như đã thấy trong ví dụ, biểu tượng thực thi hiệu quả hơn so với kiểm thử thông thường để tìm ra các đầu vào kích hoạt vi phạm tính chất.
Ngoài ra, việc thực hiện biểu tượng tạo ra ít dương tính giả mạo hơn các kỹ thuật dựa trên thuộc tính khác (ví dụ, fuzzing) mà tạo ngẫu nhiên các đầu vào cho một hàm. Nếu trạng thái lỗi được kích hoạt trong quá trình thực hiện biểu tượng, thì có thể tạo ra một giá trị cụ thể kích hoạt lỗi và tái tạo vấn đề.
Việc thực thi biểu tượng cũng có thể cung cấp một số mức độ chứng minh toán học về tính đúng đắn. Xem xét ví dụ sau về một hàm hợp đồng có bảo vệ tràn số:
Một dãy truy vết thực thi dẫn đến tràn số nguyên sẽ cần phải thỏa mãn công thức: z = x + y VÀ (z >= x) VÀ (z=>y) VÀ (z < x HOẶC z < y) Một công thức như vậy khó có thể giải quyết, do đó nó chứng minh toán học rằng hàm safe_add không bao giờ tràn số.
Tại sao sử dụng xác minh hình thức cho các hợp đồng thông minh?
Nhu cầu về đáng tin cậy
Xác minh hình thức được sử dụng để đánh giá tính chính xác của các hệ thống yêu cầu an toàn mà sự cố có thể có hậu quả tàn khốc, như cái chết, thương tích hoặc tàn phá tài chính. Các hợp đồng thông minh là các ứng dụng có giá trị cao kiểm soát số lượng lớn giá trị, và các lỗi đơn giản trong thiết kế có thể dẫn đếncác khoản thiệt hại không thể khôi phục được cho người dùng
Việc xác minh một hợp đồng một cách chính thức trước khi triển khai, tuy nhiên, có thể tăng cường đảm bảo rằng nó sẽ hoạt động như dự kiến khi chạy trên blockchain.
Đáng tin cậy là một chất lượng rất mong muốn trong bất kỳ hợp đồng thông minh nào, đặc biệt vì mã được triển khai trong Máy Ảo Ethereum (EVM) thường là bất biến. Với việc nâng cấp sau khi ra mắt không dễ dàng tiếp cận, nhu cầu đảm bảo tính đáng tin cậy của các hợp đồng là cần thiết, điều này khiến cho việc xác minh hình thức trở nên cần thiết. Xác minh hình thức có thể phát hiện các vấn đề khó chịu, chẳng hạn như tràn và tràn số nguyên, việc gọi lại, và tối ưu hóa gas kém, các vấn đề này có thể trượt qua các nhà kiểm toán và người kiểm tra.
Chứng minh tính đúng đắn chức năng
Kiểm thử chương trình là phương pháp phổ biến nhất để chứng minh rằng một hợp đồng thông minh đáp ứng một số yêu cầu. Điều này bao gồm việc thực thi một hợp đồng với một mẫu dữ liệu mà nó dự kiến xử lý và phân tích hành vi của nó. Nếu hợp đồng trả về kết quả mong đợi cho dữ liệu mẫu, thì nhà phát triển có bằng chứng khách quan về tính đúng đắn của nó.
Tuy nhiên, phương pháp này không thể chứng minh việc thực thi chính xác cho các giá trị đầu vào không phải là một phần của mẫu. Do đó, việc kiểm thử hợp đồng có thể giúp phát hiện lỗi (tức là nếu một số lối đi mã không trả về kết quả mong muốn trong quá trình thực thi), nhưng không thể chứng minh một cách khách quan sự vắng mặt của lỗi.
Ngược lại, xác minh hình thức có thể chứng minh một cách hình thức rằng một hợp đồng thông minh đáp ứng yêu cầu cho một loạt thực thi vô hạn mà không chạy hợp đồng nào cả. Điều này đòi hỏi tạo ra một đặc tả hình thức mà mô tả chính xác các hành vi hợp đồng đúng và phát triển một mô hình hình thức (toán học) của hệ thống hợp đồng. Sau đó, chúng ta có thể tuân theo một quy trình chứng minh hình thức để kiểm tra tính nhất quán giữa mô hình hợp đồng và đặc tả của nó.
Với xác minh hình thức, vấn đề xác minh xem logic kinh doanh của một hợp đồng có đáp ứng yêu cầu hay không là một mệnh đề toán học có thể được chứng minh hoặc bác bỏ. Bằng cách chứng minh một mệnh đề một cách hình thức, chúng ta có thể xác minh một số lượng vô hạn các trường hợp kiểm tra bằng một số bước hữu hạn. Theo cách này, xác minh hình thức có triển vọng tốt hơn trong việc chứng minh một hợp đồng là chính xác về mặt chức năng so với một đặc tả.
Mục tiêu xác minh lý tưởng
Một mục tiêu xác minh mô tả hệ thống cần được xác minh một cách hình thức. Xác minh hình thức được sử dụng tốt nhất trong “hệ thống nhúng” (những phần mềm nhỏ, đơn giản là một phần của hệ thống lớn hơn). Chúng cũng lý tưởng cho các lĩnh vực chuyên biệt có ít quy tắc, vì điều này làm cho việc sửa đổi công cụ để xác minh các thuộc tính cụ thể của lĩnh vực dễ dàng hơn.
Hợp đồng thông minh — ít nhất là một phần — thỏa mãn cả hai yêu cầu. Ví dụ, kích thước nhỏ của các hợp đồng Ethereum làm cho chúng dễ kiểm tra chính xác. Tương tự, EVM tuân theo các quy tắc đơn giản, điều này làm cho việc chỉ định và xác minh các thuộc tính ngữ nghĩa cho các chương trình chạy trên EVM dễ dàng hơn.
Chu kỳ phát triển nhanh hơn
Các kỹ thuật xác minh hình thức, như kiểm tra mô hình và thực thi biểu tượng, thường hiệu quả hơn so với phân tích thông thường của mã hợp đồng thông minh (thực hiện trong quá trình kiểm thử hoặc kiểm toán). Điều này bởi vì xác minh hình thức dựa vào các giá trị biểu tượng để kiểm tra các khẳng định (''thử xem người dùng có thử rút n ether không?'') khác với kiểm thử sử dụng các giá trị cụ thể (''thử xem người dùng có thử rút 5 ether không?'').
Các biến đầu vào tượng trưng có thể bao gồm nhiều lớp giá trị cụ thể, vì vậy các phương pháp xác minh hình thức hứa hẹn việc phủ sóng mã hơn trong khoảng thời gian ngắn hơn. Khi sử dụng một cách hiệu quả, xác minh hình thức có thể tăng tốc chu kỳ phát triển cho các nhà phát triển.
Xác minh chính thức cũng cải thiện quy trình xây dựng ứng dụng phi tập trung (dapps) bằng cách giảm thiểu các lỗi thiết kế đắt tiền. Nâng cấp các hợp đồng (nếu có thể) để sửa các lỗ hổng đòi hỏi việc viết lại mã nguồn một cách mở rộng và tốn nhiều công sức hơn trong quá trình phát triển. Xác minh chính thức có thể phát hiện nhiều lỗi trong việc triển khai hợp đồng mà có thể trượt qua các bài kiểm tra và kiểm toán viên và cung cấp cơ hội đáng kể để sửa chữa những vấn đề đó trước khi triển khai một hợp đồng.
NHƯỢC ĐIỂM CỦA XÁC MINH FORMAL
Chi phí lao động thủ công
Xác minh chính thức, đặc biệt là xác minh bán tự động trong đó con người hướng dẫn bằng chứng để suy luận chính xác, đòi hỏi một lượng lao động thủ công đáng kể. Hơn nữa, việc tạo ra đặc tả chính thức là một hoạt động phức tạp đòi hỏi một mức độ kỹ năng cao.
Những yếu tố này (cố gắng và kỹ năng) làm cho xác minh hình thức trở nên đòi hỏi và đắt đỏ hơn so với các phương pháp thông thường để đánh giá tính chính xác trong các hợp đồng, chẳng hạn như kiểm thử và kiểm toán. Tuy nhiên, việc trả giá cho một cuộc kiểm toán xác minh đầy đủ là hợp lý, xét đến chi phí của lỗi trong việc triển khai hợp đồng thông minh.
Kết quả âm
Xác minh chính thức chỉ có thể kiểm tra xem việc thực thi của hợp đồng thông minh có khớp với đặc tả chính thức hay không. Do đó, quan trọng là đảm bảo rằng đặc tả mô tả đúng các hành vi dự kiến của một hợp đồng thông minh.
Nếu các đặc tả được viết kém, vi phạm các thuộc tính—điều chỉ ra các thực thi dễ bị tổn thương—không thể được phát hiện bởi cuộc kiểm tra xác thực hình thức. Trong trường hợp này, một nhà phát triển có thể vô tình giả định rằng hợp đồng không có lỗi.
Vấn đề hiệu suất
Xác minh hình thức gặp phải một số vấn đề về hiệu suất. Ví dụ, các vấn đề về mở rộng trạng thái và đường dẫn gặp phải trong quá trình kiểm tra mô hình và kiểm tra biểu tượng, có thể ảnh hưởng đến các thủ tục xác minh. Ngoài ra, các công cụ xác minh hình thức thường sử dụng trình giải SMT và các trình giải ràng buộc khác trong lớp cơ bản của họ và các trình giải này dựa vào các thủ tục tính toán mất nhiều công suất tính toán.
Ngoài ra, đôi khi không thể xác định được nếu các bộ xác nhận chương trình có thể xác định xem một thuộc tính (được mô tả dưới dạng một công thức logic) có thể được thỏa mãn hay không (câu lệnhvấn đề quyết định
“) bởi vì một chương trình có thể không bao giờ kết thúc. Do đó, có thể là không thể chứng minh một số thuộc tính cho một hợp đồng ngay cả khi nó được xác định rõ ràng.”
CÔNG CỤ XÁC MINH FORMAL CHO HỢP ĐỒNG THÔNG MINH ETHEREUM
Ngôn ngữ đặc tả để tạo đặc tả hình thức
Act: Act cho phép xác định cập nhật lưu trữ, điều kiện trước/sau và hợp đồng bằng chứng minh. Bộ công cụ của nó cũng có công cụ chứng minh công cộ có thể chứng minh nhiều thuộc tính qua Coq, các bác giải SMT, hoặc hevm.
Scribble - Scribble chuyển đổi các chú thích mã trong ngôn ngữ đặc tả Scribble thành các khẳng định cụ thể kiểm tra đặc tả.
Dafny - Dafny là một ngôn ngữ lập trình sẵn sàng kiểm tra dựa vào các chú thích cấp cao để suy luận và chứng minh tính đúng đắn của mã.
Chương trình kiểm tra viên để kiểm tra tính chính xác
Certora Prover - Certora Prover là một công cụ xác minh hình thức tự động để kiểm tra tính chính xác của mã trong hợp đồng thông minh. Các thông số được viết bằng CVL (Ngôn ngữ Xác minh Certora), với vi phạm tính chất được phát hiện bằng cách kết hợp phân tích tĩnh và giải quyết ràng buộc.
Kiểm tra SMT của Solidity - SMTChecker của Solidity là một công cụ kiểm tra mô hình tích hợp dựa trên SMT (Satisfiability Modulo Theories) và giải quyết Horn. Nó xác nhận nếu mã nguồn hợp đồng khớp với các thông số kỹ thuật trong quá trình biên dịch và kiểm tra tĩnh để phát hiện vi phạm các tính chất an toàn.
solc-verify - solc-verify là một phiên bản mở rộng của trình biên dịch Solidity có thể thực hiện xác minh hình thức tự động trên mã Solidity bằng cách sử dụng chú thích và xác minh chương trình modul.
KEVM - KEVM là một ngữ nghĩa hình thức của Máy Ảo Ethereum (EVM) được viết trong K framework. KEVM có thể thực thi và chứng minh một số tuyên bố liên quan đến tính chất bằng cách sử dụng logic đạt được.
Kerangka logic cho chứng minh định lý
Isabelle - Isabelle/HOL là một trợ lý chứng minh cho phép các công thức toán học được diễn đạt bằng ngôn ngữ hình thức và cung cấp các công cụ để chứng minh những công thức đó. Ứng dụng chính là hình thức hóa chứng minh toán học và đặc biệt là xác minh hình thức, bao gồm chứng minh tính chính xác của phần cứng hoặc phần mềm máy tính và chứng minh các tính chất của ngôn ngữ và giao thức máy tính.
Coq - Coq là một công cụ chứng minh định lý tương tác cho phép bạn xác định các chương trình bằng cách sử dụng các định lý và tương tác để tạo ra các bằng chứng kiểm tra máy tính về tính chính xác.
Công cụ dựa trên thực thi biểu tượng để phát hiện mẫu dễ bị tổn thương trong hợp đồng thông minh
Manticore - Một công cụ để phân tích mã bytecode EVM dựa trên việc thực hiện biểu tượng.
hevm - hevm là một công cụ thực thi biểu tượng và kiểm tra tính tương đương cho bytecode EVM.
Mythril - Một công cụ thực thi tượng trưng để phát hiện lỗ hổng trong các hợp đồng thông minh Ethereum
免責聲明：
- Bài viết này được in lại từ []. Tất cả bản quyền thuộc về tác giả gốc [**]. Nếu có bất kỳ ý kiến phản đối nào về việc tái in này, vui lòng liên hệ với Cổng Họcđội ngũ và họ sẽ xử lý nhanh chóng.
- Tuyên bố từ chối trách nhiệm: Các quan điểm và ý kiến được thể hiện trong bài viết này chỉ là của tác giả và không đại diện cho bất kỳ lời khuyên đầu tư nào.
- Việc dịch bài báo ra các ngôn ngữ khác được thực hiện bởi nhóm Gate Learn. Trừ khi được nêu ra, việc sao chép, phân phối hoặc đạo văn các bài báo dịch là không được phép.
Artikel terkait
MakerDAO: DAPP "điên rồ nhất" của Ethereum
Hướng dẫn cách chuyển mạng trong MetaMask