📚 지식 노트

왜 필요한가

테스트는 고른 입력에서 프로그램이 맞게 동작함을 보인다. 그러나 고르지 않은 입력에 대해서는 아무것도 말하지 않는다. 다익스트라의 말로 널리 알려진 대로, 테스트는 버그가 있음을 보일 수는 있어도 없음을 보일 수는 없다. 모든 입력을 다 해 보면 되지 않느냐고 할 수 있지만, 32비트 정수 인자 둘만 받는 함수도 입력이 2⁶⁴가지다. 초당 10억 번 시험해도 약 585년이 걸린다.

동시성은 더 나쁘다. 스레드나 노드 사이의 실행 순서(인터리빙)는 입력과 별개로 폭발하고, 버그는 그중 드문 순서에서만 나타난다. 테스트를 수천 번 돌려도 안 보이던 경쟁 상태가 운영 환경에서 한 달에 한 번 터진다. 형식 검증은 프로그램이나 설계를 수학적 대상으로 보고, 원하는 성질이 모든 입력과 모든 실행 순서에서 성립함을 기계적으로 확인한다. 테스트를 대신한다기보다, 테스트가 닿지 못하는 곳을 맡는다. 테스트의 종류와 전략은 테스트 노트에 있다.

명세: 전조건·후조건·불변식

"맞다"를 따지려면 무엇이 맞는 것인지부터 적어야 한다. 그것이 명세다. 가장 오래된 틀은 Floyd(1967)의 흐름도 검증을 이어 Hoare가 1969년에 제안한 호어 삼중항 {P} C {Q}이다. "전조건 P가 참인 상태에서 C를 실행해 끝나면, 후조건 Q가 참이다." 이 형태는 끝난다는 것까지는 말하지 않아서 부분 정확성이라 하고, 끝남까지 증명하면 완전 정확성이다.

반복문에는 루프 불변식이 열쇠다. 루프에 들어가기 전에 참이고, 한 바퀴 돌 때마다 참으로 유지되는 식이다. 그러면 루프가 끝났을 때 "불변식 ∧ ¬조건"이 참이고, 이것이 후조건을 함의하면 증명이 끝난다. 아래는 1부터 n까지 더하는 루프에 불변식 s = i(i+1)/2 ∧ i ≤ n을 붙인 것이다. 끝나면 i ≤ n과 ¬(i < n)에서 i = n이 나오고, 불변식에 넣으면 후조건이 된다. 끝남은 n − i가 매번 1씩 줄어드는 0 이상의 정수라는 것으로 보인다.

어려운 부분은 불변식을 찾는 일이다. 후조건을 조금 약하게 만든 꼴이 대개 답이지만, 늘 기계적으로 찾을 수는 없다. 그래서 Dafny·Frama-C 같은 도구는 사람이 불변식을 적게 하고, 나머지 검증 조건을 만들어 아래에 나올 SMT 솔버에 넘긴다.

같은 틀을 증명 대신 실행 중에 검사하는 가벼운 방법이 계약에 의한 설계(design by contract)다. Bertrand Meyer가 Eiffel 언어와 함께 1986년부터 내놓은 생각으로, 메서드마다 전조건·후조건·클래스 불변식을 적고 실행 중에 단언(assertion)으로 확인한다. 계약 하나는 호어 삼중항과 같은 뜻이지만, 증명하는 대신 어기는 순간 그 자리에서 실패하게 만든다. 보통 개발·테스트 때 켜고 배포판에서는 성능 때문에 끈다.

모델 검사: 상태 공간을 모두 훑기

시스템의 상태가 유한하다면 증명 대신 모두 훑어볼 수 있다. 시스템을 상태와 전이로 적고, 처음 상태에서 도달 가능한 모든 상태를 만들어 성질이 깨지는 곳이 있는지 본다. 깨지는 곳이 있으면 거기까지 가는 반례 경로를 내놓는다. 이것이 모델 검사이고, Clarke·Emerson·Sifakis가 이를 세우고 발전시킨 공로로 2007년 튜링상을 함께 받았다.

