💻 computer science

Package Managers Ã la Carte: A Formal Model of Dependency Resolution

이 논문은 정밀한 교차 언어 의존성 표현을 가능하게 하고 공급망 분석을 개선하기 위해 다양한 프로그래밍 생태계의 패키지 매니저들의 다양한 의미론을 통합하는 정형 모델인 패키지 계산법(Package Calculus)을 소개한다.

원저자: Ryan Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, Anil Madhavapeddy

게시일 2026-07-20

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Ryan Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, Anil Madhavapeddy

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

거대한 소프트웨어 바벨탑

당신이 거대하고 복잡한 성을 짓고 있다고 상상해 보십시오. 현실 세계라면 한 곳에서는 벽돌을, 다른 곳에서는 모르타르를, 또 다른 곳에서는 스테인드글라스를 가져와야 할 것입니다. 만약 이 공급업체들이 서로 다른 언어를 사용하거나 서로 다른 측정 도구를 사용한다면, 당신의 성은 완공되기도 전에 무너질지도 모릅니다. 이것이 바로 디지털 세계의 소프트웨어가 직면한 문제입니다.

컴퓨터 과학, 특히 프로그래밍 언어 및 소프트웨어 공학이라는 분야에서 개발자들은 다양한 "언어"(Python, Rust, OCaml 등)로 작성된 코드를 사용하여 애플리케이션을 구축합니다. 이러한 프로그램을 작동시키기 위해 그들은 **패키지(package)**라고 불리는 미리 만들어진 코드 조각들에 의존합니다. 패키지를 성을 위한 조립식 방이라고 생각하십시오. 즉, 도구 라이브러리, 데이터베이스, 또는 그래픽 엔진과 같은 것입니다.

하지만 모든 프로그래밍 언어는 이 방들을 찾아 설치하는 디지털 포맨(foreman, 현장 감독)인 자신만의 "패키지 매니저"를 가지고 있습니다. 문제는 이 포맨들이 서로 다른 방언을 사용한다는 점입니다. Python 포맨(pip)은 Rust 포맨(Cargo)을 이해하지 못하며, 둘 다 Linux 시스템 포맨(APT)과 대화할 수 없습니다. 그들은 방들이 어떻게 결합되어야 하는지에 대해 각기 다른 규칙을 가지고 있습니다. 만약 당신이 Python, Rust, C 코드를 동시에 사용하는 프로젝트를 구축하려 한다면, Python 방이 Rust 벽에 맞지 않는 혼란스러운 상황에 처하게 되며, 전체 구조가 어떻게 연결되는지에 대한 전체 설계도를 아무도 볼 수 없게 되어 보안 위험이 발생합니다.

소프트웨어 방을 위한 보편적 번역기

케임브리지 대학교와 산업 파트너 연구진이 작성한 **"Package Managers à la Carte"**라는 제목의 이 논문은 이 혼돈에 대한 해결책을 제안합니다. 그들은 모든 패키지 매니저가 즉시 동일한 언어를 말하도록 강요하려는 것이 아닙니다. 대신, 그들은 **패키지 계산법(Package Calculus)**이라 불리는 보편적 문법을 발명했습니다.

패키지 계산법을 소프트웨어 의존성을 위한 "링구아 프랑카(lingua franca, 공용어)" 또는 보편적 번역기라고 생각하십시오. 저자들은 패키지 매니저들 사이의 엄청난 차이에도 불구하고, 그들이 공유하는 아주 작은 공통 핵심(core)이 있다는 사실을 깨달았습니다. 그들의 본질에는 세 가지 간단한 작업이 들어 있습니다:

루트 포함(Root Inclusion): 당신이 구축 중인 메인 프로젝트를 반드시 포함해야 합니다.
의존성 폐쇄(Dependency Closure): 어떤 방을 설치하려면, 그 방이 서 있기 위해 필요한 더 작은 방들도 함께 설치해야 합니다.
버전 유일성(Version Uniqueness): 동일한 위치에 같은 종류의 방을 두 가지 다른 버전으로 동시에 설치할 수 없습니다(보통의 경우).

이 논문은 이 작은 핵심이 고대 Perl 아카이브부터 현대적인 Rust 도구에 이르기까지 30개 이상의 서로 다른 패키지 매니저의 동작을 설명하기에 충분히 강력하다는 것을 증명합니다. 연구진은 단순히 추측한 것이 아니라, 엄격한 수학적 모델을 구축했으며, 자신들의 논리가 건전함을 증명하기 위해 (Lean 4라는 도구를 사용하여) 컴퓨터 프로그램을 작성했습니다.

