Rust 프로그램 분석을 위한 프레임워크 Charon의 설계, Rust 컴파일러와의 통합, ULLBC/LLBC 표현, 그리고 검증·정적 분석·C 변환 사례를 소개한다.
1 1 institutetext: Microsoft Azure Research, UK, t-sonho@microsoft.com, 2 2 institutetext: Inria Paris, France,
{guillaume.boisseau,yoann.prak,aymeric.fromherz}@inria.fr, 3 3 institutetext: Cryspen, France, lucas@cryspen.com, 4 4 institutetext: Microsoft Azure Research, USA, protz@microsoft.com Guillaume Boisseau\orcidlink 0000-0001-5244-893X 22 Lucas Franceschino 33 Yoann Prak 22 Aymeric Fromherz\orcidlink 0000-0003-2642-543X 22 Jonathan Protzenko\orcidlink 0000-0001-7347-3050 44
Rust 프로그래밍 언어의 인기가 폭발적으로 증가하면서, 최근 Rust 프로그램을 분석, 검증, 테스트하기 위한 수많은 도구가 개발되었다. 그러나 Rust 생태계는 아직 비교적 젊기 때문에, 이러한 도구들은 모두 Rust 컴파일러와 cargo 빌드 시스템에 연동하기 위한 어렵고 시간이 많이 드는 기계적 작업을 다시 구현해야 했고, Rust 컴파일러의 내부 표현에 연결해야 했으며, 효율성 최적화가 아니라 분석에 적합한 추상 구문 트리(AST)를 노출해야 했다.
우리는 Rust 생태계에서 빠져 있던 이 핵심 구성 요소를 보완하고, Rust를 위한 분석 프레임워크 Charon을 제안한다. Charon은 Rust 프로그램 분석을 위한 만능 도구처럼 동작하며, 위와 같은 번거로운 작업을 처리하고, 다양한 분석의 기반이 될 수 있는 AST를 클라이언트에 제공한다. 우리는 Rust 검증 프레임워크(Aeneas), Rust에서 C로의 컴파일러(Eurydice), 그리고 암호 코드용 새로운 taint-checker에 이르기까지 여러 사례 연구를 통해 Charon의 유용성을 입증한다. 더 나아가, 널리 사용되는 기존 분석인 Rudra도 다시 구현하여, Charon 프레임워크를 활용해 동일한 분석을 재현할 수 있음을 보인다.
정적 분석 형식 검증 Rust.
지난 10년 동안 Rust 프로그래밍 언어는 학계와 산업계 모두에서 주목을 받아 왔으며[11, 2, 12, 30, 4, 21, 41], 지난 8년 동안 개발자들이 가장 사랑하는 언어로 꾸준히 선정되어 왔다[44, 37]. 이러한 성공의 큰 부분은 언어의 몇 가지 핵심 특징에서 비롯된다. Rust는 C나 C++와 흔히 연관되는 높은 성능과 저수준 관용구를 제공하는 동시에, 풍부한 차용 기반 타입 시스템 덕분에 기본적으로 메모리 안전성도 제공한다. 이 때문에 Rust는 매우 폭넓은 응용 분야에 적합하다. 이제 Windows[42]와 Linux 커널[10] 모두 Rust를 지원하며, 후자는 Linux에서 C 이외의 언어가 승인된 최초의 사례를 의미한다. Rust의 안전성 보장은 특히 보안에 민감한 시스템에 매력적이며, 주요 정부 기관들 또한 이제 Rust를 권장하고 있다[43, 27].
물론 C나 C++보다 더 안전하다고 해도 Rust 프로그램이 버그와 취약점으로부터 완전히 자유로운 것은 아니다. 대표적인 예로, 2024년 1월 1일부터 2025년 1월 1일 사이에 Rust 생태계의 취약점 데이터베이스인 RUSTSEC에 Rust crate를 대상으로 한 137건의 보안 권고가 등록되었다. 이 데이터베이스는 Rust Secure Code 작업 그룹이 관리한다. 이러한 취약점은 여러 이유로 발생했다. 실행 중 오류로 인해 실행이 중단되는 경우(Rust의 panic, 예를 들어 배열 경계 밖 접근 이후), 구현 또는 설계 결함, 또는 Rust의 unsafe 탈출구를 사용할 때의 메모리 취약점 등이 있다. 이 기능은 Rust의 차용 기반 타입 시스템이 지나치게 제한적일 때 C와 유사한, 검사되지 않는 포인터 연산의 사용을 허용한다.
Rust의 borrow-checker 범위를 벗어나는 속성을 강제하기 위해, 정적 분석기[30, 4, 26], 모델 검사기[19, 38] 및 연역 검증 도구[25, 11, 21, 18, 2, 3, 12, 17]로 이루어진 활발한 생태계가 제안되어 Rust 프로그램을 추론하고 분석하고 있다. 그러나 현재 Rust를 대상으로 하는 새로운 도구를 개발하려면 Rust 컴파일러 rustc와 의미 있게 그리고 효율적으로 상호작용하기 위한 상당한 엔지니어링 노력이 필요하다. 첫째, Rust는 복잡한 언어이며, 많은 C 분석이 libclang에 연결되듯 Rust 분석도 rustc에 연결되어야 한다. Rust 프론트엔드를 처음부터 다시 구현하는 것은 엄청난 작업이 될 것이다. 안타깝게도 rustc의 다양한 중간 표현(IR)은 분석 도구가 소비하기 쉬운 형태가 아니라 속도와 효율에 최적화되어 있다. 구체적으로 rustc는 이용 가능한 모든 정보가 장식된 완전한 추상 구문 트리(AST)를 제공하는 대신, 예를 들어 표현식의 타입을 필요할 때만 얻기 위한 query 를 노출한다. 이런 설계는 효율적인 증분 컴파일을 가능하게 하지만, 도구 작성자에게는 추가적인 간접 계층과 여러 전역 테이블 및 IR에 흩어진 정보를 다뤄야 하므로 더 어려움을 준다. 이러한 스타일의 API는 컴파일러 내부에 대한 깊은 지식을 요구한다. 또한 컴파일에는 충분하더라도, 컴파일러가 제공하는 정보는 분석 목적상 확장되어야 하는 경우가 있다. 예를 들어 trait solver를 질의하면 코드의 한 지점에서 사용되는 trait 인스턴스에 대한 부분 정보만 얻는다. 이 정보를 복원하려면 도구 작성자가 추가적이고 오류 가능성이 높은 작업을 해야 한다. 마지막으로 Rust 컴파일러 자체는 고립되어 호출되지 않는다. 사소하지 않은 Rust 프로젝트는 모두 Cargo 빌드 시스템을 사용하며, 이는 의존성을 수집하고, 적절한 라이브러리 및 include 경로를 갖춘 rustc 호출을 합성하고, 전반적으로 rustc를 구동한다. 따라서 현실적인 분석 도구는 Cargo에 자신을 연결해야 하며, 이것 역시 Cargo와 rustc에 대한 깊은 지식을 요구하는 쉽지 않은 과업이다.
이러한 한계를 해결하기 위해, 우리는 Rust 컴파일러와 도구 체인에 분석 지향 인터페이스를 제공하는 Rust 분석 프레임워크 Charon을 제시한다. 이를 통해 도구 작성자는 Rust 컴파일러 내부의 자질구레한 세부사항이 아니라 자신의 분석 핵심에 집중할 수 있다. 우리의 기여는 다음과 같다. rustc 위에서 다양한 도구를 개발한 경험을 통해, 우리는 MIR의 많은 설계 선택이 분석에 부적합하다고 본다. 예를 들어 열거형 태그 위로 분기하는 저수준 패턴 매칭, assertion으로 bounds-check 의미론을 인코딩하는 방식, 바이트 배열로 사전 컴파일된 상수 표현 등이 있다. 따라서 첫 번째 기여는 ULLBC(Unstructured Low-Level Borrow Calculus)와 LLBC(Low-Level Borrow Calculus)라는 두 개의 쌍대적 관점을 설계한 것이다. 이들은 각각 제어 흐름 그래프(CFG)와 AST를 제공한다. 둘 다 move, copy, 명시적 borrow와 reborrow라는 저수준 MIR 의미론은 유지하면서도, 상수, 얕은 패턴 매치, checked operation을 재구성하여 추가 분석에 적합한, 의미론적으로 단순한 MIR의 관점을 제공한다. LLBC는 ULLBC로부터 Relooper 유사 제어 흐름 재구성[33, 31]을 통해 얻어진다. 두 번째 기여는 Charon 자체의 엔지니어링과 이에 수반되는 생태계 통합이다. 우리는 클라이언트가 Cargo의 빌드 시스템과 깔끔하게 통합될 수 있도록 독립적이고 재사용 가능한 인프라를 작성했다. 더 나아가, 깔끔한 ULLBC와 LLBC 표현(위)을 노출하기 위해 Rust 컴파일러 내부를 질의하는 복잡성을 숨김으로써, 부수적 복잡성 없이 사용 가능한 API를 제공한다. 세 번째이자 마지막 기여는, LLBC와 ULLBC의 설계에 영향을 주었을 뿐 아니라 그 광범위한 적용 가능성에 대한 실험적 검증 역할도 한 일련의 사례 연구이다. 이를 통해 우리는 Charon의 설계 선택이 매우 다양한 사용 사례에 적합하다는 경험적 증거를 제공하며, Charon이 Rust 분석의 만능 도구라는 우리의 주장을 뒷받침한다.
Charon은 Github에서 공개적으로 개발되며[8] 오픈소스 라이선스로 배포된다. 재현 가능성을 높이기 위해 artifact도 온라인으로 제공된다[9].
이제 Rust 컴파일러와 Charon 프레임워크의 아키텍처를 설명한다. Figure1은 다양한 단계를 시각적으로 요약한다.
Figure 1: Charon 프레임워크의 아키텍처 다이어그램, Rust 컴파일러와의 관계, 그리고 소비자와의 관계.
Rust 컴파일러 파이프라인은 초기 파싱 이후 세 개의 AST에 의존한다. HIR("High-level IR"), THIR("Typed HIR"), 그리고 MIR("Mid-level IR")이다. HIR은 매크로 확장과 이름 해석의 결과이다. 그런 다음 THIR에서는 모든 타입 정보가 채워지고, 첫 번째 단계의 desugaring이 수행되며, 특히 reborrow와 자동 차용 및 역참조가 처리된다. 이 단계에서는 의미론의 많은 세부 사항이 여전히 암묵적이다. move, copy, drop, 패턴의 제어 흐름 등은 이 AST에 나타나지 않는다. MIR에서는 이러한 의미론적 세부 사항이 모두 명시적으로 드러난다. MIR은 제한된 집합의 statement와 terminator를 갖는 CFG로, HIR과 THIR보다 더 저수준 의미론을 가진다. Rust 컴파일러는 MIR AST 위에서 동작하는 거의 60개의 컴파일 패스[34]를 갖고 있는데, 이는 표준적인 설계 선택이며 실제로 여러 단계가 MIR의 서로 다른 부분집합에 의존한다. 모든 최적화가 MIR에서 수행된 후 최종 단계는 LLVM bitcode를 생성하고, 나머지 컴파일 파이프라인을 LLVM 자체에 넘기는 것이다. 이제 우리의 설계 선택을 검토하고, 그것이 Rust 분석 개발 작업을 어떻게 용이하게 하는지 설명한다.
MIR은 Rust를 정확하게 모델링하기 어렵게 만드는 많은 의미론적 세부사항을 명시적으로 드러내기 때문에, 검증 도구[11, 19, 4, 29]와 borrow-checking 같은 컴파일러 분석에서 흔한 출발점이다. 후자는 THIR에서는 오류 가능성이 너무 높았다[1, 24]. 특히 move, copy, (re)borrow, drop은 Rust 의미론의 핵심이며 모두 MIR에서 명시적이다. 예를 들어 let x=&mut y;f(x)는 MIR에서 let x=&mut y;f(move&mut(*x))가 되어, move-out으로 인해 x 자체가 무효화되는 것을 피한다. 패턴 매치처럼 THIR에서 매우 비자명한 의미론을 갖는 다른 desugaring도 MIR에서만 명시적으로 나타난다. Rust 프로그램의 정밀한 분석을 가능하게 하기 위해 Charon 역시 MIR에서 동작한다.
MIR 표현으로부터 Charon은 ULLBC라는 정리되고 장식된 관점을 구성한다. ULLBC는 MIR처럼 CFG이지만, MIR와 달리 즉각적인 문맥 및 의미 정보를 제공하고(§2.4), 구현 특화 세부사항을 숨기면서도(§2.5) Rust 언어 전체를 노출한다. 특히 사용자가 rustc를 질의하여 보조 데이터 구조의 타입 정보를 얻거나 trait solver를 호출하는 대신, ULLBC는 이 모든 핵심 정보를 CFG에 직접 부착한다.
또한 ULLBC는 MIR에 대해 더 구조적이고 의미적인 관점을 제공하는 여러 정리 변환 패스를 포함한다. 예를 들어 저수준 표현 위에서 작동하는 패턴 매칭을 단순화하여 더 고수준의 ML 스타일 패턴 매치로 대체하고, 다양한 형태의 panic! desugaring을 하나의 통일된 statement로 변환하며, 정수 오버플로를 위한 동적 검사와 해당 산술 연산을 함께 묶어 의미론을 단순화한다. 우리는 궁극적으로 ULLBC의 소비자가 이러한 패스가 자신들에게 적합한지 판단하게 되리라 본다. 예를 들어 특정 소비자는 checked operation에 대한 명시적 assertion을 보고 싶을 수 있다. 그런 경우를 위해, 우리는 어떤 재구성 패스를 활성화할지 수동으로 선택할 수 있는 일반 API를 구상하고 있다.
그 다음 Charon은 ULLBC CFG에 제어 흐름 재구성 알고리즘을 적용하여 구조화된 루프와 분기를 구체화한 LLBC AST를 생성한다. 실제로 우리는 rustc의 CFG 구성 방식을 역공학하여, MIR basic block으로부터 loop, conditional 등을 재생성한다.
Charon은 이미 Rust의 상당한 부분집합을 지원하며, 이는 우리의 평가에서 드러난다(§3). 그러나 덜 핵심적인 몇몇 기능은 아직 지원되지 않는데, 구체적으로 동적 trait dispatch(dyn Trait), generic associated types, trait alias, async, 그리고 함수 반환 타입의 impl s 이다. 이러한 기능을 사용하는 crate의 분석을 지원하기 위해, Charon은 견고하게 설계되었다. 번역할 수 없는 선언은 missing으로 표시되고, crate의 나머지는 평소처럼 번역되어, 잘 형성된(비록 불완전할 수는 있는) (U)LLBC를 생성한다. 지금까지 이러한 누락 기능은 우리의 사례 연구를 방해하지 않았다.
rustc 위에서 동작할 때 프로그램 분석에 필요한 정보를 얻는 일은 두 가지 이유로 까다롭다. 첫째, rustc는 완전히 장식된 표현을 노출하는 대신, 컴파일러 내부를 query 하기 위한(문서가 빈약한) 지연 계산에 의존한다. 따라서 프로그램 노드가 주어졌을 때 원하는 정보를 가져올 수 있는 보조 함수가 무엇인지 찾기 위해 rustc 자체의 코드를 훑어보아야 한다. 둘째, 그리고 더 중요하게는, 일부 정보가 부분적이거나 누락될 수 있다.
예를 들어 Rust trait 메서드 호출을 생각해 보자. 이를 분석하려면 먼저 적절한 인자를 가진 해당 Rust trait 의 인스턴스(즉, 구체화된 impl)와, 인자를 포함한 메서드 참조(메서드가 generic인 경우)를 알아야 한다. 안타깝게도 구체적인 trait 인스턴스는 MIR에서 직접 사용 가능하지 않다. 예를 들어 아래 코드 조각을 보자.
{minted}
rust fn clone_vec<T>(v : &Vec<T>) -> Vec<T> where T:Clone v.clone()
이 코드를 컴파일할 때 rustc는 trait solver를 질의하여 Vec<T>에 대한 Clone 인스턴스를 찾아 clone 메서드 호출이 합법적인지 판단해야 한다. 우리의 경우 이 인스턴스는 Vec<T:Clone>에 대한 표준 라이브러리 Clone 구현(이를 CloneVec이라 부르겠다)과, 입력으로 받은 로컬 인스턴스 T:Clone(이를 CloneT라 부르겠다)이 결합된 것이다.
trait solver는 그러한 인스턴스가 존재한다 는 것만 확인하면 된다. 그러나 이 코드를 분석할 때 우리는 더 정밀한 정보, 즉 v.clone()이 정확히 CloneVec과 CloneT의 조합을 사용한다는 사실을 원할 수 있다. 안타깝게도 rustc에서 이 정보를 얻으려면 여러 비자명한 단계가 필요하다. 먼저 trait solver를 질의해야 하는데, 이를 위해 rustc 내부의 binder 표현이나 late-bound 및 early-bound region 같은 복잡한 개념들을 다뤄야 한다. 더 나쁘게도 trait solver가 주는 정보는 부분적이다. solver는 단지 v.clone()이 함수의 로컬 where 절로부터 유도될 수 있는 어떤 T:Clone 인스턴스와 결합된 CloneVec을 사용한다고 말해 줄 뿐, 이 유도를 드러내지 않는다. 이를 재구성하는 것은 일반적으로 비자명한 문제이며, 특히 super trait가 있을 때 어떤 trait 인스턴스는 다른 trait 절에 의해 함의될 수 있기 때문이다.
또 다른 문제는 함수 및 메서드 호출에 주어지는 입력 매개변수에서 비롯된다. 다음 코드 조각을 보자.
{minted}
rust fn f<V>(x : V); fn g<V>(x : V) f::<V>(x); trait Trait<U> fn f<V>(x : V); fn h<T,U,V>(x:V) where T:Trait<U> (T as Trait<U>)::f::<V>(x)
g 안에서 함수 f 호출에 전달된 generic parameter 목록을 가져올 때 rustc는 V를 준다. 그러나 h 안에서 메서드 호출 Trait::f에 전달된 parameter를 질의하면, rustc는 trait 인스턴스의 parameter와 메서드 자체에 전달된 parameter를 이어붙여, T(암묵적 Self parameter), U, V를 반환한다. 사용자는 V만 기대하므로 이 동작은 혼란스럽고 오류를 유발하기 쉽다. 그 결과 Charon은 아래와 같은 상용구 코드를 통해 parameter 목록을 가져오고 잘라낸다. 이 코드는 이를 위해 우리가 도입한 여러(여기서는 생략된) 보조 helper(빨간색)를 사용한다.
{minted}
[escapeinside=??]rust let (gens, source) = // Is this a function or method call? if let Some(assoc) = tcx.opt_associated_item(id) … // Omitted match assoc.container // Trait "decl" or impl method call? AssocItemContainer::TraitContainer => // Trait "decl" method call let num_cont_gens = tcx.?generics_of(cont_id).own_params?.len(); let impl_expr = ?self_clause_for_item?(s, &assoc, gens).unwrap(); let method_gens = gens[num_cont_gens..]; (method_gens.sinto(s), Some(impl_expr)) AssocItemContainer::ImplContainer => // Trait impl method call let cont_gens = tcx.?generics_of(cont_id)?; let cont_gens = gens.?truncate_to(tcx,cont_gens)?; let mut comb_trait_refs = ?solve_req_traits(s,cont_id,cont_gens)?; comb_trait_refs.extend(std::mem::take(&mut trait_refs)); trait_refs = comb_trait_refs; (gens.sinto(s), None) else (gens.sinto(s), None); // Fun call
상용구 코드로 이어지는 다른 기술적 세부사항도 많다. 예를 들어 trait 인스턴스만 가져오는 데에도 600줄이 넘는 코드가 필요하다. 반면 Charon은 아래의 LLBC datatype을 제공하며, 이는 적절히 잘린 parameter 목록과 함께 관련된 모든 trait 정보를 직접 노출한다. 이 정보는 Rust generic programming의 핵심인 타입 및 trait 다형성을 지원하며, 그 표현은 trait clause, parent clause, self type, trait bound의 새로운 추상 언어에 기반한다. 예를 들어 하나의 trait는 최상위 구현뿐 아니라 로컬 where 절(예: T:Clone)이나 연관 타입에 의해 함의되는 trait(예: IntoIterator는 연관 타입 IntoIter:Iterator<...>를 포함함)도 참조할 수 있다.
{minted}
rust struct FnPtr func: FunIdOrTraitMethodRef, // Function identifier generics: GenericArgs, // Generic parameters
enum FunIdOrTraitMethodRef Fun(FunId), // Top-level function Trait(TraitRef, TraitItemName, …), // Trait method
struct TraitRef kind: TraitRefKind, … enum TraitRefKind TraitImpl(TraitImplId, GenericArgs), // Top-level impl Clause(ClauseId), // Local where clause ItemClause(Box<TraitRefKind>, …), // Implied by assoc. type
trait resolution을 넘어, Charon은 Relooper 유사 알고리즘을 적용해 제어 흐름도 재구성하고, crate를 사용하기 쉬운 구조로 묶으며, 선택적으로 trait associated type을 타입 parameter로 끌어올리는 한편 서로 같다고 알려진 타입(예: 절 T::Item=u32 때문에)을 정규화한다.
Rust 프로젝트를 효율적으로 컴파일하기 위해, rustc는 프로그램 정보를 다양한 표현으로 저장하는데, 이들 중 일부는 분석 목적으로 직접 사용하기에는 너무 저수준이다. 특히 MIR에서는 상수가 이미 컴파일되어 있기 때문에, 구조체 값 대신 이미 배치된 바이트 배열만 제공될 수 있다. 예를 들어 상수로 컴파일된 열거형 값의 고수준 표현을 얻는 과정을 설명해 보자. 우리는 mir::Const 열거형에서 시작하여 매칭을 수행하고, 상수가 타입에서 사용되는 경우(예: const generic을 구체화하는 데 사용되는 경우)에는 ty::Const를, 그렇지 않으면 ConstValue를 얻는다. 더 깊이 들어가면, ty::Const로부터 한 경우(다른 경우도 많이 있다)에는 ValTree를 얻는다. 상수의 타입을 사용해, 이것이 추상 데이터 타입(ADT)이므로 이를 DestructuredConst(아래)로 바꾸는 특정 rustc helper를 호출해야 함을 알 수 있고, 여기서부터 재귀적으로 열거형 값을 복원할 수 있다.
{minted}
rust struct DestructuredConst<’tcx> variant: Option<VariantIdx>, fields: &’tcx [ty::Const<’tcx>],
다른 경우들도 비슷하게 복잡하며, 많은 코너 케이스가 있다. 반면 Charon은 상수에 대해 다음과 같은 통일된 고수준 표현을 제공한다.
{minted}
rust enum ConstantKind Adt(Option<VariantId>, Vec<Constant>), … /* Omitted */ struct Constant value: ConstantKind, ty: Ty,
상수 외에도 Charon은 다른 저수준 표현을 고수준 함수형 datatype으로 변환한다. 여기에는 예를 들어 이름 표현의 단순화, span 정보 재구성, 컴파일 과정에서 정의를 제자리에서 갱신할 수 있게 하지만 잘못된 순서로 접근하면 일부 정의를 사용할 수 없게 만드는 Steal 자료구조의 사용 제거, rustc가 "early bound" 및 "late bound" region variable이라고 부르는 것 대신 parameter를 명시적이고 일관되게 다룸으로써 binder의 사용을 명확히 하는 일, 또는 기본 메서드를 일반 메서드로 바꿔 trait 구현을 단순화하는 일이 포함된다.
앞선 절들에서 우리는 MIR을 더 쉽게 소비할 수 있도록 Charon이 수행하는 변환을 소개했다. 이제 LLBC 출력의 개요를 간단히 살펴보자. LLBC에서 crate(아래의 TranslatedCrate)는 crate 이름, 소스 파일의 내용, 그리고 선언들을 포함하며, 각 선언은 고유하게 식별된다(예: TypeDeclId 타입의 id). 또한 우리는 상호 재귀적인 선언들의 그룹도 계산하고(여기서는 보이지 않음), 이를 위상 순서로 정렬하는데, 이는 분석과 컴파일 모두에 유용하다.
{minted}
rust struct TranslatedCrate crate_name: String, files: Vector<FileId, File>, type_decls: Vector<TypeDeclId, TypeDecl>, fun_decls: Vector<FunDeclId, FunDecl>, … /* omitted */
함수 선언과 시그니처는 비교적 단순하다. 함수 선언은 고유 식별자, 선언 이름에 대한 metadata, span과 attribute, 시그니처, 그리고 선택적 body를 포함한다. body는 Charon이 오류를 만났거나 함수가 #[charon::opaque] attribute로 표시된 경우 생략된다. 시그니처는 generic parameter, 입력 타입 목록, 출력 타입을 단순히 포함한다.
{minted}
rust struct FunDecl id: FunDeclId, meta: ItemMeta, signature: FunSig, body: Result<Body, Opaque>, … /* omitted */
{minted}
rust struct FunSig … /* omitted */, generics: GenericParams, inputs: Vec<Ty>, output: Ty,
중요하게도 generic parameter(GenericParams)는 bound variable(region variable, type variable 등)와 where clause와 관련된 모든 정보를 단순하고 명시적인 형식으로 담고 있다. 이 타입은 그렇지 않으면 rustc를 여러 번 질의해야 얻을 수 있는 정보를 한곳에 모으며, 모든 정의(함수, 타입, trait 선언 등)에서 일관되게 사용된다.
{minted}
rust struct GenericParams regions: Vector<RegionId, RegionVar>, types: Vector<TypeVarId, TypeVar>, const_generics: Vector<ConstGenericVarId, ConstGenericVar>, trait_clauses: Vector<TraitClauseId, TraitClause>, // T : Clone regions_outlive: Vec<RegionBinder<RegionOutlives>>, // ’a : ’b types_outlive: Vec<RegionBinder<TypeOutlives>>, // T : ’a trait_type_constraints: …, // T::Item = u32
타입, trait 등 다른 정의도 모두 유사한 모델을 따르며, 고유 식별자, metadata(즉, ItemMeta), generic parameter, 선택적 body를 포함한다. 여기서는 생략한다. 함수 본문의 정의는 로컬 변수 목록과 statement 블록을 저장하지만 이를 건너뛰고, 이제 LLBC statement의 정의를 보자. Statement는 예상되는 종류를 가진다. 예를 들면 assignment, function call, return, loop가 있다. Switch 열거형(여기서는 보이지 않음)은 if then else, 정수에 대한 switch, 열거형에 대한 match를 구분한다. 우리는 코드 span과 사용자 주석도 보존한다.
{minted}
rust enum StatementKind Assign(Place, Rvalue), Call(Call), Abort(AbortKind), // panic Switch(Switch), Loop(Block), Return, Nop, Drop(Place), Break(usize), Continue(usize), … /* omitted */
{minted}
rust struct Statement span: Span, kind: StatementKind, comments: Vec<String>,
struct Block span: Span, statements: Vec<Statement>,
이 간단한 개요의 마무리로 함수 호출을 보자. 우리는 모든 경우가 하나의 정의 안에 묶이고 쉽게 구분되도록 Call 구조를 신중하게 작성했다. 중요한 필드는 FnOperand로, 여기에는 서로 다른 경우가 포함된다. 즉 최상위 함수 사용, trait 메서드 사용, 그리고 로컬 변수에 저장된 함수 포인터 사용(예: 익명 함수 사용 때문)이 있다.
{minted}
rust struct Call func: FnOperand, args: Vec<Operand>, dest: Place,
enum FnOperand Regular(FnPtr), Move(Place),
{minted}
rust struct FnPtr func: FunIdOrTraitMethodRef, generics: GenericArgs,
enum FunIdOrTraitMethodRef Fun(FunId), // top-level function TraitMethod(…), // trait method
FnOperand가 최상위 함수나 trait 메서드를 가리킬 때, 그것은 FnPtr를 사용하여 함수 식별자와 그 generic argument를 함께 묶는다. FnPtr 자체가 최상위 함수를 식별하는 경우, 그것은 그 함수의 고유 식별자를 직접 참조하며, 이를 통해 예를 들어 위에서 보인 TranslatedCrate에서 함수 정의를 조회할 수 있다. FnPtr가 trait 메서드 호출을 식별하는 경우, 그것은 TraitRef가 주어지는 trait 인스턴스(§2.4 참조)와 실제로 호출되는 메서드 이름을 함께 묶는다.
여기서 LLBC 개요를 마친다. 생략된 AST 부분들도 비슷한 논리를 따른다. 즉 우리는 정의를 인수분해하고, metadata를 포함해 가능한 한 많은 정보를 저장하며, 모든 정보를 명시적으로 만들고자 한다.
Rust의 빌드 시스템 cargo는 올바른 revision의 의존성을 가져오고, 이를 재귀적으로 빌드하며, 마지막으로 현재 crate에 대해 필요한 모든 의존성의 include 및 library 경로를 갖춘 rustc를 호출하는 일을 담당한다. 기존 Rust 프로젝트와 매끄럽게 통합하기 위해, Charon은 cargo 인프라를 직접 재사용한다.
이를 위해 charon 실행 파일은 먼저 cargo를 호출한다. 특수한 환경 변수를 통해 cargo는 일반 rustc를 호출하거나(의존성 분석용), 또는 컴파일러에 추가 hook을 심어 둔 우리만의 rustc 변형인 charon-driver를 호출하도록 만들 수 있다. 실행되면 charon-driver는 rustc를 구동하면서, LLVM으로의 최종 컴파일 단계를 프로그램 분석 단계, 즉 Charon 프레임워크로 대체한다. 사용자 관점에서 이 모든 저수준 구현 세부사항은 숨겨져 있으며, 필요한 것은 프로젝트의 루트(즉 crate)에서 charon 실행 파일을 호출하는 것뿐이다.
cargo build와 달리, 이는 실행 파일을 생성하지만 charon을 호출하면 (U)LLBC의 직관적인 직렬화(현재는 JSON)인 .(u)llbc 파일이 생성된다. 이후의 분석은 모두 이 파일을 바탕으로 수행된다. 분석 자체가 Rust로 작성된다면, 우리는 rustc에 링크되는 부분이 나머지 부분(정리 작업, CFG 및 AST 표현, 직렬화와 역직렬화)과 별도의 crate에 살도록 Charon을 설계하여, 분석 도구가 컴파일러 전체 도구 체인을 포함할 필요가 없게 했다.
우리는 또한 Rust 외의 다른 언어를 위해 (U)LLBC 타입 선언과 역직렬화기를 자동 생성할 수 있다. 현재 우리는 .(u)llbc 파일을 다시 읽을 수 있는 OCaml 라이브러리인 charon-ml을 제공한다. OCaml은 AST 조작에 특히 적합하고, 자동 visitor 생성 같은 편리한 기능을 제공하여 분석 도구 개발을 가속화한다. 다른 언어에 대한 지원 추가는 많지 않은 노력만으로 가능할 것이다.
우리의 도구 체인은 두 부분으로 이루어진다. 첫째는 (U)LLBC를 구성하고 추가 변환 패스를 수행하는 Charon 코드베이스 자체로, 공백과 주석을 제외하고 18kLoC 규모이다. 둘째는 hax 프로젝트[6]와 협력하여 개발한 hax-frontend-exporter crate로, 9kLoC 규모이며 rustc의 출력을 직접 소비하고 대부분의 query를 수행하며, MIR과 THIR 양쪽에서 동작하는 상수 단순화와 커스텀 trait resolution도 수행한다. 우리는 이것들이 컴파일러의 보조 구성 요소로서 Charon과 독립적으로도 유용하다고 믿기 때문에 별도로 패키징한다. 이 전체 프로젝트를 작성하는 데에는 2 인년의 노력이 들었다.
우리는 Charon 위에 두 개의 정적 분석을 구현했다. 첫째, unsafe Rust 프로그램에서 잘 알려진 버그 패턴 집합을 찾아 잠재적 메모리 안전성 문제를 탐지하는 최근의 정적 분석기 Rudra[4]를 이식하여, rustc와 직접 상호작용하는 대신 Charon을 사용하도록 했다. 이 이식에는 하루의 작업이 들었고, 특히 ULLBC가 필요한 모든 정보를 제공함을 확인해 주었다. 분석을 검증하기 위해, 우리는 원래 논문의 평가에 사용된 crate 버전들에 대해 Rudra의 이식본을 다시 실행했다. Rust 생태계의 변화와 프로젝트에 .lock 파일이 포함되지 않았던 이유로 여러 crate는 더 이상 컴파일되지 않지만, 그럼에도 우리는 원래 논문에서 고려된 가장 인기 있는 crate 6개를 분석할 수 있었고, 이전에 발견된 취약점을 다시 식별했다.
또한 우리는 LLBC 위에서 동작하는 흐름 민감, 필드 민감, 문맥 민감 taint 분석을 통해 암호 코드의 constant-time 위반을 탐지하는 분석기를 구현했다. 우리는 RustCrypto[35], 형식 검증된 HACL⋆ 라이브러리[32, 39]의 안전한 Rust 포트, 그리고 형식 검증된 암호 라이브러리 libcrux[22] 안에 있는 최근 표준화된 post-quantum ML-KEM[28] 암호 원시 구현 등 여러 암호 crate의 구현에 대해 분석을 실행했으며, 총 88k LoC를 다뤘다. 우리의 taint 분석은 널리 사용되거나 검증된 라이브러리에서 기대되는 바와 같이, 고려한 구현들에 constant-time 위반이 없음을 성공적으로 보여 주었고, 더 이른 검증되지 않은 ML-KEM 버전에서 KyberSlash 타이밍 공격을 재발견했다[5, 7].
Aeneas[17, 16]는 안전한 Rust 프로그램을 검증하기 위한 프레임워크로, Rust 프로그램의 모델을 생성하여 여러 정리 증명기로 내보내는 방식으로 동작한다. Aeneas는 LLBC 코드를 얻기 위해 Charon에 의존하며, Charon 구현의 원래 동기이기도 했다. 많은 다른 도구들이 각각 rustc와 상호작용하는 자체 로직을 재구현하고 있다는 사실을 깨달은 뒤, 우리는 이 작업을 위한 재사용 가능한 구성 요소를 패키징하고 공개하는 것이 현재와 미래의 Rust 도구 작성자들에게 도움이 되리라 강하게 느꼈다.
Eurydice 1 1 1https://github.com/AeneasVerif/eurydice는 Rust에서 C로의 트랜스파일러이며, 그 주된 동기는 엔지니어가 새 코드를 Rust로 개발하면서도 레거시 이유로 여전히 C 코드를 제공할 수 있게 하는 것이다. 이 도구는 공백과 주석을 포함하여 약 5000줄의 OCaml 코드로 이루어져 있으며, Charon을 통해 Rust 코드를 소비하고 LLBC를 C로 번역한다. Eurydice는 특히 LLBC 설계의 이점을 누린다. AST가 작고 구조화되어 있어 번역이 단순해지고, C 의미론과 정확히 맞추는 데 필요한 move 및 copy 연산이 명시적이기 때문이다.
앞서 우리는 Charon이 자신의 (U)LLBC 표현을 다른 언어에서 사용할 수 있는 재사용 가능한 형식으로 노출한다고 언급했다. Charon 코드베이스 자체는 Eurydice와 Aeneas에서 사용되는, 이 형식을 조작하기 위한 OCaml 라이브러리를 유지한다. 우리는 이 라이브러리를 수동으로 작성하는 대신, Charon을 자기 자신 위에서 실행하여 Rust로 작성된 LLBC 및 ULLBC 타입 정의를 조사하고, (U)LLBC를 읽고 조작하기 위한 적절한 OCaml 타입 정의, visitor, 역직렬화기를 출력한다.
Charon은 아직 비교적 최근의 프로젝트이지만, 우리는 이미 프레임워크의 제삼자 사용 사례를 보고할 수 있다. Kani 모델 검사기[19]는 최근 ULLBC를 생성하는 백엔드를 추가하여 Charon의 제어 흐름 재구성 패스를 활용했다. RaRust[40]는 Rust를 위한 선형 자원 경계 분석으로, Rust 프로그램의 LLBC를 얻기 위해 Charon의 (이전 버전)을 사용한다.
우리가 아는 한, 다양한 도구에 적합한 MIR 관점을 제공하려는 유일한 다른 프로젝트는 Stable-MIR[36]이다. Charon과 마찬가지로 Stable-MIR도 중요한 Rust 구성 요소에 대한 자체 표현을 가지며, 강하게 타입이 부여된 식별자를 특징으로 한다. 그러나 Charon과 달리 Stable-MIR은 그 자체로 독립적인 rustc driver가 아니다. 오히려 rustc driver를 작성하기 위한 툴킷에 더 가깝다. 적절한 메서드를 제공하고 드라이버 세부사항을 숨김으로써 컴파일러와의 상호작용을 상당히 단순화하지만, 설계상 그것은 컴파일러 내부에 대한 얇은 래퍼이다. 따라서 CFG를 정리하거나 AST로 재구성하려 하지 않으며, 우리가 하듯 상수를 단순화하거나 trait를 해석하려 하지도 않는다. 그러나 두 프로젝트는 유사한 목표를 가지며, 앞으로 생산적으로 협력할 수 있을 것이다.
Charon 프로젝트는 비슷한 요구를 가진 다른 프로젝트들과 협력하고 있다. 예를 들어 hax[6]와 Charon은 trait resolution 시스템과 상수 단순화를 포함한 중요한 구성 요소를 공유하며, Kani[19]는 최근 ULLBC를 생성하는 백엔드를 추가하여 Charon의 제어 흐름 재구성 패스를 활용했다. 일반적으로 역사적 이유로, 기존의 많은 검증기 및/또는 Rust 기반 도구는 자체 필요에 더 맞춰진 덜 일반적인 형태로 동등한 기능을 스스로 유지하고 있다. 우리는 Charon의 채택이 계속되기를 바라며, 더 많은 도구와 클라이언트가 Charon에 의존할 수 있도록 로드맵, 거버넌스 모델, 커뮤니티를 공식화할 계획이다.
Rust를 넘어, 다른 도구들이 대상으로 삼거나 소비할 수 있는 중간 표현을 제안한 여러 노력이 있다. 가장 유명하게는 LLVM 도구 체인이 많은 소스 언어를 위한 공통 기반을 제공하며, 많은 분석에 활용될 수 있다[14, 15, 13, 46]. LLVM은 처음에는 컴파일 프레임워크로 의도되었지만[20], 이제는 dominator나 alias analysis를 위한 라이브러리처럼 새로운 분석 개발에 필요한 노력을 크게 줄이는 구성 요소들을 포함하고 있다. 우리는 (U)LLBC에 대해서도 유사한 기능을 제공할 계획이다. JVM과 .NET CLR 같은 관리형 언어 런타임은 많은 언어(예: Scala, Clojure, F#)의 대상이 되었고, 다시 범용 분석의 기반을 만들어 냈다(예: CLR Profiler, Java를 위한 Abstract Interpretation[23]). Charon과 유사하게, WASM을 위한 LLVM 백엔드인 Emscripten도 더 구조화된 WASM 의미론을 목표로 Relooper 알고리즘을 사용해 구조화된 제어 흐름을 재구성하는 몇몇 정리 작업을 수행한다[45].
{credits}
이 연구는 프랑스 국가연구청이 관리하는 France 2030 프로그램의 지원을 받았으며, grant agreement ANR-22-PTCC-0001 및 ANR-22-PETQ-0008 PQ-TLS에 의해 수행되었다.
