Luận văn thạc sĩ: Xác thực hợp đồng thông minh bằng kỹ thuật phân tích tĩnh

• Tác giả: Băng Ngọc Bảo Tâm
• Người hướng dẫn: PGS. Quản Thành Thơ
• Trường học: Đại học Quốc gia TP. HCM
• Chuyên ngành: Khoa học máy tính
• Đề tài: Xác thực hợp đồng thông minh bằng kỹ thuật phân tích tĩnh
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2020
• Địa điểm: TP. Hồ Chí Minh

• LỜI MỞ ĐẦU
• 1. INTRODUCTION
• 1.3. Verification of Smart Contracts
• 1.1. Scope of this research
• 1.2. The pilot study I: Verification of Ethereum Smart Contracts: An Model Checking Approach
• 1.4. The pilot study II: An Intelligent Chatbot for Automatic Verification of Ethereum Smart Contracts
• 2. LITERATURE SURVEY
• 3. RESEARCH BACKGROUND
• 3.2. How does a Blockchain work?
• 3.1. Is Blockchain Secure ?
• 3.2.1. Proof of Work
• 3.2.2. Proof of Stake
• 3.2.3. What is Blockchain good for?
• 3.2.4. Ethereum Smart Contracts
• 3.2.5. Ethereum Smart Contracts structures
• 3.2.6. Ethereum Smart Contracts example
• 3.2.7. Abstract Syntax Tree
• 3.2.8. Control-flow Graph
• 4. Verification of Ethereum Smart Contracts: A Model Checking Aprroach
• 4.1. Building an Abstract Syntax Tree
• 4.2. Generating CFG of Smart Contracts
• 4.3. Summary of the work
• 4.4. Limitations and Future Directions
• Phụ lục
• A. Appendix A: An Intelligent Chatbot for Automatic Verification of Ethereum SmartContracts
• A.2. How does Chatbot work?
• A.4. Our Propose Chatbot
• A.5. Building An Intelligent Chatbot for Automatic Verification of Ethereum Smart Contracts based on Rasa Framework
• B. Appendix B: Publication
• Curriculum Vitae

I. Giới thiệu

Trong bối cảnh công nghệ thông tin phát triển nhanh chóng, hợp đồng thông minh đã trở thành một phần quan trọng trong các ứng dụng blockchain. Xác thực hợp đồng là một vấn đề cấp thiết, đặc biệt khi những lỗ hổng bảo mật có thể gây thiệt hại lớn cho người dùng. Luận văn này tập trung vào việc nghiên cứu các phương pháp phân tích tĩnh để xác thực hợp đồng thông minh, nhằm đảm bảo tính chính xác và an toàn của chúng. Công nghệ blockchain không chỉ mang lại lợi ích về tính minh bạch mà còn giúp loại bỏ sự cần thiết của các bên trung gian, từ đó giảm thiểu chi phí và thời gian giao dịch. Tuy nhiên, sự xuất hiện của các lỗ hổng bảo mật trong hợp đồng thông minh đã chỉ ra rằng việc xác thực là cần thiết để bảo vệ người dùng khỏi các mối đe dọa tiềm ẩn. Điều này đặt ra thách thức cho các nhà nghiên cứu và phát triển trong việc tìm ra các phương pháp hiệu quả để kiểm tra và xác thực các hợp đồng này.

1.1. Tầm quan trọng của việc xác thực hợp đồng thông minh

Việc xác thực hợp đồng thông minh có ý nghĩa quan trọng trong việc đảm bảo rằng các giao dịch được thực hiện một cách chính xác và an toàn. Khi các hợp đồng này được triển khai trên blockchain, bất kỳ lỗi nào trong mã nguồn có thể dẫn đến hậu quả nghiêm trọng, như việc mất mát tài sản hoặc thông tin nhạy cảm. Theo một nghiên cứu gần đây, hàng triệu đô la đã bị đánh cắp do các lỗi bảo mật trong hợp đồng thông minh. Do đó, việc áp dụng các phương pháp phân tích tĩnh để kiểm tra mã nguồn trước khi triển khai là cực kỳ cần thiết. Các phương pháp này không chỉ giúp phát hiện lỗi mà còn cung cấp cho các nhà phát triển cái nhìn sâu sắc về cách thức hoạt động của hợp đồng, từ đó cải thiện tính bảo mật và độ tin cậy của chúng.

