IOSG Ventures: Có cơ hội thương mại hóa các công cụ phân tích bảo mật hợp đồng thông minh không?

Tiêu đề gốc: " Tóm tắt hàng tuần của iOSG｜Có cơ hội thương mại hóa các công cụ phân tích bảo mật hợp đồng thông minh không? #151 》

Tác giả gốc: Ray Xiao, Sally Gu, IOSG Ventures  

Lời nói đầu:

Vào cuối tháng 9, Paradigm chính thức thông báo rằng họ đã hoàn thành khoản đầu tư hàng đầu vào dự án bảo mật blockchain Blowfish, một lần nữa thu hút sự chú ý rộng rãi trong lĩnh vực bảo mật hợp đồng thông minh Phân tích. Nhưng trên thực tế, nhóm Paradigm đã thực hiện rất nhiều thực hành theo hướng thử nghiệm bảo mật hợp đồng thông minh trước đây. Vào tháng 3 năm nay, Paradigm CTO Georgios đã công bố bộ thử nghiệm hợp đồng thông minh Foundry mà họ đã phát triển (nhóm Runtime Verification cũng là người đóng góp quan trọng). ). Hiện nay, phân tích bảo mật Blockchain của quận cũng đang phát triển theo hướng phân công lao động chi tiết hơn.

Đánh giá từ xu hướng tài chính và phản ứng của thị trường trong những tháng gần đây, Vốn thị trường cấp 1 hiện rất quan tâm đến lĩnh vực giám sát an ninh và tường lửa, tập trung vào tính kịp thời của thông tin bảo mật, mức độ ngăn ngừa rủi ro và công nghệ nhẹ (điều này rất khác với lĩnh vực kiểm toán nơi hầu hết đầu tư vốn trước đây).

Theo các báo cáo có liên quan từ CertiK và SlowMist, tổn thất tài sản tiền điện tử do các cuộc tấn công bảo mật chỉ trong quý 1 và quý 2 năm 2022 đã lên tới 2 tỷ USD . Chỉ riêng các cuộc tấn công cho vay chớp nhoáng đã gây ra tổng thiệt hại tài sản là 300 triệu USD trong quý hai. Tháng này đã trở thành tháng có hoạt động hacker lớn nhất trong lịch sử, trong hai tuần, đã có hơn 12 cuộc tấn công vào riêng giao thức DeFi, với hơn 700 triệu USD bị đánh cắp.

Nguồn: https://twitter.com/chainalysis/status/1580312145451180032?s=20& =QfqOMqMKjHd3EtX_0O-QjA

Nếu chúng ta coi hợp đồng thông minh trên chuỗi từ phát triển>>triển khai đến mạng blockchain>>hoạt động là một xét về mặt hoàn chỉnh vòng đời, phân tích bảo mật của hợp đồng thông minh được chia thành: phân tích trước khi triển khai hợp đồng (trước khi mạng blockchain chính thức ra mắt trực tuyến) và phân tích sau khi triển khai hợp đồng, bao gồm đại khái: danh mục thử nghiệm, kiểm toán và giám sát, theo từng danh mục. là các loại phương pháp phân tích và công cụ tương ứng (như hình bên dưới). Tái bút: Phạm vi kiểm tra hợp đồng thông minh sẽ từ trước khi triển khai hợp đồng đến sau khi triển khai (kiểm toán nâng cấp hợp đồng)

1. Phân tích bảo mật trước khi triển khai hợp đồng thông minh: thử nghiệm + kiểm toán

1.1 Kiểm thử

Kiểm thử theo hợp đồng là công việc mà các nhà phát triển và kiểm toán viên cần dành nhiều tâm sức nhất, liên quan đến Các nhà phát triển truyền thống thì khác. Do tính chất không thể giả mạo của blockchain nên một khi hợp đồng thông minh được triển khai trên máy ảo EVM thì rất khó để thay đổi nó. Do đó, phần lớn công việc phân tích bảo mật và khắc phục các lỗ hổng bảo mật đều được dành cho việc “chuẩn bị trước”. phân tích sự kiện" - kiểm tra bảo mật của hợp đồng thông minh trước khi triển khai.

Trước khi chấp nhận một cuộc kiểm tra chính thức, nhà phát triển/kiểm toán viên hợp đồng cần tiến hành một số thử nghiệm cơ bản về mã hợp đồng. Phạm vi kiểm tra ban đầu càng cao thì càng tránh được. một số lỗi đơn giản khi bước vào giai đoạn kiểm tra chính thức (nói chung, hợp đồng thông minh đạt mức độ bao phủ mã 85%-90% qua các thử nghiệm là mức hợp lý; tỷ lệ bao phủ cho các mô-đun lõi cần phải trên 95%).

