RustyDL: Rust 를 위한 프로그램 논리 (RustyDL: A Program Logic for Rust) 기술 요약

본 논문은 Rust 프로그래밍 언어의 메모리 안전성과 데이터 레이스 부재를 보장하는 강력한 타입 시스템을 기반으로, 소스 코드 수준에서 직접 작동하는 자동 상호작용 (Human-in-the-Loop, HIL) 추론 검증 도구를 구축하기 위한 프로그램 논리인 RustyDL을 제안합니다.

1. 문제 정의 (Problem)

기존의 Rust 검증 도구들 (Creusot, Prusti, Aeneas 등) 은 대부분 Rust 소스 코드와 명세를 중간 언어 (Intermediate Language, 예: Viper, Why3) 로 변환한 후 SMT 솔버를 사용하여 검증 조건을 생성하는 방식을 취합니다. 이 접근 방식에는 다음과 같은 한계가 있습니다.

• 신뢰성 문제: Rust 에서 중간 언어로의 변환 과정이 매우 복잡하며, 이 변환의 정확성을 신뢰해야 합니다.
• 상호작용 부재: 검증이 실패할 경우, SMT 솔버의 출력을 원래 소스 코드나 명세와 직접 연결하기 어렵습니다. 사용자는 증명 과정을 직접 검토하거나 수동으로 증명 단계를 적용할 수 없어, 매우 복잡한 기능적 속성을 검증하는 데 한계가 있습니다.
• HIL 검증의 부재: Java 의 경우 KeY 와 같은 도구를 통해 소스 코드 수준의 HIL 검증이 가능했으나, Rust 에서는 이러한 소스 코드 기반의 추론 검증 도구가 존재하지 않았습니다.

2. 방법론 (Methodology)

저자들은 Rust 의 고유한 기능 (소유권, 참조, 이동 semantics 등) 을 직접 모델링할 수 있는 동적 논리 (Dynamic Logic) 기반의 프로그램 논리인 RustyDL을 설계했습니다.

2.1 RustyDL 의 핵심 구성 요소

• 타입 계층 구조 (Sort Hierarchy): Rust 의 기본 타입 (bool, int, array) 과 참조 타입 (공유 참조 &T, 가변 참조 &mut T) 을 논리 타입으로 매핑합니다.
• 모달 연산자: 프로그램의 부분 p 와 명제 ϕ 에 대해 [p]ϕ(부분 정확성) 와 <p>ϕ(전체 정확성) 를 사용하여 프로그램 실행 후의 상태를 표현합니다.
• 크립크 구조 (Kripke Structure): Rust 프로그램의 상태 전이를 모델링하며, 결정론적 프로그램임을 가정합니다.
• 업데이트 (Updates): 상태 변화를 효율적으로 모델링하기 위해 **변경 업데이트 (Mutating Updates)**를 도입했습니다. 이는 가변 참조 (&mut) 를 처리하는 핵심 메커니즘으로, 값 자체뿐만 아니라 빌린 위치 (lender) 를 추적할 수 있게 합니다.
  • 예: t1 *-> t2는 t1 이 빌린 위치에 t2 를 씁니다.

2.2 Rust 특유의 도전 과제 해결 방안

RustyDL 은 Rust 의 5 가지 핵심 기능을 시퀀트 계산 (Sequent Calculus) 규칙으로 모델링합니다.

1. 소유권 (Ownership) 및 이동 (Move):
   • 값이 이동 (move) 될 때, 기존 변수는 초기화되지 않은 상태로 간주됩니다. 이를 명시적인 '초기화되지 않은 값'을 도입하는 대신, **스콜라화 (Skolemization, 익명화 업데이트)**를 사용하여 이동된 변수를 새로운 상수로 대체함으로써 효율적으로 처리합니다.
2. 정수 오버플로우 (Integer Overflow):
   • Rust 의 디버그 모드 (panic 발생) 와 릴리스 모드 (wrapping) 를 구분합니다. 검증은 안전성을 보장해야 하므로 디버그 세맨틱스를 따르며, 연산 결과의 범위를 검사하는 규칙을 도입하여 오버플로우 발생 시 panic 을 명시적으로 처리합니다.
