Vào ngày 5 tháng 9, tại Diễn đàn bảo mật hội nghị POD do Odaily tổ chức và 36Kr Group Strategy đồng tổ chức, Yang Wenyu, một chuyên gia bảo mật từ Trung tâm nghiên cứu chuỗi khối Cheetah, đã có bài phát biểu mang tên "Công nghệ kiểm toán tự động hợp đồng thông minh".

Yang Wenyu giới thiệu hiện trạng phát triển hợp đồng thông minh. Hầu hết mọi người nghĩ rằng blockchain hiện đang trong thời kỳ mùa đông lạnh giá, nhưng theo thống kê của Trung tâm nghiên cứu chuỗi khối Cheetah, trong tháng qua, số lượng hợp đồng thông minh mới là 1317 mỗi ngày. Trong số các dự án được đưa vào trung tâm nghiên cứu, cơ sở hạ tầng blockchain chiếm 9,38%, trò chơi và VR 4,44%, thương mại và bán lẻ 3,6%, mạng xã hội và truyền thông 3,4%.

Trong khi số lượng đang tăng lên đều đặn, các hợp đồng thông minh cũng đang phải đối mặt với các vấn đề về bảo mật. Từ năm 2017 đến tháng 6 năm 2018, các lỗ hổng hợp đồng thông minh thường xuyên bùng phát, gây ra nhiều tổn thất tài chính, đồng thời khiến một số nhà phát triển hoặc người dùng chuỗi khối và thậm chí cả hợp đồng thông minh đặt câu hỏi về tính bảo mật của hợp đồng thông minh, điều này cũng cản trở sự phát triển của Ethereum sau Ethereum .sự phát triển của .

Ngoài ra, khi Fomo3D đang lên, một số lượng lớn các hợp đồng giả mạo đã xuất hiện chỉ trong ngày thứ hai. Các nhà phát triển trò chơi Fomo3D sao chép đã thay đổi logic phân phối tích cực, khiến phần lớn số tiền đầu tư chuyển sang các nhà phát triển hợp đồng sao chép, điều này cũng cản trở sự phát triển của DApps.

Trong bối cảnh này, làm thế nào để đảm bảo hiệu quả tính bảo mật của các hợp đồng thông minh lớn? Yang Wenyu tin rằng cách tốt nhất là giảm sự phức tạp của kiểm toán thủ công và sử dụng hợp đồng thông minh để tự động hóa kiểm toán.

Cụ thể, các phương pháp kiểm tra tự động thuộc ba loại chính:

• Đầu tiên là khớp mã tính năng, tức là trích xuất và trừu tượng hóa mã độc, đồng thời tạo thành một mô-đun khớp để phát hiện mã nguồn cần phát hiện. Ưu điểm là tốc độ nhanh và phản ứng nhanh với các lỗ hổng mới, nhưng nhược điểm là phạm vi sử dụng hạn chế và tỷ lệ âm tính giả cao.
  

• Thứ hai là phương pháp kiểm toán tự động dựa trên xác minh chính thức. Nó được Hirai cung cấp lần đầu tiên vào năm 2016 và được cải tiến sau Grishchenko và Hildenbrandt, sử dụng khung F* và khung K để chuyển đổi EVM thành mô hình Chính thức. Chính thức là một khung xác minh chính thức phổ biến trong lĩnh vực hàng không vũ trụ, trong khi khung K là một khung chuyển đổi ngữ nghĩa.
  

• Phương pháp cuối cùng là phương pháp được sử dụng phổ biến nhất hiện nay, dựa trên việc thực thi biểu tượng và trừu tượng hóa biểu tượng để tự động kiểm tra. Khi phân tích hợp đồng thông minh, EVM OPCODE có thể được hình thành bằng cách biên dịch mã nguồn, sau đó nhập vào công cụ phân tích tự động, được chuyển đổi thành CFG, sau đó được phân tích bằng hai phương pháp này. Điển hình là hệ thống Oyente và Securify, có thể giảm tỷ lệ dương tính giả và âm tính giả, nhưng các phương pháp phân tích rất cồng kềnh và tốn thời gian.
  

