2026년 6월 25일, Ubuntu 팀의 기술 블로그에 글이 하나 조용히 올라왔다. 제목 속에는 모순처럼 보이는 두 가지 사실이 숨어 있었다. SQLite — 지구상에서 가장 널리 사용되는 데이터베이스 — 에서 버그 하나가 발견됐다는 것. 그리고 그 버그는 2010년부터 코드 속에 잠들어 있었다는 것.
다시 말해, 16년을 숨어 있었다.
16년이란 어떤 시간인가. 2010년은 iPhone 4가 막 출시되고, 위챗은 아직 탄생하기도 전이며, 사람들이 피처폰 자판으로 문자를 보내던 시절이다. 바로 그해에, 이 버그는 코드 한 줄과 함께 SQLite에 기록되었고, 그 후로 조용히 모든 스마트폰, 모든 브라우저, 모든 운영체제 속에 자리 잡았다. 수억 대의 기기, 16년의 시간 — 그 누구도 이 버그를 발견한 적이 없었다.
결국, 그것을 찾아낸 것은 인간이 아니라 수학 문제 하나였다.
그림: Ubuntu 팀이 TLA+로 SQLite WAL의 체크포인트 동작을 모델링했다. 이 모델은 단 20스텝 만에 16년 묵은 취약점을 재현해 냈다. 출처: ubuntu.com
먼저 분명히 하자: SQLite가 무엇이고, 왜 당신의 전화기 속에 들어 있는가
필자부터 한 가지 전제를 설명하려 한다. SQLite는 ‘앱’이 아니다 — 당신의 전화기에서 ‘SQLite’라는 아이콘은 어디에도 없다. 이것은 ‘데이터베이스 엔진’으로, 전화기, 컴퓨터, 브라우저 안에서 데이터를 저장하고 관리하는 역할을 전담한다.
예를 들어 보자. 당신의 위챗 채팅 기록, 전화번호부 연락처, 브라우저에 저장된 비밀번호, 알리페이·타오바오·틱톡을 사용하며 생성되는 각종 로컬 데이터 — 이 모든 것의 배후에는 거의 예외 없이 SQLite가 묵묵히 작동하고 있다. 전 세계에서 설치 대수가 가장 많은 데이터베이스, 단연 SQLite다. 추산에 따르면, 전 세계에서 1조 개 이상의 SQLite 데이터베이스가 실행 중이다.
그리고 이런 ‘기초 인프라’급 소프트웨어에 버그 하나가 16년이나 숨어 있었다. 이 사실 자체만으로 등골이 서늘해진다.
하지만 이 이야기가 진짜 빛나는 지점은 여기가 아니다. 이 버그가 어떻게 발견됐는가 하는 점이다.
인간의 손으로는 영원히 찾을 수 없었을 문제
먼저 버그 자체를 들여다보자. SQLite에는 WAL(Write-Ahead Log, 쓰기 전 로그)이라는 작동 모드가 있다. 쉽게 말하면, 여러 프로그램이 동시에 데이터베이스를 읽고 쓸 때 WAL은 ‘버퍼 노트’ 역할을 한다. 쓰기 작업은 먼저 버퍼 노트에 기록되고, 읽기 작업은 당분간 영향을 받지 않는다. 쓰기가 끝나면 한꺼번에 정식 장부로 옮긴다. 이 옮기는 과정을 ‘체크포인트(checkpoint)‘라고 부른다.
버그는 이 ‘옮기는’ 동작과 ‘쓰는’ 동작이 동시에 발생할 때 생긴다. 일상의 비유로 표현하자면:
당신과 동료가 동시에 하나의 엑셀 파일을 조작하고 있다고 상상해 보라. 동료는 ‘초안 영역’에 계속 새 데이터를 추가하고 있고, 당신은 초안 영역에서 이미 확정된 내용을 정식 파일로 옮기는 역할이다. 당신이 초안 영역을 힐끗 보니 옮겨야 할 레코드가 100개다. 그래서 50개를 옮겼다 — 바로 그 순간 동료가 새 레코드 5개를 추가하면서 초안 영역의 카운터를 ‘리셋’했다. 당신은 나머지 50개를 계속 옮기는데, 카운터가 리셋됐기 때문에 실제로는 예전 번호만 옮겼을 뿐, 진짜로 옮겼어야 할 데이터 몇 개를 빠뜨린다.
결과는: 정식 파일에 레코드 몇 개가 누락된다. 데이터가 사라진 것이다.
이것이 SQLite 공식 문서에 기술된 버그다. WAL 체크포인트 과정에서의 ‘경쟁 상태(race condition)’ — 두 개의 작업이 정확한 순서로 조율되지 못하고, 극도로 정밀한 타이밍 윈도 안에서 충돌한 것이다.
핵심은 바로 ‘극도로 정밀한’이라는 표현이다. 이 버그를 발동시키려면 까다로운 조건이 연쇄적으로 충족되어야 한다. 쓰기 작업과 체크포인트 작업이 반드시 동시에 발생해야 하고, 체크포인트가 WAL 크기를 읽어들인 후 실제로 옮기기 시작하기 전의 그 찰나 — 불과 몇 마이크로초에 불과한 순간 — 에 다른 쓰기 작업이 정확히 완료되어 WAL을 리셋해야 한다.
인간이 테스트 케이스를 작성해서 버그를 찾는 방식은, 본질적으로 ‘추측’이다 — 어디가 잘못될지 짐작하고 그 지점을 반복해서 시도하는 것. 하지만 이 버그의 발동 윈도는 ‘추측조차 할 수 없을’ 만큼 좁다. 아무리 많은 테스터를 동원하고, 아무리 많은 자동화 테스트 스크립트를 작성해도, 모든 작업 순서의 조합을 커버할 수는 없다 — 가능한 조합의 수는 천문학적 숫자이기 때문이다.
이것이 이 버그가 수억 대의 기기 속에서 16년 동안 평화롭게 잠들어 있을 수 있었던 이유다.
TLA+란 무엇인가: 테스트 도구가 아니라, 수학적 증명이다
Ubuntu 팀이 이 버그를 어떻게 찾아냈는지 이해하려면, 먼저 형식 검증(formal verification)이라는 개념을 이해해야 한다.
필자는 가장 간단한 비유로 말해 보겠다. 기존의 테스트가 ‘표본 검사’라면 — 쌀 한 자루에서 무작위로 몇 줌 집어 모래가 섞였는지 확인하는 것 — 형식 검증은 ‘수학적 증명’이다 — 논리적 추론만으로 “이 자루에 모래가 섞여 있는가”를 도출해 내며, 한 줌 한 줌 뒤질 필요가 없다.
TLA+는 바로 이 형식 검증 도구 중 하나다. 정식 명칭은 Temporal Logic of Actions. 컴퓨터 과학계의 전설적 인물 레슬리 램포트(Leslie Lamport)가 발명했다 — 이 노학자는 LaTeX(학술 논문 조판 시스템)의 창시자이기도 하고, Paxos 합의 알고리즘(오늘날 거의 모든 분산 시스템의 기초)을 설계한 사람이기도 하다.
TLA+가 하는 일을 설명하자면 간단하다. 검증하고 싶은 소프트웨어의 동작을 수학적 모델로 추상화하는 것이다 — 코드를 쓸 필요는 없고, 수학 언어로 “이것이 다양한 상황에서 어떻게 변화해야 하는지”를 기술하기만 하면 된다. 그러면 TLA+의 모델 체커가 모든 가능한 상태 조합을 전수 탐색하며, 당신이 정의한 규칙이 항상 성립하는지를 검증한다.
Ubuntu 팀의 말을 빌리자면, 그들이 TLA+로 SQLite WAL의 동작 모델을 구축한 후, 모델 체커는 “단 20스텝 만에 반례를 찾아냈다”고 한다. 20스텝. 16년 대 20스텝.
그림: TLA+ 모델의 정적 버전. 쓰기 작업과 체크포인트 작업 사이의 경쟁 상태가 어떻게 데이터 손실을 초래하는지 보여 준다. 출처: ubuntu.com
왜 인간의 육안 테스트는 이 싸움을 절대 이길 수 없는가
여기에는 한 층 더 깊이 파고들 만한 논점이 있다. 수학적 방법은 어떻게 16년 동안 아무도 발견하지 못한 버그를 찾아낼 수 있었을까? 수학적 방법이 가능했던 근원은, 방법론의 본질적 차이에 있다.
인간의 테스트 방식은 — 수동으로 이리저리 눌러 보든, 자동화 스크립트를 짜든 — 본질적으로 ‘열거형’이다. 문제가 될 만한 시나리오 몇 가지를 추려내서, 각 시나리오마다 검증을 수행한다. 문제는, 소프트웨어 시스템의 상태 공간이 조합 폭발을 일으킨다는 점이다. 100개의 작업 단계로 이루어진 시스템에서 가능한 상태 순서 배열은 100의 팩토리얼(계승)이다 — 이 숫자는 우주의 원자 수보다도 크다. 절대 전수 조사할 수 없다.
반면 TLA+ 같은 형식 검증 도구는, 이론적으로는 ‘상태 폭발’ 문제에 직면하지만, 인간이 절대 하지 못하는 일을 한 가지 해낸다. 즉, “내가 정의한 모든 경우에 문제가 발생할 수 있는가?”를 검사한다는 점이다.
이 문장은 두 번 곱씹을 가치가 있다.
인간의 테스트가 답하는 질문은: “어떤 문제를 내가 봤나?” 형식 검증이 답하는 질문은: “문제가 발생할 가능성이 있는가?”
전자는 수동적이고, 상상력에 의존하며, 빠뜨리기 쉽다. 후자는 능동적이고, 전수 탐색적이며, 계산된 어떤 상태도 빠뜨리지 않는다.
Ubuntu의 엔지니어가 SQLite 개발자보다 더 똑똑했던 것이 아니다 — SQLite 개발팀은 극도로 높은 코드 품질로 정평이 나 있으며, 그들의 테스트 스위트 커버리지는 업계 최고 수준이다. 도구가 달랐을 뿐이다. 자와 현미경이 보는 세계는 같은 차원이 아니다.
경쟁자는 왜 영향받지 않았나: 뜻밖의 발견
이 이야기에는 흥미로운 번외편도 있다. Ubuntu 팀이 애초에 이 검증에 착수한 이유는, 그들이 Dqlite라는 프로젝트를 직접 유지·관리하고 있기 때문이다 — Dqlite는 SQLite 기반의 분산 데이터베이스다. 그들은 궁금했다. SQLite의 이 버그가 Dqlite에도 영향을 미칠까?
그래서 그들은 Dqlite의 TLA+ 모델도 하나 더 구축했다. 결과는: Dqlite는 영향받지 않는다.
이유는 단순했다. Dqlite의 설계가 SQLite보다 더 ‘보수적’이었기 때문이다. Dqlite는 체크포인트를 수행할 때 전체 쓰기 작업에 락을 걸어, ‘옮기기’와 ‘쓰기’가 동시에 발생하지 않게 한다. 이 방식이 성능을 약간 희생하기는 하지만, 우연히도 바로 이 경쟁 상태를 완전히 회피했다.
Dqlite의 설계가 반드시 더 낫다고 말할 수는 없다. 하지만 당신이 무심코 내린 보수적인 선택 하나가 16년 후에 갑자기 옳았다고 증명될 수도 있다는 것이다. 소프트웨어 공학의 인과 사슬은 이토록 묘하다.
SQLite의 수정: 고작 코드 한 줄
2026년 3월 5일, SQLite 측이 공식적으로 버그 수정을 발표했다. 수정은 지극히 단순했다. 체크포인트 과정 중에 WAL이 리셋되지 않았는지 확인하는 검사를 하나 더 추가한 것이다. 리셋된 것이 확인되면, 처음부터 다시 시작한다.
다시 말해, 16년 묶은 골칫거리가 코드 한 줄로 해결됐다.
하지만 코드 자체가 단순하다고 해서 문제가 단순한 것은 아니다 — 그 한 줄을 어디에 넣어야 하는지, 어떤 조건을 검사해야 하는지 찾아내는 과정은 너무나 어려웠다. 너무 어려워서, SQLite의 그 세계에서 가장 데이터베이스를 잘 아는 엔지니어들조차 16년 동안 발견하지 못했을 정도였다.
이것이 의미하는 것: 변화하고 있는 하나의 흐름
필자가 말하고 싶은 것은 두 가지다.
첫째, SQLite 사례는 고립된 예외가 아니다. Amazon, Microsoft, Oracle 등은 이미 핵심 인프라에 TLA+를 활용한 형식 검증을 도입하고 있다 — AWS의 S3, DynamoDB 같은 핵심 서비스는 설계 초기 단계에서부터 TLA+ 모델 체킹을 거쳤다. 다만 이런 사례들은 대부분 기업 내부의 폐쇄적 시스템에서 일어난 일이라 일반인에게는 보이지 않았을 뿐이다. 반면 SQLite는 어디에나 존재하는 오픈소스 프로젝트이고, 그것의 버그가 형식 검증으로 발견됐다는 사실은 대중적 가시성을 지닌 상징적 사건이다.
둘째, 형식 검증의 ‘진입 장벽’이 낮아지고 있다. TLA+는 평범한 사람들을 위한 도구가 아니다 — 수학적 사고와 시스템 모델링 능력이 필요하다. 하지만 20년 전만 해도 “자동화 테스트는 모두가 해야 하는 일”이라고 생각하는 사람은 아무도 없었지만 지금은 업계 표준이 된 것처럼, 형식 검증도 ‘고수 전용’에서 ‘팀의 기본 장비’로 진화하는 중이다. 이번에 Ubuntu 팀이 TLA+로 발견한 것은 업계에서 가장 성숙하고 가장 광범위하게 사용되는 데이터베이스의 버그다 — 이 사실 자체가 모든 이에게 말해 주고 있다. 당신이 신뢰하는 그 기반 소프트웨어들도, 만든 사람조차 몰랐던 문제를 품고 있을 수 있다. 그리고 수학만이, 그 문제들을 찾아내는 유일하게 신뢰할 수 있는 경로다.
16년 전, 사람들은 직감과 근면으로 소프트웨어를 테스트했다. 16년 후, 수학 문제 하나가 20걸음 만에 인간의 눈으로는 영원히 볼 수 없었던 버그를 찾아냈다.
도구가 진화한 것이다.
참고 링크: