Systematic API Testing Through Model Checking and Executable Contracts

1. 문제 제기 (Problem)

기존의 API 자동화 블랙박스 테스트는 주로 OpenAPI Specification (OAS) 과 같은 인터페이스 명세에 의존합니다. 그러나 이러한 명세에는 다음과 같은 한계가 존재합니다.

• 행위적 의미의 부재 (Semantic Gap): OAS 는 엔드포인트, 데이터 스키마, HTTP 상태 코드를 정의하지만, 시스템의 상태 변화나 로직과 같은 '행위적 의미 (Behavioural Semantics)'를 포착하지 못합니다.
• 오라클 문제 (Oracle Problem): 대부분의 도구들이 HTTP 상태 코드 (특히 5xx) 를 실패의 유일한 기준으로 삼습니다. 하지만 5xx 는 명세 위반이 아닌 예기치 않은 예외일 수 있으며, 2xx 를 반환하더라도 명세와 다른 상태가 될 수 있어 신뢰성이 떨어집니다.
• 상태 의존적 시퀀스 생성의 어려움: API 호출 간의 상태 의존성 (예: 생성 후 삭제) 을 고려한 효과적인 호출 시퀀스를 자동으로 생성하기 어렵습니다.

2. 방법론 (Methodology)

ICEPICK 은 **TLA+**를 사용한 형식 모델링과 TLC 모델 체커를 활용한 상태 공간 탐색을 기반으로 합니다. 전체 프로세스는 두 단계로 나뉩니다.

A. 명세 전처리 및 모델링 (Specification Pre-processing)

1. GLACIER (계약 언어): OAS 파일을 기반으로 CRUD(생성, 읽기, 수정, 삭제) 의미론을 추론하여 GLACIER라는 1 차 논리 기반의 계약 언어로 변환합니다.
   • 사전/사후 조건 (Pre/Post-conditions): HTTP 요청과 응답을 기반으로 자동 생성됩니다 (예: postPlayer 는 생성 전에는 존재하지 않아야 하고, 후에는 존재해야 함).
   • 불변식 (Invariants): 시스템 전체의 일관성 (예: 토너먼트 등록 인원 수 ≤ 용량) 을 정의합니다.
   • 수동 확장: 자동 생성된 계약은 부분적이므로, 개발자가 GLACIER 를 사용하여 도메인 특유의 일관성 제약 (예: 참조 무결성) 을 수동으로 추가할 수 있습니다.
2. TLA+ 명세 작성: GLACIER 계약을 TLA+ 의 액션 (Action) 과 상태 전이로 변환합니다. 시스템의 상태 (리소스 맵) 와 전이를 수학적으로 정의하여 TLC 모델 체커가 탐색할 수 있는 추상 모델을 만듭니다.

B. 체계적 테스트 (Systematic Testing)

1. 상태 공간 그래프 (SSG) 생성: TLC 모델 체커를 사용하여 TLA+ 모델의 모든 도달 가능한 상태와 전이를 탐색하고 SSG 를 생성합니다.
2. 호출 시퀀스 생성: SSG 를 기반으로 커버리지 가이드 BFS(너비 우선 탐색) 알고리즘을 적용하여 초기 상태에서 최종 상태까지의 모든 전이를 포함하는 최소 길이의 호출 시퀀스를 생성합니다.
   • 주의: 병렬 전이 (Parallel transitions) 가 있는 경우 상태 시퀀스만으로는 전이 식별이 어려울 수 있으나, RESTful API 의 특성상 이는 드뭅니다.
3. 실행 및 검증:
   • 생성된 시퀀스를 실제 API 에 실행합니다.
   • 상태 에뮬레이터: 테스트 중 관찰된 리소스 상태를 추상적으로 유지합니다.
   • 평가기 (Evaluator): GLACIER 계약 (사전/사후 조건, 불변식) 을 실제 응답과 에뮬레이터 상태에 대입하여 검증합니다.
   • 결과 분류: OK, WARN(의심스러움), ERR(명시적 위반), NOT_TESTED 로 분류합니다.

3. 주요 기여 (Key Contributions)

