Rust가 안전하다면서, 왜 또 검증 도구가 필요할까 — 코드를 '수학적으로' 증명하는 Kani

Rust는 안전한데, 대체 뭘 더 검증한다는 걸까

Rust를 쓰는 큰 이유 중 하나가 '메모리 안전'이잖아요. 컴파일러의 빌림 검사기(borrow checker, 값을 누가 언제 빌려 쓰는지 추적하는 장치)가 데이터 경쟁이나 잘못된 포인터 접근을 컴파일 단계에서 막아주니까요. 그런데 여기엔 함정이 하나 있어요. Rust가 보장해주는 안전은 딱 '안전한(safe) Rust' 영역까지거든요.

예를 들어 배열 범위를 벗어나 접근하거나(arr[100]), 값이 None인데 .unwrap()을 부르거나, 정수가 최댓값을 넘겨서 오버플로우가 나는 경우는 컴파일러가 못 잡아요. 이런 건 실행 중에 패닉(panic, 프로그램이 스스로 비정상 종료해버리는 것)으로 뻥 터지죠. 게다가 unsafe 블록 안에서는 빌림 검사기도 잠깐 눈을 감고요. Kani는 바로 이 빈틈을 메우려고 나온 도구예요. AWS가 만들어서 오픈소스로 공개했고, 자기네 Firecracker(서버리스를 돌리는 초경량 가상머신)나 s2n-quic 같은 진짜 중요한 코드를 검증하는 데 실제로 쓰고 있어요.

'모델 체커'가 뭐냐면

Kani는 스스로를 '모델 체커(model checker)'라고 부르는데, 이게 뭔지부터 풀어볼게요. 우리가 평소에 하는 테스트는 '입력 몇 개를 넣어보고 결과가 맞나 확인'하는 방식이잖아요. 값 하나하나 넣어보는 거라, 우연히 안 넣어본 값에서 버그가 숨어 있으면 못 찾아요. 퍼징(fuzzing)이 여기서 조금 더 나아가서 무작위 값을 마구 던져보긴 하지만, 그래도 '운'에 기대는 건 마찬가지예요.

모델 체킹은 접근이 완전히 달라요. '가능한 모든 입력'을 한꺼번에 수학적으로 따져봐요. 예를 들어 u8(0~255 값을 담는 정수) 두 개를 더하는 함수를 검증한다면, 256 × 256 = 65,536가지 경우를 하나하나 돌려보는 게 아니라, '어떤 조합에서든 오버플로우가 나지 않는가?'라는 명제를 통째로 풀어버리는 거예요. Kani는 이걸 위해 Rust 코드를 CBMC라는 검증 엔진이 이해하는 형태로 바꾸고, 그 뒤에서 SAT/SMT 솔버(논리식이 참이 될 수 있는지 계산하는 수학 엔진)가 답을 내요. 그래서 '버그가 없다'고 나오면, 그건 정말로(정해둔 범위 안에서는) 없다는 증명이 되는 거죠.

실제로 어떻게 쓰나

사용법은 생각보다 담백해요. 테스트 함수 쓰듯이 검증용 함수(proof harness)를 하나 만들고 위에 #[kani::proof] 표시를 붙여요. 그리고 구체적인 값 대신 let a: u8 = kani::any(); 처럼 써주면, 이 a는 '모든 가능한 u8 값을 동시에 의미하는 상징적(symbolic) 값'이 돼요. 그다음 검증하고 싶은 성질을 assert!로 적어두면 Kani가 알아서 반례가 있는지 뒤져요. 반례가 있으면 '이런 입력에서 터진다'고 구체적인 값까지 짚어줘서, 디버깅이 훨씬 수월해요. 터미널에서는 cargo kani 한 방이면 돌아가고요.

대신 공짜는 아니에요. 모든 경우를 따지다 보니 상태가 폭발적으로 늘어나는(state explosion) 문제가 있어서, 반복문은 보통 몇 번까지만 펼쳐서(bounded) 검사해요. 그래서 '무한히 도는 로직 전체'를 증명하기보다는, 핵심 함수나 자료구조의 안전성을 딱 짚어 검증하는 데 강해요.

비슷한 도구들과 비교하면

Rust 생태계에는 검증 도구가 꽤 있는데 결이 조금씩 달라요. Prusti나 Creusot은 함수에 '사전조건·사후조건'을 명세로 붙여서 논리적으로 증명하는 연역적 검증(deductive verification) 쪽이에요. 좀 더 엄밀하지만 명세를 정성껏 써줘야 하죠. Miri는 Rust 코드를 특수 인터프리터로 돌려서 미정의 동작(UB)을 잡아내는 도구고, Loom은 멀티스레드 코드에서 가능한 실행 순서를 뒤섞어 동시성 버그를 찾아요. cargo-fuzz나 proptest는 앞서 말한 퍼징·속성 기반 테스트고요. Kani의 매력은 '평소 테스트 짜듯 붙였는데, 결과는 수학적 증명'이라는 접근성에 있어요. 형식 검증(formal verification)이라고 하면 학계 냄새 물씬 나서 겁먹기 쉬운데, Kani는 그 문턱을 확 낮춰준 편이거든요.

한국 개발자에게

당장 웹 CRUD 짜는 데 Kani를 붙일 일은 많지 않을 거예요. 하지만 암호화 라이브러리, 임베디드 펌웨어, 블록체인, 결제·금융 로직처럼 '한 번 틀리면 크게 다치는' 코드를 Rust로 짜고 있다면 진지하게 볼 만해요. 특정 함수의 오버플로우나 패닉 가능성을 증명으로 못 박아둘 수 있으니까요. 게다가 이런 도구를 만져보면 '테스트로 버그를 못 찾은 것'과 '버그가 없음을 증명한 것'이 얼마나 다른지 몸으로 느끼게 돼요. 이 감각 자체가 개발자로서 자산이 되고요.

핵심 한 줄: 테스트는 버그의 '존재'를 보여줄 뿐이지만, 모델 체킹은 (정한 범위 안에서) 버그의 '부재'를 증명해줍니다.

여러분은 어떤 코드라면 '테스트만으로는 불안하니 증명까지 받고 싶다'는 생각이 드나요? 실무에서 형식 검증이 필요했던 순간이 있었는지 이야기 나눠봐요.