Tuy nhiên, Yang Wenyu cũng chỉ ra rằng phương pháp kiểm toán tự động hiện tại đang ở giai đoạn rất non nớt và chủ yếu phải đối mặt với ba vấn đề lớn: tỷ lệ cảnh báo sai cao, mức độ tự động hóa thấp, phụ thuộc vào kiểm toán thứ cấp thủ công và thời gian kiểm toán tương đối dài.

Sau đây là toàn văn bài phát biểu của Yang Wenyu, mời các bạn thưởng thức:

Cảm ơn tất cả các bạn. Thật vinh dự khi được tham dự hội nghị này hôm nay. Chủ đề bài phát biểu của tôi hôm nay là phân tích công nghệ phát hiện bảo mật tự động hóa hợp đồng thông minh hiện nay. Bài phát biểu hôm nay của tôi có thể được chia thành hai phần. Đầu tiên, chúng ta sẽ thảo luận về Phần đầu tiên Chúng ta hãy xem hiện trạng phát triển hợp đồng thông minh trên Ethereum. Phần thứ hai dựa trên hiện trạng này, sau đó mô tả chi tiết một số phương pháp liên quan đến tự động hóa hợp đồng thông minh.

Trước hết, chúng ta hãy xem tình hình phát triển hợp đồng thông minh hiện tại, theo nền tảng của chúng tôi, chúng ta có thể biết rằng trong tháng vừa qua, số lượng hợp đồng thông minh đã tăng đều đặn với tốc độ tăng trưởng trung bình là 1317 mỗi ngày, điều này có thể phù hợp với hiểu biết của chúng tôi Chuỗi khối hiện đang trong thời kỳ mùa đông lạnh giá nên tốc độ tăng trưởng tương đối ổn định. Thứ hai, chúng tôi sử dụng một số phương pháp NLT để phân chia lĩnh vực hợp đồng thông minh, ngoại trừ một số lĩnh vực nhạy cảm, hợp đồng thông minh hiện được sử dụng rộng rãi trong cơ sở hạ tầng, bán lẻ thương mại, trò chơi, mạng xã hội và truyền thông. Đây là hiện trạng của hợp đồng thông minh. Tình trạng bảo mật của hợp đồng thông minh hiện nay như thế nào? Có lẽ hai vị khách đã mô tả rất chi tiết. Từ năm 2017 đến tháng 6 năm 2018, loại lỗ hổng hợp đồng thông minh này thường xuyên bùng phát, mỗi lần như vậy mang lại một lượng lớn tổn thất tài chính, đồng thời khiến một số nhà phát triển hoặc một số người dùng chuỗi khối và thậm chí cả hợp đồng thông minh có một số nghi ngờ cao về tính bảo mật của hợp đồng thông minh, điều này cũng cản trở sự phát triển của Ethereum.

Ngoài ra, chúng ta cũng có thể thấy Fomo3D vừa được vị khách đề cập, ngoài bảo mật hợp đồng thông minh cơ bản, bảo mật hiện đang nhận được sự quan tâm rất lớn. ngày. Trong loại trò chơi này, nhà phát triển thực sự đã thay đổi logic phân bổ tích cực, do đó trong quá trình chơi trò chơi tổ ong, phần lớn số tiền đầu tư đã chuyển cho nhà phát triển hợp đồng sao chép, điều này cũng góp phần vào sự phát triển của DApp.gây cản trở.

Bây giờ chúng tôi đang đối mặt với một vấn đề làm thế nào để đảm bảo an toàn hiệu quả cho các hợp đồng thông minh lớn, đây cũng là vấn đề chúng ta sẽ thảo luận hôm nay và phần thứ hai tôi muốn chia sẻ với các bạn về sự phát triển của công nghệ kiểm toán tự động hóa hợp đồng thông minh hiện tại.

