Từ blockchain đã trải qua nhiều thăng trầm trong những năm gần đây, từ các khái niệm công nghệ tiên tiến, những từ nóng trên thị trường cho đến các biểu tượng tiêu thụ quá mức. Nhiều người tin rằng blockchain là một công cụ để giải quyết các điểm đau của nhiều ngành công nghiệp và có tiềm năng trở thành chất xúc tác cho sự ra đời của thế hệ tiếp theo của "siêu nhà cung cấp dịch vụ kinh doanh".

Tuy nhiên, sự thay đổi sử thi huyền thoại vẫn chưa đến, nó đã được đưa ra ánh đèn sân khấu. Những người quan tâm sẽ kiếm được lợi nhuận từ nó, và những người tìm kiếm lợi nhuận sẽ trả tiền một cách mù quáng. Rơi vào vòng xoáy dư luận quá sớm sẽ gây hại và thử nghiệm cho công nghệ đang trong giai đoạn tăng trưởng.

Tình hình thực tế hiện nay là có rất ít ứng dụng đổ bộ, vẫn còn khoảng cách giữa công nghệ và kết nối ngành, và sự ồn ào của giới đầu cơ đã làm lu mờ “tiếng nói xương sống” thực sự quan tâm đến công nghệ và ngành. Odaily chung tay với phương tiện kinh doanh mới hàng đầu 36Kr, các nhà lãnh đạo công nghệ hàng đầu và giới tinh hoa học thuật để thảo luận về cách tuân thủ quy định, thúc đẩy ngành loại bỏ cặn bã và trích xuất bản chất, trao lưu lượng truy cập và tiếng nói cho những người làm việc nghiêm túc, và sử dụng sức mạnh để cho blockchain hạ cánh.

Vào ngày 5 tháng 9, tại hội nghị blockchain POD do Odaily tổ chức và 36Kr Group Strategy đồng tổ chức, Vilhelm Sjöberg, nhà khoa học trưởng của CertiK, đã có bài phát biểu với tựa đề "Hướng tới việc xây dựng các hợp đồng thông minh và hệ sinh thái blockchain hoàn toàn đáng tin cậy".

tiêu đề phụ

Sau đây là bản ghi lại bài phát biểu của Vilhelm Sjöberg, Nhà khoa học trưởng của CertiK:

Xin chào mọi người, tôi là Nhà khoa học trưởng của CertiK và đã thực hiện rất nhiều công việc nghiên cứu về blockchain. Blockchain là một cơ sở dữ liệu và có nhiều chủ đề nghiên cứu quan trọng về công nghệ và niềm tin. Các chương trình dễ bị lỗi khi thực thi, tại sao chúng cứ mắc lỗi khi thực hiện? Làm thế nào để làm cho chương trình đáng tin cậy hơn? Tất nhiên, không phải mọi người lập trình kém mà vì hợp đồng thông minh là một phần rất đặc biệt và quan trọng của blockchain. Trên blockchain, hợp đồng thông minh một khi được triển khai thì không thể cập nhật, nếu bản thân hợp đồng thông minh được triển khai có kẽ hở, hacker có thể tìm và khai thác kẽ hở này để đánh cắp tài sản. Những vấn đề này là những gì chúng ta cần phải tránh.

Để đảm bảo an toàn cho chương trình, một số sẽ được xem xét thủ công, nhưng chi phí thời gian tương đối cao và có thể gây ra các vấn đề khác. Tất nhiên, cũng có các bài kiểm tra tự động để kiểm tra, nhưng nó sẽ không giúp bạn tìm ra tất cả các vấn đề. Vì vậy, đối với blockchain, những giải pháp này vẫn chưa đủ tốt.

CertiK sử dụng các phương pháp toán học để chứng minh các chương trình, nghĩa là cung cấp dịch vụ bảo mật cho các hợp đồng thông minh và ứng dụng chuỗi khối thông qua xác minh chính thức.Nhân hệ điều hành đồng thời của chúng tôi, CertiKOS, có thể được chứng minh chính thức đầy đủ và công nghệ chính đằng sau nó là "đặc điểm kỹ thuật chuyên sâu".

Đối với các hệ thống phức tạp, CertiK sử dụng các kỹ thuật đặc tả chuyên sâu để đạt được chứng nhận an toàn.Chúng tôi sẽ phân lớp các hệ thống phức tạp và chúng tôi sẽ hiểu từng lớp trừu tượng viết gì, nó làm gì và nó thực hiện những hoạt động gì để chứng minh liệu nó có đáp ứng các thông số kỹ thuật chính xác của chúng tôi hay không. Nếu bạn viết một lớp trừu tượng nào đó, chúng tôi có thể đặt nó lại với nhau và xác minh nó. Các lớp trừu tượng có thể được liên kết với nhau để có thể tích hợp các bằng chứng. Đây là công việc chính mà chúng tôi làm: để đạt được xác minh hợp đồng thông minh phân tán hoàn chỉnh thông qua phân lớp và tích hợp.

Hạt nhân của chương trình điều hành CertiKOS của chúng tôi được chia thành nhiều lớp và có thể xác minh một chương trình lớn và phức tạp vì chúng tôi đang xử lý một chức năng phức tạp tại một thời điểm.

Hình ảnh này cho thấy chúng tôi đã triển khai hệ điều hành CertiKOS trên máy Landshark.

