Kể từ khi ra đời, phương pháp xác minh chính thức (Formal Verification) đã được gắn với những từ như “ngách, không phổ biến”. Một số người nói rằng các phương pháp xác minh chính thức là một phương pháp chống hack "cấp độ quân sự", điều này làm tăng thêm vẻ bí ẩn cho công nghệ này.

Phương pháp xác minh chính thức chính xác là gì?

Wikipedia giải thích xác minh chính thức như thế này:

Trong quy trình thiết kế phần cứng máy tính (đặc biệt là mạch tích hợp) và hệ thống phần mềm, ý nghĩa của xác minh hình thức là sử dụng các phương pháp toán học để chứng minh tính đúng hoặc sai của nó theo một hoặc một số thông số kỹ thuật hoặc thuộc tính hình thức.

Cảm giác bí ẩn có lẽ đến từ hai từ khóa chặt chẽ và trừu tượng trong định nghĩa - "đặc tả hình thức" và "chứng minh phương pháp toán học". Trên thực tế, khám phá lớp bí ẩn này, bạn sẽ tìm thấy nhiều khía cạnh thú vị của việc xác minh chính thức.

Câu hỏi tôi muốn thảo luận trong bài viết sau đây là: Ở giai đoạn này, câu chuyện nào sau đây thực sự có thể thỏa mãn trí tưởng tượng của bạn về việc xác minh chính thức? Xác minh chính thức có thể thực sự trở thành một công nghệ trong không gian chuỗi khối không? Nếu vậy, làm thế nào nó có thể được thực hiện?

(PS: Khái niệm "đặc điểm kỹ thuật chính thức" được đề cập ở trên cũng sẽ được thảo luận bên dưới.)

Để trả lời các câu hỏi trên, trước tiên chúng ta có thể xem xét một câu hỏi khác đơn giản hơn:

>Ở giai đoạn này, người ta sử dụng phương thức hình thức để làm gì?

Chỉ có hai câu trả lời cho câu hỏi này:

>1. Tránh sai lầm

>tiêu đề cấp đầu tiên

| tránh sai lầm

Tránh sai lầm thực chất là tránh thua lỗ.

Trước tiên chúng ta hãy khám phá, những lĩnh vực nào không khoan nhượng đối với các lỗi lập trình? Trong lĩnh vực nào, tổn thất do lỗi lập trình gây ra là vô cùng lớn?

Trên thực tế, các phương pháp hình thức đã được phổ biến kể từ khi thiết kế phần cứng. Một ví dụ nổi tiếng là: Đơn vị dấu phẩy động CPU Pentium của Intel mắc lỗi (FDIV Bug) và hàng chục nghìn CPU phải được tái chế và thay thế, gây thiệt hại lớn cho Intel (475 triệu đô la)[1].

Kể từ đó, Intel đã áp dụng rộng rãi các phương pháp chính thức trong thiết kế chip của mình.

Những gã khổng lồ phần cứng máy tính như IBM, AMD, NVIDIA và CADENCE[2] cũng là những người sử dụng các phương pháp chính thức...

Có thể nói rằng bạn có thể học được nhiều điều khôn ngoan thông qua một con mương, trên thực tế, ở mọi tầng lớp xã hội đều có người thử và sai, và trong thế giới công nghiệp cũng vậy. Ví dụ: Năm 1996, lần phóng tên lửa Ariane 5 (Ariane 5) đầu tiên của Cơ quan Vũ trụ Châu Âu, do hệ thống định vị quán tính gửi sai lệnh (số dấu phẩy động chuyển thành số nguyên gây tràn), tên lửa chỉ còn 37 vài giây sau khi phóng, sau đó nó đi lệch khỏi quỹ đạo đã định trước và cuối cùng bị rơi. Khoản tài trợ khổng lồ cho nghiên cứu và phát triển của Cơ quan Vũ trụ Châu Âu (8 tỷ đô la)[3] đã bốc cháy.