Nhìn lại, tính đến 12:00 trưa ngày hôm qua, có tổng cộng 1,93 triệu hợp đồng thông minh trong Ethereum và tốc độ tăng trưởng hàng ngày đang tăng đều đặn. Hiện tại, các phương pháp kiểm toán bao gồm kiểm toán thủ công và kiểm toán tự động. Trong số các hợp đồng thông minh khổng lồ, cách tốt nhất của chúng tôi là giảm sự phức tạp của việc kiểm toán thủ công, để có thể thực hiện được nhiều việc hơn thông qua kiểm toán tự động. Chúng tôi chia kiểm tra tự động thành ba phần. Trước hết, loại đầu tiên là khớp mã tính năng, loại thứ hai là phương pháp kiểm tra nhiệm vụ phụ dựa trên xác minh tình huống và loại cuối cùng là kiểm tra tự động dựa trên thực thi biểu tượng và trừu tượng hóa biểu tượng.

Đầu tiên hãy nhìn vào đối sánh mã tính năng. Có thể hiểu rõ ràng từ cái tên mà nó trích xuất và trừu tượng hóa mã độc. Chúng tôi là đối sánh ngữ nghĩa phù hợp với mã gốc tĩnh. Ưu điểm của phương pháp kiểm tra là rõ ràng, ví dụ, tốc độ rất nhanh nhanh chóng, bởi vì Thực hiện khớp chuỗi trên mã nguồn và người thứ hai có thể nhanh chóng tìm ra lỗ hổng mới. Nếu lỗ hổng mới xuất hiện trong quá trình kiểm tra của anh ấy, chúng tôi có thể nhanh chóng gửi một số mẫu khớp mới. Những thiếu sót của nó là gì? Chúng ta hãy xem xét lại. Chúng tôi hiểu rằng chuỗi khối hiện tại nên công khai và minh bạch, nhưng tình hình thực tế không phải như thế này. Có lẽ chúng tôi đã làm một thống kê. Tỷ lệ mở mã hiện tại chỉ chiếm 48,62%., Tức là trên Ethereum, hơn một nửa số hợp đồng không phải là mã nguồn mở, chỉ có mã được hiển thị, vị khách vừa nói rằng họ cũng đã tốn rất nhiều công sức để thiết lập mã, hạn chế này dẫn đến phạm vi sử dụng Hạn chế của phương pháp này là phương pháp kiểm tra tĩnh truyền thống, chẳng hạn như Phát hiện ứng dụng, sẽ gọi một số chức năng duy nhất trong thư viện để kiểm tra chúng. Một số chức năng và tính năng trong hợp đồng thông minh có nhiều thay đổi hơn nên tỷ lệ dễ bị tổn thương tương đối cao.

Phương pháp thứ hai, hãy thảo luận về kiểm toán tự động phổ biến dựa trên xác minh chính thức. Kiểm toán xác minh chính thức. đánh giá xem logic mã có vấn đề hay không, hai công việc cuối cùng của công việc này đã cải cách hơn nữa về khía cạnh hình thức, họ đã từ bỏ ngôn ngữ Lem. Đây cũng là một phương thức chuyển đổi tương đối kém hiệu quả. Họ sử dụng khung công tác F * và khung công tác K để chuyển đổi EVM thành một Mô hình chính thức và Chính thức có thể là một khung thường thực hiện một số xác minh chính thức trong lĩnh vực hàng không vũ trụ, trong khi khung K là một khung chuyển đổi Ngữ nghĩa, hai nghiên cứu kỹ thuật tiêu biểu này, nếu bạn muốn hiểu sâu hơn, bạn có thể tham khảo giấy tờ sau đây.

