[Paper] SseRex: 실용적인 Solana 스마트 계약 심볼릭 실행

Source: arXiv - 2603.16349v1

개요

Solana의 고처리량 블록체인은 스마트 계약 개발자들의 물결을 끌어들이고 있지만, 그 독특한 계정 모델은 또한 일련의 보안 침해를 초래했습니다. SseRex는 Solana 프로그램을 위해 특별히 구축된 최초의 심볼릭 실행 엔진으로, 기존 분석 도구가 놓치는 플랫폼 특유의 함정을 자동으로 찾아낼 수 있습니다.

주요 기여

• Solana에 초점을 맞춘 최초의 심볼릭 실행기로, Solana의 계정, 서명자, 소유자 의미론을 모델링합니다.
• Solana 특화 버그 탐지, 여기에는 소유자 검사 누락, 서명자 검사 누락, 키 검사 누락, 그리고 안전하지 않은 교차 프로그램 호출(CPI)이 포함됩니다.
• 확장 가능한 평가를 8,714개의 바이트코드 전용 계약에 수행했으며, 기존 도구보다 우수한 성능을 보이고 467개의 계약에서 버그를 표시했습니다.
• 실제 환경 검증으로 120개의 오픈소스 Solana 프로젝트를 분석하고, 네 개의 고프로파일 계약에 대한 심층 사례 연구를 수행했습니다.
• 오픈소스 프로토타입(SseRex)으로, Solana 개발을 위한 기존 CI 파이프라인에 통합할 수 있습니다.

방법론

1. Bytecode Lifting – 온‑체인 BPF 바이트코드를 중간 표현(IR)으로 변환하여 저수준 제어 흐름을 보존하면서 Solana 전용 API 호출(invoke, invoke_signed 등)을 노출합니다.
2. Account Model Modeling – 각 명령어가 요구하는 계정을 owner, signer, writable와 같은 속성을 가진 심볼릭 객체로 표현합니다. 실행기는 프로그램 전체에서 이러한 속성이 어떻게 검증되는지(또는 검증되지 않는지)를 추적합니다.
3. Path Exploration – 고전적인 깊이‑우선 심볼릭 실행 엔진을 사용해 SseRex는 실행 가능한 경로를 탐색하고, 분기 조건 및 계정 필드 값에 대한 제약을 생성합니다.
4. Vulnerability Checks – 각 경로 탐색이 끝난 후 엔진은 일련의 규칙 기반 검사를 적용합니다:
   • Missing Owner Check – 프로그램이 account.owner == expected_program_id를 확인하지 않고 계정을 읽거나 쓰는 경우가 있나요?
   • Missing Signer Check – 권한이 필요한 동작 전에 필요한 서명이 검증되나요?
   • Missing Key Check – 사용 전에 공개키가 기대값과 비교되나요?
   • Unsafe CPI – 프로그램이 호출 대상의 계정을 제한하지 않고 다른 프로그램을 호출하나요?
5. Constraint Solving – 잠재적인 버그가 감지되면 SMT 솔버가 구체적인 입력(계정 데이터, 서명)을 찾아 위험한 동작을 유발하도록 하여 재현 가능한 개념 증명을 생성합니다.

전체 파이프라인은 바이트코드만을 사용해 실행되므로, Rust 수준에서 오픈소스되지 않은 계약에도 적용할 수 있습니다.

결과 및 발견

• 커버리지: SseRex는 8,714개의 컴파일된 Solana 계약을 성공적으로 분석했으며, 각 계약당 평균 3.2 초 안에 완료했습니다.
• 버그 탐지: 대상 취약점이 하나 이상 존재하는 계약 467개(≈5.4 %)를 표시했습니다.
• 비교: Solana에 맞게 조정된 두 최신 정적 분석기와 비교했을 때, SseRex는 +27 % 높은 진양성 비율과 ‑15 % 낮은 위양성 비율을 달성했습니다.
• 사례 연구: 네 개의 인기 오픈소스 프로젝트를 심층 검토한 결과, 다음과 같은 미묘한 버그를 발견했습니다:
  • 공격자가 토큰 발행 명령을 재생할 수 있게 하는 서명자 검증 누락.
  • 악의적인 프로그램이 조작된 계정을 제공하여 자금을 탈취할 수 있게 하는 검증되지 않은 CPI.
• 실제 영향: 식별된 많은 이슈가 최근 Solana 공격에서 관찰된 패턴과 일치했으며, SseRex가 악용되기 전 사전 공격 조건을 드러낼 수 있음을 확인했습니다.

Practical Implications

• Developer Tooling: SseRex를 CI/CD 파이프라인에 통합하면 솔라나 개발자에게 플랫폼 특화 실수를 조기에 포착하는 자동 “보안 린트”를 제공하여 배포 후 비용이 많이 드는 패치를 줄일 수 있습니다.
• Auditor Efficiency: 감사 업체는 SseRex를 사용해 대규모 코드베이스를 선별하고, 엔진이 강조한 고위험 경로에 수동 검토를 집중할 수 있습니다.
• Marketplace Safety: 사용자 제출 솔라나 프로그램을 호스팅하는 플랫폼(예: DeFi 애그리게이터, NFT 마켓플레이스)은 SseRex를 게이트키퍼로 실행해 취약한 계약이 상장되는 것을 방지할 수 있습니다.
• Education: 도구가 생성한 구체적인 개념 증명 입력은 솔라나 계정 모델의 미묘함을 배우는 개발자들을 위한 교육 자료로 활용됩니다.
• Cross‑Chain Tooling: 이 방법론은 심볼릭 실행을 이더리움이 아닌 계정 의미를 가진 다른 블록체인에 적용할 수 있음을 보여주며, Web3 생태계에서 형식적 분석의 폭넓은 채택을 촉진합니다.

제한 사항 및 향후 작업

• 매우 큰 프로그램에 대한 확장성 – SseRex는 일반적인 계약을 효율적으로 처리하지만, 루프가 깊은 매우 큰 프로그램은 경로 폭발을 일으킬 수 있습니다. 향후 작업에서는 이를 완화하기 위해 휴리스틱 및 제한된 모델 검사를 탐색할 예정입니다.
• 동적 데이터 소스 – 현재 모델은 정적 계정 데이터를 가정합니다. 런타임에 로드되는 데이터(예: 체인 상에서 사용자 정의 구조체를 역직렬화하는 경우)를 처리하면 일부 버그를 놓칠 수 있습니다.
• 제한된 취약점 집합 – 이 도구는 네 가지 Solana‑특화 패턴에 초점을 맞추고 있으며, 재진입, 산술 오버플로, 가스 관련 문제 등을 포함하도록 규칙 집합을 확장할 계획입니다.
• 소스‑레벨 도구와의 통합 – 바이트코드 분석을 Rust 소스‑레벨 주석과 연결하면 개발자 사용성을 개선하고 오탐을 줄일 수 있습니다.

핵심 요점: SseRex는 블록체인의 고유한 런타임 모델에 맞게 조정된 심볼릭 실행이 Solana에서 다음 파도의 스마트 계약 악용에 대비한 실용적이고 개발자 친화적인 방어 수단이 될 수 있음을 보여줍니다.

저자

• Tobias Cloosters
• Pascal Winkler
• Jens‑Rene Giesen
• Ghassan Karame
• Lucas Davi

논문 정보

• arXiv ID: 2603.16349v1
• 분류: cs.CR, cs.SE
• 출판일: 2026년 3월 17일
• PDF: PDF 다운로드