TechFlow đưa tin, công ty an ninh blockchain Certora gần đây đã hoàn thành cuộc kiểm tra xác thực chính thức đối với phần mở rộng token của Solana, sử dụng công cụ xác minh hình thức sâu để thiết lập và xác minh các thuộc tính quan trọng trong mã nguồn. Những phát hiện chính từ đội ngũ Certora bao gồm: nhận diện một cơ hội tối ưu hóa có thể cải thiện hiệu suất chương trình lên 20%; phát triển các quy tắc xác minh cho các bản cập nhật gần đây của nhóm Solana nhằm tăng cường các biện pháp bảo mật hiện tại; xây dựng các đặc tả có thể tái sử dụng để xác minh nhiều lệnh khác nhau, đồng thời phát hiện ra một số vấn đề trước đó chưa từng được phát hiện bởi bất kỳ bên kiểm toán nào.
Cụ thể, Certora đề xuất không sử dụng hàm sol_memcmp mà nên áp dụng phương pháp so sánh độc lập nền tảng do Rust cung cấp. Cải tiến này giúp giảm khoảng 20% đơn vị tính toán của lệnh TransferChecked.
Bên cạnh đó, việc xác minh của Certora cũng phát hiện và xác nhận việc sửa chữa một vấn đề liên quan đến tính nhất quán giữa chuyển khoản đã kiểm tra và chưa kiểm tra.
Cuối cùng, nhóm phát hiện thấy các lệnh đốt cháy (Burn và BurnChecked) thiếu bản vá đã được áp dụng cho lệnh chuyển khoản, vấn đề này đã được đội ngũ phát triển SPL xác nhận và khắc phục.
