한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있지만, 상태 공간이 대가다

한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있다. 이 일을 하는 도구를 model checker라 부르며, 현재 Rust 에 가장 실용적인 것은 AWS 가 개발한 Kani 다. 평범한 Rust 단언을 작성하면 된다. Kani 는 이를 수학적 명제로 변환하고 가능한 모든 입력에 대해 검증한다. 정리 증명기도, 증명 보조 도구도, Coq 에 6개월을 빠지는 일도 없다.

문제는 “가능한 모든 입력”은 입력 공간이 충분히 작아서 전부 탐색할 수 있을 때만 작동한다는 점이다. 함수가 백만 개 요소를 가진 Vec<u8> 을 받는다면, Kani 는 모든 순열을 검증하지 않는다. 지정한 경계까지 검증하거나, 노트북의 메모리가 바닥날 때까지 실행한다. 증명은 진짜지만 유계하다.

”증명 없는 증명”이 실제로 의미하는 것

형식 검증은 보통 Coq 같은 증명 보조 도구에서 프로그램을 작성하고, 불변식을 직접 정의하며, 전술적 단계로 솔버를 이끄는 것을 의미한다. CompCert 같은 검증된 컴파일러는 수년이 걸렸다. 대부분의 팀에 그런 시간은 없다.

model checking은 다르다. 평범한 Rust 를 작성한다. #[kani::proof] 로 주석을 단 검증 함수를 추가한다. 그 안에서 kani::any() 로 기호적 값을 생성하고, 대상 코드를 호출한 뒤 속성을 단언한다. Kani 는 코드를 논리식으로 컴파일해 SMT 솔버에 넘긴다. 솔버는 경계 내의 모든 입력에서 속성이 성립함을 확인하거나, 구체적인 반례를 출력한다.

증명을 작성한 것이 아니다. 전칭 한정자를 갖는 검증을 작성한 것이다. 증명을 작성한 것은 도구다.

Kani 가 Rust 를 논리로 변환하는 방식

Kani 는 유계 model checker다. 코드를 논리식으로 펼쳐 SMT 솔버에게 어떤 실행 경로가 단언을 위반할 수 있는지 묻는다. 솔버는 변수를 기호적으로 다룬다. 평범한 검증은 x 에 값 5 를 준다. Kani 증명은 x 에 가능한 모든 u32 를 나타내는 기호를 준다.

다음은 자명한 예시다. 오버플로우해서는 안 되는 함수가 있고, 이를 증명하고자 한다.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

cargo kani 를 실행하면 Kani 는 이를 수 초 만에 검증한다. x 의 가능한 4,294,967,296 가지를 하나씩 실행하지 않고 검증한다. SMT 솔버는 기호적 표현으로부터 추론하여 반례가 존재하지 않는다고 결론 내린다.

#[cfg(kani)] 가드는 이 코드가 Kani 하에서만 컴파일됨을 의미한다. 릴리스 빌드를 부풀리지 않는다.

실제 예시: 파서의 크래시 없음을 증명하기

오버플로우는 쉽다. 흥미로운 경우는 데이터에 의존하는 경우다. 작은 프로토콜 헤더를 구문 분석하는 함수가 있고, 어떤 바이트열을 넣어도 절대 패닉하지 않음을 증명하고자 하자.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani 는 parse_header 가 길이 0부터 8까지의 모든 입력 버퍼에 대해 패닉하지 않음을 검증한다. 경계 검사, 버전 검사, 배열 첨자 접근을 모두 검증한다. 길이 확인을 먼저 하지 않고 buf[1] 이라고 썼다면, Kani 는 반례를 발견할 것이다. 1바이트 버퍼에서 buf[1] 이 범위를 벗어나는 경우다.

#[kani::unwind(5)] 주석은 Kani 에게 루프를 몇 번 펼치라고 지시한다. 이 함수에는 루프가 없으므로 이 값은 보수적이다.

