BẢO MẬT HỢP ĐỒNG THÔNG MINH

Hợp đồng thông minh là các chương trình chạy trên Blockchain, tự động thực hiện, kiểm soát và ghi lại những sự kiện, hành động có liên quan đến nhau về mặt pháp lý dựa theo những điều khoản của hợp đồng hoặc thỏa thuận. Hai bên trong hợp đồng có thể đưa ra những cam kết thông qua Blockchain mà không cần phải biết về danh tính hay tin tưởng lẫn nhau nhưng vẫn đảm bảo nếu các điều kiện của hợp đồng không được thỏa mãn thì hợp đồng sẽ không được thực thi, đồng thời có thể tự động hóa quy trình, kích thích hành động tiếp theo nếu đáp ứng được các điều kiện. Hợp đồng thông minh có khả năng tùy chỉnh cao nên có thể thiết kế theo những cách khác nhau tùy theo loại dịch vụ và giải pháp. Công nghệ này cũng là các chương trình phi tập trung và tự thực hiện, giúp tăng tính minh bạch, giảm chi phí hoạt động và tăng hiệu quả vận hành.

Tuy nhiên, có thể có những sai lầm và những lỗ hổng trong chính mã của hợp đồng thông minh như Reentrancy, tràn số nguyên, không kiểm tra giá trị trả về,… Lỗ hổng Reentrancy xảy ra khi hợp đồng thông minh có thể gọi và sử dụng mã của các hợp đồng bên ngoài khác. Khi hợp đồng thực hiện thao tác chuyển khoản, nếu tài khoản đối tác là tài khoản hợp đồng thì chức năng gọi lại trong tài khoản hợp đồng sẽ được gọi. Nếu hợp đồng được gọi là hợp đồng do kẻ tấn công xây dựng thì có khả năng tồn tại mã độc trong đó. Một ví dụ cụ thể vào năm 2016, tin tặc đã khai thác lỗ hổng Reentrancy của hợp đồng DAO để đánh cắp 3,6 triệu Ether, trị giá 50 triệu USD.

Có một số lý do khiến các hợp đồng thông minh rất dễ xuất hiện các lỗ hổng mà tin tặc có thể khai thác. Đầu tiên, các ngôn ngữ lập trình và các công cụ vẫn còn mới và đơn giản, tồn tại nhiều lỗi. Thứ hai, hợp đồng thông minh là bất biến sau khi được triển khai, vì vậy yêu cầu các nhà phát triển phải dự đoán được tất cả các trạng thái và môi trường có thể xảy ra mà hợp đồng gặp phải trong tương lai, điều này chắc chắn là rất khó khăn. Khác với các ứng dụng phân tán thông thường có thể được cập nhật khi phát hiện lỗi, không có cách nào để vá lỗi của hợp đồng thông minh mà không phân tách chuỗi khối (gần như là một nhiệm vụ bất khả thi), bất kể hợp đồng nắm giữ bao nhiêu tiền hoặc mức độ phổ biến của nó. Do đó, các kỹ thuật kiểm tra phát hiện lỗ hổng hiệu quả cho các hợp đồng thông minh trước khi triển khai là rất cần thiết.

PHÁT HIỆN LỖ HỔNG HỢP ĐỒNG THÔNG MINH DỰA TRÊN KỸ THUẬT THỰC THI TƯỢNG TRƯNG

Phương pháp phát hiện dựa trên kỹ thuật Thực thi tượng trưng được thiết kế để phát hiện các loại lỗ hổng phổ biến như lỗ hổng Reentrancy, lỗ hổng tràn số nguyên trong hợp đồng thông minh. Phương pháp này sử dụng bytecode, địa chỉ hoặc mã nguồn của hợp đồng thông minh làm đầu vào và xuất ra kết quả phát hiện lỗ hổng bao gồm thông tin cụ thể như loại và vị trí của lỗ hổng.

Hình 1. Luồng thực thi của kỹ thuật Thực thi tượng trưng

Kỹ thuật này được xây dựng bao gồm 4 mô-đun chính, bao gồm: Tạo luồng điều khiển (Control Flow Generation), Thực thi tượng trưng, Phát hiện lỗ hổng (Vulnerability detection) và Giải quyết ràng buộc (Constraint Solving).