두 프로세스의 상호 배제를 깃발 두 개로 지키려는 순진한 프로토콜을 보자. 들어가고 싶으면 상대 깃발을 보고, 내려가 있으면 내 깃발을 올리고 임계 구역에 들어간다. 그럴듯하지만 "보기"와 "올리기"가 따로 일어난다. 너비 우선 탐색으로 상태를 훑으면 상태 16개 가운데 둘이 함께 임계 구역에 있는 상태가 나오고, 가장 짧은 경로는 6걸음이다.

먼저 깃발을 올리고 차례 변수를 상대에게 양보하는 피터슨 알고리즘은 같은 검사기로 상태 20개를 모두 훑어도 위반이 없다. 이 결론은 테스트와 다르다. 이 모델 안에서는 어떤 실행 순서에서도 깨지지 않는다는 뜻이다. 현실 CPU는 메모리 쓰기 순서를 바꿀 수 있어 그대로 옮기면 깨지는데, 그 이야기는 운영체제 노트의 동기화 절과 이어진다.

대가는 상태 폭발이다. 프로세스나 변수가 하나 늘 때마다 상태 수가 곱으로 늘어난다. 같은 상태를 한 번만 보는 해시, 대칭인 상태를 하나로 묶기, 순서가 상관없는 전이를 하나만 보기(부분 순서 축약), 상태 집합을 논리식으로 한꺼번에 다루는 기호 모델 검사(BDD·SAT 기반) 같은 기법이 이 폭발과 싸운다. 그래도 실무에서는 "서버 3대, 메시지 2개"처럼 작은 모델을 검사한다. 버그 대부분은 작은 반례를 가진다는 경험에 기댄 것이다.

시간 논리: 안전성과 활성

동시성 시스템의 성질은 "어느 시점에"가 아니라 "실행 내내"에 관한 것이 많다. Pnueli가 1977년 프로그램 검증에 들여온 선형 시간 논리(LTL)는 무한히 이어지는 실행 위에서 참·거짓을 따진다. 연산자 넷이면 대부분을 적는다. G p(언제나 p), F p(언젠가 p), X p(다음 상태에서 p), p U q(q가 될 때까지 계속 p, 그리고 q는 반드시 온다).

• 안전성(safety): "나쁜 일은 결코 일어나지 않는다." G ¬(crit0 ∧ crit1)처럼 적는다. 깨지면 유한한 반례 경로가 있다. 앞 절의 검사가 이것이다.
• 활성(liveness): "좋은 일은 언젠가 일어난다." G(wait0 → F crit0) — 기다리는 프로세스는 언젠가 들어간다. 유한한 접두부만으로는 깨졌다고 말할 수 없다. 반례는 같은 상태를 영원히 되풀이하는 올가미 모양 실행이다.

활성을 검사할 때는 공정성 가정을 함께 적는다. "할 수 있는 걸음은 언젠가 한다"는 가정이 없으면 스케줄러가 한 프로세스만 영원히 돌리는 실행 때문에 거의 모든 활성 성질이 깨진다. 아래 AWS 사례 표에서 활성을 검사하지 않아 활성 버그를 놓친 경우가 나오는데, 안전성만 보는 검사가 흔한 이유는 활성 검사가 그만큼 비싸고 까다롭기 때문이다.

TLA+와 산업 사례

TLA+는 Leslie Lamport가 만든 명세 언어다. 시스템을 "처음 상태(Init)"와 "한 걸음에 상태가 어떻게 바뀔 수 있는가(Next)"라는 두 논리식으로 적고, 불변식과 시간 논리 성질을 함께 적는다. 코드가 아니라 설계를 적는다는 점이 중요하다. 프로토콜이 서버 몇 대, 메시지 몇 개로 어떻게 엇갈릴 수 있는지를 실행 가능한 수준보다 높게 적고, 모델 검사기 TLC가 작은 모델의 상태를 모두 훑는다. 의사 코드에 가까운 문법의 PlusCal로 쓰면 TLA+로 번역해 준다.

가장 많이 인용되는 사례는 AWS다. 2014년 9월 자 보고서 「Use of Formal Methods at Amazon Web Services」(Newcombe 외)에 따르면 AWS 엔지니어들은 2011년부터 형식 명세와 모델 검사를 써 왔고, 보고서 시점에 7개 팀이 TLA+를 쓰고 있었다. 신입부터 수석 엔지니어까지 2~3주 만에 혼자 배워 쓸모 있는 결과를 냈다고 한다. 보고서의 표 일부를 옮기면 다음과 같다.