Các thử nghiệm cơ bản phổ biến bao gồm thử nghiệm đơn vị (kiểm thử tập trung vào một chức năng duy nhất) và thử nghiệm tích hợp (để đảm bảo rằng tất cả các phần của mã có thể chạy bình thường khi được kết hợp) . Các công cụ thường được sử dụng ở giai đoạn này bao gồm Hardhat, khung kiểm tra Truffle, v.v. Nội dung kiểm tra phổ biến bao gồm: kiểm tra trạng thái, kích hoạt sự kiện, đặt lại giao dịch, tính toán chức năng và kiểm tra chức năng hoàn chỉnh.

Nguồn: https://betterprogramming.pub/how-to-test -ethereum-smart-contracts-35abc8fa199d

1.2 Kiểm toán

"Kiểm thử có thể phát hiện ra các khiếm khuyết trong một chương trình một cách hiệu quả, nhưng nó không thể chứng minh rằng chương trình đó không có khiếm khuyết." - Edsger Wybe Dijkstra (nhà khoa học máy tính, người đoạt giải Turing năm 1972)

Theo định nghĩa của tài liệu chính thức của Ethereum, kiểm toán là đánh giá chi tiết từng dòng mã nguồn của hợp đồng thông minh và cách suy nghĩ của kẻ tấn công để lập bản đồ có thể rủi ro trong hợp đồng thông minh. Các vectơ tấn công để phát hiện các điểm lỗi có thể xảy ra, lỗ hổng bảo mật và phương thức phát triển kém. Giai đoạn kiểm tra bao gồm: phân tích tĩnh, phân tích động (kiểm tra mờ, thực thi ký hiệu), phân tích thủ công và xác minh chính thức. Như Dijkstra đã nói trong hình trên, chỉ thử nghiệm thôi thì không thể hoàn toàn tin rằng chương trình không có lỗi. Kiểm tra và xác minh chính thức thiên về việc tiến gần hơn đến mục tiêu là chương trình không có lỗi.

Chi phí tiền

Theo dữ liệu từ công ty bảo mật hợp đồng thông minh Hacken, chi phí trung bình trong ngành của dịch vụ kiểm toán hợp đồng thông minh dao động từ 5.000 USD đến 30.000 USD (đối với các dự án vừa và nhỏ). Đối với những dự án lớn, chi phí đôi khi có thể lên tới 500.000 USD trở lên. Chi phí kiểm tra hợp đồng thông minh phụ thuộc trực tiếp vào độ phức tạp của mã và phạm vi công việc đã được thống nhất. Các yếu tố khác ảnh hưởng đến giá bao gồm mức độ khẩn cấp, quy mô của hợp đồng thông minh (có bao nhiêu dòng mã), số giờ kỹ thuật cần thiết để hoàn thành quy trình, tính sẵn có của tài liệu liên quan đến dự án và các yếu tố khác. các nhân tố.

Chi phí thời gian

Yêu cầu kiểm tra ban đầu trung bình 2 đến 14 ngày, tùy thuộc vào độ phức tạp của dự án, quy mô hợp đồng thông minh và mức độ khẩn cấp. Đối với các dự án hoặc thỏa thuận lớn, quá trình xem xét ban đầu có thể mất tới 1 tháng. Sau khi quá trình xem xét ban đầu hoàn tất, khách hàng sẽ nhận được đề xuất về những sửa đổi cần thực hiện.

Chi phí lao động

Theo IOSG năm khu vực Theo phản hồi từ Runtime Verification, một dự án đầu tư hàng đầu trong lĩnh vực xác minh chính thức blockchain, chi phí nhân công kiểm tra phụ thuộc vào độ phức tạp của giao thức. Đối với hầu hết các công ty kiểm toán bảo mật hàng đầu có kinh nghiệm cao cấp trong ngành và kinh nghiệm học thuật, về cơ bản không khó để hiểu logic kinh doanh và tính kinh tế mã thông báo của các dự án khách hàng tiền điện tử. Thông thường, phải mất khoảng 1 đến 2 tuần để hoàn thành các bước ban đầu.

Nhưng phần tiếp theo sẽ phụ thuộc vào nhu cầu cụ thể của khách hàng. Một số khách hàng chỉ yêu cầu kiểm tra thủ công logic kinh doanh cơ bản của dự án được kiểm toán (xem mã của họ và xem xét thủ công xem nó có phù hợp với logic kinh doanh được yêu cầu hay không), đây là dịch vụ rẻ nhất. Một số khách hàng muốn mô hình hóa logic kinh doanh và kinh tế mã thông báo, sau đó thực hiện các bằng chứng toán học theo cách thủ công để đảm bảo rằng một số kết quả quan trọng nhất định được thiết lập, chẳng hạn như bảo mật, tính sống động, tính nhất quán, v.v. Một số khách hàng lớn, chẳng hạn như MakerDAO và Ethereum Foundation, muốn tiến thêm một bước nữa và thực hiện xác minh chính thức (Formal Verification) trên mã.