Mô-đun Tạo luồng điều khiển Mô-đun

Tạo luồng điều khiển được sử dụng để xác định tất cả các điều kiện đường dẫn có thể xảy ra trong quá trình thực hiện chương trình. Các cạnh của đồ thị luồng điều khiển biểu thị từng khối cơ bản trong quá trình thực hiện chương trình và các cạnh giữa các nút biểu thị các điều kiện nhảy giữa các nút. Việc tạo đồ thị luồng điều khiển có thể giúp hiểu rõ hơn về mối quan hệ gọi giữa các chương trình hoặc thực hiện bước phân tích tiếp theo. Chi tiết quá trình tạo luồng điều khiển như sau:

1. Sau khi tạo chuỗi opcode, tìm nạp một lệnh từ nó.

2. Xác định xem lệnh này là JUMP (nhảy không điều kiện) hay JUMPI (nhảy có điều kiện).

3. Nếu là JUMP, hãy loại bỏ tham số là địa chỉ đích của lệnh này.

4. Nếu là JUMPI thì lấy ra các tham số bao gồm điều kiện nhảy và địa chỉ nhảy.

5. Nếu đó là CALL/ CALLCODE/ DELEGATECALL/ STATICCALL, thì cần đặt địa chỉ này làm điểm cuối của nút hiện tại.

6. Nếu đó là lệnh RETURN, hãy ghi phần bù của lệnh này là điểm cuối của nút hiện tại. Kiểm tra xem lệnh tiếp theo là lệnh cuối cùng hay JUMPDST, nếu không sẽ báo lỗi.

Hình 2. Ví dụ đồ thị luồng điều khiển

7. Nếu lệnh là JUMPDST, hãy duyệt qua tất cả các nút để tìm địa chỉ bắt đầu của lệnh JUMPDST và đặt NodeID hiện đang thực thi làm ID của nút này.

Mô-đun Thực thi tượng trưng

Thực thi tượng trưng có thể khám phá nhiều đường dẫn mà một chương trình có thể thực hiện dưới các đầu vào khác nhau. Ý tưởng chính là cho phép một chương trình lấy các giá trị tượng trưng làm đầu vào. Việc thực thi được thực hiện để xây dựng cho mỗi đường dẫn điều khiển đã kiểm tra một công thức biểu diễn các điều kiện của các nhánh được thực hiện dọc theo đường dẫn đó và một bộ nhớ ký hiệu lưu trữ ánh xạ các biến thành các biểu thức hoặc giá trị tượng trưng. Hình 3 dưới đây trình bày một ví dụ về mã C (tương tự như mã Solidity) và cây thực thi ký hiệu của nó, cùng với các kho ký hiệu và ràng buộc đường dẫn của nó.

Cụ thể, trong bài toán này mô-đun Thực thi tượng trưng sử dụng nguyên tắc tìm kiếm theo chiều sâu để thực thi từng nút trong biểu đồ và cập nhật trạng thái chung cùng một lúc dựa trên biểu đồ luồng điều khiển. Khi gặp lệnh nhảy có điều kiện hoặc lệnh thao tác toán hạng, tiến hành chuyển đổi nó thành một loại biến để giải quyết ràng buộc, sau đó mô-đun phát hiện lỗ hổng có thể giải quyết ràng buộc đối với lỗ hổng. Mô-đun này được chia thành ba phần: thiết kế trạng thái của máy ảo, thực hiện lệnh của máy ảo và lệnh gọi đường dẫn của Thực thi tượng trưng.

1. Thiết kế trạng thái của máy ảo: Máy ảo của hệ thống được mô phỏng theo máy ảo Ethereum (EVM). Sau mỗi giao dịch được thực hiện, trạng thái của EVM, bao gồm bộ đếm chương trình, ngăn xếp và số dư tài khoản có thể thay đổi.

2. Thực hiện lệnh của máy ảo: Các lệnh EVM hiện tại đã triển khai tổng cộng 142 lệnh. Theo lệnh của EVM, phương pháp này đã thực hiện phân tích được 117 lệnh thường được sử dụng.