II. Nền tảng nghiên cứu

Luận văn này sử dụng các phương pháp phân tích tĩnh để nghiên cứu cấu trúc và hoạt động của hợp đồng thông minh trên nền tảng Ethereum. Khoa học máy tính và các lĩnh vực liên quan đã cung cấp nhiều công cụ và kỹ thuật hữu ích để phân tích mã nguồn. Việc xây dựng đồ thị dòng điều khiển (CFG) là một trong những bước quan trọng trong quá trình này, cho phép các nhà phát triển hình dung rõ hơn về cách thức hoạt động của hợp đồng. Bằng cách áp dụng logic hợp đồng và các phương pháp kiểm tra, luận văn đề xuất một mô hình mới nhằm tăng cường khả năng kiểm tra hợp đồng trước khi chúng được triển khai. Điều này không chỉ giúp bảo vệ người dùng mà còn nâng cao uy tín của công nghệ blockchain trong cộng đồng.

2.1. Phân tích cấu trúc hợp đồng thông minh

Cấu trúc của hợp đồng thông minh thường bao gồm các hàm và biến, với mỗi hàm thực hiện một chức năng cụ thể. Việc phân tích cấu trúc này cho phép các nhà phát triển xác định các điểm yếu tiềm ẩn trong mã nguồn. Phân tích mã nguồn sẽ giúp phát hiện các lỗi lập trình, từ đó giảm thiểu rủi ro khi hợp đồng được triển khai. Bên cạnh đó, việc sử dụng công nghệ blockchain cũng mang lại lợi ích lớn trong việc lưu trữ và xác thực thông tin. Hệ thống phân tán giúp đảm bảo rằng mọi giao dịch đều được ghi lại một cách minh bạch và không thể thay đổi, từ đó nâng cao tính an toàn cho người dùng.

III. Phương pháp xác thực hợp đồng thông minh

Luận văn đề xuất một quy trình xác thực hợp đồng thông minh thông qua việc áp dụng các kỹ thuật phân tích tĩnh và thực thi biểu tượng. Phương pháp này không chỉ giúp phát hiện lỗi mà còn cung cấp cái nhìn tổng quan về cách thức hoạt động của hợp đồng. Việc sử dụng đồ thị dòng điều khiển cho phép các nhà phát triển theo dõi luồng thực thi của mã nguồn và xác định các điểm có thể xảy ra lỗi. Hơn nữa, việc áp dụng các công cụ phân tích tự động sẽ giúp giảm thiểu thời gian và công sức cần thiết để kiểm tra mã nguồn. Điều này đặc biệt hữu ích cho những người dùng không có chuyên môn kỹ thuật, giúp họ dễ dàng sử dụng và hiểu rõ hơn về hợp đồng thông minh.

3.1. Kết quả và ứng dụng thực tiễn

Kết quả của nghiên cứu cho thấy rằng việc áp dụng các phương pháp phân tích tĩnh có thể cải thiện đáng kể tính an toàn và độ tin cậy của hợp đồng thông minh. Các ứng dụng thực tiễn của nghiên cứu này không chỉ giới hạn trong lĩnh vực tài chính mà còn mở rộng ra nhiều lĩnh vực khác như bảo hiểm, bất động sản và quản lý dữ liệu. Việc phát triển một ứng dụng web đi kèm để trực quan hóa quá trình xác thực sẽ giúp người dùng dễ dàng hơn trong việc kiểm tra và xác thực hợp đồng. Điều này không chỉ tạo ra một nền tảng an toàn cho người dùng mà còn thúc đẩy sự phát triển của công nghệ blockchain trong tương lai.

Tổng quan nghiên cứu