경계화 문제: model checking이 벽에 부딪히는 지점

model checking은 경계 내에서는 전수적이다. 경계 밖에서는 아무것도 말하지 않는다. 이것이 근본적인 트레이드오프다.

루프가 첫 번째 벽이다. Kani 는 모든 루프를 고정 횟수만큼 펼쳐야 한다. 함수가 Vec 을 순회하고 언와인드 경계를 10으로 설정하면, Kani 는 길이 0부터 10까지의 벡터에 대해 정확성을 증명한다. 길이 11에 대해서는 아무것도 말하지 않는다. 경계를 1 높일 때마다 상태 공간이 배로 늘어난다. 언와인드 50이면 몇 분이면 끝날 수 있다. 언와인드 500이면 영원히 끝나지 않을 수 있다.

재귀도 마찬가지다. 호출마다 논리식이 팽창한다. 깊은 재귀는 메모리 사용량을 폭발시킨다.

데이터 크기가 두 번째 벽이다. Kani 는 고정 길이 배열을 잘 다룬다. 동적으로 할당된 컬렉션은 크기를 명시적으로 제한하지 않는 한 어렵다.

표준 라이브러리가 세 번째 벽이다. Kani 는 이를 상당 부분 모델화했지만 전부는 아니다. Kani 가 이해하지 못하는 것을 호출하면 증명은 함수 정의 누락으로 실패한다.

Kani 가 증명할 수 있는 것과 한계

Kani 는 유계한 코드에서 패닉, 정수 오버플로우, 단언 위반을 찾는 데 능하다. 암호 프리미티브, 프로토콜 파서, 작은 state machine에 탁월하다. 잘못된 입력 하나가 대참사가 되고 코드가 자연스럽게 유계한 곳이다.

Kani 는 라이브니스 같은 활성 속성의 증명에는 적합하지 않다. “모든 요청이 최종적으로 응답을 받는다”는 속성은 무한 실행에 대한 추론이 필요한데, 유계 model checking은 의도적으로 그러지 않는다. 활성에는 TLA+ 같은 시간적 model checker이 필요하다.

Kani 는 테스트의 대체도 아니다. 증명이 통과하면 경계 내에 반례가 없음을 안다. 테스트가 통과하면 마음에 드는 특정 입력에서 코드가 올바르게 작동함을 안다. Kani 는 떠올리지 못한 경계값을 잡는다. 테스트는 Kani 가 볼 수 없는 통합 문제를 잡는다.

러너를 녹이지 않고 CI 에서 Kani 돌리기

작은 함수에 대한 Kani 증명 하나는 수 초다. 실제 crate 에 대한 스위트는 수 분이다. 언와인드 경계가 높은 증명은 수 시간이 걸릴 수 있다. 2시간짜리 SMT 풀이를 CI 파이프라인이 기다리고 싶지는 않을 것이다.

Kani 증명은 작고 빠르게 유지하라. 안전상 필수적인 함수, 즉 버그가 사고가 되는 함수를 증명하라. 웹 프레임워크 전체를 증명하려 들지 마라. 타임아웃을 설정하고, 증명당 예를 들어 5분으로 하며, 타임아웃은 “증명 실패”가 아니라 “증명 불능”으로 취급하라.

다음은 유효한 Makefile 패턴이다:

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast 는 모든 풀 리퀘스트에서 CI 를 돌린다. kani 는 매일 밤 돌린다. 증명이 퇴화해도 출하 후가 아니라 하루 이내에 알 수 있다.

공개 API 를 제공한다면, 공개 함수마다 완전히 기호적인 입력으로 호출하는 Kani 증명을 하나씩 작성하라. 이것이 형식적 계약 검증에 가장 가까운 것이다. 구현이 올바르다는 것을 증명하는 것은 아니지만, 임의의 유효한 입력에서 구현이 크래시하지 않음을 증명한다.

