Vitalik: Chìa khóa cho giai đoạn tiếp theo của Ethereum là gì?
Tuyển chọn TechFlowTuyển chọn TechFlow
Vitalik: Chìa khóa cho giai đoạn tiếp theo của Ethereum là gì?
“Mã nguồn là pháp luật” — đây là một trong những niềm tin đầu tiên của thế giới blockchain. Nhưng nếu chính mã nguồn đó chứa lỗi (bug) thì sao?
Chuyên sâu báo cáo Web3Tác giả: Vitalik Buterin
Biên dịch: Gia Hoan, ChainCatcher
Cảm ơn đặc biệt Yoichi Hirai, Justin Drake, Nadim Kobeissi và Alex Hicks đã cung cấp phản hồi và hiệu đính.
Trong vài tháng qua, một kiểu lập trình mới đã nhanh chóng trở nên phổ biến trong giới nghiên cứu tiên phong về Ethereum cũng như nhiều lĩnh vực tính toán khác: viết mã trực tiếp bằng các ngôn ngữ rất thấp cấp (ví dụ: mã byte EVM, ngôn ngữ lắp ráp) hoặc Lean, đồng thời sử dụng các chứng minh toán học tự động kiểm chứng được—được viết bằng Lean—để xác minh tính đúng đắn của mã đó.
Nếu thực hiện đúng cách, phương pháp này không chỉ có khả năng tạo ra mã cực kỳ hiệu quả mà còn an toàn hơn đáng kể so với mọi cách lập trình trước đây. Yoichi Hirai gọi đây là “hình thái tối thượng của phát triển phần mềm”.
Bài viết này sẽ cố gắng làm rõ những nguyên lý cơ bản đằng sau phương pháp này, khám phá những điều mà việc xác minh hình thức (formal verification) có thể làm được đối với phần mềm, cũng như những điểm yếu và giới hạn của nó trong bối cảnh Ethereum và các lĩnh vực khác.
Xác minh hình thức là gì?
Xác minh hình thức là việc viết các chứng minh cho các định lý toán học theo cách có thể được kiểm tra tự động. Để minh họa bằng một ví dụ tương đối đơn giản nhưng vẫn thú vị, hãy xem xét một định lý cơ bản về dãy Fibonacci: mỗi số thứ ba là số chẵn, còn lại là số lẻ.
1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 ...
Một cách chứng minh đơn giản là dùng quy nạp toán học, tiến từng bước ba số một.
Đầu tiên là trường hợp cơ sở. Đặt F₁ = F₂ = 1, F₃ = 2. Quan sát cho thấy mệnh đề (“Fᵢ là số chẵn nếu i chia hết cho 3, ngược lại là số lẻ”) đúng với mọi i < 3.
Tiếp theo là bước quy nạp. Giả sử mệnh đề đúng với mọi số nhỏ hơn 3k+3, tức là ta đã biết tính chẵn lẻ của F₃ₖ₊₁, F₃ₖ₊₂ và F₃ₖ₊₃ lần lượt là lẻ, lẻ và chẵn. Ta có thể tính tính chẵn lẻ của ba số tiếp theo:
F₃ₖ₊₄ = F₃ₖ₊₂ + F₃ₖ₊₃ = lẻ + chẵn = lẻ
F₃ₖ₊₅ = F₃ₖ₊₃ + F₃ₖ₊₄ = chẵn + lẻ = lẻ
F₃ₖ₊₆ = F₃ₖ₊₄ + F₃ₖ₊₅ = lẻ + lẻ = chẵn
Do đó, từ việc mệnh đề đúng với mọi số nhỏ hơn 3k+3, ta suy ra nó cũng đúng với mọi số nhỏ hơn 3k+6. Bằng cách áp dụng lặp lại suy luận này, ta khẳng định chắc chắn rằng quy luật trên đúng với mọi số nguyên.
Lập luận này đủ thuyết phục con người. Nhưng nếu bạn muốn chứng minh một điều phức tạp hơn gấp trăm lần và muốn cực kỳ chắc chắn rằng mình không mắc sai sót nào thì sao? Khi ấy, bạn có thể cung cấp cho máy tính một chứng minh mà nó có thể tin tưởng.
Dưới đây là cách trình bày cụ thể:
-- Dãy Fibonacci với fib 0 = 0, fib 1 = 1, fib 2 = 1 (chỉ số bị dịch 1 đơn vị)def fib : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fib (n + 1) + fib n-- Phát biểu: fib (3k+1) là số lẻ, fib (3k+2) là số lẻ, fib (3k+3) là số chẵn.-- Tương đương: mỗi số Fibonacci thứ ba kể từ fib 3 là số chẵn.-- Chúng ta chứng minh cả ba phát biểu này đồng thời bằng quy nạp theo k, vì mỗi trường hợp trong khối tiếp theo đều được xây dựng từ khối trước.theorem fib_triple (k : Nat) : fib (3 * k + 1) % 2 = 1 ∧ fib (3 * k + 2) % 2 = 1 ∧ fib (3 * k + 3) % 2 = 0 := by induction k with | zero => decide | succ k ih => -- Viết lại các chỉ số mới dưới dạng (cái-gì-đó) + 2 để fib có thể mở rộng. refine ⟨?_, ?_, ?_⟩ · show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1 omega · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1 omega · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3) + (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0 omega
Đây là cùng một lập luận, nhưng được biểu đạt bằng ngôn ngữ Lean — một ngôn ngữ lập trình thường được dùng để viết và xác minh các chứng minh toán học.
Nó trông khác hẳn với chứng minh “cho con người đọc” ở trên, và điều đó hoàn toàn dễ hiểu: những điều trực quan đối với máy tính (theo nghĩa truyền thống, tức là chương trình “xác định” gồm các câu lệnh if/then, chứ không phải mô hình ngôn ngữ lớn) hoàn toàn khác biệt với những điều trực quan đối với con người.
Trong chứng minh trên, bạn không nhấn mạnh vào sự kiện fib(3k+4) = fib(3k+3) + fib(3k+2), mà thay vào đó nhấn mạnh rằng fib(3k+3) + fib(3k+2) là số lẻ, và chiến lược tên gọi hoành tráng trong Lean mang tên “omega” sẽ tự động kết hợp điều này với kiến thức của nó về định nghĩa fib(3k+4).
Trong các chứng minh phức tạp hơn, đôi khi bạn phải chỉ rõ từng bước là dựa trên định luật toán học nào, thậm chí còn phải dùng đến những tên gọi khó hiểu như Prod.mk.inj.
Nhưng mặt khác, bạn có thể khai triển một biểu thức đa thức khổng lồ trong một bước duy nhất và chỉ cần một dòng lệnh như “omega” hay “ring” để chứng minh tính đúng đắn của nó.
Sự thiếu trực quan và rườm rà này phần lớn giải thích vì sao dù chứng minh có thể kiểm tra bởi máy tính đã tồn tại gần 60 năm, lĩnh vực này vẫn còn khá nhỏ hẹp. Tuy nhiên, mặt khác, nhờ sự phát triển nhanh chóng của trí tuệ nhân tạo, nhiều điều từng được coi là bất khả thi giờ đây đang nhanh chóng trở thành hiện thực.
Khi các chứng minh toán học bắt đầu bảo vệ mã nguồn
Tới đây, bạn có thể nghĩ: “Được rồi, máy tính có thể xác minh các chứng minh định lý toán học rồi, vậy cuối cùng chúng ta đã có thể xác định chắc chắn đâu là những kết luận mới điên rồ về số nguyên tố thực sự đúng, và đâu chỉ là những sai lầm trong bài báo PDF dài trăm trang.”
Thậm chí có thể chúng ta sẽ làm rõ được liệu quan điểm của Shinichi Mochizuki về giả thuyết ABC có đúng hay không!
Nhưng bỏ qua tò mò thuần túy, điều đó có ý nghĩa gì?
Có rất nhiều câu trả lời khả dĩ. Nhưng với tôi, một đáp án đặc biệt quan trọng là xác minh tính đúng đắn của các chương trình máy tính, đặc biệt là những chương trình thực hiện các tác vụ mật mã hoặc liên quan đến bảo mật.
Dẫu sao, chương trình máy tính là một đối tượng toán học, do đó chứng minh rằng một chương trình máy tính hoạt động theo một cách nhất định bản thân nó chính là một định lý toán học.
Ví dụ, giả sử bạn muốn chứng minh phần mềm giao tiếp mã hóa như Signal thực sự an toàn. Bạn có thể viết ra định nghĩa toán học cho khái niệm “an toàn” trong bối cảnh này.
Ở mức độ cao, bạn cần chứng minh rằng, dưới giả thiết một số giả định mật mã nhất định đúng, chỉ người nắm giữ khóa riêng mới có thể biết bất kỳ thông tin nào về nội dung tin nhắn. Trong thực tế, có rất nhiều thuộc tính an toàn khác nhau đều rất quan trọng.
Hóa ra thật vậy, có một nhóm nghiên cứu đang cố gắng giải quyết chính vấn đề này! Một trong những định lý an toàn của họ trông như sau:
theorem passive_secrecy_le_ddh (g : G) (adv : PassiveAdversary G SK) : passiveSecrecyAdvantage (F := F) g adv ≤ ProbComp.boolDistAdvantage (DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv)) (DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))
Dưới đây là tóm tắt của Leanstral về ý nghĩa của định lý này:
Định lý passive_secrecy_le_ddh là một phép quy giảm gọn, cho thấy tính bảo mật thông tin thụ động của X3DH ít nhất khó phá vỡ như giả định DDH trong mô hình tiên tri ngẫu nhiên. Nếu kẻ tấn công có thể phá vỡ tính bảo mật thông tin thụ động của X3DH, thì chúng cũng có thể phá vỡ DDH.
Vì chúng ta giả định DDH rất khó phá vỡ, nên X3DH cũng an toàn trước các cuộc tấn công thụ động. Định lý này chứng minh rằng nếu kẻ tấn công có thể quan sát thụ động các thông điệp trao đổi khóa của Signal, chúng sẽ không thể phân biệt được khóa phiên được tạo ra với một khóa ngẫu nhiên với xác suất vượt quá một lượng có thể bỏ qua.
Nếu kết hợp điều này với chứng minh rằng việc triển khai mã hóa AES là đúng, bạn sẽ có được chứng minh rằng giao thức Signal an toàn trước các kẻ tấn công thụ động.
Các dự án tương tự cũng đã chứng minh tính an toàn của các triển khai TLS và các phần khác của mật mã trong trình duyệt.
Nếu bạn thực hiện xác minh hình thức đầy đủ từ đầu tới cuối, bạn không chỉ chứng minh rằng một mô tả lý thuyết nào đó của giao thức là an toàn, mà còn chứng minh rằng mã cụ thể mà người dùng chạy trong thực tế cũng an toàn.
Từ góc nhìn người dùng, điều này nâng cao đáng kể mức độ không cần tin cậy (trustlessness): để tin tưởng hoàn toàn vào mã, bạn không cần kiểm tra toàn bộ kho mã, mà chỉ cần kiểm tra các tuyên bố mà nó được chứng minh là đúng.
Hiện nay, có một số tiền đề lớn quan trọng cần ghi nhớ, đặc biệt là về việc từ then chốt “an toàn” thực chất có nghĩa là gì.
Người ta dễ dàng quên chứng minh những tuyên bố thực sự quan trọng. Cũng dễ nhận thấy đôi khi tuyên bố cần chứng minh lại không hề đơn giản hơn mô tả mã nguồn.
Dễ dàng vô tình đưa vào chứng minh những giả định cuối cùng lại không đúng. Cũng dễ rơi vào tình trạng chỉ chọn một phần hệ thống để chứng minh hình thức, nhưng lại bị đánh bại bởi những lỗ hổng nghiêm trọng ở các phần khác (thậm chí cả phần cứng).
Ngay cả bản thân triển khai Lean cũng có thể chứa lỗi. Nhưng trước khi bàn đến tất cả những chi tiết phiền toái này, hãy cùng đi sâu vào viễn cảnh Utopia mà xác minh hình thức, khi được thực hiện đúng và lý tưởng, có thể mang lại.
Xác minh hình thức vì mục tiêu an toàn
Lỗi trong mã máy tính thật đáng sợ.
Khi bạn gửi tiền điện tử vào một hợp đồng thông minh trên chuỗi bất biến, và Triều Tiên có thể tự động rút sạch toàn bộ tài sản của bạn bất cứ khi nào mã gặp lỗi mà bạn không thể kháng cáo, thì lỗi trong mã lại càng đáng sợ hơn.
Khi tất cả điều này được đóng gói trong một bằng chứng kiến thức không (zero-knowledge proof), lỗi lại càng đáng sợ hơn nữa, bởi vì nếu ai đó thành công trong việc xâm nhập hệ thống bằng chứng kiến thức không, họ có thể rút toàn bộ tiền, trong khi chúng ta hoàn toàn không biết điều gì đã xảy ra (và tệ hơn nữa, thậm chí còn không biết khi nào điều đó xảy ra).
Khi chúng ta sở hữu các mô hình AI mạnh mẽ, ví dụ như Claude Mythos sau hai vòng lặp cải tiến nữa, có khả năng tự động phát hiện những lỗi này, thì lỗi trong mã lại càng đáng sợ hơn nữa.
Một số người phản ứng trước thực tế này bằng cách kêu gọi từ bỏ hoàn toàn ý tưởng về hợp đồng thông minh, thậm chí cho rằng lĩnh vực mạng lưới vốn không thể trở thành nơi phòng thủ có lợi thế bất cân xứng so với kẻ tấn công.
Một số trích dẫn:
“Để gia cố một hệ thống, bạn cần chi tiêu nhiều hơn kẻ tấn công về mặt chi phí để tìm ra lỗ hổng.”
Và:
“Ngành công nghiệp của chúng ta được xây dựng trên nền tảng của mã xác định. Viết nó, kiểm thử nó, phát hành nó, và tin chắc rằng nó sẽ hoạt động—nhưng theo kinh nghiệm của tôi, thỏa thuận này đang dần sụp đổ.”
“Trong số những nhà vận hành hàng đầu của các công ty thực sự gốc AI, kho mã giờ đây đã trở thành thứ mà bạn ‘tin rằng’ nó sẽ hoạt động, chứ bạn không còn có thể xác định chính xác xác suất thành công của nó nữa.”
Tệ hơn nữa, một số người cho rằng giải pháp duy nhất là từ bỏ mã nguồn mở.
Đối với an ninh mạng, đó sẽ là một tương lai u ám. Đặc biệt đối với những người quan tâm đến sự phi tập trung và tự do trên Internet, đây là một viễn cảnh bi quan đến mức cực đoan.
Toàn bộ tinh thần mật mã (cypherpunk) được xây dựng trên một niềm tin cốt lõi: trên Internet, bên phòng thủ có lợi thế; việc xây dựng một “pháo đài kỹ thuật số” (dù là mã hóa, chữ ký hay bằng chứng) dễ dàng hơn nhiều so với việc phá hủy nó.
Nếu chúng ta đánh mất điều này, thì an ninh mạng sẽ chỉ còn phụ thuộc vào lợi thế kinh tế nhờ quy mô, phụ thuộc vào việc truy tìm kẻ tấn công tiềm tàng trên toàn cầu, và nói rộng hơn, chỉ còn lựa chọn giữa thống trị và hủy diệt.
Tôi không đồng ý với điều đó, và tôi có một tầm nhìn lạc quan hơn về tương lai của an ninh mạng.
Tôi cho rằng thách thức do khả năng tìm lỗi mạnh mẽ của AI mang lại là nghiêm trọng, nhưng chỉ là một thách thức mang tính chuyển tiếp. Một khi mọi thứ lắng xuống và chúng ta đạt tới trạng thái cân bằng mới, môi trường an ninh sẽ nghiêng mạnh hơn về phía bên phòng thủ so với quá khứ.
Mozilla đồng ý với quan điểm của tôi. Trích dẫn từ họ:
“Bạn có thể cần điều chỉnh lại ưu tiên của mọi thứ khác, dành toàn lực và tập trung liên tục vào nhiệm vụ này, nhưng cuối đường hầm vẫn có ánh sáng.”
“Chúng tôi rất tự hào về cách đội ngũ của mình đối mặt với thách thức này, và những người khác cũng sẽ làm được. Công việc của chúng tôi chưa hoàn tất, nhưng chúng tôi đã vượt qua giai đoạn khó khăn nhất và có thể thoáng nhìn thấy một tương lai không chỉ tạm đủ theo kịp, mà còn tốt đẹp hơn nhiều.”
“Bên phòng thủ cuối cùng đã có cơ hội giành chiến thắng quyết định… Các lỗi là hữu hạn, và chúng ta đang bước vào một thế giới nơi cuối cùng chúng ta có thể tìm ra hết tất cả chúng.”
Giờ đây, nếu bạn dùng Ctrl+F để tìm các từ “hình thức” và “xác minh” trong bài đăng của Mozilla, bạn sẽ thấy không có kết quả nào khớp. Tương lai tích cực của an ninh mạng không hoàn toàn phụ thuộc vào xác minh hình thức, hay bất kỳ công nghệ đơn lẻ nào khác.
Vậy nó phụ thuộc vào cái gì? Về cơ bản là biểu đồ sau:
Xu hướng giảm số lượng lỗ hổng CVE theo thời gian
Trong vài thập kỷ qua, nhiều công nghệ đã góp phần làm giảm số lượng lỗ hổng:
- Hệ thống kiểu dữ liệu (type system)
- Ngôn ngữ đảm bảo an toàn bộ nhớ
- Cải tiến kiến trúc phần mềm (bao gồm cách ly môi trường (sandboxing), kiểm soát quyền hạn, và nói rộng hơn là phân biệt rõ ràng giữa “cơ sở tính toán đáng tin cậy” và “các mã khác”)
- Phương pháp kiểm thử tốt hơn
- Kiến thức ngày càng phong phú về các mẫu mã hóa an toàn và không an toàn
- Các thư viện phần mềm được viết sẵn và kiểm toán kỹ lưỡng ngày càng tăng
Xác minh hình thức được hỗ trợ bởi AI không nên được xem là một phạm trù mới hoàn toàn, mà nên được coi là một bộ tăng tốc mạnh mẽ cho xu hướng và phạm trù đang phát triển.
Xác minh hình thức không phải là “thuốc thần”. Tuy nhiên, nó đặc biệt phù hợp trong các tình huống mà mục tiêu cần đạt được đơn giản hơn nhiều so với cách triển khai. Điều này đặc biệt đúng với một số công nghệ phức tạp và nan giải mà chúng ta sẽ cần triển khai trong phiên bản chủ chốt tiếp theo của Ethereum: chữ ký chống lượng tử, STARKs, thuật toán đồng thuận và ZK-EVMs.
STARK là một phần mềm rất phức tạp. Nhưng thuộc tính an toàn cốt lõi mà nó thực hiện lại dễ hiểu và dễ xác minh hình thức: nếu bạn thấy một bằng chứng cho chương trình P với hàm băm H, đầu vào x và đầu ra y, thì hoặc (i) hàm băm được dùng trong STARK đã bị phá vỡ, hoặc (ii) P(x) = y.
Do đó, chúng ta có dự án Arklib, đang cố gắng tạo ra một triển khai STARK được xác minh hình thức hoàn toàn (xem VCV-io, cung cấp cơ sở hạ tầng tính toán tiên tri cơ bản để xác minh hình thức nhiều giao thức mật mã khác, trong đó nhiều giao thức là phụ thuộc của STARK).
Tham vọng hơn nữa là evm-asm: một dự án nhằm xây dựng một triển khai EVM hoàn toàn được xác minh hình thức.
Ở đây thuộc tính an toàn lại không đơn giản như vậy: về cơ bản, mục tiêu là chứng minh nó tương đương với một triển khai EVM khác được viết bằng Lean, tuy nhiên triển khai này có thể được viết để tối đa hóa tính trực quan và dễ đọc, hoàn toàn không cần quan tâm đến hiệu suất chạy cụ thể.
Có thể chúng ta sẽ có mười triển khai EVM, tất cả đều có thể chứng minh được là tương đương lẫn nhau, và tình cờ tất cả đều chứa cùng một lỗi chết người cho phép kẻ tấn công rút sạch toàn bộ ETH từ các địa chỉ mà chúng không có quyền truy cập.
Nhưng khả năng xảy ra tình huống này thấp hơn nhiều so với khả năng một triển khai EVM hiện tại tồn tại lỗi như vậy. Còn một thuộc tính an toàn khác, mà chúng ta chỉ hiểu được tầm quan trọng của nó sau những bài học đau đớn, là khả năng chống tấn công từ chối dịch vụ (DoS), thì lại rất dễ đặc tả.
Hai lĩnh vực quan trọng khác là:
- Đồng thuận chịu lỗi Byzantine. Ở đây, việc đặc tả hình thức tất cả các thuộc tính an toàn mong muốn cũng khó khăn, nhưng do lỗi từng xuất hiện phổ biến đến mức vẫn đáng để thử. Vì vậy, chúng ta đang có các triển khai và chứng minh giao thức đồng thuận trong Lean.
- Ngôn ngữ lập trình hợp đồng thông minh: xem xác minh hình thức trong Vyper và Verity.
Trong tất cả các trường hợp này, một trong những giá trị gia tăng lớn nhất của xác minh hình thức nằm ở chỗ các chứng minh này thực sự là “đầu cuối” (end-to-end). Thông thường, những lỗi khó chịu nhất là lỗi tương tác (interaction bugs), ẩn nấp ở ranh giới giữa hai tiểu hệ thống được xem xét độc lập.
Đối với con người, việc suy luận toàn bộ hệ thống từ đầu đến cuối là quá khó khăn. Nhưng hệ thống kiểm tra quy tắc tự động thì có thể làm được điều đó.
Xác minh hình thức vì mục tiêu hiệu quả
Hãy xem lại evm-asm. Đây là một triển khai EVM. Nhưng đây là một triển khai EVM được viết trực tiếp bằng mã lắp ráp RISC-V.
Thật vậy.
Đây là mã lệnh ADD:
import EvmAsm.Rv64.Programnamespace EvmAsm.Evm64open EvmAsm.Rv64/-- 256-bit EVM ADD: binary, pops 2, pushes 1. Limb 0: LD, LD, ADD, SLTU (carry), SD (5 instructions). Limbs 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (8 each). Then ADDI sp, sp, 32. Registers: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/def evm_add : Program := -- Limb 0 (5 instructions) LD .x7 .x12 0 ;; LD .x6 .x12 32 ;; ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;; -- Limb 1 (8 instructions) LD .x7 .x12 8 ;; LD .x6 .x12 40 ;; ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;; ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;; OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;; -- Limb 2 (8 instructions) LD .x7 .x12 16 ;; LD .x6 .x12 48 ;; ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;; ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;; OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;; -- Limb 3 (8 instructions) LD .x7 .x12 24 ;; LD .x6 .x12 56 ;; ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;; ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;; OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;; -- sp adjustment ADDI .x12 .x12 32end EvmAsm.Evm64
Lý do chọn RISC-V là vì bộ chứng minh ZK-EVM đang được xây dựng thường hoạt động bằng cách chứng minh RISC-V và biên dịch client Ethereum sang RISC-V. Do đó, nếu bạn có một triển khai EVM được viết trực tiếp bằng RISC-V, thì đây sẽ là triển khai nhanh nhất mà bạn có thể đạt được.
RISC-V cũng có thể được mô phỏng rất hiệu quả trên máy tính thông thường (và hiện nay trên thị trường đã có laptop RISC-V).
Tất nhiên, để thực sự đạt được tính đầu cuối, bạn phải xác minh hình thức chính triển khai RISC-V (hoặc phép số học hóa của bộ chứng minh), nhưng đừng lo, công việc này cũng đã tồn tại.
Viết mã trực tiếp bằng mã lắp ráp là điều chúng ta thường làm cách đây năm mươi năm. Từ đó đến nay, chúng ta đã từ bỏ việc này và chuyển sang viết mã bằng các ngôn ngữ cấp cao.
Các ngôn ngữ cấp cao chấp nhận đánh đổi hiệu quả để đổi lấy việc viết mã nhanh hơn rất nhiều, và quan trọng hơn, việc hiểu mã của người khác cũng nhanh hơn rất nhiều—điều này là thiết yếu cho bảo mật.
Nhờ sự kết hợp giữa xác minh hình thức và trí tuệ nhân tạo, chúng ta có cơ hội “trở về tương lai”.
Cụ thể, chúng ta có thể để AI viết mã lắp ráp, sau đó viết một chứng minh hình thức để xác minh mã lắp ráp đó có các thuộc tính mong muốn.
Ít nhất, các thuộc tính mong muốn có thể đơn giản chỉ là tương đương hoàn hảo với một triển khai được tối ưu hóa cho tính dễ đọc, được viết bằng một ngôn ngữ cấp cao thân thiện với con người.
Chúng ta không còn cần một đối tượng mã duy nhất phải cân bằng giữa tính dễ đọc và hiệu quả nữa, mà thay vào đó sở hữu hai đối tượng độc lập: một (triển khai mã lắp ráp) chỉ tối ưu hóa hiệu quả, đồng thời xem xét nhu cầu cụ thể của môi trường thực thi; đối tượng kia (tuyên bố an toàn, hoặc triển khai ngôn ngữ cấp cao) chỉ tối ưu hóa tính dễ đọc, sau đó chúng ta dùng chứng minh toán học để chứng minh tính tương đương giữa hai đối tượng.
Người dùng có thể (tự động) xác minh một lần chứng minh này, và từ đó chỉ cần chạy phiên bản nhanh.
Phương pháp này rất mạnh mẽ, và Yoichi Hirai gọi nó là “hình thái tối thượng của phát triển phần mềm” là có lý do.
Xác minh hình thức không phải là thuốc thần
Trong lĩnh vực mật mã và khoa học máy tính, có một truyền thống gần như lâu đời ngang với lịch sử của chính các phương pháp hình thức: đó là truyền thống chỉ trích các phương pháp hình thức (hoặc nói rộng hơn là chỉ trích sự phụ thuộc vào “chứng minh”).
Các tài liệu này đầy ắp các ví dụ thực tế. Hãy bắt đầu từ những chứng minh viết tay trong thời kỳ mật mã sơ khai, trích dẫn phê bình của Menezes và Koblitz năm 2004:
Năm 1979, Rabin đề xuất một hàm mã hóa được cho là “có thể chứng minh” an toàn theo một nghĩa nào đó, tức là có một thuộc tính an toàn dạng quy giảm.
Phát biểu an toàn dạng quy giảm nêu rằng người có thể tìm ra thông điệp m từ văn bản mã y cũng phải có khả năng phân tích thừa số n… Ngay sau khi Rabin đề xuất sơ đồ mã hóa của mình, Rivest chỉ ra một nghịch lý: chính đặc tính mang lại thêm tính an toàn cho sơ đồ này lại khiến nó sụp đổ hoàn toàn trước một loại kẻ tấn công khác mang tên “tấn công văn bản mã được chọn”.
Nói cách khác, nếu kẻ tấn công có thể bằng cách nào đó lừa Alice giải mã một văn bản mã do chúng chọn, thì kẻ tấn công có thể làm theo đúng các bước mà Sam đã dùng trong đoạn trên để phân tích thừa số n.
Menezes và Koblitz sau đó đưa ra thêm nhiều ví dụ. Quy luật chung là: các thiết kế nhằm làm cho giao thức mã hóa trở nên “có thể chứng minh” hơn thường khiến chúng trở nên kém “tự nhiên” hơn, do đó khả năng chúng sụp đổ trong các tình huống mà chính người thiết kế thậm chí chưa từng nghĩ tới là cao hơn.
Bây giờ, hãy trở lại với các chứng minh có thể kiểm tra bằng máy và mã nguồn. Đây là một bài báo năm 2011 phát hiện ra lỗi trong trình biên dịch C được xác minh hình thức CompCert:
Vấn đề thứ hai chúng tôi phát hiện trong CompCert thể hiện ở hai lỗi gây ra việc sinh ra mã sau: stwu r1, -44432(r1). Ở đây đang cấp phát một vùng stack frame PowerPC lớn.
Vấn đề nằm ở việc trường dịch chuyển 16 bit bị tràn. Ngữ nghĩa PPC của CompCert không quy định giới hạn về độ rộng của toán hạng ngay lập tức này, và họ giả định trình biên dịch sẽ bắt được các giá trị vượt ngoài phạm vi.
Còn đây là một bài báo năm 2022:
Trong CompCert-KVX, commit e2618b31 đã sửa một lỗi: lệnh “nand” bị in ra thành “and”; “nand” chỉ được dùng trong mẫu rất hiếm ~(a & b). Lỗi này được phát hiện bằng cách biên dịch các chương trình được sinh ngẫu nhiên.
Và hôm nay, năm 2026, đây là mô tả của Nadim Kobeissi về các lỗ hổng trong phần mềm được xác minh hình thức tại Cryspen:
Tháng 11 năm 2025, Filippo Valsorda độc lập báo cáo rằng libcrux-ml-dsa v0.0.3 tạo ra các khóa công khai và chữ ký khác nhau trên các nền tảng khác nhau khi được cung cấp cùng một đầu vào xác định.
Lỗi này nằm trong hàm bao (_vxarq_u64) bên trong, thực hiện phép toán XAR được dùng trong hoán vị Keccak-f của SHA-3. Cơ chế dự phòng truyền tham số sai cho phép toán dịch chuyển, làm hỏng bản tóm tắt SHA-3 trên các nền tảng ARM64 không hỗ trợ phần cứng SHA-3.
Đây thuộc loại lỗi I: hàm nội bộ này được gắn thẻ, nhưng toàn bộ backend NEON chưa hoàn tất chứng minh về tính an toàn hoặc tính đúng đắn trong thời gian chạy.
Và:
Thư viện libcrux-psq triển khai một giao thức tiền chia sẻ khóa hậu lượng tử. Trong phương thức decrypt_out, đường dẫn giải mã AES-GCM 128 gọi .unwrap() trên kết quả giải mã thay vì lan truyền lỗi. Một văn bản mã bị định dạng sai có thể khiến tiến trình sập.
Bốn vấn đề trên đều thuộc một trong hai loại sau:
- Chỉ xác minh một phần mã (vì xác minh phần còn lại quá khó), nhưng kết quả cho thấy phần chưa được xác minh lại chứa nhiều lỗ hổng hơn và nghiêm trọng hơn so với những gì tác giả tưởng tượng.
- Tác giả quên quy định các thuộc tính then chốt cần chứng minh.
Bài viết của Nadim bao gồm phân loại các mô hình thất bại của xác minh hình thức; ông cũng đưa ra các loại thất bại khác (ví dụ, một loại chính khác là “đặc tả hình thức bản thân đã sai, hoặc chứng minh chứa các tuyên bố giả mà hệ thống xây dựng lặng lẽ chấp nhận”).
Cuối cùng, chúng ta có thể xem xét các thất bại của xác minh hình thức tại ranh giới phần mềm và phần cứng. Một vấn đề phổ biến ở đây là khả năng chứng minh tính chống lại các cuộc tấn công kênh bên (side-channel attacks).
Ngay cả khi bạn có dạng mã hóa an toàn tuyệt đối để bảo vệ tin nhắn, bạn vẫn không an toàn nếu người cách bạn vài mét có thể bắt được dao động tín hiệu điện và trích xuất khóa riêng của bạn sau hàng trăm nghìn lần mã hóa.
Đây là một bài viết về “phân tích công suất vi phân” (differential power analysis), một ví dụ điển hình về kỹ thuật loại này, hiện đã được hiểu rõ.
Phân tích công suất vi phân là một loại tấn công kênh bên phổ biến. Nguồn: Wikipedia
Luôn có người cố gắng chứng minh khả năng chống lại các kẻ tấn công như vậy. Tuy nhiên, bất kỳ chứng minh nào như vậy đều cần một mô hình toán học về kẻ tấn công, để bạn có thể chứng minh tính an toàn đối với mô hình đó.
Đôi khi người ta dùng “mô hình d-đo”: chúng ta giả định rằng kẻ tấn công có giới hạn đã biết về số vị trí có thể truy vấn trên mạch. Nhưng một số dạng rò rỉ lại không thể được mô hình này nắm bắt.
Như bài viết này quan sát, một vấn đề phổ biến là rò rỉ quá độ (transient leakage): nếu bạn có thể quan sát một tín hiệu không chỉ phụ thuộc vào giá trị tại một vị trí nào đó, mà còn phụ thuộc vào sự thay đổi của giá trị đó, thì điều này thường đủ để bạn khôi phục thông tin cần thiết từ hai giá trị (giá trị cũ và mới) thay vì chỉ một giá trị.
Bài viết này đưa ra phân loại các dạng rò rỉ khác.
Trong vài thập kỷ qua, những chỉ trích này đối với xác minh hình thức đã giúp xác minh hình thức ngày càng tốt hơn. So với quá khứ, giờ đây chúng ta giỏi hơn nhiều trong việc đề phòng các vấn đề như vậy. Nhưng ngay cả hôm nay, nó vẫn chưa hoàn hảo.
Nhìn tổng quan, ở đây có một sợi dây xuyên suốt. Xác minh hình thức rất mạnh mẽ.
Nhưng bất kể các thuật ngữ tiếp thị có làm cho xác minh hình thức nghe như thể nó trao cho bạn “tính đúng đắn có thể chứng minh”, thì “tính đúng đắn có thể chứng minh” ấy về bản chất không chứng minh được rằng phần mềm (hoặc phần cứng) là “đúng đắn”.
Theo cách hiểu phổ biến của đa số con người, “đúng đắn” có nghĩa gần giống như: “hành vi của hệ thống phù hợp với sự hiểu biết của người dùng về ý định của người phát triển”.
Còn “an toàn” có nghĩa gần giống như: “hành vi của hệ thống không vi phạm kỳ vọng của người dùng, không làm điều gì bất lợi cho lợi ích của họ”.
Trong cả hai trường hợp, tính đúng đắn và an toàn đều quy về việc so sánh một đối tượng toán học với ý định hoặc kỳ vọng của con người.
Ý định và kỳ vọng của con người về mặt kỹ thuật cũng là các đối tượng toán học, bởi lẽ bộ não con người cũng là một phần của vũ trụ, tuân theo các định luật vật lý mà nếu có đủ sức mạnh tính toán thì bạn có thể mô phỏng được.
Nhưng chúng là những đối tượng toán học vô cùng phức tạp, cả máy tính lẫn chính chúng ta đều không thể hiểu nổi, thậm chí không thể đọc được.
Về mọi mục đích thực tế, chúng là những “hộp đen”; chúng ta chỉ có chút hiểu biết nào đó về ý định và kỳ vọng của mình vì mỗi người đều có nhiều năm quan sát tư duy của bản thân và suy luận tư duy của người khác.
Và vì chúng ta không thể nhét trực tiếp ý định nguyên thủy của con người vào máy tính, nên xác minh hình thức không thể chứng minh sự so sánh với ý định của con người.
Do đó, “tính đúng đắn có thể chứng minh” và “tính an toàn có thể chứng minh” thực tế không chứng minh được “tính đúng đắn” và “tính an toàn” theo cách mà con người hiểu. Không điều gì có thể làm được điều này, trừ khi chúng ta có thể mô phỏng hoàn toàn bộ não người.
Vậy nó thực sự hữu ích ở đâu?
Tôi có xu hướng xem bộ kiểm thử, hệ thống kiểu dữ liệu và xác minh hình thức như những cách triển khai khác nhau của cùng một phương pháp nền tảng đối với tính an toàn của ngôn ngữ lập trình (đây có thể cũng là cách duy nhất hợp lý).
Tất cả đều liên quan đến việc đặc tả ý định của chúng ta theo nhiều cách khác nhau một cách dư thừa, sau đó tự động kiểm tra xem các đặc tả khác nhau này có tương thích với nhau hay không.
Hãy xem đoạn mã Python sau:
def fib(n: int) -> int: if n < 0: raise Exception("Negative values not supported") elif 0 <= n < 2: return n else: return fib(n-1) + fib(n-2)if __name__ == '__main__': assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34] assert fib(15) == 610
Ở đây, bạn diễn đạt ý định của mình theo ba cách khác nhau:
- Một cách tường minh, thông qua việc triển khai công thức Fibonacci trong mã
- Một cách ngầm, thông qua hệ thống kiểu dữ liệu (chỉ định đầu vào, đầu ra và các bước trung gian đệ quy đều là số nguyên)
- Thông qua phương pháp “gói ví dụ”: các ca kiểm thử
Việc chạy file sẽ đối chiếu công thức với các ví dụ. Trình kiểm tra kiểu dữ liệu có thể xác minh tính tương thích của các kiểu: cộng hai số nguyên là một thao tác hợp lệ và sẽ sinh ra một số nguyên khác.
Hệ thống kiểu dữ liệu thường là một cách tốt để kiểm tra bài tập trong vật lý: nếu bạn đang tính gia tốc nhưng lại thu được đáp án có đơn vị là mét/giây thay vì mét/giây², thì bạn biết mình đã làm sai.
Còn các ca kiểm thử là một ví dụ cụ thể của định nghĩa “gói ví dụ”, và đối với con người, cách xử lý khái niệm này thường tự nhiên hơn nhiều so với định nghĩa tường minh trực tiếp.
Bạn càng có thể đặc tả ý định của mình bằng nhiều cách khác nhau—lý tưởng nhất là những cách yêu cầu bạn sử dụng các kiểu tư duy khác biệt để giải quyết vấn đề—thì khi tất cả các biểu đạt này được chứng minh là tương thích với nhau, khả năng bạn thực sự diễn đạt đúng điều mình muốn sẽ càng cao.
Lập trình an toàn nằm ở việc diễn đạt ý định của bạn bằng nhiều cách khác nhau, sau đó tự động xác minh rằng tất cả các biểu đạt này đều tương thích lẫn nhau.
Xác minh hình thức cho phép bạn đẩy phương pháp này lên xa hơn nữa. Nhờ xác minh hình thức, bạn có thể đặc tả ý định của mình bằng vô số cách dư thừa khác nhau, và chương trình chỉ được xác minh thành công khi tất cả chúng đều tương thích.
Bạn có thể đặc tả một triển khai được tối ưu hóa cao và một triển khai kém hiệu quả nhưng dễ đọc cho con người, rồi xác minh xem chúng có khớp nhau hay không. Bạn có thể yêu cầu mười người bạn cung cấp danh sách các thuộc tính toán học mà họ cho rằng chương trình của bạn nên có, rồi kiểm tra xem nó có đáp ứng tất cả hay không.
Nếu không đáp ứng, hãy xác định xem là chương trình sai hay thuộc tính toán học được định nghĩa sai. Và bạn có thể sử dụng trí tuệ nhân tạo để thực hiện tất cả những điều này một cách cực kỳ hiệu quả.
Vậy tôi nên bắt đầu từ đâu?
Thực tế mà nói, bạn sẽ không tự viết các chứng minh. Lý do các phương pháp hình thức chưa từng trở nên phổ biến là vì đa số mọi người không thể hiểu nổi cách viết những nội dung khó hiểu này. Bạn có thể giải thích ý nghĩa của đoạn mã sau không?
/-- Trợ giúp: ≤ từng phần tử ở cấp độ foldl với một bộ tích luỹ. -/private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b) (hLE : Forall₂ (· ≤ ·) ds1 ds2) : List.foldl (λ acc d => acc * w + d) a ds1 ≤ List.foldl (λ acc d => acc * w + d) b ds2 := by match ds1, ds2, hLE with | [], [], .nil => exact hAcc | d1::ds1', d2::ds2', .cons hd htl => simp [List.foldl] refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd
(Nếu bạn tò mò, đây là một trong nhiều bổ đề con trong chứng minh cho một tuyên bố an toàn cụ thể của một biến thể chữ ký SPHINCS.
Cụ thể, tuyên bố này là: trừ khi xảy ra va chạm băm, chữ ký của một thông điệp nào đó sẽ đòi hỏi giá trị cao hơn bất kỳ chữ ký nào khác của thông điệp khác ở ít nhất một vị trí nào đó trên một bậc thang băm, do đó nó chứa thông tin không thể tính toán được từ chữ ký kia.)
Thay vì viết mã và chứng minh thủ công, bạn chỉ cần để trí tuệ nhân tạo viết chương trình cho bạn (dù là viết trực tiếp bằng Lean hay để tăng tốc thì viết bằng mã lắp ráp), đồng thời chứng minh bất kỳ thuộc tính mong muốn nào trong quá trình đó.
Nhiệm vụ này có một lợi thế là nó tự xác minh, do đó bạn không cần giám sát, chỉ cần để trí tuệ nhân tạo chạy liên tục vài tiếng đồng hồ.
Kết quả tệ nhất cũng chỉ là nó xoay vòng tại chỗ mà không tiến triển (hoặc, như leanstral của tôi từng làm, nó tự ý thay thế tuyên bố cần chứng minh để giảm nhẹ gánh nặng công việc của chính nó).
Điều duy nhất bạn cần kiểm tra ở cuối cùng là tuyên bố mà nó chứng minh có đúng như yêu cầu của bạn hay không.
Trong biến thể chữ ký SPHINCS, đây là tuyên bố cuối cùng:
theorem wots_fullDigits_incomparable {dig1 dig2 : List Nat} {w l1 l2 : Nat} (hw : 0 < w) (hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1) (hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w) (hL2suff : l1 * (w - 1) < w ^ l2) (hNeq : dig1 ≠ dig2) : ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧ ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)
Thực tế, tuyên bố này nằm ở ranh giới vừa đủ đọc được:
Nếu dãy số được tạo từ một bản tóm tắt băm (dig1) không bằng dãy số được tạo từ một bản tóm tắt băm khác (dig2)
thì cả hai điều sau đều không đúng:
- Với mọi số, số trong dig1 <= số trong dig2
- Với mọi số, số trong dig2 <= số trong dig1
Điều này cũng đúng với các “dãy số mở rộng” (wotsFullDigits) được tạo bằng cách thêm tổng kiểm tra. Nói cách khác, trong dãy mở rộng của dig1, sẽ luôn có những vị trí mà số ở đó cao hơn, và ở những vị trí khác, số trong dãy mở rộng của dig2 lại cao hơn.
Trong việc sử dụng mô hình ngôn ngữ lớn để viết chứng minh, tôi thấy cả Claude và Deepseek 4 Pro đều có thể đảm nhiệm tốt. Leanstral là một mô hình trọng số nguồn mở nhỏ được tinh chỉnh đặc biệt để viết Lean, và đây là một lựa chọn thay thế đầy hứa hẹn.
Nó có 119 tỷ tham số, kích hoạt 6 tỷ tham số mỗi token, và bạn có thể chạy nó cục bộ, mặc dù tốc độ chậm hơn (khoảng 15 token/giây trên laptop của tôi). Theo các bài kiểm tra chuẩn, Leanstral vượt trội hơn các mô hình chung lớn hơn nhiều:
Theo kinh nghiệm cá nhân hiện tại của tôi, nó hơi kém hơn một chút so với Deepseek 4 Pro, nhưng vẫn rất hiệu quả.
Xác minh hình thức không thể giải quyết tất cả các vấn đề của chúng ta.
Tuy nhiên, nếu chúng ta muốn mô hình an ninh Internet không còn dựa trên việc mọi người tin tưởng vào một vài tổ chức quyền lực, thì chúng ta buộc phải chuyển sang tin tưởng vào mã nguồn—bao gồm cả việc tin tưởng vào mã nguồn ngay cả khi đối mặt với những kẻ tấn công AI mạnh mẽ.
Xác minh hình thức được hỗ trợ bởi AI đã đưa chúng ta tiến một bước vững chắc trên con đường thực hiện mục tiêu này.
Giống như blockchain và ZK-SNARKs, trí tuệ nhân tạo và xác minh hình thức cũng là những công nghệ bổ trợ nhau rất mạnh mẽ.
Blockchain trao cho bạn khả năng kiểm chứng mở và khả năng chống kiểm duyệt, nhưng đổi lại là sự hy sinh về quyền riêng tư và khả năng mở rộng, trong khi ZK-SNARKs lại hoàn trả quyền riêng tư và khả năng mở rộng cho bạn (thậm chí còn nhiều hơn cả trước đây).
Trí tuệ nhân tạo trao cho bạn khả năng viết lượng mã khổng lồ, nhưng đổi lại là sự hy sinh về độ chính xác, trong khi xác minh hình thức lại hoàn trả độ chính xác cho bạn (thậm chí còn cao hơn cả trước đây).
Theo mặc định, trí tuệ nhân tạo sẽ sinh ra một lượng lớn mã rất cẩu thả, và số lượng lỗi sẽ tăng lên.
Thực tế, trong một số trường hợp, việc dung thứ cho sự gia tăng lỗi lại là sự đánh đổi đúng đắn: nếu lỗi chỉ nhẹ, thì ngay cả phần mềm có lỗi cũng vẫn tốt hơn việc không có phần mềm đó.
Nhưng ở đây, an ninh mạng lại có một tương lai lạc quan: phần mềm sẽ (tiếp tục) phân tách thành “phần rìa không an toàn” xoay quanh một “lõi an toàn”.
Phần rìa không an toàn sẽ chạy trong môi trường cách ly (sandbox), chỉ được cấp mức quyền tối thiểu cần thiết để hoàn thành công việc.
Lõi an toàn sẽ quản lý mọi thứ. Nếu lõi an toàn sập, mọi thứ sẽ sập theo, bao gồm dữ liệu cá nhân và tiền bạc của bạn. Nhưng nếu một phần rìa không an toàn nào đó sập, lõi an toàn vẫn có thể bảo vệ bạn.
Khi nói đến lõi an toàn, chúng ta không thể để mã có lỗi lan tràn. Chúng ta sẽ hành động quyết liệt để giữ cho lõi an toàn luôn nhỏ gọn, thậm chí còn thu nhỏ nó hơn nữa.
Ngược lại, chúng ta sẽ đầu tư toàn bộ hiệu năng bổ sung do trí tuệ nhân tạo mang lại vào nhiệm vụ làm cho lõi an toàn an toàn hơn, để nó có thể gánh vác trọng trách tin cậy cực cao mà xã hội kỹ thuật số đặt lên vai nó.
Nhân kernel của hệ điều hành (hoặc ít nhất là một phần của nó) sẽ trở thành một lõi an toàn như vậy.
Ethereum sẽ là một lõi an toàn khác.
Hy vọng rằng, ít nhất với mọi phép tính không đòi hỏi hiệu năng cao, phần cứng bạn sử dụng cũng sẽ trở thành lõi an toàn thứ ba.
Các hệ thống liên quan đến Internet vạn vật (IoT) sẽ là lõi an toàn thứ tư.
Ít nhất trong các lõi an toàn này, câu ngạn ngữ cổ xưa “lỗi là điều không thể tránh khỏi, bạn chỉ có thể cố gắng tìm chúng trước kẻ tấn công” sẽ bị bác bỏ, thay vào đó là một thế giới đầy hy vọng hơn, nơi bạn thực sự đạt được sự an toàn.
Nhưng nếu bạn sẵn sàng giao tài sản và dữ liệu của mình cho những phần mềm được viết cẩu thả, có thể vô tình nuốt chửng chúng vào một hố đen, thì bạn đương nhiên cũng có quyền tự do đó.
Chào mừng tham gia cộng đồng chính thức TechFlow
Nhóm Telegram:https://t.me/TechFlowDaily
Tài khoản Twitter chính thức:https://x.com/TechFlowPost
Tài khoản Twitter tiếng Anh:https://x.com/BlockFlow_News
@VitalikButerin