Trong thập kỷ vừa qua, công nghệ blockchain đã trở thành một trong những đột phá lớn nhất trong lĩnh vực công nghệ thông tin, với tiềm năng thay đổi cách thức vận hành của nhiều ngành công nghiệp. Theo báo cáo của ngành, Ethereum là nền tảng blockchain phổ biến nhất hiện nay, cho phép triển khai các hợp đồng thông minh (smart contracts) tự động thực thi các giao dịch mà không cần bên trung gian. Tuy nhiên, việc đảm bảo tính chính xác và an toàn của các hợp đồng thông minh vẫn là thách thức lớn, khi các lỗ hổng bảo mật có thể dẫn đến thiệt hại hàng triệu đô la, như vụ mất cắp Ether trị giá khoảng 31 triệu USD gần đây. Mục tiêu nghiên cứu của luận văn là phát triển một phương pháp xác thực hợp đồng thông minh Ethereum dựa trên kỹ thuật phân tích tĩnh, kết hợp phân tích cấu trúc ngữ nghĩa và thực thi ký hiệu trên đồ thị dòng điều khiển (CFG). Nghiên cứu tập trung vào các hợp đồng thực hiện các thao tác cơ bản như trao đổi trực tiếp ETH và token giữa người dùng và chủ hợp đồng, trong phạm vi thời gian từ năm 2019 đến 2020 tại Việt Nam. Kết quả nghiên cứu không chỉ nâng cao độ tin cậy của hợp đồng mà còn giúp người dùng phổ thông dễ dàng hiểu và kiểm tra tính chính xác của hợp đồng trước khi thực hiện giao dịch, góp phần tăng cường an toàn trong hệ sinh thái blockchain.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Luận văn dựa trên các lý thuyết và mô hình sau:

• Blockchain và hợp đồng thông minh (Smart Contracts): Blockchain là hệ thống sổ cái phân tán, phi tập trung, đảm bảo tính bất biến và minh bạch của dữ liệu giao dịch. Hợp đồng thông minh là các đoạn mã tự động thực thi trên blockchain khi các điều kiện được đáp ứng, giúp loại bỏ bên trung gian và tăng tính tin cậy.
• Phân tích tĩnh (Static Analysis): Kỹ thuật phân tích mã nguồn mà không cần thực thi chương trình, nhằm phát hiện lỗi và lỗ hổng bảo mật.
• Đồ thị dòng điều khiển (Control-flow Graph - CFG): Biểu diễn đồ họa các đường đi có thể trong chương trình, giúp phân tích luồng điều khiển và các trạng thái của hợp đồng.
• Thực thi ký hiệu (Symbolic Execution): Phân tích chương trình bằng cách sử dụng biến ký hiệu thay vì giá trị cụ thể, nhằm kiểm tra các điều kiện và trạng thái có thể xảy ra trong hợp đồng.
• Cấu trúc ngữ nghĩa (Semantic Structure Analysis): Phân tích cấu trúc logic và ý nghĩa của mã nguồn để hiểu rõ hơn về hành vi của hợp đồng.

Các khái niệm chính bao gồm: trạng thái hợp đồng, hàm gửi token (sendtoken), hàm gửi ether (sendeth), cây cú pháp trừu tượng (AST), và các trạng thái trước-sau giao dịch.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp phân tích tĩnh kết hợp thực thi ký hiệu trên CFG để xác thực hợp đồng thông minh Ethereum. Cụ thể:

• Nguồn dữ liệu: Mã nguồn hợp đồng thông minh viết bằng ngôn ngữ Solidity, tập trung vào các hợp đồng thực hiện trao đổi ETH và token.
• Phương pháp chọn mẫu: Lựa chọn các hợp đồng có cấu trúc và chức năng cơ bản, phù hợp với phạm vi nghiên cứu nhằm đảm bảo tính khả thi và hiệu quả của phương pháp.
• Phương pháp phân tích:
  • Xây dựng cây cú pháp trừu tượng (AST) từ mã nguồn để trích xuất các trạng thái ban đầu.
  • Tạo đồ thị dòng điều khiển (CFG) cho từng hàm trong hợp đồng.
  • Thực thi ký hiệu trên CFG để mô phỏng các trạng thái mới sau khi thực thi hàm.
  • So sánh các trạng thái thu được từ AST và CFG để đánh giá tính chính xác và tin cậy của hợp đồng.
• Timeline nghiên cứu: Nghiên cứu được thực hiện từ tháng 8/2019 đến tháng 6/2020, bao gồm giai đoạn thu thập dữ liệu, phát triển mô hình, triển khai ứng dụng web trực quan hóa và kiểm thử thực tế.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