진짜 증명 보조 도구가 필요해지는 상황

“이 연결 리스트는 항상 비순환적이다”처럼 무계한 데이터 구조에 관한 속성을 증명해야 한다면, Kani 는 도움이 되지 않는다. 언와인드 경계가 주장을 무산시킨다. 이를 위해서는 Creusot 같은 도구가 필요하다. Rust 를 WhyML 로 번역하고 증명 보조 도구를 사용한다. 수고는 더 들지만 무계한 구조를 다룰 수 있다.

동치성 증명이나 정의되지 않은 동작 검출이 필요하다면, MIRI 나 KLEE 같은 도구는 노력과 포괄성의 스펙트럼 상 다른 지점에 위치한다. Kani 는 “유계한 코드가 있고 패닉하는지 알고 싶다”는 상황의 스위트 스팟이다. 파서, 디코더, 시리얼라이저, 설정 검증기가 모두 해당한다. Rust 의 타입 시스템은 이미 수많은 버그 클래스를 제거하고 있다. Kani 는 타입 시스템이 닿지 않는 것을 제거한다.

먼저 시도해 볼 것

불안을 느끼는 함수가 있는 Rust crate 를 가지고 있다면, Kani 를 추가하라. 불안한 함수는 보통 신뢰할 수 없는 입력을 구문 분석하거나, 비트 조작을 하거나, 배열에 첨자 접근을 하는 것이다. kani::any() 로 호출하는 증명 하네스를 작성하라. cargo kani 를 실행하라. 통과하면 크래시하지 않음에 대한 유계한 증명을 얻은 것이다. 실패하면 버그 보고서가 될 수 있었던 구체적인 반례를 얻은 것이다.

새로운 언어를 배울 필요는 없다. 시퀀트 계산을 이해할 필요도 없다. Rust 단언을 작성하고, 솔버에 성립하는지 물으면 된다. 그것은 학술적 의미에서의 형식적 증명은 아니다. 실용적 의미에서의 기계적 증명이다. 그리고 대부분의 소프트웨어에 있어 실용적인 것이야말로 정확히 필요한 것이다.

---

자주 묻는 질문

소프트웨어 검증에서 model checking란 무엇인가

model checking은 지정된 속성이 성립하는지 확인하기 위해, 시스템의 가능한 모든 상태를 전수적으로 탐색하는 자동화 기법이다. Rust 에서는 Kani 같은 도구가 유계 model checking을 사용하여 정의된 경계 내의 모든 가능한 입력에 대한 단언을 증명하며, 수작업 증명 구축을 필요로 하지 않는다.

Kani 는 단위 검증 작성과 무엇이 다른가

단위 검증은 특정 입력 하나를 조사한다. Kani 의 증명은 경계 내의 모든 입력을 조사한다. Kani 의 증명이 통과하면, 유계한 상태 공간 내에 반례가 존재하지 않음을 안다. 증명은 더 강력하지만, 설정한 경계에 의해 제한된다.

Kani 는 Rust 애플리케이션 전체의 정확성을 증명할 수 있는가

아니오. Kani 는 작고 유계한 함수에서 가장 효과를 발휘한다. 상태 공간은 루프 반복 횟수, 재귀 깊이, 데이터 크기에 따라 기하급수적으로 증가한다. 파서나 프로토콜 핸들러 같은 안전상 필수적인 컴포넌트에 Kani 를 사용하고, 애플리케이션 수준 논리에는 사용하지 말라.

고정 경계가 없는 루프를 Kani 가 만나면 어떻게 되는가

Kani 는 루프의 언와인드 경계를 필요로 한다. 루프가 경계를 초과해 실행될 수 있다면, Kani 는 실패하는 언와인드 단언을 삽입한다. 경계를 높이거나, 코드를 정적으로 알려진 횟수로 재구성해야 한다. 이것이 유계 model checking의 주요 한계다.