1. GLACIER: RESTful API 를 위한 1 차 논리 기반의 계약 명세 언어입니다. OAS 에서 자동 생성되며, 개발자가 수동으로 도메인 논리를 추가할 수 있는 확장성을 제공합니다.
2. ICEPICK 프레임워크: TLA+ 모델 체킹을 활용하여 명세된 행위를 체계적으로 커버하는 블랙박스 테스트 프레임워크입니다.
3. 커버리지 가이드 탐색 알고리즘: 상태 공간 폭발을 완화하고 효율적인 시퀀스를 추출하기 위해 SSG 를 BFS 로 탐색하는 알고리즘을 제안했습니다.
4. 실증 평가: EvoMaster 벤치마크 (Tournaments, Swagger-Petstore 등) 를 사용하여 프레임워크의 유효성과 확장성을 검증했습니다.

4. 평가 결과 (Results)

• 상태 커버리지: 모델 체킹 기반 탐색은 명세된 행위에 대해 완전한 상태 커버리지를 달성했습니다.
• 결함 탐지:
  • Tournaments 시스템: 주입된 3 가지 결함 (삭제 실패, 무작위 삭제, 참조 무결성 위반) 을 모두 탐지했습니다. 특히, 단순 HTTP 상태 코드만으로는 발견하기 어려운 **다중 연산 간의 상태 불일치 (참조 무결성 위반)**를 성공적으로 발견했습니다.
  • Features-Service: REST 원칙을 준수하지 않는 API 의 경우, GLACIER 계약 생성 단계에서 명세 오류를 발견하고 테스트를 중단시켰습니다. 이는 ICEPICK 이 REST 준수 여부에 민감함을 보여주지만, 동시에 명세/구현의 구조적 결함을 조기에 발견할 수 있음을 의미합니다.
• 확장성 (Scalability):
  • 모델 크기가 작을 때 (예: 3~12 개의 리소스) 는 TLC 가 수백만 개의 상태와 전이를 생성할 수 있어 실용적입니다.
  • 하지만 모델 크기가 커지면 (예: 12 개 리소스) 상태 공간이 기하급수적으로 증가하여 (467GB, 16 시간 이상) 처리가 어려워지므로, 적절한 모델 크기 조절이 필요합니다.
  • 메모리 제한 (100GB Heap) 내에서 약 46,000 개의 상태와 349,000 개의 전이를 처리할 수 있었습니다.
• 수동 명세의 효과: 주입된 결함의 경우 자동 생성된 계약으로도 모든 결함을 발견했으나, 도메인 특유의 복잡한 의미론적 결함은 수동으로 정의된 GLACIER 계약이 더 유용할 것으로 예상됩니다.

5. 의의 및 결론 (Significance)

• 오라클 문제 해결: HTTP 상태 코드에 의존하지 않고, 실행 가능한 계약 (GLACIER) 을 통해 시스템의 내부 상태 일관성을 검증함으로써 테스트 오라클의 신뢰성을 높였습니다.
• 재현 가능성: 모델 체킹 기반의 탐색은 무작위성 (Randomness) 이 적어, 동일한 명세에 대해 재현 가능한 테스트 스위트를 생성합니다. 이는 검색 기반 (Search-based) 이나 퍼징 (Fuzzing) 접근법의 비결정적 결과와 대비됩니다.
• REST 준수 중요성 강조: ICEPICK 은 REST 원칙 (리소스 지향, 정확한 상태 코드 등) 을 철저히 준수하는 API 에서 가장 효과적입니다. REST 비준수 시스템에서는 테스트 자체가 불가능할 수 있음을 보여주며, 이는 연구 커뮤니티에 더 나은 벤치마크의 필요성을 시사합니다.
• 향후 과제: TLA+ 명세 작성의 수동 부담을 줄이기 위한 자동화, 부분적으로 REST 를 준수하는 API 에 대한 적용, 병렬 전이를 고려한 전이 커버리지 보장 알고리즘 개선 등이 필요합니다.

요약하자면, ICEPICK 은 형식적 모델 체킹과 실행 가능한 계약을 결합하여 RESTful API 의 상태 의존적 결함을 체계적으로 발견하고, 높은 커버리지와 재현성을 보장하는 새로운 테스트 패러다임을 제시합니다.