Xem mẫu
- 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.
nguon tai.lieu . vn
