Certora, 솔라나(Solana)의 P-토큰 업그레이드가 SPL 토큰과 동등함을 공식적으로 검증

P-Token이 최대 98% 더 많은 연산 유닛을 확보해 주는 동시에, Certora는 SPL 토큰과의 바이트 단위 호환성을 여전히 보장하며, 어떠한 취약점도 발견되지 않았음을 입증했습니다.

발행됨:
편집됨:

솔라나(Solana)가 최근 배포한 P-토큰 업그레이드는 네트워크 역사상 가장 중요한 인프라 변경 사항 중 하나입니다. 이번 업그레이드는 기존 SPL 토큰 프로그램과의 호환성을 유지하면서 토큰 운영에 필요한 컴퓨팅 리소스를 획기적으로 줄여줍니다.

이러한 주장을 검증하기 위해 솔라나 재단은 Certora에 의뢰하여 기존 SPL 토큰 구현과 새로운 피노키오(Pinocchio) 기반 P-토큰 프로그램 간의 행동적 동등성을 입증하는 형식적 검증을 수행했습니다. 연구 개발 기업인 안자 ( Anza )는 이전에 형식적 검증을 P-토큰의 동등성을 입증하는 “가장 강력한 보증”이라고 설명한 바 있으며, Certora의 결과는 솔라나에서 가장 널리 사용되는 프로그램 중 하나를 “드롭인(drop-in)” 방식으로 대체할 수 있는 P-토큰의 역할을 한층 더 입증해 줍니다.

토큰 프로그램이 중요한 이유

SPL 토큰 프로그램은 솔라나(Solana) 토큰 경제의 중심에 위치합니다. 이 프로그램은 네트워크상의 대다수 자산에 대한 민트 생성, 토큰 계정 관리, 전송, 소각 및 위임을 처리합니다. 솔라나에서 투표와 무관한 거의 모든 거래가 어떤 형태로든 토큰과 상호작용하기 때문에, 토큰 프로그램에 대한 어떠한 변경도 생태계에 광범위한 영향을 미칩니다.

P-토큰은 Pinocchio Rust 라이브러리를 기반으로 한 새로운 구현 방식을 도입합니다. 이번 업그레이드는 상당한 성능 향상을 제공하며, 많은 일반적인 작업에서 컴퓨팅 소비량을 약 95~98% 줄여줍니다. 예를 들어, 표준 토큰 전송에 소요되는 컴퓨트 유닛은 4,645개에서 76개로 줄어들며, transfer_checked 명령어의 경우 6,200개에서 105개로 감소합니다.

이러한 효율성 향상으로 네트워크 전반에 걸쳐 블록 공간의 약 12~13%를 확보할 수 있어, 블록 한도를 늘리지 않고도 추가 용량을 창출할 수 있습니다.

“드롭인(Drop-In)” 대체품임을 입증해야 하는 과제

성능 개선이 주목을 받고 있지만, 이 정도 규모의 인프라 업그레이드에서는 호환성이 여전히 가장 중요한 요건입니다. 기존 지갑, dApp, 프로토콜 및 스마트 계약은 SPL 토큰 프로그램의 동작에 의존하고 있습니다. 예상치 못한 편차가 발생하면 통합 문제가 발생하거나 개발자와 사용자에게 위험을 초래할 수 있습니다.

P Token

P-Token은 단순히 기존 코드베이스를 복사하지 않습니다. 새로운 구현은 제로 카피 계정 액세스, 최적화된 실행 경로, 추가 기능 등을 포함한 다른 아키텍처를 채택합니다. 그 결과, 개발자들은 호환성을 확인하기 위해 기존의 테스트 방법에만 의존할 수 없었습니다.

대신 Certora는 형식 검증 기법을 사용하여, 정의된 검증 범위 내의 모든 가능한 입력에 대해 두 프로그램이 동일한 방식으로 동작하는지 수학적으로 분석했습니다.

P-Token에 있어 동등성이란 무엇을 의미할까요?

Certora의 검증 프레임워크는 분석된 각 명령어에 대해 세 가지 결과 범주를 평가했습니다.