DynamoDB 쪽에서 찾은 버그 하나는 특정한 장애와 복구 순서가 다른 처리와 엇갈릴 때 데이터를 잃을 수 있는 것이었고, 그것을 보여 주는 가장 짧은 반례가 고수준 걸음으로 35걸음이었다. 이런 겹친 사건은 드물어 보이지만, 큰 규모에서는 드문 일이 실제로 일어난다는 것이 보고서의 요지다. 분산 합의·복제 프로토콜 자체는 분산 시스템 노트에 있다.

SAT·SMT 솔버

많은 검증 문제는 결국 "이 논리식을 참으로 만드는 값이 있는가"로 바뀐다. 변수가 참·거짓뿐이고 식이 절(리터럴의 ∨)들의 ∧인 꼴(CNF)이면 SAT 문제다. SAT는 NP-완전이라 최악에는 지수 시간이 들 수 있지만, 현대 솔버는 실무에서 나오는 변수 수백만 개짜리 식도 자주 푼다.

기본 알고리즘은 Davis·Logemann·Loveland가 1961년에 내놓은 DPLL(Davis·Putnam의 1960년 방법을 다듬은 것)이다. 변수 하나를 정해 보고(결정), 그 결과 미정 리터럴이 하나만 남은 절이 생기면 그 값을 강제로 정하고(단위 전파), 모든 리터럴이 거짓인 절이 생기면(충돌) 마지막 결정을 뒤집는다. 한쪽 부호로만 나오는 변수를 그 부호로 정하는 순수 리터럴 제거도 있지만 아래 예에서는 쓰이지 않는다.

현대 솔버의 바탕인 CDCL(충돌 기반 절 학습)은 충돌이 나면 그 원인을 새 절로 배워 같은 실수를 다시 하지 않고, 원인이 된 결정까지 한 번에 건너뛰어 되돌아간다. SMT 솔버는 여기에 정수·실수 산술, 비트 벡터, 배열, 자료형 같은 이론을 결합한다. SAT 쪽이 불리언 뼈대를 탐색하고, 이론 쪽이 "x > 3 ∧ x < 2는 모순"처럼 그 할당이 말이 되는지 판정한다. 대표가 Microsoft Research의 Z3(MIT 라이선스, 파이썬·C++·Java 등 바인딩)다.

고전적인 예가 이진 탐색의 mid = (lo + hi) / 2다. 수학으로는 늘 lo와 hi 사이지만, 고정 폭 정수에서는 lo + hi가 넘쳐 음수가 된다. 8비트라면 모든 쌍을 직접 확인할 수 있다.

32비트에서는 전수 확인이 불가능하지만, SMT 솔버에는 같은 질문을 그대로 적으면 된다. 솔버는 비트 벡터 산술을 기호로 다뤄 곧바로 반례를 낸다.

from z3 import BitVecs, Solver

lo, hi = BitVecs('lo hi', 32)   # 32비트 부호 있는 정수
mid = (lo + hi) / 2              # 넘칠 수 있는 덧셈

solver = Solver()
solver.add(lo >= 0, hi >= lo, lo > mid)   # mid가 lo보다 작아지는 경우가 있나?
print(solver.check())            # sat — 있다
print(solver.model())            # 그런 lo, hi 한 쌍

심볼릭 실행 도구(KLEE 등), 경계 모델 검사기(CBMC 등), 프로그램 검증기(Dafny 등)가 모두 이렇게 코드에서 식을 만들어 SMT 솔버에 넘긴다. 문제 크기가 커지면 솔버가 끝나지 않을 수 있다는 점이 한계다. SAT가 NP-완전이라는 것의 뜻은 계산 이론 노트에 있다.

정리 증명기: Rocq·Lean·Isabelle

모델 검사와 솔버는 자동이지만 다룰 수 있는 범위가 정해져 있다. 무한히 많은 상태, 임의 크기의 자료 구조, 수학 정리처럼 더 일반적인 성질은 사람이 증명의 뼈대를 짜고 기계가 한 걸음씩 검사하는 대화형 정리 증명기(증명 보조기)로 다룬다. 대표가 셋이다.

• Rocq(옛 이름 Coq): 의존 타입 이론 위에 선 증명 보조기. 증명이 곧 프로그램이고 명제가 곧 타입이다.
• Lean: 같은 계열의 의존 타입 언어이자 증명기로, 일반 프로그래밍 언어로도 쓰인다. 수학 정리를 형식화하는 공동체가 크다.
• Isabelle: 고차 논리(Isabelle/HOL)를 주로 쓰고, 증명을 사람이 읽는 문서처럼 적는 Isar 언어와 강한 자동화를 갖췄다.

Lean 4로 쓴 아주 작은 증명은 이런 모양이다. 자연수 덧셈은 오른쪽 인자에 대한 재귀로 정의돼 있어 n + 0 = n은 계산으로 나오지만 0 + n = n은 귀납법이 필요하다.

-- 모든 자연수 n에 대해 0 + n = n (덧셈은 오른쪽 인자로 정의돼 있어 자명하지 않다)
theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl           -- 0 + 0 = 0은 계산으로 참
  | succ k ih => omega    -- 귀납 가정 ih: 0 + k = k를 써서 선형 산술로 닫는다

굵직한 성과도 있다. Appel과 Haken이 1976년 컴퓨터를 써서 증명한 4색 정리는, 그 컴퓨터 계산을 믿을 수 있느냐는 논란이 이어지다 2005년 Gonthier와 Werner가 Coq 안에서 증명 전체를 형식화했다. CompCert는 ISO C 2011의 거의 전부를 받아 ARM·PowerPC·RISC-V·x86 코드를 만드는 C 컴파일러로, 만든 기계어가 원본 프로그램의 의미대로 동작한다는 기계 검사 증명이 붙어 있다. 컴파일러가 버그를 끼워 넣을 가능성을 증명으로 없앤 것이다. 마이크로커널 seL4는 고수준 명세에서 바이너리 코드까지 이어지는 기계 검사 증명으로 기능 정확성부터 정보 누출 없음까지를 보였고, 증명이 무엇을 가정하는지(어셈블리 코드, 부트 코드, 기계 인터페이스, 하드웨어, DMA)도 공개한다.

타입 시스템이라는 가벼운 형식 검증

가장 널리 쓰이는 형식 검증은 이미 매일 돌고 있다. 타입 검사다. 정적 타입 언어의 컴파일러는 "이 변수에는 문자열만 들어간다", "이 함수는 정수를 돌려준다" 같은 성질을 모든 실행에 대해 증명한 뒤에야 코드를 받아 준다. 덜 정밀하지만 완전히 자동이고 빠르며, 프로그래머가 적는 타입 표기가 곧 명세다.

타입은 갈수록 많은 것을 담는다. 널이 될 수 있는 값을 타입으로 구분하는 언어(Kotlin·Swift)는 널 참조 오류를, Rust의 소유권·빌림 검사는 데이터 경쟁과 해제 후 사용을 컴파일 시간에 막는다. 다른 상태의 값을 서로 다른 타입으로 두어 "검증 안 된 입력"을 "검증된 입력" 자리에 못 넣게 하는 설계도 같은 생각이다. 끝까지 가면 값에 기댄 타입(의존 타입)이 되는데, 그것이 위 정리 증명기들이다. 타입 검사와 추론이 컴파일러 안에서 어떻게 도는지는 컴파일러 노트에 있다.

추상 해석과 정적 분석

실행하지 않고 코드만 보고 성질을 따지는 것이 정적 분석이다. 그 이론적 바탕이 Cousot 부부가 1977년 POPL에서 내놓은 추상 해석이다. 실제 값 대신 값들의 요약(부호, 구간, 짝홀 같은 추상 도메인) 위에서 프로그램을 "실행"한다. 요약은 실제 값을 빠짐없이 덮도록(과대 근사) 잡으므로, 요약에서 오류가 안 보이면 실제로도 없다.

루프가 문제다. 요약을 한 바퀴씩 넓혀 가면 x = 0; while (x < 100) x++;에서 구간이 [0, 0], [0, 1], [0, 2] … 로 100번 넘게 반복해야 멈춘다. 반복 횟수가 정해지지 않은 루프라면 영영 안 멈춘다. 그래서 몇 번 돌린 뒤에도 커지는 끝은 무한대로 확 넓혀 버리고(확대, widening), 멈춘 뒤에 루프 조건으로 다시 좁힌다(축소, narrowing).

