실제 배포된 Solidity 소스에 대한 스마트 계약 재진입 방어의 삼방향 판별력 형식 검증

우리는 실제 배포된 Solidity 소스의 Lean 4 상태 머신 (state-machine) 모델에 대하여 OpenZeppelin 재진입 방어 (reentrancy-guard) 패턴의 최초의 기계 검증된 정확성 증명을 제시합니다. 총 13개의 정리는 'sorry' 없이, 사용자가 도입한 공리 없이, 그리고 지속적 통합 (CI) 하에 제어되는 [propext] (표준 mathlib4 공리)로 제한된 공리 발자국 (axiom footprint)을 통해 기계적으로 검증되었습니다. 스마트 계약 재진입 (reentrancy) 공격은 2016년 이후 기록된 손실액이 5억 달러(US$500M)를 넘어섰으며, 특히 2016년 DAO 공격은 약 360만 ETH를 유출시켜 Ethereum을 분리시킨 하드 포크 (hard fork)를 강제했습니다. OpenZeppelin ReentrancyGuard 패턴은 실제 운영 중인 DeFi 전반에서 사실상의 표준 방어 수단이지만, 그 판별력 (discriminating power), 즉 방어 기제가 취약한 인스턴스에 대한 공격을 차단하고, 공격하지 않는 트랜잭션에 대해서는 올바른 실행을 보존하며, 인접한 안전한 변종과 취약한 변종을 구별한다는 점을 입증한 선행 연구는 없었습니다. 이전의 노력들은 장난감 계약 (toy contracts)에 대한 방어의 정확성을 형식화하거나 고립된 인스턴스에 대한 공격 가능성을 형식화했을 뿐, 실제 소스를 대상으로 이 두 방향과 경계 사례 (boundary cases)를 모두 다루지는 못했습니다. 우리는 변이 테스트 (mutation testing)를 통해 세 가지 실제 구현 사례인 DAO 2016, Compound v2, Aave V3 flashLoan과, 보안상 중요한 단 하나의 차이점을 격리한 Aave V3 flashLoan의 최소 차이 변이체 (minimal-diff mutant, flashLoanVulnerable)를 검증합니다. 삼방향 (tridirectional) 구조는 (a) DAO 2016 패턴의 공격 재현, (b) Compound v2에 대한 정확성 증명, (c) Aave V3의 CEI-올바른 flashLoan과 변이체를 구별하는 경계 사례 증명을 결합합니다. 핵심 메타 정리 (capstone meta-theorem)는 사후 수정 금지 (no-retrofit) 원칙 하에 이 세 가지를 결합하며, 이는 첫 번째 프로토콜 간 스트레스 테스트 (Compound v2에서 Aave V3로)를 통해 입증되었습니다. 더 넓은 계열로의 이식성 (portability)은 향후 연구 과제입니다. 전체 Lean 4 소스, CI 설정 및 재현 명령은 https://github.com/rayiskander2406/qanary-contracts 에서 확인할 수 있으며, v1.6-phase7-closure (기반: v1.3-layer6-closure)에서 재현 가능합니다.