Turso 강화: Formal Methods와 Quint를 이용한 SQLite 버그 찾기

데이터베이스를 구축하는 모든 팀에게 SQLite는 신뢰성의 금본위입니다. Turso는 SQLite를 재작성한 것이기 때문에, 동일한 수준의 신뢰를 유지하는 것은 목표가 아니라 필수입니다.

이를 달성하기 위해 Turso는 Deterministic Simulation Testing (DST), 차등 테스트 도구, 퍼저, 그리고 동시성 시뮬레이터를 포함한 엄격한 테스트 스택을 사용합니다.

이러한 포괄적인 접근에도 불구하고, 팀은 전략에 격차가 있음을 인식했습니다: 형식 방법(formal methods). 전통적으로 접근하기 어렵거나 지나치게 복잡하다고 여겨졌지만, 형식 방법은 전통적인 테스트가 제공하지 못하는 수학적 확실성을 제공합니다. 최신 형식 검증 도구인 Quint를 통합함으로써 Turso는 강화 과정을 한 단계 더 진행할 수 있었으며, 결국 SQLite 자체에서 10개 이상의 버그를 발견했습니다.

형식 방법의 도전 과제

TLA+와 같은 형식 방법은 시스템 정확성을 검증하는 업계 표준입니다. 그러나 이들은 진입 장벽이 높고 “감시자를 누가 감시하느냐”라는 문제, 즉 시스템 모델 자체가 실제로 올바른지 검증하기 어려운 점이 있습니다.

이를 극복하기 위해 Turso는 커뮤니티 멤버 Pavan Nambi와 협력하여 Quint를 활용했습니다. Quint는 Temporal Logic of Actions (TLA)의 이론적 기반을 현대적인 타입 검사와 개발 도구와 결합하여 엔지니어가 더 쉽게 접근할 수 있게 합니다.

전체 SQLite 시스템을 모델링하는 불가능한 작업에 도전하기보다는, 팀은 C API에 집중했습니다. C API는 문서화가 잘 되어 있고 대부분의 SQLite 드라이버가 사용하는 주요 인터페이스이므로, 이를 모델링하면 높은 커버리지를 얻을 수 있습니다. 이 접근법을 통해 팀은 API 사양을 진실의 근원으로 사용하여 모델과 실제 구현을 모두 검증할 수 있었습니다.

“Quinting” 프로세스

버그를 찾는 방법론은 반복적인 네 단계 사이클이었습니다:

  1. Model the Contract: 문서화된 SQLite C API 계약을 식별하고, 필요한 상태와 속성을 Quint로 모델링합니다.
  2. Generate Traces: Quint를 사용해 계약을 위반할 가능성이 있는 상태 시퀀스(트레이스)를 생성합니다.
  3. Execute: 이러한 트레이스를 작은 C 프로그램으로 변환하고 SQLite에 실행합니다.
  4. Compare: 시스템에서 관찰된 동작을 문서화된 결과와 비교합니다.

모델 체커가 실패를 식별하면, 위반으로 이어지는 특정 상태 시퀀스인 반례(counter-example)를 생성합니다. 이러한 반례 중 다수는 모델이 올바름을 검증했지만, 일부는 시스템이 자체 사양에서 벗어나고 있음을 밝혀냈습니다.

사례 연구: sqlite3_deserialize()

sqlite3_deserialize() 함수는 직렬화된 데이터베이스 이미지를 메모리 내 데이터베이스로 연결에 로드할 수 있게 하는 대표적인 예시였습니다.

사양에 따르면, 대상 데이터베이스가 현재 읽기 트랜잭션 중이거나 백업 작업에 관여하고 있을 경우 sqlite3_deserialize()는 SQLITE_BUSY를 반환해야 합니다. Quint 모델은 다음과 같은 순서의 트레이스를 생성했습니다:

  1. 데이터베이스 열기 → 테이블 생성 → 데이터베이스 직렬화.
  2. 데이터베이스에서 읽기 시작.
  3. 읽기 트랜잭션이 활성화된 상태에서 sqlite3_deserialize() 호출.

예상은 SQLITE_BUSY 반환 코드였지만 실제 결과는 시스템 크래시였습니다. 크래시는 거의 의도된 동작이 아니므로, 이는 버그가 모델이 아니라 구현에 있음을 즉시 확인시켜 주었습니다. 이 문제는 이후 SQLite 소스에서 수정되었습니다.

결과 및 발견

Quint를 활용한 탐색은 매우 생산적이었으며, 최적화 논리 오류부터 치명적인 크래시까지 다양한 버그를 발견했습니다. 주요 발견 사항은 다음과 같습니다:

  • Optimization Failures: EXISTS-to-join 최적화가 LIMIT/OFFSET을 잘못 적용하거나 외부 상관관계를 잃어 유효한 행을 필터링하는 문제.
  • Constraint Violations: 인용된 제약 조건 이름이 삭제 불가능해지거나 xfer 최적화가 체크 제약을 우회해 일관성 없는 데이터베이스를 초래하는 버그.
  • Stability Issues: 내부 테이블에 대한 ALTER ADD CHECK 수행 중 발생하는 크래시 또는 sqlite3changegroup_change_finish()에서 NULL pzErr로 인한 크래시.
  • Memory and Alignment: sqlite3_mutex 128바이트 정렬과 관련된 정의되지 않은 동작.

결론

SQLite는 존재하는 소프트웨어 중 가장 철저히 테스트된 사례 중 하나입니다. 그러나 Quint를 통한 형식 방법을 적용함으로써 Turso는 수십 년간 전통적인 테스트를 피한 버그들을 찾아낼 수 있었습니다.

형식 트레이스를 실행 가능한 C 프로그램으로 변환함으로써 Turso는 자체 구현을 강화했을 뿐만 아니라 광범위한 SQLite 생태계의 안정성에도 크게 기여했습니다. 이는 C API와 같이 구체적이고 명확히 정의된 인터페이스에 형식 방법을 적용하면 현대 소프트웨어 신뢰성을 위한 강력한 도구가 된다는 것을 보여줍니다.

Sources