시간 논리를 배우지 않고도 코드를 model checking할 수 있다

model checker을 사용하는 데 LTL이 필요 없다

model checker을 사용하기 위해 선형 시간 논리를 배울 필요는 없다. Kani, CBMC, Alloy 같은 도구는 일반적인 어서션과 관계 제약으로 속성을 검증할 수 있게 한다. 활성 속성을 증명하는 능력을 포기하는 대신, 학습 곡선은 주 대신 시간 단위로 측정되며, 대부분의 소프트웨어 버그에 대해 그것은 가치 있는 거래다.

시간 논리는 대부분의 model checker이 요구하는 문지기다

고전적인 model checker인 SPIN과 NuSMV는 속성을 LTL이나 CTL로 표현하도록 요구한다. G(request -> F(response))처럼 써서 “전역적으로, 모든 요청은 결국 응답을 따른다”는 의미를 표현한다. 이것은 강력하다. 프로토콜이 deadlock에 빠지지 않는다는 것, 모든 메시지가 결국 승인된다는 것, 시스템이 공정하다는 것을 증명할 수 있다.

또한 이것은 대부분의 현업 개발자가 갖고 있지 않은 전문 기술이다. LTL 공식을 읽는 것은 코드를 읽는 것과 다르다. 연산자는 모달이고, 의미론은 무한 추적 위에서 정의되며, 단위 테스트를 작성하며 쌓은 직관은 옮겨지지 않는다. 그러므로 질문은 정당하다: model checking의 버그 발견 능력을 원한다면, 정말로 먼저 그 산을 오를 필요가 있는가?

아니다. 다른 종류의 도구는 수십 년 동안 존재해 왔으며, 이미 쓰고 있는 동일한 어서션으로 코드를 검증한다.

경계 model checker은 어서션을 SAT 문제로 변환한다

경계 model checker은 새로운 논리를 배우라고 요구하지 않는다. 테스트 하네스를 작성하라고 요구한다. 비결정적 입력을 선언하고, 가정으로 제약하며, 호스트 언어로 속성을 단언한다. 도구는 루프를 경계까지 펼치고, 프로그램을 SAT 또는 SMT 공식으로 인코딩한 뒤, 솔버에 반례를 찾도록 요청한다.

솔버가 UNSAT를 반환하면, 해당 경계 내의 모든 경로에서 속성이 성립한다. 반례를 찾으면 어떤 입력이 버그를 유발하는지 정확히 보여주는 구체적인 추적을 얻는다. 시간 연산자 없음. 무한 추적 없음. 재현 가능한 입력 벡터를 가진 실패한 어서션뿐이다.

Kani는 Rust를 위한 가장 접근하기 쉬운 경계 model checker다. cargo install kani-verifier로 설치하고 일반 Rust 코드에서 동작한다.

실제 예시: Rust에서 state machine 검사

여기 버그가 있는 state machine이 있다. 단순한 카운터를 추적하며, 각 틱마다 감소하다가 0에 도달하면 유휴 상태로 전환한다.

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

버그는 미묘하다. stop을 보라. 상태를 Stopped로 설정하지만 count는 변경하지 않는다. 나중에 무언가가 state == State::Stopped일 때 count == 0이라고 가정하면 그 가정은 틀리다.

이를 포착하는 Kani 증명 하네스는 다음과 같다:

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani는 모든 경로를 탐색한다. initial == 2이면 start 후 기계는 count == 2로 Running 상태다. 한 번의 tick은 count를 1로 감소시키지만 상태는 Running을 유지한다. 그런 다음 stop은 상태를 Stopped로, count는 1인 채로 설정한다. 어서션이 실패한다. Kani는 이 정확한 추적을 보고한다.

이것이 시간 논리 없는 model checking 경험이다. Rust를 쓴다. Rust로 어서션을 쓴다. 도구가 어떤 입력이 이를 깨는지 알려준다.

Alloy는 관계 논리로 설계 수준의 버그를 찾는다

경계 model checker은 코드를 검증한다. Alloy는 설계를 검증한다.

Alloy는 전통적인 model checker이 아닌 모델 탐색기지만, 그 차이는 워크플로우만큼 중요하지 않다. 시스템을 관계의 집합으로 기술하고, 상태 불변식을 1차 논리 제약으로 표현한 뒤, Alloy에 반례를 찾도록 요청한다. 사용자 정의 범위까지 모든 가능한 인스턴스를 검색하고 실패 다이어그램을 보여준다.

다음은 단순한 방향 그래프 속성에 대한 Alloy 모델이다:

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