Một điều nữa về xác minh chính thức sử dụng các phương pháp toán học để xác minh tính đúng đắn của chương trình - việc thực hiện chương trình và ý định của người lập trình. cuối cùng đã được chứng minh rằng hệ thống dự án không có lỗi. Hay nói cách khác, xác minh chính thức giống như một cuộc "thử nghiệm" toàn diện hơn. Về mặt lý thuyết, nó sẽ bao gồm tất cả các đầu vào và trạng thái có thể có, điều mà việc thử nghiệm không thể thực hiện được (như trong ví dụ bên dưới, có lỗi tràn trong hợp đồng chuyển nhượng), nếu bạn dùng thử nghiệm thì người thử nghiệm cần nhập một giá trị rất lớn mới tìm ra, nhưng người xác minh chính thức sẽ tìm ra lỗi tràn thông qua logic toán học "tổng số lượng token = tổng số dư của tất cả các địa chỉ")

Từ góc độ ứng dụng thực tế trên quy mô lớn, việc xác minh chính thức sẽ kém hiệu quả hơn ở quy mô lớn hơn so với các giải pháp thử nghiệm truyền thống. Đối với hầu hết các dự án tiền điện tử, việc hoàn thành kiểm toán hợp đồng thông minh là đủ. Về mặt chi phí đầu tư và lợi ích tiềm năng, điều đó là không cần thiết đối với các dự án nhỏ (hoặc chi phí chứng minh rằng chương trình không có lỗi vẫn tương đối cao). Cốt lõi Lý do là việc xác minh chính thức cần có sự tham gia của các nhân tài chính thức chuyên nghiệp, bởi vì việc tạo ra một đặc tả chính thức cho mã dự án là một vấn đề rất phức tạp. Nó cần bao gồm các thuộc tính của mã hợp đồng và xác định cách thức hoạt động của hợp đồng trong các trường hợp khác nhau. Cần có sự tham gia của những người có chuyên môn. (Bạn đọc quan tâm có thể tham khảo bài viết trước của chúng tôi "Tại sao chúng tôi dẫn đầu đầu tư vào xác minh thời gian chạy" https://mp.weixin.qq.com/s/VWVgn4k9k0XqbM-O7-TVXg)

Kiểm toán hợp đồng thông minh vẫn là một ngành sử dụng nhiều lao động và có yêu cầu kỹ thuật cao đối với nhân tài. Mặc dù hiện có hơn chục công cụ kiểm tra phổ biến trên thị trường (chủ yếu được phát triển bởi các công ty kiểm toán bảo mật chính thống hoặc các nhà nghiên cứu hàn lâm), mục đích của việc phát triển các công cụ kiểm toán này là để phát hiện ra các lỗ hổng phổ biến hơn. Ví dụ: phụ thuộc thứ tự giao dịch, số ngẫu nhiên, dấu thời gian, độ sâu ngăn xếp cuộc gọi, Reentrancy, cuộc gọi đại biểu nguy hiểm, v.v.). Do đó, rất khó để hoàn thành công việc kiểm toán nếu chỉ dựa vào các công cụ này và có thể bỏ sót nhiều lỗ hổng liên quan đến logic nghiệp vụ. Nói chung, việc xem xét hợp đồng thông minh yêu cầu sử dụng kết hợp các công cụ tự động + xem xét mã thủ công và yêu cầu xem xét thủ công trong từng trường hợp tùy thuộc vào logic kinh doanh hợp đồng thông minh và mô hình Token của khách hàng.

Phân tích và kiểm tra bảo mật hợp đồng thông minh thường xác minh tính đúng đắn của chương trình, tức là việc triển khai chương trình phù hợp với ý định của người lập trình. Bởi vì lỗi chương trình thực chất là do sự khác biệt giữa việc thực hiện chương trình và ý định của người lập trình. Ngữ nghĩa chính thức được đề cập trong bài viết trước chia sẻ khoản đầu tư của chúng tôi vào Xác minh thời gian chạy thực sự là một khung ngôn ngữ có thể khớp chính xác với ý định phát triển của nhà phát triển (tức là "ngữ nghĩa") và việc triển khai (tức là "cú pháp" của ngôn ngữ lập trình), vì vậy Giảm thiểu sự xuất hiện của lỗi.

