💻 computer science

Chiral Analysis of Smart Contracts: Detecting Vulnerabilities from Relational Inconsistencies Across Business Paths

이 논문은 의미론적으로 쌍을 이루는 비즈니스 경로 간의 불일치를 식별함으로써 전통적인 단일 함수 분석기가 놓치는 복잡한 로직 버그를 효과적으로 찾아내는 관계형 정적 분석 모델인 '카이럴 분석(chiral analysis)'과 이를 구현한 ChiralDetector 도구를 소개한다.

원저자: Yue Xue

게시일 2026-07-21

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Yue Xue

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

탐정의 딜레마: 코드가 생략을 통해 거짓말을 할 때

당신이 북적이는 도시에서 미스터리를 풀려는 탐정이라고 상상해 보십시오. 보통 당신은 결정적인 증거를 찾습니다: 깨진 창문, 진흙 묻은 발자국, 혹은 수상한 쪽지 같은 것 말입니다. 컴퓨터 코드, 특히 블록체인에서 실행되는 '스마트 컨트랙트'의 세계에서 전통적인 보안 도구들은 바로 이 탐정 역할을 합니다. 이 도구들은 코드를 한 줄씩 스캔하며 문에 잠금장치가 빠졌거나 계산 오류가 있는 것과 같은 명백한 실수들을 찾아냅니다. 이러한 도구들은 '로컬(local)' 버그, 즉 단일 방 안에서 발생하는 종류의 버그를 찾는 데는 탁월합니다.

하지만 만약 범죄가 방 안에서 일어난 것이 아니라면 어떨까요? 만약 앞문은 잠겨 있는데 뒷문은 활짝 열려 있고, 이 두 문이 원래 하나의 보안 시스템의 일부여야 했다면 그 미스터리는 무엇일까요? 컴퓨터 과학에서는 이를 '관계적(relational)' 문제라고 부릅니다. 이는 하나의 부서진 조각에 관한 것이 아니라, 서로 일치해야 하지만 그렇지 않은 두 조각에 관한 문제입니다. 이 논문은 두 코드 경로를 마치 서로의 진실을 비추어야 하는 거울 이미지처럼 비교함으로써, 이러한 교묘한 버그를 잡아내는 새로운 방법을 탐구합니다. 만약 한 경로가 "정지"라고 말하고 다른 경로가 "진행"이라고 말한다면, 설령 "정지"와 "진행" 각각은 완벽해 보일지라도 그 시스템은 고장 난 것입니다.

논문: 카이럴 분석(Chiral Analysis)과 거울 테스트

이 논문은 **카이럴 분석(Chiral Analysis)**이라는 영리하고 새로운 방법을 소개합니다. '카이럴(chiral, 카이랄)'이라는 단어는 화학에서 유래되었으며, 서로 거울상 관계에 있지만 완벽하게 겹쳐질 수 없는 물체(예: 왼손과 오른손)를 설명할 때 사용됩니다. 스마트 컨트랙트의 세계에서 저자들은 많은 비즈니스 운영이 쌍으로 이루어진다고 제안합니다: '단일(single)' 거래와 '배치(batch)' 거래, '구매(buy)'와 '판매(sell)', 또는 가격의 '미리보기(preview)'와 그 가격의 '실행(execution)' 등이 그것입니다. 이 쌍들은 코드의 카이럴 쌍둥이들입니다.

핵심 아이디어는 단순하면서도 강력합니다: 이 쌍들이 서로의 숙제를 검사하는 것처럼 취급하는 것입니다. 사용자가 아이템을 구매하면, 코드는 사용자에게 수수료를 부과해야 합니다. 만약 동일한 사용자가 나중에 그 아이템을 판매한다면, 코드는 원래의 구매와 맥락이 맞도록 돈을 처리해야 합니다. 만약 '구매' 경로는 수수료를 달러로 부과하는데 '판매' 경로가 실수로 다른 통화로 환불하거나, 혹은 '배치' 버전이 '단일' 버전이 반환하는 돈을 환불하는 것을 잊어버린다면 버그가 존재하는 것입니다. 논문은 이러한 버그들이 표준 스캐너들에게는 보이지 않는 이유가 각 코드 라인 자체는 올바르게 보이기 때문이라고 주장합니다. 오류는 두 경로를 거울에 비추어 보았을 때 서로 일치하지 않는다는 것을 발견할 때 비로-로 드러납니다.

이 보이지 않는 오류를 찾기 위해 저자들은 **카이럴 디텍터(ChiralDetector)**라는 프로토타입 도구를 구축했습니다. 이 도구를 특정 직무 기술서를 가진 매우 똑똑한 인턴이라고 생각하십시오. 먼저, 이 도구는 전체 코드베이스를 읽고 모든 가능한 '비즈니스 경로'(예: 고객이 상점을 통과할 수 있는 모든 경로를 추적하는 것)를 맵핑합니다. 그런 다음, '정적 랭커(static ranker)'—즉, 일련의 간단한 규칙들—를 사용하여 어떤 경로들이 카이럴 쌍둥이일 가능성이 있는지 추측합니다. 예를 들어, buy라는 이름의 함수와 동일한 은행 계좌를 건드리는 sell이라는 이름의 다른 함수를 찾아낼 수 있습니다.

잠재적인 쌍 목록을 확보하면, 이제 핵심적인 역할을 수행할 LLM(대규모 언로 모델, 인간의 언어와 코드를 이해하는 유형의 AI)을 호출합니다. 이 AI는 단순히 오류를 찾는 것에 그치지 않고, 논리학자처럼 행동합니다. AI는 다음과 같이 질문합니다: "만약 이 두 경로가 서로의 거울이라면, 그들은 어떤 규칙을 따라야 하는가?" AI는 일곱 가지 특정 차원을 점검합니다:

가드(Guards): 두 경로 모두 동일한 비밀번호나 권한을 확인했는가?
액터(Actors): 두 경로 모두에서 동일한 사람이 돈을 지불하고 받았는가?
상태(State): 두 경로 모두 데이터베이스를 동일한 방식으로 업데이트했는가?
값(Value): 수수료와 환불을 일관되게 처리했는가?
순서(Order): 동일한 순서로 작업을 수행했는가?
실패(Failure): 문제가 발생했을 때, 두 경로 모두 동일하게 중단되거나 복구되는가?
외부(External): 동일한 외부 소스를 신뢰하는가?

만약 AI가 불일치를 발견하면, 즉시 "버그!"라고 외치지 않습니다. 대신 발견 내용을 '엄격한 검증기(strict validator)'에게 전달합니다. 이 검증기는 AI가 틀렸음을 증명하려고 노력하는 회의적인 편집자 역할을 합니다. 검증기는 다음과 같이 묻습니다: "이것이 정말 버그인가, 아니면 단순히 설계상의 선택인가?" 마지막으로, 도구는 유사한 결과들을 그룹화하여 100개의 작은 오류를 보고하는 대신, 하나의 큰 근본 원인을 보고합니다.

결과: 숨겨진 결함 찾기

저자들은 이 시스템을 **Phi 프로토콜(Phi protocol)**이라는 실제 프로젝트에 테스트했습니다. 결과는 이 접근 방식이 작동하고 있음을 시사하지만, 여전히 진행 중인 작업임을 보여줍니다.

실험에서 일어난 과정은 다음과 같습니다:

도구는 3,217개의 코드 경로 쌍을 조사하는 것으로 시작했습니다.
분명히 관련이 없는 것들을 필터링한 후, 심층 조사를 위해 1,643개의 쌍을 유지했습니다.
AI 디텍터는 201개의 잠재적 이슈(의심스러운 후보와 확정된 후보의 혼합)를 찾아냈습니다.
유사한 보고를 그룹화하고 중복을 제거한 후, 이 숫자는 101개의 그룹으로 줄어들었습니다.
엄격한 검증기를 거치면서 이 숫자는 44개의 확정된 양성 사례로 더 줄어들었습니다.
마지막으로, 인간 전문가가 근본 원인을 검토한 후, 팀은 13개의 고유하고 효과적인 이슈를 식별했습니다.

이 13개의 이슈는 표준 도구들이 놓쳤던 종류의 것들이었습니다. 예를 들면 다음과 같습니다:

"증명(Proof)" 혼동: 시스템이 소유권 증명을 다른 아이템에 재사용할 수 있도록 허용했는데, 이는 '구매'와 '청구(claim)' 경로가 해당 증명을 특정 아이템에 올바르게 결합하지 않았기 때문입니다.
수수료 혼선: 시스템의 한 부분은 수수료를 '베이시스 포인트(basis points, 백분율 단위)'로 계산하는 반면, 다른 부분은 동일한 숫자를 '웨이(wei, 아주 작은 화폐 단위)'로 취급하여 막대한 금융 오류를 초래했습니다.
환불 함정: 사용자가 과다 지불했을 때, '단일' 거래 경로는 사용자에게 돈을 환불했지만, '배치' 거래 경로는 실수로 중간 컨트랙트로 환불을 보내 사용자가 돈을 받지 못하게 만들었습니다.

저자들은 이 방법이 단순한 오타보다는 시스템이 돈과 규칙에 대해 어떻게 '생각'하는지에 대한 오류인 '비즈니스 로직' 버그를 잡는 데 특히 유용하다고 제안합니다. 또한 이 과정이 완벽하지는 않다고 언급했습니다. 즉, 많은 '노이즈(오탐)'가 발생하여 이를 정제해야 했으며, AI가 관계를 포착할 만큼 충분히 똑똑해야 한다는 점에 의존한다는 것입니다. 그러나 이 방법이 다른 도구들이 놓친 13개의 독특하고 영향력 있는 이슈를 찾아냈다는 사실은, 코드를 '카이럴 쌍'의 관점에서 바라보는 것이 유망한 새로운 방향임을 시사합니다.

논문은 이 방식이 모든 보안 문제를 해결하는 마법 지팡이는 아니지만, 코드 라인 사이의 공간에 숨어 있는 버그를 찾는 구조화된 방법을 제공한다고 결론짓습니다. 코드 경로를 거울 이미지로 취급함으로써, 우리는 마침내 반영된 모습이 실체와 일치하지 않을 때 나타나는 균열을 볼 수 있습니다.

기술 요약: 스마트 컨트랙트의 카이랄 분석 (Chiral Analysis)

1. 문제 정의

스마트 컨트랙트의 취약점은 종종 고립된 안전하지 않은 문구에서 발생하는 것이 아니라, 의미적으로는 쌍을 이루지만 구문적으로는 서로 다른 비즈니스 경로 간의 **관계적 불일치(relational inconsistencies)**에서 비롯됩니다. 일반적인 예시는 다음과 같습니다:

단일 진입점(Single) 대 배치(Batch) 진입점.
직접 흐름(Direct) 대 어댑터 기반 흐름(Adapter-based).
견적(Quote/Preview) 경로 대 실행(Execution) 경로.
역 연산(예: 구매 vs 판매, 민팅 vs 소각).

기존의 정적 분석 도구들은 로컬 구문 패턴, 테인트(taint) 스타일의 의존성, 그리고 단일 함수 취약점(예: 재진입성, 체크되지 않은 호출)을 탐지하는 데 탁월합니다. 그러나 이들은 관계적 버그를 위한 "오라클(oracle)"이 부족합니다. 즉, 두 대응하는 경로가 동일한 가드(guard), 상태 전이, 값의 흐름 또는 실패 동작을 보존하는지 판단할 수 없습니다. 이러한 버그를 탐지하려면 코어 함수와 래퍼(wrapper)의 로직을 비교하거나, 배치 디스패처와 단일 연산 경로를 비교해야 합니다.

2. 방법론: 카이랄 분석 (Chiral Analysis)

본 논문은 의미적으로 쌍을 이루는 비즈니스 경로를 서로에 대한 암묵적 명세로 취급하는 관계적 모델인 카이랄 분석을 소개합니다. "카이랄(chiral)"이라는 용어는 구문적 동일성을 요구하지 않으면서도 거울을 비춘 듯 대칭적이거나, 대안적이거나, 라이프사이클과 관련된 연산(예: 단일/배치, 래퍼/코어)을 포착합니다.

2.1 카이랄 취약점 모델

