Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

기술 요약: Cargo Sherlock

문제 정의

SolarWinds 사건, XZ Utils 백도어, 그리고 rustdecimal 및 faster_log와 같은 악성 Rust 라이브러리 사례와 같은 소프트웨어 공급망 공격은 오픈 소스 생태계에 중대한 위협이 됩니다. 기존의 탐지 방법은 다음 두 가지 범주로 나뉩니다:

1. 형식적으로 검증 가능한 도구: 정적 분석, 퍼징(fuzzing), 타입 시스템 등은 구체적인 구문적 또는 의미론적 보장을 제공하지만, 종종 특정 프로그램 속성에 국한됩니다.
2. 인간 중심의 신뢰: 다운로드 수, 저자 평판, 수동 감사와 같은 휴리스틱에 의존하는 산업계의 관행입니다. 이는 실용적이지만 형식적인 보장이 부족하여, 신뢰 가정이 어떻게 결합되는지 이해하거나 의존성을 신뢰하는 근거를 형식적으로 검증하기 어렵습니다.

핵심적으로 다루는 문제는 개발자들이 실제로 의존하는 요소(메타데이터, 감사 이력 등)를 포함하면서도, 형식적으로 검증 가능한 방식으로 신뢰를 정량화할 수 있는 프레임워크가 부족하다는 것입니다. 저자들은 신뢰가 구체적이고, 감사 가능하며, 설정 가능하고, 결합 가능한 시스템을 구축하고자 합니다.

방법론

본 논문은 **만족 가능 이론(Satisfiability Modulo Theories, SMT)**을 사용하여 Rust 라이브 library(crate)의 공급망 신뢰도를 정량화하는 도구인 Cargo Sherlock을 제안합니다. 이 접근 방식은 **최소 신뢰 문제(Minimum Trust Problem)**를 기반으로 합니다.

최소 신뢰 문제

저자들은 신뢰를 다음과 같은 논리적 최적화 문제로 공식화합니다:

• 입력: 소프트웨어 의존성에 대한 후보 가정 집합($\Gamma$, 예: "해당 crate의 다운로드 수가 많다면 안전하다"), 결론($c$, 예: "해당 crate는 안전하다"), 그리고 각 가정에 비용을 할당하는 비용 함수($C$).
• 목표: 가정의 부분 집합 $\Delta \subseteq \Gamma$ 중, $\Delta$가 $c$를 논리적으로 함축하고($\Delta \models c$), $\Delta$에 포함된 비용의 합이 최소가 되는 것을 찾는 것.
• 해석: 낮은 "신뢰 비용(trust cost)"은 사용자가 설정한 가정에 기반하여 안전성에 대한 더 강력하고 정당한 근거가 있음을 의미합니다. 높은 비용은 더 많은 "믿음"을 요구하는 위험한 코드를 나타냅니다.

알고리즘

최소 신뢰 문제를 해결하기 위해 두 가지 알고리즘이 제안됩니다:

1. Naive 알고리즘 (Algorithm 1): 명제 변수에 대한 한정자(quantifiers)와 선형 정수 산술을 사용하여 문제를 인코딩합니다. 의존성 트리를 나타내는 공식을 재귀적으로 구성하고 SMT 솔버를 사용하여 최소 비용을 찾습니다. 이 방식은 정확하지만 중첩된 한정자로 인해 계산 비용이 많이 듭니다.
2. Horn Clause 알고리즘 (Algorithm 2): 가정을 **비순환적 정의적 Horn 절(acyclic definite Horn clauses)**로 제한합니다. 이는 문제를 논리합 정규형(DNF) 공식으로 변환하기 위해 언폴딩(unfolding) 절차(SLD 분해와 유사)를 사용합니다. 그 후, 한정자가 없는 SMT 쿼리를 사용하여 비용 공간에 대한 이진 탐색을 수행합니다. 생성된 공식은 최악의 경우 지수적일 수 있지만, 이 방식은 실제 적용 시 훨씬 효율적입니다.

복잡도: 일반적인 최소 신뢰 문제는 $\Sigma^P_2$-hard임이 입증되었습니다. Horn 절로 제한된 HORN-MINTRUST는 NP-complete임이 증명되어 SMT 솔버 사용의 타당성을 뒷받침합니다.

구현 및 설계

Cargo Sherlock은 다음을 통합하는 Python 기반 도구입니다:

• 데이터 수집: crates.io(다운로드, 스타, 저자), GitHub, RustSec(취약점), Cargo Vet(감사 보고서), 그리고 정적 분석 도구(Miri, Cargo Scan)로부터 메타데이터를 수집합니다.
• 관계 모델: 데이터를 엔티티(Crates, Authors, Audits, Dependencies, Tool Results)로 구성합니다.
• 가정 유형:
  • 긍정적(Positive): 안전성에 대한 정당화 (예: 신뢰할 수 있는 저자, 감사 통과, 부작용 없음).
  • 부정적(Negative): 불신에 대한 정당화 (예: RustSec에 존재, Miri에 의해 플래그 지정).
  • 매개변수화된(Parameterized): 메타데이터에 따라 연속적으로 변하는 비용 (예: 다운로드 수).