Ngay sau đó, EADS bắt đầu sử dụng các phương pháp chính thức để phát triển mô hình lập kế hoạch nhiệm vụ cho tên lửa Ariane.

Cơ quan Hàng không và Vũ trụ Quốc gia NASA và Bộ Quốc phòng Anh liên tiếp ban hành các tiêu chuẩn thiết kế vào những năm 1990 [4], trong đó liệt kê việc sử dụng các phương pháp chính thức. hệ thống điều khiển xe tự hành trên mặt trăng Yutu của đất nước tôi và phương tiện không gian tự phát triển đầu tiên được nhúng hệ điều hành thời gian thực SpaceOS[5] của đất nước tôi cũng xác minh tính chính xác của chúng thông qua các phương pháp chính thức.

Sự phát triển của lịch sử cho chúng ta biết rằng tiền là động lực đầu tiên thúc đẩy xã hội phát triển! Không ai có thể thở dài trước những tổn thất to lớn do lỗi chương trình gây ra.

Nếu hai câu chuyện trên nghe có vẻ nặng nề quá, hãy cùng xem qua bức tranh sau:

Hình trên cho thấy sự phân bổ toàn cầu của các dự án tàu điện ngầm được phát triển bằng các phương pháp chính thức [6].

Có thể thấy rằng bắt đầu từ hệ thống tín hiệu tàu điện ngầm ở Paris, các phương pháp chính thức đã được sử dụng rộng rãi trong việc phát triển hệ thống tàu điện ngầm ở các quốc gia lớn ở Bắc Mỹ, Châu Âu, Châu Á và một số quốc gia ở Nam Mỹ. Đây có lẽ là lý do tại sao chúng ta hầu như không bao giờ nghe nói về những tổn thất và thảm họa lớn do sự cố hệ thống tàu điện ngầm.

Một lần nữa, tiền là lực lượng sản xuất chính.

Giờ đây, sự đóng góp của các phương pháp chính thức trong việc đảm bảo việc đi lại hàng ngày đã được công nhận rộng rãi, trong lĩnh vực tài sản kỹ thuật số được phát triển trên cơ sở công nghệ chuỗi khối, công nghệ xác minh chính thức có thể được sử dụng để đảm bảo tính bảo mật của hợp đồng thông minh, từ đó bảo vệ tài sản Ý tưởng của an ninh trở nên hợp lý và thậm chí cấp bách.

Tôi nên làm gì? Dưới đây là một giới thiệu ngắn gọn.

Trước hết, cần đưa ra khái niệm “đặc tả hình thức”.

Đặc tả chính thức (đặc tả chính thức) đề cập đến việc triển khai nghiêm ngặt và toàn diện hành vi dự kiến ​​​​của hệ thống (chẳng hạn như chuyển một số mã thông báo S từ tài khoản A sang tài khoản B) và các thuộc tính (chẳng hạn như chuyển sẽ không gây tràn tài khoản B ) thông qua ngôn ngữ toán học.Định nghĩa. Thông số kỹ thuật chính thức thường xác định tính chính xác và bảo mật của hệ thống.

Đưa ra một đặc điểm kỹ thuật chính thức của một hệ thống, chúng ta có thể lặp lại thiết kế và triển khai hệ thống bắt đầu từ đặc điểm kỹ thuật. Trong mỗi bước của phép lặp, chúng ta có thể đảm bảo nghiêm ngặt về mặt toán học rằng hệ thống do phép lặp tạo ra nhất quán với thông số kỹ thuật hoặc hệ thống trước phép lặp thông qua một loạt phương pháp bao gồm sàng lọc, tổng hợp và chứng minh chính thức.

Ngoài việc thiết kế và triển khai một hệ thống từ một đặc tả chính thức, chúng ta cũng có thể sử dụng một loạt các phương pháp bao gồm thực thi tượng trưng, ​​kiểm tra mô hình và chứng minh chính thức để xác minh thiết kế và triển khai hiện có phù hợp với đặc tả này.

