Chứng chỉ biên dịch cho hợp đồng thông minh
Translation Certification for Smart Contracts.
Tính chính xác của trình biên dịch là một vấn đề cũ, nhưng với sự xuất hiện của các hợp đồng thông minh trên Blockchain, vấn đề đó lại xuất hiện với góc nhìn mới. Hợp đồng thông minh là các phần mềm độc lập kiểm soát các tài sản (có giá trị) trong môi trường đối nghịch; khi đã cam kết với Blockchain, các hợp đồng thông minh này không thể bị sửa đổi. Hợp đồng thông minh thường được phát triển bằng ngôn ngữ hợp đồng cấp cao và được biên dịch thành mã máy ảo cấp thấp trước khi được cam kết với Blockchain. Để người dùng hợp đồng thông minh tin tưởng một đoạn mã cấp thấp nhất định trên Blockchain, họ phải tự thuyết phục mình rằng (a) họ đang sở hữu mã nguồn phù hợp và (b) trình biên dịch đã dịch đúng mã nguồn sang mã cấp thấp đã cho. Các phương pháp tiếp cận cổ điển về tính chính xác của trình biên dịch giải quyết điểm thứ hai. Các tác giả lập luận rằng chứng chỉ biên dịch cũng giải quyết triệt để điểm đầu tiên. Các tác giả mô tả kiến trúc bằng chứng của một khung chứng chỉ biên dịch mới, được triển khai trong Coq, cho một ngôn ngữ hợp đồng thông minh chức năng. Các tác giả chứng minh có thể mô hình hóa đường ống biên dịch như một chuỗi các mối liên hệ biên dịch tạo điều kiện cho phương pháp xác minh mô đun và mạnh mẽ khi đối mặt với việc triển khai trình biên dịch đang phát triển.