Gần đây, ChatGPT đã trở nên phổ biến và số người dùng tích cực của nó đã vượt quá 100 triệu chỉ sau hai tháng kể từ khi ra mắt. Việc sử dụng nó để viết bài, viết code, yêu đương, tìm việc và trả lời email đã trở thành một thao tác thường xuyên, có rất nhiều cách dạy bạn sử dụng phần mềm này để "kiếm tiền" trên Internet, thậm chí có giáo sư từ Trường Kinh doanh Wharton thuộc Đại học Pennsylvania tuyên bố rằng "sinh viên" ChatGPT đã vượt qua kỳ thi quản lý kinh doanh.

Do đó, chủ đề trí tuệ nhân tạo thay thế một số công việc nhất định hay thậm chí con người bị trí tuệ nhân tạo thay thế đã trở thành chủ đề nóng, trong thời đại ai cũng bị cầm tù, trái tim ai cũng dần loạn nhịp.

Vậy trí tuệ nhân tạo, hay "sản phẩm máy tính" như xác minh chính thức, có thể thay thế con người không? Trong thế giới của Web3.0, xác minh chính thức có thể thay thế đánh giá thủ công không?

xác minh chính thức

Xác minh chính thức là một phương pháp chứng minh toán học để xác minh rằng một chương trình máy tính hoạt động như mong đợi. Nó thể hiện các thuộc tính và hành vi dự kiến ​​của các chương trình dưới dạng các công thức toán học, sau đó sử dụng các công cụ tự động để kiểm tra xem các công thức này có đúng hay không. Quá trình này giúp đảm bảo rằng các chương trình của nó đáp ứng mong đợi.

Áp dụng xác minh chính thức

Xác minh chính thức là một công cụ có thể được sử dụng rộng rãi trong các hệ thống khác nhau, bao gồm:

• Thiết kế phần cứng máy tính: Đảm bảo rằng các mạch tích hợp và hệ thống kỹ thuật số đáp ứng các thông số kỹ thuật cần thiết và hoạt động chính xác.

• Kỹ thuật phần mềm: Xác thực tính chính xác và độ tin cậy của hệ thống phần mềm, đặc biệt là trong các ứng dụng/lĩnh vực quan trọng như hàng không, thiết bị y tế và hệ thống tài chính.

• An ninh mạng: Đánh giá tính bảo mật của các thuật toán và giao thức mật mã, đồng thời xác định các lỗ hổng bảo mật trong các hệ thống nhạy cảm về bảo mật.

• AI và Machine Learning: Xác thực các thuộc tính và hành vi của các mô hình AI và ML để đảm bảo chúng hoạt động như mong đợi và đưa ra dự đoán chính xác.

• Chứng minh định lý tự động: kiểm chứng các định lý toán học và chứng minh các phỏng đoán toán học, ứng dụng trong lĩnh vực toán học, vật lý và khoa học máy tính.

• Chuỗi khối và hợp đồng thông minh: Đảm bảo tính chính xác, bảo mật và độ tin cậy của hệ thống chuỗi khối và hợp đồng thông minh.

Xác minh chính thức hợp đồng thông minh

Việc xác minh chính thức hợp đồng thông minh là thể hiện logic và hành vi dự kiến ​​của hợp đồng thông minh bằng các biểu thức toán học, sau đó sử dụng các công cụ tự động để kiểm tra xem các biểu thức toán học này có đúng không.

Quá trình này bao gồm:

• Đặc điểm kỹ thuật và các thuộc tính của hợp đồng được xác định bằng ngôn ngữ chính thức.

• Dịch mã hợp đồng"” thành một biểu diễn chính thức, chẳng hạn như logic toán học hoặc một mô hình.

• Sử dụng một trình chứng minh định lý tự động hoặc trình kiểm tra mô hình để xác minh rằng thông số kỹ thuật và các thuộc tính của hợp đồng được giữ nguyên.

• Lặp lại quá trình xác minh để tìm và sửa bất kỳ lỗi hoặc sai lệch nào so với mong đợi.

Đôi khi một trình chứng minh định lý hoặc trình kiểm tra mô hình tự động không thể chứng minh hoặc bác bỏ một thuộc tính. Trong trường hợp này, có thể cần phải tinh chỉnh thông số kỹ thuật và các thuộc tính mong muốn và lặp lại quy trình xác minh.

Việc chia nhỏ đặc tả thành các đoạn mã nhỏ hơn hoặc cung cấp thêm thông tin đặc tả có thể tinh chỉnh đặc tả và các thuộc tính dự kiến ​​của nó. Điều này có thể giúp những người chứng minh định lý và người kiểm tra mô hình dễ dàng xác minh rằng các thông số kỹ thuật và đặc tính phù hợp.

Việc xác minh chính thức có thể được áp dụng cho một hợp đồng hoặc nhiều hợp đồng cùng một lúc. Các dự án Web3.0 thường sử dụng nhiều hợp đồng và điều quan trọng là phải đảm bảo rằng các hợp đồng này hoạt động cùng nhau và triển khai đúng chức năng dự án mong muốn.