Âm thanh lớn, phải không?

Ví dụ: đối với chương trình hợp đồng thông minh, chúng ta có thể bắt đầu từ tất cả các đầu vào có thể có (chẳng hạn như sự kết hợp của các tham số chức năng) và trạng thái ban đầu (chẳng hạn như sự kết hợp của các giá trị ban đầu của các biến trạng thái), theo ngữ nghĩa của từng câu lệnh , từng câu Suy ra tất cả các trạng thái kết thúc có thể có của chương trình (chẳng hạn như giá trị của biến trạng thái và nhật ký sự kiện được tạo sau khi thực hiện hợp đồng) và kiểm tra xem sự kết hợp của tất cả các đầu vào, trạng thái ban đầu và trạng thái kết thúc của hợp đồng phù hợp với đặc điểm kỹ thuật chính thức. Điều này hơi giống với cách Conan giải quyết vụ án, từng bước một. Tuy nhiên, tất cả các định nghĩa ở đây được mô tả bằng ngôn ngữ toán học nghiêm ngặt, và việc suy ra và kiểm tra cũng là suy diễn và chứng minh toán học nghiêm ngặt. Tùy thuộc vào mức độ phức tạp của hệ thống được xác minh và thông số kỹ thuật chính thức của nó, các dẫn xuất và bằng chứng có thể được xây dựng thủ công hoặc do máy tạo tự động.

tiêu đề cấp đầu tiên

| Chống lại sự tấn công

Tấn công đối thủ thực sự là một ý nghĩa khác để tránh tổn thất.

Câu chuyện bắt đầu bằng một cuộc tấn công điện tử của quân đội Hoa Kỳ. Vào mùa hè năm 2015, một hacker được lệnh thực hiện một cuộc tấn công điện tử vào máy bay trực thăng không người lái Little Bird của quân đội Hoa Kỳ và chiếm quyền kiểm soát máy bay không người lái. Tuy nhiên, khi Bộ Quốc phòng Mỹ phát triển lại chương trình điều khiển cốt lõi của UAV, tin tặc đã sử dụng tất cả các phương thức tấn công hiện nay trên thế giới nhưng không thể chọc thủng hệ thống mới được triển khai [7].

Loại công nghệ nào mang lại cho Little Bird khả năng phòng thủ siêu hạng, để nó chặn đứng mọi đòn tấn công? Câu trả lời là: phương pháp xác minh chính thức.

Các phương pháp xác minh chính thức đảm bảo rằng hành vi của chương trình phù hợp với mong đợi thông qua các bằng chứng toán học nghiêm ngặt, nhưng tính đúng đắn của các chương trình xác minh chính thức rất tốn công sức. , chẳng hạn như xác minh tính chính xác của chương trình cho máy bay không người lái, tàu vũ trụ, hệ điều hành, v.v.

Điều tôi phải đề cập ở đây là Dirty Cow (CVE-2016-5195)[8], một lỗ hổng nhân hệ điều hành Linux rất nghiêm trọng được phát hiện vào năm 2016. Những kẻ tấn công có thể sử dụng lỗ hổng này để giành được đặc quyền cao nhất của hệ thống, do đó toàn bộ hệ thống có thể khai thác được.đang trong tình trạng sử dụng.

tiêu đề cấp đầu tiên

| Lĩnh vực blockchain quan trọng về bảo mật

Điều này cũng đúng trong lĩnh vực blockchain, một mặt, những sai lầm nhỏ có thể dẫn đến tổn thất lớn, mặt khác, lợi ích kinh tế to lớn cũng có thể thu hút một lượng lớn kẻ tấn công.