1. Phương pháp kết hợp phân tích cấu trúc ngữ nghĩa và thực thi ký hiệu trên CFG giúp xác thực hợp đồng hiệu quả: Qua việc xây dựng và so sánh trạng thái hợp đồng trước và sau giao dịch, phương pháp cho phép phát hiện các hành vi không nhất quán hoặc lỗi tiềm ẩn. Ví dụ, trong trường hợp mô phỏng chuyển 30 ether từ địa chỉ A sang B, số dư ether của A giảm từ 100 xuống 70, trong khi B tăng từ 100 lên 130, đồng thời token được chuyển đổi tương ứng, đảm bảo tính đúng đắn của giao dịch.

2. Tính khả thi trong việc hỗ trợ người dùng phổ thông: Phương pháp cung cấp kết quả xác thực dưới dạng các trạng thái logic dễ hiểu, giúp người dùng không chuyên có thể kiểm tra hợp đồng trước khi thực hiện giao dịch, giảm thiểu rủi ro bị lừa đảo hoặc mất tài sản.

3. Ứng dụng thành công trong các hợp đồng trao đổi ETH và token cơ bản: Nghiên cứu giới hạn phạm vi vào các hợp đồng có chức năng trao đổi trực tiếp, với số liệu mô phỏng cho thấy độ chính xác xác thực đạt trên 90% trong các trường hợp thử nghiệm.

4. So sánh với các công cụ hiện có: Các công cụ như Mythril, Manticore hay Securify thường cung cấp báo cáo kỹ thuật phức tạp, khó hiểu với người dùng phổ thông. Phương pháp đề xuất trong luận văn đơn giản hóa kết quả, tập trung vào trạng thái logic và luồng giao dịch, giúp tăng khả năng tiếp cận và ứng dụng thực tế.

Thảo luận kết quả

Nguyên nhân thành công của phương pháp nằm ở việc kết hợp phân tích tĩnh và thực thi ký hiệu trên CFG, cho phép mô phỏng chính xác các trạng thái hợp đồng mà không cần thực thi thực tế trên blockchain, từ đó phát hiện lỗi tiềm ẩn trước khi triển khai. Kết quả này phù hợp với các nghiên cứu gần đây về xác thực hợp đồng thông minh, đồng thời khắc phục hạn chế về độ phức tạp và khó hiểu của báo cáo xác thực truyền thống.

Việc trình bày dữ liệu qua biểu đồ trạng thái trước và sau giao dịch, cũng như bảng so sánh số dư ether và token giữa các địa chỉ, giúp minh họa rõ ràng quá trình xác thực. Điều này không chỉ nâng cao độ tin cậy của hợp đồng mà còn tăng cường sự tin tưởng của người dùng vào công nghệ blockchain.

Tuy nhiên, phạm vi nghiên cứu còn hạn chế ở các hợp đồng đơn giản, chưa bao gồm các hợp đồng phức tạp với nhiều chức năng và tương tác đa chiều. Đây là hướng phát triển tiếp theo để mở rộng ứng dụng của phương pháp.

Đề xuất và khuyến nghị

1. Phát triển công cụ xác thực hợp đồng thông minh thân thiện với người dùng: Thiết kế giao diện trực quan, đơn giản hóa báo cáo xác thực để người dùng phổ thông có thể dễ dàng kiểm tra hợp đồng trước khi giao dịch, nhằm giảm thiểu rủi ro mất tài sản. Thời gian thực hiện: 6-12 tháng; Chủ thể: các nhóm phát triển phần mềm blockchain.

2. Mở rộng phạm vi xác thực cho các hợp đồng phức tạp: Nghiên cứu và áp dụng kỹ thuật phân tích tĩnh và thực thi ký hiệu cho các hợp đồng đa chức năng, tương tác phức tạp nhằm nâng cao độ bao phủ và hiệu quả xác thực. Thời gian thực hiện: 12-18 tháng; Chủ thể: các viện nghiên cứu và doanh nghiệp công nghệ.

3. Tăng cường đào tạo và phổ biến kiến thức về xác thực hợp đồng thông minh: Tổ chức các khóa học, hội thảo nhằm nâng cao nhận thức và kỹ năng cho nhà phát triển và người dùng về tầm quan trọng của xác thực hợp đồng. Thời gian thực hiện: liên tục; Chủ thể: các trường đại học, tổ chức đào tạo.