"À La Carte" 방식의 기능 메뉴

이 논문의 진짜 마법은 차이점을 처리하는 방식에 있습니다. 저자들은 패키지 매니저를 독특하게 만드는 복잡한 기능들—예를 들어, 라이브러리의 여러 버전이 공존하도록 허용하거나, 패키지가 "라이브러리 A 또는 라이브러리 B가 필요하다"라고 말할 수 있게 하는 것들—이 단순한 핵심에 추가되는 특수한 "애드온(add-ons)"에 불과하다는 것을 깨달았습니다.

그들은 이 접근 방식을 메뉴에서 주문하는 것과 같은 "à la carte" 방식이라고 부릅니다. 기본 핵심을 주문한 다음, 다음과 같은 것들을 위한 특정 확장 기능을 추가할 수 있습니다:

충돌(Conflicts): "나는 이 패키지를 저 패키지와 절대 함께 설치할 수 없다."
동시 버전(Concurrent Versions): "나는 이 라이브러리의 두 가지 다른 버전을 나란히 실행해야 한다."
피어 의존성(Peer Dependencies): "내가 직접 사용하지 않더라도, 내 이웃이 특정 버전의 라이브러리를 가지고 있어야 한다."
기능(Features): "'그래픽' 옵션을 켜면, 추가적인 도구들이 필요하다."

논문은 이러한 모든 복잡한 기능들이 단순한 핵심으로 수학적으로 "환원(reduced)"될 수 있음을 보여줍니다. 이는 마치 수플레를 만드는 복잡한 레시피를 섞기, 가열하기, 접기라는 기본적인 단계로 분해할 수 있음을 보여주는 것과 같습니다. 모든 생태계의 규칙을 이 공통 핵심으로 번역함으로써, 연구진은 여러 언어에 걸친 프로젝트의 의존성 퍼즐을 마침내 풀 수 있음을 입증합니다.

왜 이것이 중요한가: 폴리글랏 리졸버(Polyglot Resolver)

이 논문에서 설명하는 궁극적인 목표는 **폴리글랏 리졸버(polyglot resolver)**입니다. 현재 만약 당신이 Python, Rust, C를 사용하는 프로젝트를 구축하고 싶다면, 서로 충돌하지 않기를 바라며 세 개의 별도 패키지 매니저를 실행해야 합니다. 저자들은 미래에 단 하나의 "슈퍼 리졸버"를 가질 수 있을 것이라고 제안합니다.

작동 방식은 다음과 같습니다:

프로젝트의 Python 부분은 자신의 요구사항을 패키지 계산법으로 번역합니다.
Rust 부분도 동일하게 수행합니다.
C 부분도 동일하게 수행합니다.
슈퍼 리졸버는 이들을 하나의 거대하고 통합된 퍼즐로 결합하여 해결하며, Python 라이브러리, Rust 라이브러리, C 드라이버가 어떤 버전을 사용할지 서로 합의하도록 보장합니다.

논문은 이것이 단순히 좋은 아이디어일 뿐만 아니라, 보안과 안정성을 위해 필수적인 단계라고 주장합니다. 서로 다른 생태계 간에 의존성이 숨겨져 있거나 버전이 지정되지 않은 경우, 보안 취약점을 추적하는 것이 불가능해집니다. 의존성의 의미론(semantics)을 통일함으로써, 우리는 소프트웨어가 의존하는 모든 코드 조각의 전체 "의존성 그래프"—즉, 완전한 지도를 볼 수 있습니다.

저자들은 이것이 모든 패키지 매니저가 내일 당장 사라진다는 의미가 아님을 주의 깊게 명시합니다. 대신, 이 형식적 모델은 생태계 간을 번역할 수 있는 도구를 구축하기 위한 이론적 토대를 제공합니다. 그들은 문제를 해결하기 위한 최적의 버전 세트를 찾는 것이 수학적으로 매우 어렵지만(구체적으로 "NP-완전" 문제이며, 프로젝트가 커짐에 따라 기하급수적으로 어려워짐을 의미함), 근본적인 규칙을 이해함으로써 이 복잡성을 헤쳐 나갈 수 있음을 보여줍니다.