Trong xác minh chính thức, việc sử dụng phương pháp toán học này giúp đảm bảo rằng các hợp đồng thông minh không có lỗi, lỗi và các hành vi không mong muốn khác, vì các thuộc tính của chúng đã được chứng minh một cách chặt chẽ về mặt toán học.

chính thức hóa mã

Đoạn mã ví dụ một

Đoạn mã sau trình bày một chương trình chức năng chuyển mã thông báo được đơn giản hóa: Có hai người dùng, mỗi người có một số mã thông báo (số dư và số dư 2). Hàm transferFromUser 1 chuyển mã thông báo từ Người dùng 1 sang Người dùng 2 . Chương trình có một bất biến là tổng nguồn cung cấp mã thông báo luôn bằng tổng số dư.

Đoạn mã 1: Chương trình chuyển mã thông báo

Chúng tôi biểu thị các bất biến bằng các công thức toán học và đánh số các công thức. Trong các công thức toán học, "=" có nghĩa là "bằng", không phải phép gán.

Đoạn mã ví dụ 2

Đoạn mã sau đây cho biết cách thêm các công thức logic (tràn số nguyên được bỏ qua vì mục đích đơn giản và rõ ràng của ví dụ).

Đoạn mã 2: Hàm công thức logic thể hiện ý nghĩa của đoạn mã

Nếu một người muốn kiểm tra xem transferFromUser 1 có giữ một bất biến trong chương trình hay không, thì chúng ta có thể kiểm tra Phương trình 7 (ở cuối hàm) để tìm bất biến (Phương trình 1). Dưới đây là chứng minh bằng phương pháp đại số THPT.

Hợp tác xác minh chính thức và kiểm toán thủ công

Về mặt đảm bảo tính bảo mật của hợp đồng thông minh, xác minh chính thức và kiểm toán thủ công có thể nói là bổ sung cho nhau.

Xác minh chính thức:

Xác minh chính thức cung cấp một cách tự động và có hệ thống để kiểm tra logic và hành vi của hợp đồng cũng như các thuộc tính dự kiến ​​của hợp đồng, giúp dễ dàng xác định và khắc phục các lỗi hoặc lỗ hổng tiềm ẩn. Nó rất hiệu quả để tìm các vấn đề phức tạp hoặc tế nhị mà có thể khó phát hiện thông qua kiểm tra thủ công.

Khi xử lý các hợp đồng phức tạp hoặc nhiều hợp đồng, con người khó có thể suy luận về tất cả các kết hợp và khả năng cần kiểm tra, trong khi máy móc thì “không áp lực”.

Kiểm toán thủ công:

Kiểm toán con người cung cấp đánh giá của chuyên gia về mã hợp đồng, thiết kế và triển khai. Các chuyên gia kiểm toán có thể sử dụng kinh nghiệm và chuyên môn của mình để xác định các rủi ro bảo mật tiềm ẩn và đánh giá tình hình bảo mật tổng thể của hợp đồng.

Ngoài ra, con người cũng có thể xác minh rằng quy trình xác minh chính thức đã được thực hiện chính xác và kiểm tra các vấn đề không thể phát hiện được bằng các công cụ tự động. Do đó, đánh giá của chuyên gia con người sẽ hữu ích hơn để đảm bảo tính chính xác của các thông số kỹ thuật và các thuộc tính bắt buộc được sử dụng trong quá trình xác minh chính thức.

Tóm lại, chỉ bằng cách kết hợp hai phương pháp xác minh chính thức và kiểm toán thủ công thì mới có thể tiến hành đánh giá toàn diện và kỹ lưỡng về tính bảo mật của hợp đồng thông minh, đồng thời tăng cơ hội phát hiện và sửa lỗi. Đó cũng là một cách tiếp cận bảo mật kết hợp sức mạnh của con người và máy móc và được gọi là “phòng thủ theo chiều sâu”.

Chuyên gia bảo mật AMA trực tuyến

Không thể đánh giá thấp sức mạnh của xác minh chính thức, nhưng không thể bỏ qua tầm quan trọng của kiểm toán thủ công. Trên trang web chính thức của ChatGPT, nó đã thừa nhận những thiếu sót của mình và cuộc thảo luận sáo rỗng rằng trí tuệ nhân tạo không thể thay thế tư duy và sáng tạo của con người cũng có thể bỏ qua 10.000 từ ở đây ... Không, Bard đã phạm sai lầm và giá cổ phiếu của Google lao dốc.

Tương tự, xác minh chính thức không thể thay thế kiểm tra thủ công và cả hai bổ sung cho nhau để tiến hành kiểm tra toàn bộ hợp đồng thông minh.

Có bất kỳ câu hỏi sau khi đọc bài viết? Tại sao không trở thành khách mời tại [CertiK Twitter AMA] vào [Thứ Sáu, ngày 10 tháng 2 tại Nhật Bản] và có phần Hỏi & Đáp trực tuyến với các chuyên gia! Những người bạn không thể tham dự do lệch múi giờ có thể để lại lời nhắn ở chế độ nền, chúng tôi sẽ chuyển lời nhắn đó đến khách mời thay bạn và công bố nội dung phát lại AMA!