Trong vụ hack Ethereum lớn đầu tiên, The DAO, những kẻ tấn công đã đánh cắp Ethereum trị giá 55 triệu đô la Mỹ vào thời điểm đó, dẫn đến một đợt hard fork của Ethereum[11]; sau đó, các cuộc tấn công liên quan đến hợp đồng thông minh Ethereum đã được tiếp tục—chẳng hạn , vào tháng 11 năm 2017, ví Ethereum Parity đã bị hack, khiến người dùng mất tài sản kỹ thuật số trị giá khoảng 150 triệu đô la [11].

Theo thống kê từ Ambi Labs, chỉ trong nửa đầu năm 2018, khoảng 1,1 tỷ đô la tài sản kỹ thuật số đã bị đánh cắp và các lỗ hổng liên quan đến hệ thống chuỗi khối (chẳng hạn như lỗ hổng hợp đồng thông minh trong Ethereum) và hệ sinh thái xung quanh tài sản kỹ thuật số Các vấn đề bảo mật (chẳng hạn như như hành vi trộm cắp của nhiều sàn giao dịch tập trung) đang nổi lên như một dòng vô tận.

Hiện tại, các lỗ hổng liên quan trong hệ thống chuỗi khối và các vấn đề bảo mật của hệ sinh thái tài sản kỹ thuật số cuối cùng đều liên quan đến việc thiết kế và triển khai các chương trình liên quan. Trước các phương pháp chính thức, những vấn đề như vậy chủ yếu được tìm thấy thông qua thử nghiệm chương trình.

Trong những ngày đầu khi xác minh chính thức được đưa vào lĩnh vực blockchain, Yoichi Hirai của cộng đồng Ethereum đã thực hiện một mô hình chính thức hoàn chỉnh về EVM máy ảo hợp đồng thông minh của Ethereum. Ngoài ra, một nhóm từ Đại học UIUC cũng chính thức lập mô hình và xác minh EVM [12]. EVM là cốt lõi cơ bản của hợp đồng thông minh Ethereum, liên quan đến tính bảo mật của Ethereum và liên quan đến các vấn đề lớn như bảo vệ tài sản kỹ thuật số, đã thu hút sự chú ý rộng rãi của cộng đồng.

Ngoài ra, dự án MakerDAO đã phát hành ứng dụng phi tập trung (DApp) đầu tiên được xác minh chính thức [13]. MakerDAO là một nền tảng hợp đồng thông minh dựa trên Ethereum, cung cấp stablecoin, khoản vay thế chấp và các chức năng quản trị cộng đồng phi tập trung. Để đảm bảo tính bảo mật của các hợp đồng thông minh được triển khai, nhóm MakerDAO đã xác minh mã hợp đồng của hợp đồng động cơ cốt lõi của khoản vay thế chấp (CDP) thông qua K-Framewok, từ đó cho thấy chương trình hợp đồng thông minh của họ hoàn toàn có thể chống lại các cuộc tấn công của tin tặc.

Ambi Labs cũng đã thực hiện rất nhiều công việc về xác minh chính thức hợp đồng thông minh Ethereum, đề xuất khung xác minh chính thức cho hợp đồng thông minh và chứng minh một số hợp đồng Token phổ biến trong khuôn khổ này, chẳng hạn như ERC20, ERC721, v.v. (bao gồm các chức năng Chung như như chuyển khoản, tổng số lượng Token, v.v.). Các hợp đồng thông minh đã được chứng minh bằng toán học này có thể được sử dụng trực tiếp mà không phải lo lắng về các vấn đề bảo mật. Các mã nguồn hợp đồng và quy trình chứng minh này đã được đóng góp cho cộng đồng dưới dạng mã nguồn mở [14].

tiêu đề cấp đầu tiên

https://github.com/sec-bit/tokenlibs-with-proofs

|Kết luận