3. Nguyên tắc gọi đường dẫn: Trước khi thực hiện ký hiệu biểu đồ luồng điều khiển, nguyên tắc gọi của đường dẫn phải được xác định trước. Ở đây sẽ sử dụng nguyên tắc tìm kiếm theo chiều sâu. Khác với tiến trình duyệt đồ thị chung, phương pháp này sẽ cần lưu trạng thái của đường đi này khi nó kết thúc.

Hình 3. Ví dụ về Thực thi tượng trưng

Mô-đun Phát hiện lỗ hổng

Phát hiện lỗ hổng Reentrancy: Có những lý do mà lỗ hổng Reentrancy tồn tại như khi sử dụng lệnh gọi để chuyển tiền vào tài khoản hợp đồng, chức năng gọi lại của hợp đồng sẽ được gọi; lệnh Call không hạn chế việc sử dụng Gas (khoản phí cần phải trả để thực hiện các giao dịch hay hoạt động tương tác với hợp đồng thông minh trên nền tảng Blockchain) theo mặc định; hoàn tất thao tác chuyển tiền trước khi giảm số dư tài khoản người dùng. Lượng Gas giới hạn của hai thao tác transfer và send đều là 2300, nếu Gas lớn hơn 2300 thì tương đương với không hạn chế. Nên ta sử dụng Gas lớn hơn 2300 như ràng buộc lỗ hổng và nếu địa chỉ có thể bằng với địa chỉ hợp đồng độc hại thì có thể xuất hiện lỗ hổng Reentrancy.

Phát hiện lỗ hổng tràn số nguyên: Lỗ hổng tràn số nguyên đã trở nên phổ biến và gây ra rất nhiều thiệt hại đáng kể. Trong EVM, có thể có các hoạt động tràn số nguyên như cộng, trừ, nhân và chia. Lỗi có thể xảy ra trong các trường hợp như nếu tổng của hai toán hạng nhỏ hơn một trong các toán hạng được giải; nếu phép nhân của hai toán hạng lớn hơn 2^256; nếu số bị trừ lớn hơn số bị trừ; nếu số chia có thể bằng 0.

Mô-đun Giải quyết ràng buộc

Bộ giải z3 (thư viện được hỗ trợ trong ngôn ngữ Python) hỗ trợ tất cả các phân loại giải pháp lý thuyết, vì vậy sử dụng bộ giải z3 ở đây để giải quyết các ràng buộc của trạng thái đường dẫn. Theo các loại tham số trong EVM, sử dụng bộ giải z3 để thực hiện hai loại biến đó là Bool và BitVec. Bool đại diện cho kiểu Boolean, BitVec là kiểu mảng bit. Thông thường độ dài là 256 bit, vì EVM không có hàng loạt kiểu dữ liệu như int8/int16/int24/.../int256 như Solidity. Khi loại dữ liệu này được chuyển đổi thành bytecode, nó sẽ được lưu trữ dưới dạng biến 256 bit. Bằng việc sử dụng hai loại dữ liệu này và các chức năng của thư viện giải z3 sẽ cho ta kết quả về các lỗi có thể xảy ra.

KẾT LUẬN

Khả năng lưu trữ giá trị, tính minh bạch và tính bất biến, là ba thuộc tính chính rất cần thiết để hợp đồng thông minh hoạt động hiệu quả. Tuy nhiên, những thuộc tính này cũng khiến cho nhiều hợp đồng thông minh phát sinh những rủi ro bảo mật và cũng chính là kẽ hở mà các tin tặc nhắm tới. Do vậy, việc bảo đảm tính đúng đắn của hợp đồng thông minh là rất quan trọng, trong đó việc ứng dụng kỹ thuật Thực thi tượng trưng sẽ góp phần hữu ích trong khả năng phát hiện các lỗ hổng bảo mật tồn tại trong mã hợp đồng thông minh. Với kỹ thuật này, người kiểm thử chỉ định các hàm không quan trọng để bỏ qua trong quá trình phân tích, vì thế nó cho phép kiểm tra một mô-đun cụ thể mà không cần phải thực thiện thực thi tượng trưng trên toàn bộ chương trình, giúp tiết kiệm rất nhiều thời gian cho quá trình kiểm thử chương trình.