3. 참조 (References) 모델링:
   • 공유 참조 (&): 빌린 값은 읽기 전용이므로, 참조를 빌린 값 그 자체로 취급합니다.
   • 가변 참조 (&mut): 빌린 위치 (lender) 를 추적하기 위해 Place 개념을 도입합니다. 가변 참조를 통한 쓰기는 *x = val을 x 의 값이 아닌 x 가 가리키는 Place 에 대한 업데이트 (x *-> val) 로 변환하여 모델링합니다.
4. 배열 접근:
   • 배열 인덱스 범위를 검사하여 범위를 벗어나면 panic 으로 이어지는 규칙을 적용합니다.
5. 루프 및 제어 흐름:
   • Rust 의 loop, break, continue 는 복잡한 제어 흐름을 가집니다. 이를 처리하기 위해 루프 스코프 (Loop Scope) 개념을 도입하여, 루프의 한 번의 일반적 반복을 기호적으로 실행하고 종료 이유 (break 여부) 를 기록하는 방식으로 불변식 (Invariant) 규칙을 설계했습니다.

2.3 구현 (Implementation)

RustyDL 계산 규칙은 잘 알려진 추론 검증 도구인 KeY를 기반으로 프로토타입 (Rusty KeY) 으로 구현되었습니다. 이는 'taclets'이라는 도메인 특화 언어로 규칙을 정의하여 기계적으로 검증 가능한 형태로 유지합니다.

3. 주요 기여 (Key Contributions)

1. RustyDL 프로그램 논리 제안: Rust 의 소유권, 참조, 이동 semantics 를 소스 코드 수준에서 직접 모델링하는 최초의 동적 논리 체계.
2. HIL 검증 가능성 입증: 중간 언어 변환 없이 Rust 소스 코드에 대해 인간이 개입하여 복잡한 속성을 검증할 수 있음을 이론적으로 증명.
3. 변경 업데이트 (Mutating Updates) 도입: 가변 참조를 모델링할 때 메모리 모델이나 로트 (loan) 집합을 명시적으로 추적하는 복잡한 방식 대신, 논리적 업데이트를 통해 간결하고 효율적으로 처리하는 방법 제시.
4. 프로토타입 구현 및 검증: KeY 기반의 Rusty KeY 를 구현하여 이진 탐색 (Binary Search) 등 다양한 Rust 함수 (루프, 참조, 배열 포함) 에 대한 검증 성공 사례 제시.

4. 결과 (Results)

• 이진 탐색 검증: 구현된 프로토타입을 사용하여 Rust 의 이진 탐색 알고리즘을 검증한 결과, 2.1 초 내에 4,260 개의 규칙 적용으로 증명을 완료했습니다.
• 기능적 검증: 소유권, 빌림 (borrowing), 루프, 배열, 튜플, 일부 열거형 (enum) 을 포함하는 Rust 프로그램에 대한 검증이 성공적으로 수행됨을 확인했습니다.
• 상호작용성: 사용자가 증명 과정에서 수동으로 단계를 적용하고 복잡한 속성을 검증할 수 있는 HIL 방식의 가능성을 보여주었습니다.

5. 의의 및 결론 (Significance)

이 논문은 Rust 검증 분야에서 중간 언어 변환에 의존하지 않는 소스 코드 수준의 추론 검증이 가능함을 처음으로 보여주었습니다.

• 신뢰성 향상: 변환 과정의 신뢰성 문제를 제거하여 검증 결과에 대한 신뢰도를 높였습니다.
• 복잡한 속성 검증: 자동화만으로는 해결하기 어려운 매우 복잡하고 미묘한 Rust 프로그램의 기능적 속성을 인간이 개입하여 검증할 수 있는 길을 열었습니다.
• 미래 작업: Traits, 반복자, 패턴 매칭, 제네릭 함수 지원 확대, unsafe Rust 에 대한 모델링 (보다 명시적인 메모리 모델 필요), 그리고 사용자 친화적인 GUI 및 명세 언어 (JML 유사) 개발이 향후 과제로 제시되었습니다.

결론적으로, RustyDL 은 Rust 의 강력한 타입 시스템과 소유권 모델을 논리적으로 정교하게 포착하여, 안전이 최우선인 시스템 (예: Linux 커널) 에 대한 형식적 검증을 위한 새로운 패러다임을 제시합니다.