첫째, 두 프로그램 모두 실행 중에 절대 패닉 상태에 빠져서는 안 됩니다. 즉, 버그나 경계 사례 등으로 인해 프로그램이 충돌하거나 중단되어서는 안 됩니다.
둘째, SPL 토큰 프로그램이 명령어를 성공적으로 처리하고 Ok(()를 반환하면, P-Token도 Ok(()를 반환해야 합니다. 이러한 경우, 두 프로그램 모두 실행 후 계정 데이터를 바이트 단위로 동일한 상태로 유지해야 합니다.
셋째, P-Token이 오류를 반환할 경우, SPL 토큰 프로그램도 동일한 조건에서 동일한 오류를 반환해야 합니다.

Certora의 프레임워크는 가능한 모든 입력 계정 상태와 명령에 대해 프로그램이 성공 (Ok())) 하거나 정상적으로 실패 (Err(e))하도록 보장하며, 내부적으로 크래시되는 일은 절대 없습니다. P-Token의 구현은 SPL Token 기능의 상위 집합으로 설계되었으므로, SPL Token이 허용하는 모든 작업은 P-Token에서도 허용되어야 합니다.

검증 과정에서 두 프로그램 간의 몇 가지 의도적인 차이점이 확인되었습니다. P-Token은 대리인의 자체 권한 철회를 허용하여, 토큰 계정 소유자가 트랜잭션에 서명할 필요 없이 대리인이 자신의 권한을 철회할 수 있게 합니다. 반면 SPL Token은 동일한 작업에 대해 소유자의 서명을 요구합니다.

또한 P-Token은 Token-2022 멀티시그 권한에 대한 지원을 확장했습니다. SPL Token은 이러한 계정을 거부하는 반면, P-Token은 이를 허용합니다.

세 번째 차이점은 비표준 COption 태그가 포함된 잘못된 형식의 계정 데이터에 대한 오류 처리와 관련됩니다. SPL 토큰은 InvalidAccountData 오류를 발생시켜 이러한 계정을 즉시 거부합니다. 반면 P-Token의 최적화된 계정 로딩 프로세스는 오류를 발생시키기 전에 명령어 로직을 더 깊이 분석하므로, 실행 중인 명령어에 따라 다른 결과가 나올 수 있습니다.

이러한 차이점은 의도된 것이며 문서화되어 있었기 때문에, Certora는 검증 프로세스의 일부에 가정을 반영하여 분석이 합의된 호환성 경계에 집중되도록 했습니다.

검증 방식

Certora의 Prover는 소스 코드가 저수준 중간 표현으로 컴파일된 후 이를 분석합니다. 그런 다음 엔지니어들은 CVLR(Certora Verification Language for Rust)을 사용하여 형식적 사양을 작성합니다.

검증 하네스는 계정 정보와 명령어 데이터의 동일한 복사본을 생성하여, 프로버가 동일한 조건 하에서 두 프로그램을 비교할 수 있도록 했습니다. 이 시스템은 Satisfiability Modulo Theories 기법을 사용하여 제한된 테스트 케이스 모음에 의존하는 대신, 가능한 모든 입력을 동시에 평가했습니다.

검증 범위에는 AmountToUiAmount 및 UiAmountToAmount를 제외한 SPL 토큰과 P-토큰이 공유하는 모든 명령어가 포함되었습니다. 또한 이번 검토에서는 P-토큰 전용의 세 가지 새로운 명령어인 batch, unwrap_lamports, withdraw_excess_lamports도 제외되었습니다.

전 과정에 걸쳐 증명기는 정합성 증명을 생성하거나, 검토가 필요한 동작상의 차이를 강조하는 구체적인 반례를 도출했습니다.

조사 결과 및 결론

Certora는 검증 과정에서 악용 가능한 취약점이 발견되지 않았다고 보고했습니다. 분석 결과, 추가적인 가정 없이도 범위 내의 모든 명령어에 대해 ‘No Panics’ 및 ‘Equivalence on Ok’ 속성이 성립함이 확인되었습니다. 또한, 앞서 식별된 세 가지 의도적인 동작 차이를 고려할 때, ‘Equivalence on Error’ 속성도 공유 명령어 세트 전반에 걸쳐 성립하는 것으로 나타났습니다.

가장 중요한 점은, 이번 검증 결과 두 프로그램이 동일한 입력을 성공적으로 처리할 때마다 바이트 단위로 완전히 동일한 연산 후 계정 상태를 산출한다는 사실이 입증되었다는 것입니다. 또한 이 과정을 통해 형식적 검증이 기존 테스트에서는 놓칠 수 있는 경계 사례를 어떻게 밝혀낼 수 있는지 보여주었습니다.

솔라나 인프라의 중요한 이정표

이 검증 결과는 P-Token이 메인넷에 배포된 직후에 나왔으며, 솔라나(Solana)의 가장 중요한 인프라 업그레이드 중 하나에 대한 신뢰도를 한층 높여주었습니다.

이 업그레이드는 상당한 컴퓨팅 자원 절감과 형식적으로 검증된 동작 동등성을 결합함으로써, 토큰 프로그램에 매일 의존하는 애플리케이션과 자산에 차질을 주지 않으면서 네트워크 효율성을 향상시키는 것을 목표로 합니다.

SolanaFloor에서 더 읽어보기

솔라나, 마침내 네이티브 온체인 구독 서비스 도입… 급여, AI 에이전트 예산, 정기 청구 기능 활성화
전 미국 대선 후보 앤드류 양의 노블 모바일, 헬륨 모바일 인수 - $HNT의 향방은?