이런 분석이 늘 정확할 수는 없다. 라이스 정리에 따르면 프로그램의 의미에 관한 자명하지 않은 성질은 모두 결정 불가능하다. 즉 모든 프로그램에 대해 놓침도 오경보도 없이 끝나는 분석기는 만들 수 없다. 그 근거인 정지 문제와 결정 불가능성은 계산 이론 노트에 있다. 그래서 도구는 어느 쪽을 희생할지 고른다.

건전한 쪽의 대표가 Astrée다. C 프로그램에 런타임 오류(0으로 나누기, 배열 범위 밖 접근, 산술 오버플로 등)가 없음을 증명하는 것을 목표로 하며, 2003년 11월 에어버스 A340 플라이 바이 와이어 시스템의 주 비행 제어 소프트웨어(C 13만 2천 줄)에 런타임 오류가 없음을 증명했다. 2004년부터는 A380의 전기식 비행 제어 코드로 넓혔다. 반대쪽에는 Meta의 Infer처럼 코드 리뷰 단계에서 널 역참조·자원 누수 같은 버그를 빨리 찾아 주는 도구들이 있다. 개발자가 오경보에 지쳐 경보를 무시하기 시작하면 도구가 쓸모없어지므로, 이런 도구는 정밀도를 더 중시한다.

비용과 한계, 어디에 쓰나

형식 검증이 "버그 없음"을 보장한다는 말은 늘 단서를 단다. 증명되는 것은 명세와 구현 사이의 관계다. 명세가 원하는 것을 잘못 적었으면 증명은 틀린 것을 정확히 지킨다. 또 증명은 그 아래 층을 가정한다. 컴파일러, 운영체제, 하드웨어가 맞다는 가정이다. seL4가 가정 목록을 공개하고 CompCert가 컴파일러 층을 메우는 것도 이 틈을 줄이려는 일이다.

• 비용: 정리 증명은 코드보다 증명이 몇 배 길어지기 쉽고, 코드를 바꾸면 증명도 고쳐야 한다. 모델 검사는 자동이지만 모델을 작게 만드는 기술이 필요하다.
• 규모: 상태 폭발과 솔버 시간 초과 때문에 시스템 전체보다 핵심 프로토콜이나 핵심 모듈을 골라 검증한다.
• 사람: 명세를 쓰는 능력은 따로 배워야 한다. AWS 보고서는 엔지니어들이 2~3주 만에 익혔다고 하지만, 무엇을 명세할지 고르는 감각은 경험에서 온다.

테스트와 증명 사이에는 속성 기반 테스트(property-based testing)가 있다. 입력 예를 손으로 고르는 대신 "정렬한 결과는 입력과 길이가 같고 오름차순이다"처럼 모든 입력에서 성립해야 할 성질을 적으면, 도구가 무작위 입력을 만들어 그 성질을 깨 보려 하고, 깨는 입력을 찾으면 군더더기를 덜어 작은 반례로 줄여 보여 준다. 1999년 Claessen과 Hughes가 Haskell로 만든 QuickCheck이 시작이고, 파이썬에는 Hypothesis가 있다. 증명은 아니지만 "무엇이 맞는가"를 명세로 적는 습관을 테스트 비용으로 들일 수 있어, 형식 검증으로 가는 첫걸음으로 좋다.

그래서 어디에 쓸지는 "버그 하나의 값"으로 정한다. 비행 제어·철도·의료 기기처럼 버그가 사람을 다치게 하는 곳, 운영체제 커널·컴파일러·암호 라이브러리처럼 그 위의 모든 것이 기대는 곳, 분산 합의·복제처럼 테스트로는 드문 순서를 재현하기 어려운 곳, 하드웨어 설계처럼 한 번 만들면 고칠 수 없는 곳이 대표다. 그 밖의 대부분은 타입 검사와 정적 분석으로 넓게 깔고, 위험한 설계 몇 개만 TLA+나 모델 검사로 확인하는 조합이 가장 흔하다.

핵심 자료

결정 불가능성과 복잡도 이론은 계산 이론 노트, 테스트 전략은 테스트 노트, 형식 검증을 많이 쓰는 분산 프로토콜은 분산 시스템 노트에 있다.