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

Luận văn thạc sĩ nghiên cứu máy tính xác thực hợp đồng thông minh bằng kỹ thuật phân tích tĩnh, đánh giá hiện trạng, phân tích vấn đề, đề xuất biện pháp hoàn thiện trong lĩnh vực

• 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

Mục lục chi tiết

• 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

Tóm tắt

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.

Nội dung chính

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.

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.

Trích đoạn nội dung tài liệu

ĐẠI HỌC QUỐC GIA TP. HCM TRƯỜNG ĐẠI HỌC BÁCH KHOA -------------------- BĂNG NGỌC BẢO TÂM XÁC THỰC HỢP ĐỒNG THÔNG MINH BẰNG KỸ THUẬT PHÂN TÍCH TĨNH Chuyên ngành: KHOA HỌC MÁY TÍNH Mã số: 8.01 LUẬN VĂN THẠC SĨ TP. HỒ CHÍ MINH, tháng 08 năm 2020 CÔNG TRÌNH ĐƯỢC HOÀN THÀNH TẠI TRƯỜNG ĐẠI HỌC BÁCH KHOA – ĐHQG – HCM Cán bộ hướng dẫn khoa học: PGS. Quản Thành Thơ Cán bộ chấm nhận xét 1: PGS.

TS Huỳnh Tường Nguyên Cán bộ chấm nhận xét 2: TS. Trần Thanh Tùng Luận văn thạc sỹ được bảo vệ tại Trường Đại học Bách Khoa, ĐHQG Tp.HCM ngày 18 tháng 08 năm 2020. Thành phần Hội đồng đánh giá luận văn thạc sỹ gồm: 1. Chủ tịch: PGS.

TS Trần Văn Hoài 2. Nguyễn Lê Duy Lai 3. Phản biện 1: PGS. TS Huỳnh Tường Nguyên 4.

Phản biện 2: TS. Trần Thanh Tùng 5. Ủy viên: TS. Nguyễn Văn Sinh Xác nhận của Chủ tịch Hội đồng đánh giá LV và Trưởng Khoa quản lý chuyên ngành sau khi luận văn đã được sửa chữa (nếu có).

CHỦ TỊCH HỘI ĐỒNG TRƯỞNG KHOA KH&KTM i ĐẠI HỌC QUỐC GIA TP.HCM CỘNG HÒA XÃ HỘI CHỦ NGHĨA VIỆT NAM TRƯỜNG ĐẠI HỌC BÁCH KHOA Độc lập - Tự do - Hạnh phúc NHIỆM VỤ LUẬN VĂN THẠC SĨ Họ tên học viên: Băng Ngọc Bảo Tâm MSHV: 1870378 Ngày, tháng, năm sinh: 06/11/1996 Nơi sinh: Tp.HCM Chuyên ngành: Khoa học máy tính Mã số: 8480101 I. TÊN ĐỀ TÀI: Xác thực hợp đồng thông minh bằng kỹ thuật phân tích tĩnh. NHIỆM VỤ VÀ NỘI DUNG: Nghiên cứu các phương pháp phân tích tĩnh và cấu trúc của hợp đồng thông minh để đưa ra các giải pháp xác thực đúng đắn. Xây dựng một ứng dụng web đi kèm để trực quan hóa đề tài, đồng thời kiểm tra tính chính xác của giải pháp đề xuất đối với các ứng dụng thực tế.

NGÀY GIAO NHIỆM VỤ: 19/08/2019 IV. NGÀY HOÀN THÀNH NHIỆM VỤ: 07/06/2020 V. CÁN BỘ HƯỚNG DẪN: PGS. Quản Thành Thơ Tp.

HCM, ngày 03 tháng 08 năm 2020 CÁN BỘ HƯỚNG DẪN CHỦ NHIỆM BỘ MÔN ĐÀO TẠO (Họ tên và chữ ký) (Họ tên và chữ ký) TRƯỞNG KHOA KH&KTMT (Họ tên và chữ ký) Ghi chú: Học viên phải đóng tờ nhiệm vụ này vào trang đầu tiên của tập thuyết minh LV ii Acknowledgments I would like to extend thanks to the many people, who so generously contributed to the work presented in this thesis report. Special mention goes to my supervisor, Prof. Quan Thanh Tho. My master course is an amazing experience, he always help me when I am in troubles.