Mặc dù có rất nhiều công cụ trên thị trường trong lĩnh vực kiểm tra bảo mật hợp đồng thông minh, hầu hết đều là nguồn mở nhưng rất ít trong số đó đã được sử dụng để đạt được thành công. thương mại hóa. Chúng tôi sẽ phân tích nguyên nhân gốc rễ sau. Tóm lại, chúng tôi vẫn dựa vào các công cụ tự động hóa của chính nhà cung cấp dịch vụ bảo mật + đọc thủ công từng dòng mã hoặc mô hình hóa. công cụ kiểm toán.

PS: Dựa trên phản hồi từ Hexens, tổ chức mà chúng tôi mới lãnh đạo, ban đầu chúng tôi đang thử nghiệm Slither đối với một số phân tích tĩnh và MythX là các công cụ nguồn mở được sử dụng phổ biến của họ, mặc dù kết quả không khả quan lắm đối với họ. Đối với thử nghiệm ở cấp độ cao hơn, họ chủ yếu sử dụng các bộ mờ như Echidna và Forge+ được tích hợp trong bộ mờ

2 Phân tích bảo mật sau khi triển khai hợp đồng thông minh - Giám sát)

Trong số 10 cuộc tấn công bảo mật mạng blockchain phổ biến nhất hiện nay, Scam xuất hiện thường xuyên nhất và gây tổn thất tài sản trực tiếp cao nhất cho người dùng. Theo dữ liệu của Peckshield, vào năm 2021, tổn thất kinh tế trên chuỗi của tiền điện tử do nhiều vụ lừa đảo khác nhau lên tới 12 tỷ USD, cao gấp 6,7 lần so với tổn thất do các cuộc tấn công trực tiếp của tin tặc gây ra.

Các cuộc tấn công lừa đảo phổ biến:

Lừa đảo (Một kỹ thuật lừa đảo phổ biến là gửi email/trang web yêu cầu người dùng đặt lại mật khẩu/khôi phục tài khoản của họ. Sau khi người dùng đăng nhập vào các trang web giả mạo này, họ sẽ đánh cắp Quyền riêng tư key)

Trường hợp: Alice đăng nhập vào nền tảng giao dịch và kết nối với ví MetaMask. Cô nhận được một cửa sổ bật lên thông báo rằng ví bị lỗi và cần phải khắc phục. khôi phục cụm từ ghi nhớ Sau khi khôi phục, ví Tất cả tài sản đã bị đánh cắp.

Mạo danh/Mạo danh (Một người tự xưng là nhân viên hoặc đại diện của một số dapp/tổ chức nhất định có thể liên lạc qua email, điện thoại hoặc mạng xã hội media Media liên hệ với người dùng. Họ sẽ đánh cắp tiền từ người dùng bằng cách gửi cho họ các trang web đào tiền/airdrop miễn phí giả mạo hoặc thao túng nạn nhân thông qua việc mạo danh để rút tiền hoặc dữ liệu nhạy cảm)

Trường hợp : Chính phủ Ukraine đã chấp nhận các khoản quyên góp bằng tiền điện tử và công bố các đợt airdrop NFT. Kẻ mạo danh đã giả danh chính phủ Ukraine và phát hành các đợt airdrop mã thông báo giả để thực hiện hành vi lừa đảo.

Chiếm đoạt danh tính quản lý Discord (Kẻ tấn công kiểm soát bot của người kiểm duyệt được cộng đồng tin cậy để đăng thông báo sai sự thật, liên kết lừa đảo hoặc giả mạo. tiền điện tử hoặc NFT của họ)

Trường hợp: Tin tặc đã chiếm quyền kiểm soát các máy chủ bất hòa chính thức dành cho các NFT blue-chip như Bored Ape Yacht Club và gửi hàng loạt liên kết không chính xác đến các thành viên , tài sản sẽ bị đánh cắp không thể phục hồi sau khi người dùng nhấp vào

Chiếm quyền điều khiển BGP (được thực hiện bằng cách tuyên bố sai rằng mình sở hữu tiền tố IP mà người ta không thực sự kiểm soát và thêm nó vào bảng định tuyến trong bộ định tuyến Internet BGP , Kẻ tấn công có thể chiếm đoạt lưu lượng truy cập từ địa chỉ IP này, trong trường hợp đó người dùng sẽ được chuyển hướng đến địa chỉ bẫy do kẻ tấn công đặt khi họ cố gắng đăng nhập)

Trường hợp: Celer bị tấn công chiếm quyền điều khiển BGP, ảnh hưởng đến 32 người dùng và thiệt hại 235.000 USD (2022.08)

Cửa hậu mã & bẫy mã