4. Hợp tác với các tổ chức kiểm toán và bảo mật blockchain: Thiết lập quy trình kiểm tra và xác thực hợp đồng trước khi triển khai trên các nền tảng blockchain lớn, nhằm đảm bảo an toàn và giảm thiểu rủi ro cho hệ sinh thái. Thời gian thực hiện: 6 tháng; Chủ thể: các công ty kiểm toán, tổ chức bảo mật.

Đối tượng nên tham khảo luận văn

1. Nhà phát triển hợp đồng thông minh: Nghiên cứu cung cấp phương pháp xác thực giúp phát hiện lỗi và lỗ hổng trước khi triển khai, nâng cao chất lượng sản phẩm.

2. Người dùng phổ thông và nhà đầu tư blockchain: Giúp hiểu và kiểm tra tính chính xác của hợp đồng trước khi thực hiện giao dịch, giảm thiểu rủi ro mất tài sản.

3. Các tổ chức kiểm toán và bảo mật: Cung cấp cơ sở lý thuyết và công cụ hỗ trợ trong việc đánh giá an toàn hợp đồng thông minh.

4. Nhà nghiên cứu và sinh viên ngành khoa học máy tính, công nghệ blockchain: Là tài liệu tham khảo về kỹ thuật phân tích tĩnh, thực thi ký hiệu và ứng dụng trong xác thực hợp đồng thông minh.

Câu hỏi thường gặp

1. Phân tích tĩnh là gì và tại sao quan trọng trong xác thực hợp đồng thông minh?
   Phân tích tĩnh là kỹ thuật kiểm tra mã nguồn mà không cần thực thi chương trình, giúp phát hiện lỗi và lỗ hổng bảo mật sớm. Điều này rất quan trọng để đảm bảo hợp đồng không chứa các lỗi nghiêm trọng trước khi triển khai trên blockchain.

2. Thực thi ký hiệu hoạt động như thế nào trong việc xác thực hợp đồng?
   Thực thi ký hiệu sử dụng biến ký hiệu thay vì giá trị cụ thể để mô phỏng tất cả các đường đi có thể trong hợp đồng, từ đó phát hiện các điều kiện gây lỗi hoặc hành vi không mong muốn.

3. Phương pháp này có áp dụng được cho các hợp đồng phức tạp không?
   Hiện tại, nghiên cứu tập trung vào các hợp đồng cơ bản với chức năng trao đổi ETH và token. Tuy nhiên, phương pháp có thể được mở rộng để xử lý các hợp đồng phức tạp hơn trong tương lai.

4. Làm thế nào người dùng phổ thông có thể sử dụng kết quả xác thực?
   Phương pháp cung cấp kết quả dưới dạng trạng thái logic dễ hiểu, giúp người dùng không chuyên có thể kiểm tra tính chính xác của hợp đồng trước khi thực hiện giao dịch, tránh rủi ro bị lừa đảo.

5. So sánh với các công cụ xác thực hiện có, phương pháp này có ưu điểm gì?
   Khác với các công cụ hiện tại thường cung cấp báo cáo kỹ thuật phức tạp, phương pháp này đơn giản hóa kết quả, tập trung vào trạng thái logic và luồng giao dịch, giúp người dùng phổ thông dễ dàng tiếp cận và hiểu được.

Kết luận

• Đã phát triển thành công phương pháp xác thực hợp đồng thông minh Ethereum dựa trên phân tích tĩnh kết hợp thực thi ký hiệu trên CFG, giúp phát hiện lỗi và đảm bảo tính chính xác của hợp đồng.
• Phương pháp cung cấp kết quả dễ hiểu, phù hợp với người dùng không chuyên, góp phần nâng cao an toàn trong giao dịch blockchain.
• Nghiên cứu tập trung vào các hợp đồng thực hiện trao đổi ETH và token cơ bản, với độ chính xác xác thực trên 90% trong thử nghiệm.
• Đề xuất mở rộng phạm vi nghiên cứu và phát triển công cụ hỗ trợ người dùng phổ thông trong tương lai.
• Khuyến khích các tổ chức, nhà phát triển và người dùng áp dụng phương pháp để tăng cường bảo mật và tin cậy cho hệ sinh thái blockchain.

Hành động tiếp theo: Triển khai ứng dụng web trực quan hóa kết quả xác thực, mở rộng nghiên cứu cho các hợp đồng phức tạp và tổ chức đào tạo nâng cao nhận thức về an toàn hợp đồng thông minh.