Moreover, I also thanks to Mr. Nguyen Huu Hoang and other faculties wholeheartedly. I am very appreciated for their support, not only about the tremendous academic guide but also for giving me so many wonderful opportunities and important advises. Profound gratitude goes to all members in the group of Professor Tho for their whole- hearted support.

Ho Chi Minh City, 03 August 2020 iii Declaration I, Bang Ngoc Bao Tam, declare that my thesis, "Verification of Ethereum Smart Con- tracts: A Model Checking Approach" and the work presented in it are my own. I confirm that: • This work was done wholly or mainly while in candidature for a master by research degree at this University. • Where any part of this thesis has previously been submitted for a degree or any other qualification at this University or any other institution, this has been clearly stated. • Where I have consulted the published work of others, this is always clearly attributed.

• Where I have quoted from the work of others, the source is always given. With the exception of such quotations, this thesis is entirely my own work. • I have acknowledged all of the main sources of help. Ho Chi Minh City, 03 August 2020 iv Abstract (English) This decade has already witnessed an extraordinary evolution in the technology and computing ecosystem.

Technology innovation and its impact are already running very high. From Internet of Things to Artificial Intelligence to Blockchain. Each of them has a disruptive force within multiple industries and Blockchain is termed as one of the most disruptive technologies of today [30]. So much so, Blockchain has the potential to change almost every industry today and its working [21].The applicability of Blockchain because of its advantages and pervasiveness has already picked up stream and seems like it will continue to long time to come.

Blockchain is not a new technology however it has gained super momentum in the last couple of years. "It is a big leap forward in terms of things about decentralized and distributed applica- tions. It is about thinking of current architectural landscape and strategizing to move towards immutable distributed databases" [21]. The advantages and many helping organizations reach out to their stakeholders without requiring any central authority and intermediaries.

While the first generation of blockchain was designed only to solve cryptocurrencies problems, Ethereum, one of the most popular current systems, focuses on imple- menting decentralized computing approaches [5]. One new prominent of these reliable platforms is to enable smart contract, which can automatically execute on the blockchain and enforce by the consensus protocol. These properties help smart contracts allow the performance of credible transactions without third parties. Thus, smart contracts are likely to apply in a wide range of fields including ownership of copyrights, financial instruments, document existence and asset tracking for the IoT.

However, only the correctness of executions is not sufficient to keep smart contracts secure. In fact, adversaries may take advantage of undocumented methods and ex- ploit potential bugs as well as vulnerabilities in the contracts, which can cause harm to users. More recently, $31M worth of Ether was stolen due to a critical security bug in a digital wallet contract. Hence, verifying smart contract behaviors and solving security issues are extremely crucial and challenging when blockchain technologies evolve with much diversity v Abstract across their ecosystems.

However, current security-verifying programs tend to provide many technical details which are pretty hard for normal people to understand briefly. To tackle this problem, we designed a process aiming to mitigate these limitations, with our key insight being a combination of semantic structure analysis and sym- bolic execution on control-flow graphs (CFG for short). This article proposes a new approach for verification Ethereum smart contracts, applying this technique would benefit for average users without any technical knowledge. Keywords: Ethereum smart contracts, Semantic structure analysis, Symbolic execu- tion, Control-flow graph.

vi Abstract (Vietnamese) Trong thập kỷ vừa qua đã đã đánh dấu một cột mốc phát triển vượt bật của các ngành, nghề, lĩnh vực về công nghệ, và đặc biệt là các hệ thống máy tính. Từ nền tảng Kết nối vạn vật (IoT), Trí tuệ nhân tạo cho đến Blockchain, đã góp phần đổi mới nền công nghệ hiện tại, tạo tiền đề để thúc đẩy công cuộc cách mạng công nghiệp 4. Tất cả các nền tảng công nghệ kể trên đều đạt được những đột phá nhất định trong nhiều lĩnh vực, tuy nhiên, Blockchain vẫn được đánh là một trong những công nghệ đột phá nhất hiện nay [1]. Blockchain có đủ tiềm năng để thay đổi sự vận hành, cách thức giao dịch, lưu trữ dữ liệu,.