Hầu hết mọi người đều cho rằng phương pháp xác minh chính thức là không thể đo lường được, lý do là phương pháp xác minh chính thức không phải là một công nghệ chung mà là một công nghệ cụ thể cần được kết hợp với lĩnh vực này để phát huy giá trị của nó. Trong lĩnh vực chuỗi khối, cho dù phương pháp chính thức là tốt hay phải có cũng không thể tách rời khỏi đặc điểm của dự án.

Khi việc khám phá công nghệ chuỗi khối và các ứng dụng dự án tiếp tục sâu rộng hơn, yêu cầu của bên dự án về việc tránh sai lầm, chống lại các cuộc tấn công của tin tặc và tránh tổn thất tài sản ngày càng trở nên mạnh mẽ hơn.

tiêu đề cấp đầu tiên

Viết ở cuối | Bạn biết bao nhiêu về sự vướng víu giữa Xác minh và Kiểm tra?

Cuối cùng, hãy nói về mối quan hệ giữa Xác minh chính thức và Thử nghiệm.

"Thử nghiệm chương trình có thể chứng minh sự tồn tại của lỗi, nhưng nó không thể chứng minh là không có lỗi." Edsger Dijkstra (người đoạt giải Turing năm 1972 và là người đề xuất ý tưởng cốt lõi của phương pháp hình thức) đã nhận xét như vậy.

Trong thực tế, đặc biệt là trong các tình huống mà mã đủ phức tạp, hiệu quả xác minh của xác minh chính thức (Xác minh) và phương pháp kiểm tra chương trình (Thử nghiệm) khác nhau như mây và bùn.

Ví dụ: Năm 2009, các nhà khoa học ở Úc đã sử dụng các phương pháp chính thức để tiến hành xác minh chức năng hoàn chỉnh của hạt nhân seL4 của hệ điều hành cấp công nghiệp [15]. kết quả của việc xác minh là: hơn 460 lỗi được tìm thấy bằng phương pháp chính thức, nhưng chỉ có 16 lỗi được tìm thấy bằng kiểm tra chương trình.

Điều thú vị hơn là trong lĩnh vực xác minh chính thức được biết đến với chi phí xác minh cao, chi phí xác minh để xác minh đầy đủ vi hạt nhân seL4 chỉ là 6 triệu đô la Mỹ, trong khi chi phí để vượt qua chứng nhận CC EAL6 bằng thử nghiệm cao tới 87 triệu đô la Mỹ. triệu đô la Mỹ [15 ].

Có thể thấy rằng việc xác minh chính thức có thể mang lại sự đảm bảo an ninh mạnh mẽ hơn cho hạt nhân seL4 một cách kinh tế hơn.

người giới thiệu

người giới thiệu

【1】History of Formal Verification at Intel

https://dac.com/blog/post/history-formal-verification-intel

[2] Wang Jian: Hãy nói về Xác minh chính thức

http://chainb.com/?P=Cont&id=1957

【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher

https://link.springer.com/chapter/10.1007/11768869_6

【4】Tenth NASA Formal Methods Symposium 

https://shemesh.larc.nasa.gov/NFM2018/

[5] Hệ điều hành SpaceOS nội địa do Yutu sử dụng dự kiến ​​sẽ được chuyển thành phiên bản dân sự trong tương lai

http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html

【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.

【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/

[8] Sử dụng Dirty Cow để thoát docker

https://www.anquanke.com/post/id/84866

【9】CertiKOS: Yale develops world’s first hacker-resistant operating system

https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712

【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)

【11】Phân tích các phương pháp tấn công THE DAO từ quan điểm kỹ thuật

https://www.8btc.com/article/93713

【12】kframework/evm-semantics

https://github.com/kframework/evm-semantics

【13】Đầu tư mạo hiểm khổng lồ A16Z đầu tư vào dự án tiền tệ ổn định MakerDAO

https://www.jinse.com/bitcoin/246582.html

[14] Xây dựng bằng chứng chính thức để giải quyết vấn đề bảo mật hợp đồng thông minh - hợp đồng của bạn cần được chứng minh gấp

https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg

【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09).