Turso, Quint로 SQLite 버그 10개 이상 찾아내다!
Turso는 SQLite의 신뢰성 확보를 위해 다양한 테스트 기법을 활용하며, 특히 형식 검증(Formal Verification)에 주목함
Quint를 사용하여 SQLite C API를 모델링하고, 자동 생성된 테스트 케이스(Test Cases)를 통해 버그를 발견함
sqlite3_deserialize() 함수의 SQLITE_BUSY 반환 오류 등, 10개 이상의 SQLite 버그를 찾아내고 수정함
커뮤니티에서는 SQLite의 견고한 테스트(Robust Testing)에도 불구하고, 형식 검증을 통해 새로운 취약점을 발견한 점에 주목함
형식 검증(Formal Verification) 도입의 중요성
Turso는 SQLite의 신뢰성을 높이기 위해 형식 검증(Formal Verification)을 적극적으로 도입했다. 기존의 테스트 기법으로는 발견하기 어려웠던 버그들을 Quint를 통해 찾아내면서, 테스트 커버리지(Test Coverage)를 획기적으로 개선했다. 이는 데이터베이스 시스템의 안정성(Stability)을 확보하는 데 중요한 역할을 한다.
Quint를 활용한 SQLite C API 모델링
Turso는 SQLite의 C API를 Quint로 모델링하여, API의 정확성(Accuracy)을 검증했다. Quint는 TLA+를 기반으로 하는 형식 검증 도구로, API의 상태(State)와 속성(Property)을 정의하고, 자동으로 테스트 케이스(Test Cases)를 생성한다. 이를 통해 SQLite의 예상치 못한 동작(Unexpected Behavior)을 찾아낼 수 있었다.
sqlite3_deserialize() 함수의 SQLITE_BUSY 오류
Quint를 사용한 결과, sqlite3_deserialize() 함수가 특정 상황에서 SQLITE_BUSY를 반환하지 않고 크래시(Crash)되는 버그를 발견했다. 이는 데이터베이스의 일관성(Database Consistency)을 해치는 심각한 문제로, Turso는 이 버그를 SQLite 팀에 보고하고 수정했다. 이처럼 형식 검증은 잠재적인 취약점(Potential Vulnerabilities)을 조기에 발견하는 데 기여한다.
SQLite 버그 발견 및 수정 과정
Turso는 Quint를 통해 SQLite에서 10개 이상의 버그를 발견하고, SQLite 팀과 협력하여 수정했다. 발견된 버그들은 성능 최적화(Performance Optimization), 데이터 무결성(Data Integrity), API 동작의 일관성(API Consistency) 등 다양한 측면에 걸쳐 있었다. 이러한 협력은 오픈소스 커뮤니티의 지속적인 발전(Continuous Improvement)을 이끌어내는 중요한 사례이다.