• 출력: **신뢰 비용(Trust Cost)**과 **불신 비용(Distrust Cost)**을 계산합니다(0–100 척도). 이들은 결합되어 심각도 레이블(Safe, Low/Medium/High Severity, Critical)을 생성합니다.

주요 기여

1. 형식적 모델: 공급망 신뢰 문제를 SMT로 해결 가능한 최소 신뢰 문제로 공식화하여, 구체성, 감사 가능성, 설정 가능성, 결합성 요구 사항을 충족했습니다.
2. 알고리즘: 대규모 의존성 트리를 Naive 방식보다 더 효과적으로 처리하는 최적화된 Horn-clause 기반 접근 방식을 포함하여, 문제를 해결하기 위한 두 가지 알고리즘을 제안했습니다.
3. 도구 구현: 실제 메타데이터와 프로그램 분석 결과를 통합하여 신뢰 비용을 계산하는 Rust용 작동 프로토타입(Cargo Sherlock)을 구현했습니다.
4. 평가: 합성 및 실제 세계의 공급망 공격을 탐지하는 도구의 능력을 보여주는 경험적 연구를 수행했습니다.

평가 결과

저자들은 네 가지 연구 질문(RQ)에 대해 Cargo Sherlock을 평가했습니다:

• RQ1 (합성 타이포스쿼팅): 상위 100개 Rust crate의 합성 타이포스쿼팅 변형에 대해 테스트했을 때, 도구는 원본의 안전한 crate에 비해 현저히 높은 신뢰 비용과 심각도 레이블(종종 "Critical")을 할당했습니다. 대부분의 원본 crate는 "Safe"로 분류되었으나, 타이포스쿼트들은 낮은 다운로드 수와 신뢰할 수 없는 저자로 인해 위험한 것으로 분류되었습니다.
• RQ2 (실제 사례):
  • faster_log: fast_log의 악성 타이포스쿼트입니다. Cargo Sherlock은 원본의 "Medium Severity"(신뢰: 37, 불신: 73)와 비교하여, 신뢰할 수 없는 저자와 부작용에 의해 유도된 "Critical" 레이블(신뢰: 75, 불신: 80)을 정확하게 할당했습니다.
  • serde_yml: serde_yaml의 AI 유지 관리 포크(fork)입니다. 도구는 유사한 불신 비용에도 불구하고, 저자 변경으로 인해 이 포크에 "Low Severity" 레이블을 할당했습니다(원본은 "Safe").
• RQ3 (알려진 취약점): RustSec 데이터베이스에 나열된 592개 crate를 대상으로 테스트했을 때(RustSec 전용 가정을 비활성화한 상태), 많은 것들이 여전히 "Safe" 또는 "Low Severity"로 분류되었습니다. 이는 인기(높은 다운로드 수)가 신뢰 모델 내에서 알려진 취약점을 가릴 수 있음을 나타내며, 사용자가 인기 지표에만 의존할 경우 취약한 crate를 안전하다고 인식할 수 있음을 시사합니다.
• RQ4 (확장성):
  • Algorithm 1: 약 10개 이상의 의존성을 가진 crate에서 타임아웃이 발생하거나 충돌하여 확장성에 실패했습니다.
  • Algorithm 2: 최대 150개의 의존성을 가진 crate를 10분 이내에 성공적으로 평가하여, 대부분의 실제 시나리오에 대한 실질적인 확장성을 입증했습니다.

의의 및 주장

본 논문은 Cargo Sherlock이 엄격한 형식적 방법론과 산업계 개발자들의 휴리스틱 기반 관행 사이의 간극을 메우는, 소프트웨어 신뢰를 정량화하기 위한 형식적으로 검증 가능한 프레임링을 제공한다고 주장합니다.

• 구체성: 블랙박스 머신러닝 접근 방식과 달리, Cargo Sherlock은 신뢰 비용을 정당화하는 구체적인 가정 세트(예: "Alice에 의해 신뢰됨", "높은 다운로드 수")를 생성하여 추론 과정을 감사할 수 있게 합니다.
• 설정 가능성: 사용자는 자신의 위험 허용 범위에 맞춰 가정의 비용(예: AI 유지 관리 코드에 페널티를 부여하거나 특정 감사인에게 보상을 주는 것)을 조정할 수 있습니다.
• 결합성: 모델은 의존성 트리 전체에서 신뢰 비용을 결합할 수 있어, 공급망 위험에 대한 총체적인 뷰를 가능하게 합니다.

저자들은 Cargo Sherlock이 위험한 의존성(타이포스쿼트 및 신뢰할 수 없는 포크 등)을 효과적으로 식별하지만, 현재의 신뢰 지표의 한계 또한 드러낸다고 결론지었습니다. 예를 들어, 인기 있는 crate는 높은 다운로드 수 덕분에, 특정 취약점이 가정에 명시적으로 모델링되지 않는 한 도구에 의해 "Safe"로 분류될 수 있습니다. 이 도구는 오픈 소스이며 Rust 개발 워크플로우에서 사용할 수 있습니다.