요컨대, 이 논문은 단순히 현재의 시스템이 망가졌다고 지적하는 데 그치지 않고, 서로 다른 세계의 소프트웨어가 무너지지 않고 함께 구축될 수 있는 새로운 종류의 건설 현장을 위한 설계도를 제공합니다. 이는 혼란스러운 고립된 도구들의 집합을 일관되고 통합된 시스템으로 바꾸어 놓으며, 더 안전하고 신뢰할 수 있는, 진정한 교차 언어 소프트웨어 프로젝트를 향한 길을 열어줍니다.

기술 요약: 패키지 매니저 아 라 까르트 (Package Managers à la Carte)

문제 정의

패키지 매니저는 운영 체제와 프로그래밍 언어 전반에 걸쳐 편재해 있지만, 근본적으로 상호 운용이 불가능한 상태로 남아 있다. 각 생태계는 프로젝트의 의존성을 충족하기 위해 일관된 패키지 버전 세트를 선택한다는 동일한 핵심 문제를 해결하고 있음에도 불구하고, 각기 파편화된 임의의 의미론(semantics)을 사용한다. 이러한 파편화는 다국어 프로젝트가 생태계를 넘나드는 정밀한 의존성을 표현하는 것을 방해하며, 외부 시스템 의존성을 암시적이고 버전 정보 없이 남겨두며, 공급망 보안 분석에 필요한 전체 의존성 그래프를 모호하게 만든다. 현재의 상호 운용성 노력은 동일한 의미론을 가진 생태계 간에 해결 메커니즘을 공유하는 데 집중되어 있으며, 의존성이 표현되는 방식의 근본적인 다양성을 해결하는 데는 실패하고 있다.

방법론

저자들은 의존성 표현을 위한 공통 언어(lingua franca) 역할을 수행하도록 설계된 최소한의 형식 체계인 **패키지 계산법(Package Calculus)**을 제안한다. 이 방법론은 "코어 및 확장(core-and-extension)" 접근 방식을 따른다:

코어 형식화: 저자들은 의서 결정(dependency resolution)의 보편적 조건을 포착하는 최소한의 커널을 정의한다: 루트 포함(Root Inclusion) (요청된 패키지가 설치됨), 의존성 폐쇄(Dependency Closure) (모든 의존성이 충족됨), 그리고 버전 유일성(Version Uniqueness) (패키지 이름에 대해 최대 하나의 버전만 설치됨). 저자들은 3-SAT으로부터의 환원을 통해 이 코어 문제를 해결하는 것이 **NP-완전(NP-complete)**임을 증명한다.
확장 및 환원: 논문은 실제 패키지 매니저들이 나타내는 구체적인 차이의 축(예: 충돌, 동시 버전, 피어 의존성, 기능(features), 불리언 공식, 가상 패키지)을 식별한다. 각 축에 대해 저자들은 **확장된 계산법(extended calculus)**을 정의하며, 결정적으로 이를 코어 계산법으로 되돌리는 **건전하고 완전한 환원(sound and complete reduction)**을 제공한다. 이러한 환원은 복잡하고 생태계 특유적인 의존성 표현을 코어 형식으로 변환하는 컴파일 패스(compilation pass) 역할을 한다.
합성(Composition): 저자들은 이러한 확장들이 어떻게 결합되어 실제 패키지 매니저(예: 동시 버전과 기능을 결합한 Cargo)를 모델링할 수 있는지 보여준다. 또한 확장 간의 불변성 위반 처리를 포함하여, 환원을 합성할 때 고려해야 할 사항들을 설명한다.
기계화: 논문에 제시된 모든 정리는 Lean 4를 통해 기계화되었다.

주요 기여

통합 조사: 30개 이상의 패키지 매니저를 조사하여 공유된 코어와, 버전 제약, 충돌, 동시 버전, 피어 의존성, 기능, 패키지 공식, 변수 공식, 가상 패키지, 선택적 의존성 등 생태계가 갈라지는 구체적인 축을 식별하였다.
패키지 계산법: 의존성 결정의 본질을 포착하는 최소한의 형식 체계이다. 저자들은 코어 문제가 NP-완전임을 확인하였으나, 이는 실제 세계의 표현력을 포착하기 위해 내재된 복잡성임을 밝힌다. 제한적인 접근 방식(Go의 MVS와 같은)은 표현력을 희생함으로써 NP-완전성을 피한다.
차이를 위한 환원: 코어에 대한 확장으로서 각 차이의 축에 대한 형식적 모델과, 코어로 되돌리는 환원을 함께 제공한다. 이러한 환원은 만족 가능성(satisfiability)을 보존하지만(유효한 결정은 여전히 유효함), 반드시 최적성을 보존하는 것은 아니다.
합성 가능성: 확장이 어떻게 결합되어 현대적 생태계(예: Rust의 Cargo)에서 흔히 볼 수 있는 복잡한 패키지 매니저를 모델링할 수 있는지 입증한다. 논문은 여러 확장(예: Concurrent Feature Package Calculus)을 결합하는 프레임워크를 제공한다.
폴리글랏 리졸버 경로: "폴리글랏 리졸버(polyglot resolver)"를 위한 이론적 토대를 마련하였다. 여러 생태계의 의존성을 코어 계산법으로 환원함으로써, 단일 리졸버가 여러 언어와 운영 체제를 아우르는 프로젝트를 하나의 통합된 인스턴스로 해결할 수 있다.

