TechFlow 소식에 따르면, 블록체인 보안 회사 Certora가 최근 Solana 토큰 확장 기능에 대한 공식 형식 검증 리뷰를 완료했다. 이 과정에서 Certora는 자체의 심층적인 형식 검증 도구를 활용해 코드 내 핵심 속성들의 명세를 작성하고 검증을 수행했다. Certora 팀의 주요 성과로는 프로그램 성능을 20% 향상시킬 수 있는 최적화 기회를 식별한 것, Solana 팀이 최근 업데이트한 내용을 검증할 수 있는 새로운 규칙을 개발하여 기존 보안 조치를 강화한 것, 그리고 다수의 명령어를 검증할 수 있는 재사용 가능한 명세를 작성함으로써 그간 모든 감사 담당자들이 놓쳤던 문제점을 발견한 것이다.
구체적으로, Certora는 sol_memcmp 사용을 권장하지 않고 Rust에서 제공하는 플랫폼 독립적 비교 방법을 채택할 것을 제안했다. 이 개선을 통해 TransferChecked 명령어의 계산 단위(compute units)가 약 20% 감소하는 효과를 얻었다.
또한, Certora의 검증을 통해 확인되지 않은 전송(unchecked transfer)과 확인된 전송(checked transfer) 간 일관성 문제에 대한 수정 사항이 정확히 반영되었는지 확인 및 검증되었다.
마지막으로, 팀은 Burn 및 BurnChecked와 같은 소각 명령어(burn instruction)에 전송 명령어에서 시행된 수정 사항이 누락되어 있음을 발견했으며, 이 문제는 SPL 개발팀에 의해 확인되어 이미 수정된 상태다.




