Ứng dụng Chatbot thông minh trong việc xác thực hợp đồng thông minh Ethereum

Chia sẻ: _ _ | Ngày: | Loại File: PDF | Số trang:7

Thêm vào BST

Báo xấu

41
lượt xem 3
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Bài viết trình bày tập trung hướng nghiên cứu của mình vào việc tích hợp với chatbot thông minh cùng với thực thi Symbolic Execution để xác minh các hợp đồng thông minh Ethereum. Thông qua trò chuyện với người dùng, chatbot đóng vai trò là một đại diện trung gian nắm bắt ý định của người dùng, dẫn dắt và lấy các thông tin cần thiết cho việc xác thực.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Ứng dụng Chatbot thông minh trong việc xác thực hợp đồng thông minh Ethereum

Kỷ yếu Hội nghị KHCN Quốc gia lần thứ XIII về Nghiên cứu cơ bản và ứng dụng Công nghệ thông tin (FAIR), Nha Trang, ngày 8-9/10/2020 DOI: 10.15625/vap.2020.00221 ỨNG DỤNG CHATBOT THÔNG MINH TRONG VIỆC XÁC THỰC HỢP ĐỒNG THÔNG MINH ETHEREUM Băng Ngọc Bảo Tâm, Trần Quang, Quản Thành Thơ Đại Học Bách khoa Thành phố Hồ Chí Minh bnbaotam@hcmut.edu.vn, tranquang@hcmut.edu.vn, qttho@hcmut.edu.vn TÓM TẮT: Hợp đồng thông minh Ethereum hoạt động dựa trên nền tảng công nghệ Blockchain là một trong những ứng dụng mạnh mẽ và đầy hứa hẹn sẽ cung cấp một nền tảng giao dịch phi tập trung, hỗ trợ tất cả các lĩnh vực trong đời sống. Bên cạnh đó, các hợp đồng thông minh sau khi được triển khai trên hệ thống sẽ hoạt động theo cơ chế phân tán, không thể thay đổi và được truy cập công khai. Điều đó khiến chúng rất dễ bị tấn công bởi nhiều hình thức tấn công khác nhau và yếu tố bảo mật cho các hợp đồng thông minh được đặt lên hàng đầu. Trong bài viết này, chúng tôi tập trung hướng nghiên cứu của mình vào việc tích hợp với chatbot thông minh cùng với thực thi Symbolic Execution để xác minh các hợp đồng thông minh Ethereum. Thông qua trò chuyện với người dùng, chatbot đóng vai trò là một đại diện trung gian nắm bắt ý định của người dùng, dẫn dắt và lấy các thông tin cần thiết cho việc xác thực. Sau đó, chúng tôi dùng Symbolic Execution để xác minh xem các hợp đồng thông minh này có thực sự phản ánh ý định của người dùng mà không có lỗi bảo mật hay không. Cần lưu ý rằng khi hợp đồng thông minh thực thi, thông tin sẽ được ghi vào blockchain và không thể sửa đổi sau đó. Do đó, việc xác minh biểu tượng của hợp đồng thông minh mà không thực thi nó trong tình huống này là rất quan trọng. Ngoài ra, phương pháp của chúng tôi còn giúp cho người dùng không có nhiều kiến thức về lĩnh vực này vẫn có thể hiểu được một cách dễ dàng. Từ khóa: Intelligence chatbot, smart contracts, control-flow graph, Symbolic Execution. I. GIỚI THIỆU Blockchain tuy không phải là một công nghệ mới nhưng nó đã đạt được nhiều thành tựu to lớn trong thập kỷ này. Đây là một bước tiến vượt bậc trong các hệ thống phi tập trung và các ứng dụng phân tán. Để loại bỏ sự cần thiết của các bên thứ ba, blockchain được phát triển để hoạt động trên một mạng ngang hàng và dựa vào các thuật toán đồng thuận thực hiện các giao dịch mua bán. Một điểm nổi bật mới trên các nền tảng này là cho phép sự hoạt động các hợp đồng thông minh, hợp đồng có thể tự động thực thi trên blockchain khi đã thỏa mãn tất cả các điều khoản bên trong [1]. Tuy nhiên, thật khó để tạo ra các hợp đồng thông minh mà không vướng phải các lỗi bảo mật. Hơn nữa, ngoài tính bảo mật, do đã bỏ qua các bên trung gian, nên chúng ta cần thêm yêu cầu tính đúng đắn của các quá trình thực thi, để giữ cho các hợp đồng thông minh an toàn hơn. Bên cạnh đó, 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 và tìm ra đúng những thông tin mà mình cần. Trong thời đại mà trí tuệ nhân tạo ngày càng thay đổi dần cách làm việc của con người thì không thể không kể đến Chatbot. Chatbot là một phần mềm trí tuệ nhân tạo có thể giao tiếp với con người. Bạn có thể trò chuyện thông qua giọng nói, văn bản hoặc thậm chí giao diện đồ họa. Hơn nữa, một chatbot thông minh có thể hiểu ngôn ngữ của chúng ta và có thể học hỏi từ các cuộc trò chuyện với người dùng của họ. II. CÔNG TRÌNH LIÊN QUAN Nhiều ứng dụng phi tập trung hoạt động xoay quanh hợp đồng thông minh đã triển khai các công cụ phần mềm khác nhau nhằm hỗ trợ việc xác thực các dạng hợp đồng này. Những công cụ này, chẳng hạn như kiểm tra tự động mã nguồn cho các lỗ hổng, có thể được sử dụng như một phần bổ sung, nhưng không nên thay thế quy trình đánh giá chính thức. Một số công cụ khác, như là Mythril [2], có thể được sử dụng để phát hiện “overflows” và “underflows”. Một công cụ khác là Etherscrape [2], hoặc, Securify có thể phân tích các lỗi bảo mật của các hợp đồng ở mức bytecode thông qua phân tích ngữ nghĩa [3], trong khiSmartCheck dùng để phân tích ngữ nghĩa hợp đồng cũng như từ vựng và cú pháp [4]. Tuy nhiên, để xác thực một hợp đồng thông minh đơn giản có giá khoảng 4000$. Còn đối với các hợp đồng thông minh phức tạp và nâng cao hơn thì giá có thể từ 50.000$, và thậm chí lên đến 100.000$. Ngoài ra, việc xác thực một hợp đồng thông minh thường sẽ kéo dài 4 tuần và sau đó phải mất 8 tuần để quá trình đánh giá hoàn thành [5]. Một điều đáng chú ý là cho dù bản báo cáo có chi tiết như thế nào thì nếu người dùng không am hiểu về kỹ thuật, họ có thể không hiểu kết quả xác thực hợp đồng thông minh và tìm ra những thông tin họ muốn ngay cả khi họ đọc báo cáo một cách cẩn thận III. KIẾN THỨC NỀN TẢNG A. Chatbot thông minh Chatbot thông minh là một chương trình kết hợp với trí tuệ nhân tạo hay các kỹ thuật xử lý ngôn ngữ tự nhiên để tương tác với con người. Chatbot thông minh có khả năng mô phỏng cuộc trò chuyện tự nhiên của con người. Người dùng giao tiếp với chatbot thông qua giao diện trò chuyện hoặc bằng giọng nói, giống như cách họ nói chuyện với một người thực trong cuộc sống.
Băng Ngọc Bảo Tâm, Trần Quang, Quản Thành Thơ 629 B. Blockchain và hợp đồng thông minh Blockchain là hệ thống cơ sở dữ liệu cho phép lưu trữ và truyền tải các khối tin (có thể hiểu là các giao dịch trong thực tế) được mã hóa và liên kết với nhau. Các khối tin này hoạt động độc lập và minh bạch đối với tất cả mọi người. Do đặc tính của Blockchain mà các khối thông tin này được lưu giữ bởi tất cả những người tham gia hệ thống chứ không tập trung tại một cơ sở dữ liệu nào [6]. Và khi một khối thông tin được ghi vào hệ thống Blockchain thì không có cách nào thay đổi được mà chỉ có thể bổ sung thêm khi đạt được sự đồng thuận của tất cả mọi người. Mục đích chính của hợp đồng thông minh là tự thực thi dựa trên các quy luật cụ thể được viết trên mã nguồn của chúng khi tất cả các điều kiện đều thỏa mãn. Hợp đồng thông minh hoạt động bằng cách tuân theo các câu lệnh điều kiện đơn giản "nếu... thì ..." được phát triển thành mã trên blockchain. Một mạng lưới các hệ thống/máy tính sẽ không thực hiện các hành động được mã hóa trong hợp đồng thông minh như giải phóng tiền cho bên phù hợp, phát hành token,... khi các điều kiện định trước chưa được đáp ứng [7]. Sau khi thực hiện hợp đồng thông minh đó, trạng thái của blockchain được cập nhật và công khai với tất cả thành viên tham gia trên hệ thống. Trong đề tài này, chúng tôi chọn nền tảng Ethereum bởi vì đây được xem như là nền tảng hỗ trợ tốt nhất cho hợp đồng thông minh tính đến thời điểm hiện tại. IV. GIẢI PHÁP ĐỀ XUẤT Phân tích và phát hiện các vấn đề bảo mật trong việc thiết kế và thực hiện các hợp đồng thông minh trên nền tảng phi tập trung là mục tiêu chính của chúng tôi trong bài viết này. Tuy nhiên, chúng tôi cũng tập trung vào việc dẫn dắt người dùng để xác định những điều họ muốn, cung cấp các thông tin cụ thể, rõ ràng và dễ hiểu về việc xác thực hợp đồng thông minh cho cả những người dùng không am hiểu về công nghệ. Cách tiếp cận của chúng tôi để giải quyết vấn đề trên bao gồm 5 bước như sau: 1. Đầu tiên, chatbot của chúng tôi sẽ trò chuyện với người dùng để tìm ra yêu cầu của họ thông qua các ý định và các thực thể đã được huấn luyện bằng mô hình học có giám sát. Từ đó, dẫn dắt câu chuyện để họ cung cấp các thông tin một cách tự nhiên, sau đó trích xuất các thông tin đó cho các bước tiếp theo. 2. Chúng tôi cũng định nghĩa một vài trạng thái để biểu diễn kết quả của giao dịch nếu như nó xảy ra theo các ngữ nghĩa thông thường và dễ hiểu. 3. Dựa trên hợp đồng thông minh mà người dùng cung cấp, chúng tôi tổ chức và phân loại các trường nội dung bên trong. Sau đó tiến hành phân tích để xây dựng các đồ thị luồng điều khiển, thể hiện quá trình vận hành của từng thành phần bên trong hợp đồng. 4. Tiếp theo, dựa trên thông tin từ các đồ thị luồng điều khiển, chúng tôi chỉ lấy các thành phần quan trọng để xử lý và vẫn giữ các kết nối đến các thành phần khác trong đồ thị. Sau đó, tiến hành phân tích luồng điều khiển và luồng dữ liệu của các phương pháp dựa trên các đồ thị này mà vẫn tạo ra được các kết nối, các mối quan hệ phụ thuộc có thể xảy ra giữa các đối tượng và các lệnh gọi hàm cần thiết để hiện thực từng phương pháp này. 5. Cuối cùng, chúng tôi so sánh các kết quả trạng thái thu được ở bước 2 dựa trên các ngữ nghĩa thông thường và bước 4 khi tiến hành symbolic execution. Nếu các trạng thái hoàn toàn khớp với nhau, thì chúng tôi có thể tự tin thông báo với người dùng là hợp đồng thông minh này hoàn toàn không có gian lận và người dùng có thể giao dịch thông qua hợp đồng này. Và ngược lại, hợp đồng này không đáng tin cậy và người dùng không nên tiếp tục giao dịch. Luồng thực thi của giải pháp xác thực hợp đồng thông minh đề xuất
630 ỨNG DỤNG CHATBOT THÔNG MINH TRONG VIỆC XÁC THỰC HỢP ĐỒNG THỒNG MINH ETHEREUM V. CHI TIẾT PHƢƠNG PHÁP ĐỀ XUẤT VÀ KẾT QUẢ Trong Chương này, chúng tôi sẽ trình bày chi tiết hơn về các giải thuật mà chúng tối đã đề xuất ở chương trước trong việc dùng chatbot thông minh để xác thực hợp đồng thông minh Ethereum. A. Chatbot Hệ thống gồm 3 khối chính: chatbot, cơ sở dữ liệu và giao diện lập trình ứng dụng. Chatbot chịu trách nhiệm phát hiện ý định của người dùng, từ đó lấy thông tin cần thiết từ cơ sở dữ liệu và hệ thống gọi các giao diện lập trình ứng dụng, tổng hợp lại và trả thông tin thích hợp về cho người dùng. Phần xử lý ngôn ngữ tự nhiên (NLU): Xử lý nội dung các đoạn hội thoại do người dùng nhập vào dựa trên dữ liệu đã được huấn luyện. Phân loại ý định (intent classification): Xác định ý định của người dùng dựa trên những ý định đã được học. Trích xuất thực thể (entity extraction): phát hiện và trích xuất những dữ liệu có cấu trúc. Phần trung tâm xử lý: Dựa trên học máy để dự đoán hành động tiếp theo dựa trên dữ liệu từ NLU, lịch sử cuộc hội thoại và dữ liệu huấn luyện. Các thành phần quan trọng của chatbot thông minh. B. Xây dựng cây cú pháp trừu tượng Chúng tôi tự định nghĩa một cấu trúc chương trình bao gồm các cú pháp và ngữ nghĩa theo cách hiểu thông thường để dựa vào cấu trúc ấy, chúng tôi có thể tạo ra cây cú pháp trừu tượng [8] phục vụ cho yêu câu bài toán dựa trên ngôn ngữ không phụ thuộc ngữ cảnh. Sau đó chúng tôi tiến hành duyệt cây cú pháp trừu tượng này (chương trình → hàm → tham số). Kết quả cuối cùng của chúng tôi là một tập hợp tất cả các trạng thái của một giao dịch theo cách hiểu thông thường và kết quả này có thể được sử dụng để so sánh trong các bước sau. Ví dụ: chúng tôi phát triển một hệ thống để giao dịch giữa token và ether thông qua hợp đồng thông minh. Do đó, chúng tôi xây dưng một số cú pháp đơn giản như: AMOUNT, chỉ có giá trị số hoặc ADDRESS, một chuỗi ký tự bắt đầu bằng “0x” và theo sau đó là một chuỗi khác bao gồm số, các ký tự từ “a” đến “f” (kể cả ký tự viết hoa). Ngoài ra, chúng tôi định nghĩa hai cú pháp quan trọng để thực hiện giao dịch, đầu tiên là sendtoken (, , ); và thứ hai là sendeth (, < địa chỉ người nhận >, < số lượng ether >); Với mục đích như sau: sendtoken: Gửi một số lượng token từ địa chỉ người gửi đến địa chỉ người nhận. sendeth: Gửi một số lượng ether từ địa chỉ người gửi đến địa chỉ người nhận.
Băng Ngọc Bảo Tâm, Trần Quang, Quản Thành Thơ 631 Ngôn ngữ không phụ thuộc ngữ cảnh của 2 lệnh: sendeth và sendtoken. Két quả sau khi tiến hành duyệt cây trú pháp trừu tượng để sinh ra các trạng thái sau khi giao dịch thành công. Cụ thể, trong bài toán này sẽ có hai giá trị ban đầu là: 0xAAAA(100,1): Người giữ tài khoản có địa chỉ 0xAAAA có 100 ether và 1 token 0xBBBB(100,1): Người giữ tài khoản có địa chỉ 0xBBBB có 100 ether và 1 token Sau khi thực hiện sendeth (0xAAAA, 0xBBBB, 30), thì số dư của 0xAAAA giảm đi 70 ether trong khi lượng ether của địa chỉ 0xBBBB tăng từ 100 lên 130. Sau đó, trạng thái cuối cùng chỉ ra rằng 0xBBBB chuyển 1 token sang tài khoản của 0xAAAA bằng cách gọi sendtoken (0xBBBB, 0xAAAA, 1). C. Sinh ra đồ thị dòng điều khiển (CFG) dựa trên hợp đồng thông minh Trong khoa học máy tính, đồ thị luồng điều khiển [9] là đồ thị biểu diễn tất cả các đường đi có thể được duyệt qua của một chương trình trong quá trình thực thi. Nhiều kỹ thuật phân tích tĩnh dùng để tiếp cận nhằm tối ưu hóa hoặc xác minh ngữ nghĩa của chương trình đều thông qua các đồ thị này. Dựa vào ví dụ ở phần B, trong bước này, chúng tôi xây dựng các hợp đồng thông minh thực hiện việc giao dịch ether và token. Tuy nhiên, để đơn giản hóa vấn đề, chúng tôi giả sử khởi tạo hai đối tượng A và B với 100 ether và 1 token cho mỗi tài khoản. Các phương thức sendeth và sendtoken thực hiện để chuyển lượng ether từ A sang B và lượng token từ B sang A. pragma solidity ^0.5.8; contract SimpleContract { uint etherA = 100; uint etherB = 100; uint tokenA = 1; uint tokenB = 1; bool check = false; function sendeth(uint amountE) public returns (string memory) { if (etherA > amountE) { etherA = etherA - amountE; etherB = etherB + amountE; check = true; return "Success"; }
632 ỨNG DỤNG CHATBOT THÔNG MINH TRONG VIỆC XÁC THỰC HỢP ĐỒNG THỒNG MINH ETHEREUM else return "Fail"; } function sendtoken(uint amountT) public returns(string memory) { if (tokenB > amountT && check = true) { tokenB = tokenB - amountT; tokenA = tokenA + amountT; return "Success"; } else return "Fail"; } } Đồ thị luồng điều khiển của hàm sendeth. D. Tiến hành Symbolic Execution Symbolic Execution [10] là một kỹ thuật phân tích chương trình để xác định kết quả của chương trình ứng với các dữ liệu đầu vào khác nhau trước khi thực thi chương trình. Kỹ thuật này giả định các giá trị tượng trưng cho các đầu vào thay vì nhận được các giá trị đầu vào thực tế như việc thực thi bình thường của chương trình. Do đó, các biểu thức kết quả sẽ ở dạng các ký hiệu cùng với các ràng buộc về các ký hiệu đó đối với các kết quả có thể có ở mỗi nhánh điều kiện.
Băng Ngọc Bảo Tâm, Trần Quang, Quản Thành Thơ 633 Ví dụ: chúng ta sẽ tiến hành phân tích hàm sendeth để hiểu rõ hơn về cơ chế hoạt động của symbolic execution. Nhiệm vụ của hàm sendeth là đọc giá trị amountE và trả về “Fail” nếu số lượng etherA > amountE. Ngược lại, trả về “Success”. Trong quá trình symbolic execution, các biến sẽ được ánh xạ thành các giá trị biểu tượng (ví dụ, số lượng E được gán cho α, etherA thành β và etherB thành θ). Khi đến câu lệnh if, α, β có thể nhận bất kỳ giá trị nào, và do đó, việc thực thi biểu tượng có thể tiến hành dọc theo cả hai nhánh, bằng cách phân ra hai đường. Mỗi đường đi được gán một bản sao của trạng thái chương trình tại lệnh rẽ nhánh cũng như một ràng buộc đường dẫn. Trong ví dụ này, ràng buộc đường dẫn là β > α đối với nhánh then và β ≤ α đối với nhánh còn lại. Cả hai đường dẫn đều có thể được thực thi một cách độc lập. Khi đến các vị trí kết thúc, nó sẽ tính giá trị cụ thể cho α, β bằng cách giải quyết các ràng buộc tích lũy trên mỗi đường đi. Thực thi symbolic execution đối với hàm sendeth dựa trên đồ thị luồng thực thi Do đó sau khi thực hiện symbolic execution trên đồ thị luồng điều khiển với amountE = 30 và số amounT = 1, sẽ tạo ra có một số trạng thái sau: Kết quả các trạng thái đạt được nếu đi theo nhánh “then” Kết quả các trạng thái đạt được nếu đi theo nhánh “else” E. So sánh các trạng thái để đưa ra kết quả Chúng tôi tiến hành so sánh kết quả thu được ở bước duyệt cây cú pháp trừu tượng và symbolic execution trên đồ thị luồng điều kiện. Chúng tôi giả sử giá của 1 token là 30 ether và chỉ cần chú ý vào nhánh “then”, bởi vì các trạng thái của nhánh “else” tương tự như trạng thái ban đầu (Hình 4 và Hình 8). Do đó, có hai khả năng xảy ra: Tài khoản khoản cỏ địa chỉ 0xAAAA muốn mua 1 token từ người dùng 0xBBBB, vì vậy 0xAAAA trả 30 ether và sau đó nhận 1 token. Do hợp đồng thông minh trong tường hợp này được thực thi chính xác giống như chúng ta hiểu theo ngữ nghĩa thông thường đối với một giao dịch thành công (Hình 4 và Hình 7). Vì vậy hợp đồng đáng tin cậy và có thể triển khai trên hệ thống blockchain. Mặt khác, chúng ta hãy xem xét một tình huống như sau, hợp đồng thông minh được sửa đổi bằng cách xóa dòng 24, 25 (được tô đậm ở phần mã nguồn) trong mã nguồn của nó. Do đó, kết quả của việc symbolic execution và duyệt cây cú pháp sẽ hoàn toàn khác nhau, đặc biệt là ở trạng thái thứ hai và thứ ba (Hình 4 và Hình 9). Trong trường hợp này, ngay cả khi 0xAAAA đã gửi 30 ether đến 0xBBBB, hợp đồng thông minh sẽ không trả lại bất kỳ token nào và chủ sở hữu của địa chỉ 0xAAAA cũng sẽ không nhận được gì. Do đó, hợp đồng thông minh này có nhiều khả năng là lừa đảo và không nên được triển khai trên bất kỳ nền tảng blockchain nào. Kết quả các trạng thái của nhánh “then” đối với hợp đồng đã chỉnh sửa
634 ỨNG DỤNG CHATBOT THÔNG MINH TRONG VIỆC XÁC THỰC HỢP ĐỒNG THỒNG MINH ETHEREUM VI. KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN Trong nghiên cứu này, chúng tôi đề xuất một quy trình mới để xác thực hợp đồng thông minh Ethereum thông qua chatbot. Chúng tôi muốn làm cho quá trình giống như một cuộc trò chuyện giữa hai người dùng và nhân viên tư vấn trong đời thực. Vì vậy, tất cả mọi người, ngay cả những người không am hiểu về công nghệ vẫn có thể sử dụng nó một cách dễ dàng. Nói chính xác hơn, đầu tiên, chatbot của chúng tôi sẽ tương tác với người dùng để tìm ra vấn đề của họ và thu thập, trích xuất thông tin mà chúng tôi cần, để giải quyết vấn đề một cách hiệu quả. Thứ hai, quy trình của chúng tôi tạo ra các trạng thái bằng cách duyệt qua cây cú pháp trừu tượng được xây dựng các cú pháp để mô tả ngữ nghĩa mà mọi người có thể hiểu được dễ dàng. Sau đó, chúng tôi tạo ra các đồ thị luồng điều khiên và tiến hành symbolic execution trên chúng. Sau đó, chúng tôi nhận được một số trạng thái mới và bắt đầu so sánh với những trạng thái ban đầu để đưa ra kết luận. Chắc chắn, việc áp dụng kỹ thuật này sẽ mang lại lợi ích cho cả người dùng với một vốn kiến thức hạn hẹp trong lĩnh vực này và kể cả các chuyên gia bảo mật. Đối với trường hợp người dùng không am hiểu nhiều về công nghệ, họ có thể tương tác với chatbot và xác thực các hợp đồng mới này trước khi chuyển để đảm bảo rằng tiền điện tử của họ không bị chuyển hướng đến bất kỳ địa chỉ nào khác. Ngược lại, các chuyên gia bảo mật có thể nghiên cứu phương pháp của chúng tôi để nhanh chóng tìm ra các lỗi đáng ngờ bên trong các hợp đồng thông minh của nền tảng Ethereum. Hơn nữa, chúng tôi có thể xây dựng các ứng dụng dựa trên công nghệ blockchain và áp dụng cách tiếp cận của chúng tôi để xác minh các hợp đồng thông minh trước khi người dùng đồng ý sử dụng chúng. Các hướng nghiên cứu tiếp theo mà chúng tôi hướng đến có thể là gợi ý chỉnh sửa mã nguồn hoặc xây dựng chatbot tích hợp với phân tích động. TÀI LIỆU THAM KHẢO [1] Melanie Swan.Blockchain: Blueprint for a new economy. "O’Reilly Media, Inc.", 2015. [2] Security tools. https://consensys.github.io/smart-contract-best-practices/security_tools/. Accessed: 2017. [3] Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buen-zli, and Martin Vechev. “Securify: Practical security analysis of smart contracts”. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communica-tions Security, pp. 67-82, 2018. [4] Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko, and Yaroslav Alexandrov. “Smartcheck: Static analysis ofethereum smart contracts”. In Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain, pp. 9-16, 2018. [5] Blockgeeks. Why are smart contract security audits so important?, 2018. [6] Lakshmi Siva Sankar, M Sindhu, and M Sethumadhavan. “Survey of consensusprotocols on blockchain applications”. In 2017 4th International Conference onAdvanced Computing and Communication Systems (ICACCS), pp. 1-5. IEEE, 2017. [7] Ritesh Modi.Solidity, Programming Essentials: A beginner’s guide to build smartcontracts for Ethereum and blockchain.Birmingham: Packt Publishing, 2018. [8] P. H. Dave and H. B. Dave, Compilers: principles and practice. Pearson EducationIndia, 2012. [9] L. Torczon and K. Cooper, “Engineering a compiler (Vol. 13),” 2012. [10] J. C. King, “Symbolic execution and program testing,”, Communications of the ACM, Vol. 19, No. 7, pp. 385- 394, 1976. AN INTELLIGENT CHATBOT FOR AUTOMATIC VERIFICATION OF ETHEREUM SMART CONTRACTS Bang Ngoc Bao Tam, Tran Quang, Quan Thanh Tho ABSTRACT: Ethereum smart contracts based on blockchain technology are powerful and promising applications that provide a decentralized platform for exchanging cryptocurrencies and public services. In addition, since Ethereum and its smart contracts are a publicly accessible, unchangeable and distributed platform, they are extremely vulnerable to various forms of attack, making their security a top priority. In this article, we focus our attention on the integration of an intelligent chatbot with the Symbolic Execution technique to verify Ethereum smart contracts. Through conversing with users, the chatbot generates an intermediate representation capturing the user's intention. Then, the symbolic execution is applied to verify if the involved Ethereum smart contracts truly reflect the user intention without security flaws or not. It is noted that once the smart contract executes, the information is written into blockchain and cannot be modified afterward. Hence, the symbolic verification of the smart contract without executing it in this situation is very crucial.