저자들은 카이랄 관계( $R_\chi$ )를 메타모픽 관계(metamorphic relation)의 정적 유사체로 정형화했습니다. 이는 두 경로( $p, q$ ), 관계 유형( $\tau$ ), 그리고 일련의 **관계 유도 의무(relation-induced obligations)**로 구성됩니다. 이 의무들은 다음 7가지 의미적 차원에 걸친 기대 동작의 근사치입니다:

가드 (Guard): 수정자(modifier), 전제 조건 및 자격 검증.
액터 (Actor): 호출자, 서명자, 지불자 및 환급 수취인의 신원.
상태 (State): 읽기/쓰기 집합, 플래그, 카운터 및 상태 변화량(delta).
값 (Value): 단위, 수수료, 보상, 전송 및 환급 처리.
순서 (Order): 체크-이펙트-인터랙션(check-effect-interaction) 시퀀스 및 결제 타이밍.
실패 (Failure): 리버트(revert) 동작, 부분 성공 세만틱 및 이벤트 발행.
외부 (External): 오라클 사용, 콜백 및 크로스 컨트랙트 의존성.

카이랄 취약점은 이러한 의무를 위반하여 보안 또는 프로토콜에 영향(예: 자금 손실, 승인되지 않은 상태 변경 또는 회계 오류)을 미치는 것으로 정의됩니다.

2.2 ChiralDetector 파이프라인

저자들은 LLM 비용을 관리하면서 재현율(recall)과 정밀도(precision)의 균형을 맞추기 위해 설계된 4단계 파이프라인인 ChiralDetector를 구현했습니다.

경로 추출 및 요약 (Path Extraction & Summarization):
- Solidity 소스 코드로부터 프로젝트 수준의 호출 그래프(call graph)를 구축합니다.
- "비즈니스 경로"(단일 함수, 진입-리프 체인, 포크 세그먼트)를 추출합니다.
- 각 경로에 대해 스토리지 읽기/쓰기, 값 전송, 수정자, 외부 호출을 포착하는 의미적 팩트 요약( $\Phi(p)$ )을 생성합니다. 이 추상화는 의도적으로 손실적(lossy)이지만 관계 지향적입니다.
후보 쌍 감소 (Candidate Pair Reduction):
- 정적 랭커(static ranker)를 사용하여 모든 $O(n^2)$ 비교를 피합니다.
- 공유된 스토리지 풋프린트, 중복되는 외부 호출, 명명 힌트(예: "claim" vs "batchClaim"), 액터/값 흐름의 유사성을 기반으로 경로 쌍의 점수를 매깁니다.
- 불확실한 고재현 신호를 삭제하지 않으면서, 카이랄 관계를 형성할 가능성이 높은 쌍을 우선순위에 둡니다.
의미적 필터링 및 탐지 (LLM 기반) (Semantic Filtering & Detection):
- 의미적 필터 (Semantic Filter): 쌍이 카이랄 관계를 형성할 가능성이 있는지 판단하고 관계 유형(예: 역 관계, 래퍼/코어)을 할당합니다. 경로 길이가 다르거나 경제적 방향이 반대인 쌍도 수용하도록 지시됩니다.
- 관계 인지 탐지기 (Relation-Aware Detector): 확인된 관계가 주어지면, LLM은 위반된 특정 의무를 식별하고, 소스 증거를 제공하며, 영향력 가설(impact thesis)을 수립합니다. 프롬프트는 모호한 결론 대신 명시적 추론을 강제하기 위해 "계약(contracts)" 형태로 구조화되었습니다.
엄격한 검증 및 중복 제거 (Strict Validation & Deduplication):
- **엄격한 검증기 (Strict Validator)**는 관계가 정당한지, 증거가 존재하는지, 대체 코드 경로가 영향을 무효화하는지 확인하여 발견 사항을 반증(falsify)하려고 시도합니다.
- **근본 원인 중복 제거 (Root-cause deduplication)**는 동일한 근본 결함과 예상되는 수정 사항을 공유하는 여러 보고를 병합하여, 쌍 수준의 노이즈와 근본적인 문제를 구분합니다.

3. 주요 기여