của hầu hết mọi ngành công nghiệp ngày nay [2]. Bởi vì những lợi thế cũng như sự phổ biến của nó mà khả năng ứng dụng của Blockchain dường như sẽ còn tiếp tục phát triển trong nhiều lĩnh vực hơn nữa. Blockchain tuy không phải là một công nghệ mới, nhưng nó đã gặt hái được nhiều kết quả, thêm nhiều động lực để nâng tầm vị thế trong vài năm qua. “Đó là một bước tiến lớn trong mọi mặt về các ứng dụng phân tán và phi tập trung.

Là sự thay đổi trong suy nghĩ về tổng thể kiến trúc hiện tại và chiến lược để hướng tới cơ sở dữ liệu phân tán bất biến” [2]. Một ví dụ cụ thể để minh họa cho lợi ích của các ứng dụng phân tán là các tổ chức hoặc cá nhân có thể dễ dàng tiếp cận với các bên liên quan của họ mà không cần bất kỷ yếu tố trung gian nào và vẫn đáp ứng được các yêu cầu, quyền lợi đôi bên. Trong khi các thế hệ blockchain đầu tiên được thiết kế chỉ để giải quyết các vấn đề về tiền điện tử thì Ethereum, một trong những nền tảng phổ biến nhất trong thời gian trở lại đây, được tạo ra để tiếp cận các phương pháp giải quyết cho các hệ thống, ứng dụng phi tập trung [3]. Một điểm quan trọng đáng lưu ý của các nền tảng xác thực này là nó cho phép thực hiện các giao dịch thông qua hợp đồng thông minh.

Toàn bộ hoạt động của hợp đồng thông minh được thực hiện một cách tự động và không có sự can thiệp từ bên ngoài, hay thông qua một bên thứ ba trung gian mà chỉ dựa vào các ràng buộc được định nghĩa sẵn bên trong hợp đồng. Do đó, hợp đồng thông minh có khả năng áp dụng trong rất nhiều lĩnh vực bao gồm xác thực bản quyền, công việc về tài chính, truy vết dữ liệu,. Tuy nhiên, chỉ dựa vào tính chính xác trong quá trình thực thi là không đủ để giữ an toàn cho các hợp đồng thông minh. Trong thực tế, các viii Abstract kẻ xấu có thể lợi dụng các phương pháp chưa được biết đến và khai thác các lỗi tiềm ẩn cũng như các lỗ hổng trong hợp đồng.

Điều đó có thể gây ra hậu quả to lớn cho người dùng. Cũng trong khoảng thời gian gần đây, một số lượng lớn Ether (trị giá khoảng 31 triệu đô la) đã bị đánh cắp do một lỗi nghiêm trọng liên quan đến bảo mật vấn đề bảo mật của ví điện tử. Qua đó có thể thấy rằng, việc xác thực các hành vi hợp đồng thông minh và giải quyết các vấn đề bảo mật là vô cùng cần thiết, những cũng đặt ra rất nhiều khó khăn, thách thức khi các công nghệ blockchain ngày càng phát triển với một số lượng lớn các hệ sinh thái đi kèm. Tuy nhiên, các giao thức xác thực hiện tại dường như đưa ra quá nhiều chi tiết kỹ thuật.

Điều đó có thể khiển cho một phần lớn người dùng chưa có nhiều kiến thức về mảng này sẽ không thể hiểu hết được. Để khắc phục nhược điểm này, chúng tôi thiết kế một mô hình với ý tưởng chính là thực hiện phân tích tĩnh trên đồ thị dòng điều khiển. Bài luận này đề xuất một hướng tiếp cận hoàn toàn mới trong việc xác thực hợp đồng thông minh. Áp dụng mô hình này sẽ đem lại nhiều lợi ích nhiều hơn cho người dùng, kể cả những người không có kiến thức về công nghệ thông tin.

ii viii Contents Acknowledgments iii Declaration iv Abstract (English) v Abstract (Vietnamese) vii List of Figures xii List of Tables xiv 1 INTRODUCTION 1 1.3 Verification of Smart Contracts .6 Scope of this research .1 The pilot study I: Verification of Ethereum Smart Contracts: An Model Checking Approach .2 The pilot study II: An Intelligent Chatbot for Automatic Verifica- tion of Ethereum Smart Contracts. 8 2 LITERATURE SURVEY 9 3 RESEARCH BACKGROUND 10 3.2 How does a Blockchain work? .2 Is Blockchain Secure ? .1 Proof of Work .2 Proof of Stake .4 What is Blockchain good for? .5 Ethereum Smart Contracts .2 Ethereum Smart Contracts structures: .