CVE-2026-72704 in Rocq
Tóm tắt
Bởi VulDB • 24/08/2026
Bộ kiểm tra guard trong Rocq Prover không thực hiện việc kiểm tra lại biểu diễn cây đệ quy của một tham số kiểu inductive sau khi tham số đó đã bị thay đổi bởi quá trình vận chuyển (transport). Một hàm cố định (fixpoint) có thể áp dụng phép rewrite dọc theo một đẳng thức giữa các kiểu cho đối số đệ quy của nó, và bộ kiểm tra guard chấp nhận điều này vì kiểu inductive được bảo toàn, trong khi cây đệ quy đã ghi lại cho tham số đó bị thay đổi. Một hàm fixpoint thứ hai gọi đến hàm đầu tiên sẽ thừa kế cây đệ quy đã bị thay đổi mà không có bất kỳ xác minh nào, do đó một lời gọi không giảm dần về mặt cấu trúc (structurally decreasing) được chấp nhận là kết thúc (terminating). Định nghĩa không kết thúc dẫn đến việc chứng minh rằng một số tự nhiên bằng với hậu tố của chính nó và do đó suy ra False, từ đó mọi mệnh đề đều có thể được suy ra. Chứng minh này sử dụng hai tiên đề bắt nguồn từ tính bất biến (univalence) và nhất quán với phép tính các kiểu inductive (calculus of inductive constructions), vì vậy mâu thuẫn xuất phát từ việc kiểm tra guard chứ không phải từ các giả thiết. Một bản sửa lỗi đã được đề xuất nhưng chưa được hợp nhất (merged).
If you want to get best quality of vulnerability data, you may have to visit VulDB.