이 어서션은 도달 가능성이 대칭이라고 주장한다. Alloy는 최대 3개 노드를 가진 모든 그래프에서 이를 검사하고 즉시 반례를 그린다: n1이 n2를 가리키지만 n2에는 나가는 변이 없는 그래프. G, F, U 연산자는 어디에도 나타나지 않는다.

포기하는 것: 활성과 무한 동작

이 편의에는 대가가 있다. 경계 model checker은 루프 경계나 추적 길이까지만 동작을 검증한다. 요청이 결국 응답된다는 것을 증명할 수 없고, 처음 N 단계 내에 나쁜 일이 일어나지 않는다는 것만 증명할 수 있다. Alloy도 자신의 범위 내 인스턴스만 검사한다. 임의로 큰 시스템의 속성을 증명할 수 없고, 경계 아래에 반례가 존재하지 않는다는 것만 보여줄 수 있다.

합의 프로토콜이 커밋된 쓰기를 잃지 않는다는 것, 또는 모든 메시지가 결전달된다는 것을 증명해야 한다면, 여전히 시간 논리와 비경계 model checking이 필요하다. TLA+ 같은 도구는 시간 논리를 수학처럼 보이는 구문으로 포장하지만, 근본 의미론은 여전히 시간적이다.

데이터 구조 불변식, API 계약 강제, 47번째 실행 경로에서만 발동하는 race condition을 찾는 데는 경계 도구로 보통 충분하다. 단위 테스트가 놓치는 버그를 잡고, 교과서 없이 읽을 수 있는 어서션으로 이를 수행한다.

5분 만에 Kani 시작하기

Rust가 설치되어 있다면 경계 model checking은 명령어 하나 거리다.

cargo install kani-verifier
cargo kani setup

새 크레이트를 만들고, 미묘한 버그가 있는 함수를 작성한 뒤, #[kani::proof] 하네스를 추가한다. cargo kani를 실행한다. Kani가 반례를 찾으면 실패를 유발하는 구체적인 입력을 출력한다. VERIFICATION SUCCESSFUL을 보고하면 기본 경계 내의 모든 경로에서 속성이 성립한다.

상태 공간이 작고 불변식이 명확한 함수부터 시작하라. state machine, 파서 검증, 프로토콜 상태 전환은 이상적인 첫 번째 대상이다. 처음부터 전체 HTTP 서버를 검증하려 하지 마라. SAT 솔버에도 한계가 있고, 당신의 인내도 마찬가지다.

FAQ: 경계 대 비경계, 활성, 어디서 시작할까

경계 model checking은 정말 model checking인가?

기술적으로, 이것은 상태 그래프를 명시적으로 탐색하는 대신 문제를 충족성 쿼리로 인코딩하는 변종이다. 버그를 찾으려는 개발자에게 그 차이는 학문적이다. 모든 경로를 체계적으로 탐색하는데, 이것이 실제로 model checking의 의미다.

Kani나 CBMC으로 활성을 증명할 수 있나?

직접적으로는 아니다. 활성 속성은 무한 동작에 대한 추론을 필요로 하며, 경계 도구는 명시적으로 탐색을 제한한다. 고정점에 도달할 만큼 충분한 단계를 펼쳐 경계 활성 검사를 인코딩할 수도 있지만, 그것은 고급 기법이다.

TLA+는 어떤가? 시간 논리가 필요한가?

TLA+는 Temporal Logic of Actions를 사용하므로, 기술적으로는 그렇다. 하지만 Leslie Lamport는 구문을 일반 수학처럼 읽히도록 설계했다. 대부분의 TLA+ 명세는 텍스트의 90%를 상태 불변식과 데이터 구조 제약에 쓰며, 시간 연산자에는 쓰지 않는다. 비경계 시간 추론이 필요하다면 가장 접근하기 쉬운 경로다.

Alloy와 Kani 중 무엇을 써야 하나?

Rust 코드가 있고 구현 세부 사항을 검증하고 싶다면 Kani를 써라. 아직 시스템을 설계 중이고 코드를 쓰기 전에 불변식이 가능한지 탐색하고 싶다면 Alloy를 써라.

야망이 아닌 문제에 맞는 도구를 선택하라

시간 논리는 아름답고 강력하지만, 형식 검증의 전제 조건은 아니다. 경계 model checker과 관계 모델 탐색기는 이미 아는 언어로 속성을 표현할 수 있게 한다. 시스템이 결국 종료됨을 증명하지는 않겠지만, 데이터베이스 state machine을 손상시키는 1 오차를 찾을 것이다. 대부분의 팀에게 그것이 중요한 버그다.

단일 상태 함수에서 Kani로 시작하라. 하나의 어서션을 써라. 솔버가 놓친 것을 알려주도록 하라.