Điểm thứ ba là hôm nay tôi muốn tập trung vào việc giao tiếp với bạn và một số phương pháp được sử dụng phổ biến nhất là kiểm toán tự động dựa trên thực thi ký hiệu và trừu tượng hóa ký hiệu. Hãy xem xét kiểm toán tự động này. Khi chúng ta phân tích hợp đồng thông minh, trước tiên chúng ta phải phân tích rõ ràng đối tượng là gì. Giống như chúng ta vừa giải thích mã khớp tính năng, chúng ta biết rằng hầu hết các mã hợp đồng thông minh trên EVM đều không công khai. Bây giờ chúng ta phân tích đối tượng và xác nhận rằng đó phải là EVM OPCODE. Sau khi chuyển một số mã nguồn, chúng tôi biên dịch, có thể tạo EVM OPCODE, nhập vào công cụ phân tích tự động. Trong khung kiểm toán tự động này dựa trên thực thi ký hiệu và trừu tượng hóa ký hiệu, có một số tính năng chung. OPCODE sẽ được chuyển đổi thành CFG khi được nhập vào công cụ, đây là sơ đồ luồng điều khiển từng cái một. Thông qua CFG này, bạn có thể hiểu một cách đơn giản CFG này có nghĩa là gì? CFG là gói logic trong mã hợp đồng thành một mã nhanh. Khi logic bên trong được rẽ nhánh, hợp đồng bên trái tạo thành một CFD rất lớn và hoàn chỉnh, để các lập trình viên có thể hiểu và thực hiện tốt hơn logic nào đó.

Sau khi CFG ra đời, hiện nay có hai phương pháp phân tích. Loại thứ nhất là xác minh dựa trên thực thi ký hiệu. Loại này mang tính đại diện hơn. Mọi người đều quen thuộc với Mythril, Oyente và Maian. Một phương pháp phân tích trừu tượng tượng trưng có sẵn công khai là Securify .Hôm nay tôi sẽ chủ yếu nói về kiến ​​trúc cụ thể và phương thức triển khai của hai hệ thống Oyente và Securify. Đầu tiên, hãy nhìn vào Oyente. Chúng ta có thể thấy logic của Oyente từ bên trái. Trong CFG Sau ứng dụng, đầu tiên là một nhà thám hiểm , sẽ xác minh từng quy trình trong mã và thực hiện xác minh chính thức, cứ như vậy, chúng ta xác minh xem mình có X hay không, để X không chỉ thỏa mãn các điều kiện của C1, C2, C3. Lúc này, chúng ta có thể xác định trạng thái là không hay có, để xác minh luồng của toàn bộ logic. Phân tích cốt lõi thứ hai thực sự là phần cốt lõi nhất của Oyente. Nó chuyển đổi đường dẫn thám hiểm chỉ là đầu ra và chỉ thực hiện một số xác minh lỗ hổng. Hiện tại, nó chỉ cung cấp TOD, phụ thuộc Dấu thời gian và các ngoại lệ Xử lý sai, ba Xác minh này. Cuối cùng, phần này hệ thống có thể đảm bảo tỷ lệ dương tính giả và âm tính giả. Nó sử dụng trình xác minh mã nguồn mở của Microsoft để đóng gói kiến ​​trúc tổng thể. Trong quá trình chúng tôi vừa mô tả, bạn cũng nên hiểu rằng xác minh CFG để thám hiểm Đôi khi, chúng ta cần duyệt qua anh ta, và mỗi lần là một lần xác minh, vì vậy phương pháp phân tích này đặc biệt tốn thời gian và có thể không thành công. Đây là nơi Oyente hiện đang có một vấn đề lớn.

Trên cơ sở của vấn đề này, giống như Securify, họ cung cấp một phương pháp khác. Họ tin rằng mã hợp đồng hiện tại thực sự đặc biệt dễ tách rời. Không giống như mã truyền thống, tính liên kết đặc biệt cao, chẳng hạn như một số dạng mã hợp đồng tương đối cố định. Chúng tôi không cần tiến hành kiểm tra toàn bộ logic hợp đồng. Chúng tôi phân tích từng mô-đun của hợp đồng tách rời để cải thiện mức độ tự động hóa. Hình bên trái hiển thị toàn bộ quá trình xác minh. Mã byte hợp đồng được chuyển qua ngôn ngữ miền Sau đó, có là một mô-đun xác minh, đặc biệt giống như khớp mẫu đã đề cập trước đó, mô-đun này chuyển đổi một số lỗ hổng thành khung khớp mẫu ngôn ngữ xác minh và xác minh xem ngữ nghĩa có tương thích với mô-đun này hay không. Cuối cùng, một báo cáo cũng được đưa ra.Thông qua phương pháp kiểm tra tự động này, người quản lý cuối cùng có thể xuất ví có thể được sửa đổi.