결과

본 논문은 코어 패키지 계산법이 일련의 형식적 환원을 통해 실제 세계의 다양한 의존성 표현 언어를 모델링할 만큼 충분히 표현력이 있음을 입증한다.

복잡도: 저자들은 일반적인 경우 의존성 결정이 NP-완전함을 확인한다. 그들은 서로 다른 생태계가 이 스펙트럼을 어떻게 탐색하는지 분석한다: Go의 MVS는 제약을 하한선(lower bounds)으로 제한하고 메이저 버전의 버전 유일성을 제거함으로써 선형 시간 해결을 달로한다. Nix는 정확한 버전(단일 의존성)을 요구함으로써 문제를 우회한다. 반면 opam이나 Cargo와 같은 시스템은 표현력을 유지하기 위해 NP-완전성을 수용한다.
환원의 유효성: 모든 확장(충돌, 동시 버전, 피어 의존성, 기능, 패키지 공식, 변수 공식, 가상 패키지)에 대해 코어로의 환원을 제공한다. 건전성(Soundness)과 완전성(Completeness) 정리가 각 확장에 대해 증명되었으며, 이는 확장된 계산법에서의 결정이 존재할 때 그리고 오직 그때만 환원된 코어 계산법에서의 결정이 존재함을 보장한다.
합성: 논문은 확장의 합성을 성공적으로 모델링하며, 특히 Rust(Cargo)와 같이 현대적 생태계에서 흔한 동시 버전과 기능을 결합하는 방법을 시연한다.

의의 및 주장

본 논문은 지금까지 결여되었던 원칙적인 교차 생태계 도구를 위한 이론적 토대를 제공한다고 주장한다. 의존성 표현의 의미론을 통합함으로써 패키지 계산법은 다음을 가능하게 한다:

교차 생태계 비교: 표면적으로 다른 메커니즘들이 동일한 구조이거나, 혹은 어디에서 다른지를 식별할 수 있다.
폴리글랏 리졸루션(Polyglot Resolution): 여러 생태계를 가로지르는 프로젝트를 각 생태계의 의존성을 코어로 컴파일하여 결합된 인스턴스로 하나의 단위로서 해결할 수 있다.
중간 표현으로서의 번역: 코어 계산법은 한 생태계의 의ependency 언어를 다른 생태계로 번역하기 위한 중간 표현(Intermediate Representation) 역할을 할 수 있으며, 이를 통해 교차 생태계 번역의 복잡도를 $O(n^2)$ 의 직접 번역기에서 $2n$ 개의 프론트엔드/백엔드 번역기로 줄일 수 있다.

저자들은 이러한 목표의 즉각적인 실현에 대해서는 신중한 태도를 유지한다. 단일 확장 환원은 원래의 인스턴스를 복구하기 위해 역으로 올릴(lift) 수 있지만, 합성된 환원(합성된 구조가 서로 얽혀 있는 경우)을 역으로 취하는 것은 각 합성에 대한 명시적인 정의가 필요한 미해결 과제라고 언급한다. 따라서 패키지 계산법이 교차 생태계 번역을 잘 정의된 문제(합성된 환원을 역으로 취하는 문제)로 축소시키기는 하지만, 실제 번역기와 폴리글랏 리졸버의 구현은 향후 과제로 남겨둔다. 본 논문은 빌드 시스템 통합이나 샌드박스 빌드의 구체적인 과제를 해결하는 것이 아니라, 이러한 경계를 넘나드는 의존성 결정을 다루기 위해 필요한 형식적 의미론을 제공하는 데 목적이 있다.