Chúng tôi cũng đã hợp tác với nhiều chuyên gia trong giới học thuật và họ giúp chúng tôi phát triển một dự án như vậy. Vào năm 2015, Giáo sư Gu Ronghui và Giáo sư Shao Zhong đã đề xuất khái niệm "đặc điểm kỹ thuật sâu" và đã xác minh nó. Trong năm 2016, chúng tôi đã bán sản phẩm và dịch vụ sẵn sàng sử dụng này cho các doanh nghiệp. Vào năm 2017, chúng tôi đã mở rộng CertiK để xác minh các hợp đồng thông minh. Vì vậy, chúng tôi cũng có thể thực hiện một số nghiên cứu học thuật và chúng tôi có thể thực hiện xác minh chính thức cho chuỗi khối.

Tiếp theo, hãy để tôi giới thiệu chi tiết về một dự án nghiên cứu đang diễn ra mà chúng tôi đã tiến hành - DeepSEA, một ngôn ngữ lập trình để xác minh các hợp đồng thông minh.

Trước đó, hãy nói về xác minh chính thức là gì để giúp bạn hiểu.Xác minh chính thức bao gồm nhiều kỹ thuật xác minh khác nhau, bao gồm xác minh nông và xác minh sâu.

Xác minh mức độ nông đề cập đến một số xác minh phổ biến, chẳng hạn như vấn đề tràn số nguyên rất phổ biến của hợp đồng thông minh.Để xác minh tương đối nông, chúng tôi đã thiết kế thế hệ đầu tiên của công cụ phát hiện tự động hợp đồng thông minh hiệu suất cao CertiK AutoScanEngine (CASE), có thể giúp bạn tự động quét các hợp đồng thông minh và xác định vị trí các lỗ hổng. Xác minh phân tán được hoàn thành bằng cách tinh chỉnh hợp đồng thành các mô-đun khác nhau. Người dùng có thể tải hợp đồng lên công cụ xác minh của chúng tôi để xem cái nào đúng khi gọi một phương thức nhất định hoặc cách xử lý khi xảy ra lỗi. Toàn bộ quá trình đạt được sự xác minh máy móc tối đa, ít phụ thuộc vào nhân lực.

Tiếp theo, tôi muốn nói về xác minh sâu.Ví dụ cần kiểm chứng thuộc tính nào của giá trị thì phải nghĩ cách chứng minh. Có một số thuộc tính cục bộ, có thể áp dụng cho một kiến ​​trúc nhất định hoặc cho một phương thức nhất định. Nhưng xác minh chuyên sâu, nó có thể được áp dụng cho toàn bộ hệ sinh thái của tất cả các hợp đồng thông minh. Như được mô tả trong sách trắng của chúng tôi, chúng tôi có thể tích hợp và kết hợp các chuỗi khác nhau, bao gồm một số hệ thống thanh toán, trên chuỗi, ngoài chuỗi, v.v., nhằm cung cấp bảo mật cho toàn bộ hệ sinh thái chuỗi khối.

Đôi khi chúng ta không chỉ phụ thuộc hoàn toàn vào máy móc mà còn nhờ đến sự can thiệp nào đó của con người, chẳng hạn đối với những hệ thống phức tạp, cần phải viết các thông số kỹ thuật trong sách hướng dẫn.Trong CertiK, mỗi hệ thống có thể được chia thành các lớp khác nhau. Vì vậy, một dự án như vậy có thể giúp chúng tôi tạo ra một hệ thống xác minh và đặc điểm kỹ thuật chuyên sâu. Vì mục đích này, chúng tôi đã phát triển ngôn ngữ DeepSEA của riêng mình. Nếu bạn chỉ muốn viết một hợp đồng, bạn có thể viết nó bằng ngôn ngữ được cá nhân hóa. Nhưng đối với một số hợp đồng có độ tin cậy cao, chúng tôi có thể không có mức độ tin cậy cao như vậy ở các khía cạnh khác. Tất nhiên chúng ta có thể viết nó bằng ngôn ngữ của EVM, nhưng đó không phải là mã đáng tin cậy lắm. Vì vậy, chúng tôi đã khởi chạy ngôn ngữ DeepSEA của CertiK, ngôn ngữ ban đầu được phát triển để viết CertiK và giờ đây ngôn ngữ này cũng có thể được ánh xạ tới các hợp đồng Ethereum. Ngoài việc có thể tạo thông số kỹ thuật, bạn cũng có thể sử dụng trình biên dịch đã được chứng minh của chúng tôi.

Có một hợp đồng trên blockchain để đảm bảo rằng mọi thứ chúng tôi làm đều đúng. Vì vậy, tôi nghĩ rằng đó cũng là một minh chứng rất tốt về một số quy trình mà chúng tôi đang thực hiện xác nhận ở cấp độ sâu. Nếu chúng tôi đi sâu, có một số bước chúng tôi cần thực hiện để giúp chúng tôi xác minh rằng hợp đồng của chúng tôi đang ở trạng thái chính xác và tốt. Vì vậy, chúng tôi có thể viết ra khái niệm này, và cuối cùng thông qua một loạt các bước như vậy, chúng tôi có thể đảm bảo tính đúng đắn của hợp đồng.

Chúng tôi có các dự án khác mà bạn cũng có thể xem trực tuyến. Có một số dự án liên quan đến thanh toán mà chúng tôi có thể mở rộng. Ngoài ra còn có các dự án liên quan đến hợp đồng thông minh, trình biên dịch và mô hình EVM. Trong các lĩnh vực sau được liệt kê dưới đây, chúng tôi sẽ giúp bạn. Nếu bạn quan tâm, bạn có thể tham gia với chúng tôi như một đối tác và giữ liên lạc với chúng tôi. Cảm ơn tất cả!