Một điểm cụ thể hơn là làm thế nào để phân tích ngữ nghĩa. Trên thực tế, việc phân tích mã thám hiểm này là từ hai chiều, thứ nhất là logic và thứ hai là dữ liệu. Phương pháp logic xác định hai loại logic. Loại thứ nhất được gọi là MayFollow và thứ hai được gọi là MustFollow, MayFollow có nghĩa là L2 phải có một đường dẫn sau L1 và MustFollow có nghĩa là mọi đường dẫn của L2 phải tuân theo L1. Hai sự khác biệt này xác định toàn bộ khung logic.

Thứ hai là dữ liệu.Cách xác định thay đổi dữ liệu trong hợp đồng sử dụng ba loại.MayDepOn đầu tiên là hai yếu tố, một được gọi là Y và yếu tố kia được gọi là T. Khi T thay đổi, Y có thể thay đổi hoặc không. Thứ hai là Eq, nghĩa là Y được xác định bởi T. Cái thứ ba là DetBy, Y và T tương ứng với nhau, chỉ cần T chuyển thành Y nhất định sẽ thay đổi, đây là một cách hình dung sinh động hơn, thực ra Maydepon giống như biến T của chúng ta là thời gian, trong một khoảng thời gian, Y có thể là một giá trị, T thay đổi, Y có thể không thay đổi, thứ ba là mối quan hệ một đối một, giống như chúng ta tính toán hàm băm, chỉ cần bạn thay đổi T, Y phải thay đổi, thông qua hai chiều logic và dữ liệu, họ đã tiến hành một số xác minh và mô-đun xác minh cuối cùng hiện cung cấp khoảng sáu hoặc bảy ngôn ngữ xác minh lỗ hổng hợp đồng thông minh. Ngôn ngữ này được viết trong phần bổ trợ và các nhà phát triển bảo mật khác có thể tiếp tục làm phong phú thêm quá trình xác minh ngôn ngữ của lỗ hổng. .

Cuối cùng, khi chúng tôi đánh giá kiểm toán tự động, chúng tôi cần cung cấp vấn đề này từ mức độ tự động hóa, tỷ lệ dương tính giả và tỷ lệ dương tính giả. Bây giờ chúng tôi biết rằng dữ liệu có thể bị ràng buộc và dữ liệu được phát hiện vẫn cần phải được xác nhận lại theo cách thủ công.Công việc này rất cồng kềnh và tỷ lệ dương tính giả có thể được giảm thông qua phương pháp này.Hai phương pháp kiểm tra tự động này là thực thi ký hiệu và trừu tượng hóa ký hiệu.

Cuối cùng, để xem lại, hiện tại có ba loại phương pháp kiểm tra tự động, khớp mã tính năng, xác minh chính thức, thực thi tượng trưng và trừu tượng hóa tượng trưng. Nhìn lại toàn bộ quá trình phân tích, chúng ta có thể biết rõ rằng phương pháp kiểm tra tự động hiện tại đang ở giai đoạn rất non nớt và chủ yếu gặp phải ba vấn đề lớn: Thứ nhất là tỷ lệ dương tính giả cao, không thể tự động hóa hoàn toàn và cần có sự tham gia của thủ công . . Thứ hai là mức độ tự động hóa tương đối thấp và cần được kiểm toán liên tục, thứ ba là thời gian kiểm toán tương đối dài.

Cuối cùng là xem lại toàn bộ phân tích của chúng ta. Trước tiên, hãy làm rõ tình trạng phát triển của hợp đồng thông minh và thử nghiệm các phương pháp kiểm tra tự động. Có các nhóm trao đổi kỹ thuật của chúng tôi ở bên trái và bên phải. Trẻ em quan tâm có thể tham gia và chúng ta có thể có một thảo luận sâu hơn cùng nhau. Đây là những gì tôi đang làm ngày hôm nay. Cảm ơn bạn đã chia sẻ nội dung.