카이랄 분석 모델: 단일 함수 분석을 넘어, 대응하는 비즈니스 경로를 암묵적 명세로 취급하는 관계적 취약점 프레임워크를 제시합니다.
정형화: 카이랄 관계를 정적 메타모픽 유사체로 정의하고 7가지 특정 의무 차원을 도출했습니다.
ChiralDetector 구현: 정적 분석, 정적 쌍 랭킹, LLM 기반 의미적 탐지, 엄격한 허위 판별 검증 및 근본 원인 중복 제거를 통합한 프로토타입 파이프라인을 구현했습니다.
실증적 증거: 다양한 관계 형태(claim/batch, adapter/factory, quote/execution)를 포함하는 Phi 프로토콜에 대한 예비 평가를 통해 단일 함수 규칙으로는 표현하기 어려운 비즈니스 로직 불일치를 탐지함을 보여주었습니다.

4. 평가 결과

저자들은 다양한 관계 형상을 가진 Solidity 프로젝트인 Phi 프로토콜에서 ChiralDetector를 평가했습니다.

깔때기 지표 (Funnel Metrics):
- 정적으로 랭킹된 3,217개의 후보 쌍에서 시작.
- 의미적 탐지를 위해 1,643개의 쌍으로 감소.
- 201개의 정제된 발견 사항/의심스러운 후보 생성.
- 101개의 로컬 중복 제거 그룹으로 압축.
- 44개의 그룹이 엄격한 검증을 통과.
- 최종 수동 근본 원인 중복 제거를 통해 13개의 유효한 고유 이슈 도출.
대표적인 발견 사항:
- M10: 교차 아트(Cross-art) 머클 증명 재사용 (유사한 흐름/가드 위반).
- M13: 수수료 단위 불일치 (basis points vs wei) (값/단위 위반).
- M12: 큐레이터 상태를 손상시키는 퍼블릭 트래킹 헬퍼 (상태/액세스 위반).
- M05/M02/M04: 환급 전파 격차 및 단일/배치 경로 간의 가드 비대칭 (래퍼/코어 및 단일/배치 값 흐름 위반).
비용 분석:
- 전체 실행 비용은 약 212.70 CNY(인건비 제외)였습니다.
- 주요 비용은 정적 분석이 아닌 LLM 추론(의미적 필터링, 탐지 및 검증)이었습니다.
- 엄격한 검증기는 101개의 로컬 중복 제거 그룹 중 57개를 거부함으로써 노이즈를 크게 줄였습니다.

5. 의의 및 주장

본 논문은 카이랄 분석이 관계적 불일치라는, 단일 함수 규칙으로는 표현하기 어렵지만 프로토콜 보안에 결정적인 버그 클래스를 노출한다고 주장합니다.

통찰: 많은 비즈니스 로직 버그는 단일 함수가 국소적으로 안전하지 않아서가 아니라, 두 관련 경로가 공유된 비즈니스 객체(예: 환급 수취인 또는 수수료 계산 방식)를 처리하는 방식에 대해 서로 동의하지 않기 때문에 발생합니다.
구조화된 LLM 사용: 논문은 LLM을 구조화된 파이프라인(정적 감소 $\to$ 의미적 필터링 $\to$ 엄격한 검증) 내에서 사용하는 것이 "직접 에이전트 감사(direct agent auditing, 제한 없는 코드 읽기)"보다 더 효과적이고 비용 효율적이라고 주장합니다. 이 파이프라인은 중간 결정 사항(쌍, 관계, 의무)을 외재화하여 분석 과정을 검사 가능하고 디버깅 가능하게 만듭니다.
겸허한 태도: 저자들은 현재의 평가가 단일 프로토콜에 대한 예비 사례 연구임을 명시적으로 밝힙니다. 그들은 아직 일반적인 재현율이나 정밀도 지표를 확립하지 못했음을 인정합니다. 또한 경로 추출에서의 Solidity 의미론 근사, LLM의 환각(hallucination) 가능성, 자동화된 증거(실행 가능한 PoC 트랜잭션) 생성의 부재 등 한계점을 인정합니다.

이 연구는 비즈니스 로직 추론을 명시적이고 반복 가능하게 만드는 방향으로 나아가는 단계로서, 특정 불일치가 왜 중요한지를 설명하기 위한 어휘를 제공하며 스스로를 포지셔닝합니다.