- AWS는 보안·내구성·무결성·가용성을 지키기 위해 시스템 정확성을 핵심 기반으로 삼고, TLA+에서 시작해 모델 검사·퍼징·속성 기반 테스트·런타임 검증·형식 증명까지 적용 범위를 넓혀왔음
- TLA+는 전통적 테스트로 잡기 어려운 버그를 초기에 제거하고 성능 최적화에 대한 확신을 줬지만, 개발자 접근성을 높이기 위해 P 프로그래밍 언어와 PObserve 같은 도구가 함께 도입됨
- S3 ShardStore의 속성 기반 테스트, 결정적 시뮬레이션, Aurora Limitless Database의 SQL 퍼징은 형식 기법을 일상적인 개발·통합 테스트에 더 가깝게 끌어온 사례임
- Fault Injection Service는 API 오류, I/O 일시 중지, 인스턴스 실패 같은 장애를 주입해 복원력 메커니즘을 검증하며, Amazon.com은 Prime Day 2024 준비 과정에서 FIS 기반 실험 733건을 실행함
- Cedar, Firecracker, Graviton 2 RSA 최적화처럼 보안 경계와 성능 최적화가 중요한 영역에서는 형식 증명이 쓰이고, 높은 학습 곡선과 도구 접근성은 여전히 채택의 제약으로 남아 있음
AWS가 시스템 정확성을 다루는 방식
- AWS는 고객이 신뢰할 수 있는 서비스를 제공하려면 보안, 내구성, 무결성, 가용성의 높은 기준을 유지해야 하며, 시스템 정확성이 이를 뒷받침함
- 2015년 CACM의 “How Amazon Web Services Uses Formal Methods”는 AWS 핵심 서비스의 정확성을 보장하기 위한 접근을 소개했고, 이후 이 서비스들은 AWS 고객에게 널리 쓰이게 됨
- 초기 중심 도구는 Leslie Lamport가 개발한 형식 명세 언어 TLA+ 였음
- 전통적인 테스트로 놓칠 수 있는 미묘한 버그를 개발 초기에 발견하고 제거하는 데 도움을 줌
- 시스템 정확성을 유지하면서 공격적인 성능 최적화를 구현할 수 있다는 확신을 제공함
- 15년 전 AWS의 테스트 관행은 주로 빌드 시점 단위 테스트와 제한적인 배포 시점 통합 테스트에 의존했음
- 이후 AWS는 형식 기법과 준형식 기법을 개발 과정에 통합함
- 정리 증명, 연역 검증, 모델 검사
- 속성 기반 테스트, 퍼징, 런타임 모니터링
P 프로그래밍 언어와 PObserve
- AWS는 2010년대 초 형식 기법을 초기 팀 밖으로 확장하면서 많은 엔지니어가 TLA+ 학습과 생산성 확보에 어려움을 겪는다는 점을 확인함
- TLA+는 수학에 가까운 고수준 추상 언어라는 점이 강점이지만, 명령형 언어에 익숙한 개발자에게는 접근 장벽이 됨
- 분산 시스템 모델링과 분석을 위한 상태 머신 기반 언어 P가 이 간극을 줄이는 역할을 맡음
- 개발자는 시스템 설계를 통신하는 상태 머신으로 모델링함
- 이 정신 모델은 마이크로서비스와 서비스 지향 아키텍처(SOA)를 많이 다루는 Amazon 개발자에게 익숙함
- P는 2019년부터 AWS에서 개발됐고 전략적 오픈소스 프로젝트로 유지됨
- 여러 AWS 대표 제품 팀이 P를 시스템 설계 정확성 검토에 사용함
- 스토리지: Amazon S3, EBS
- 데이터베이스: Amazon DynamoDB, MemoryDB, Aurora
- 컴퓨트: EC2, IoT
- S3는 eventual consistency에서 strong read-after-write consistency로 이전하는 과정에서 P를 사용함
- S3 인덱스 서브시스템은 빠른 데이터 조회를 가능하게 하는 객체 메타데이터 저장소임
- 강한 일관성을 달성하려면 S3 인덱스 프로토콜 스택에 여러 비자명한 변경이 필요했음
- P는 프로토콜 설계를 형식 모델링·검증해 설계 수준 버그를 초기에 제거하고, 위험한 최적화를 모델 검사로 확인할 수 있게 함
- 2023년 AWS P 팀은 PObserve를 구축함
- 분산 시스템 실행에서 나온 구조화 로그를 사용함
- 로그가 시스템의 형식 P 명세가 허용하는 동작과 일치하는지 사후 검증함
- Rust나 Java 같은 언어로 작성된 프로덕션 구현과 설계 시점 P 명세 사이의 간극을 줄임
- 설계 시점 검증과 구현의 런타임 모니터링을 연결해 형식 명세 투자의 가치를 높임
경량 형식 기법을 개발 흐름에 붙이는 방식
- AWS는 경량 형식 기법을 도입해 형식 기법을 엔지니어링 팀의 개발·테스트 흐름에 더 가깝게 가져감
-
속성 기반 테스트
- Amazon S3의 ShardStore는 개발 주기 전반에서 정확성 테스트와 개발 속도 향상을 위해 속성 기반 테스트를 사용함
- 여러 기법을 함께 써서 사람이 기대 동작을 명세하고, 자동화된 테스트가 더 많은 입력과 실패 조건을 탐색하게 함
- 개발자가 제공한 정확성 명세
- 코드 커버리지 지표로 입력 분포를 안내하는 커버리지 가이드 퍼징
- 하드웨어 및 기타 시스템 실패를 테스트 중 시뮬레이션하는 장애 주입
- 반례를 자동으로 축소해 사람이 디버깅하기 쉽게 하는 최소화
-
결정적 시뮬레이션
- 결정적 시뮬레이션 테스트는 분산 시스템을 단일 스레드 시뮬레이터에서 실행하고 모든 무작위성의 출처를 제어함
- 스레드 스케줄링
- 타이밍
- 메시지 전달 순서
- 개발자는 분산 프로토콜의 특정 단계에서 참여자가 실패하는 상황처럼 특정 실패·성공 시나리오를 작성할 수 있음
- 테스트 프레임워크가 비결정성을 제어하므로, 과거 버그를 유발한 순서 같은 흥미로운 실행 순서를 지정할 수 있음
- 스케줄러는 순서 퍼징이나 가능한 모든 순서 탐색으로 확장될 수 있음
- 지연과 실패 상황의 시스템 속성 테스트를 통합 테스트보다 빌드 시점에 가깝게 이동시켜 개발을 가속하고 동작 커버리지를 넓힘
- AWS의 스레드 순서와 시스템 실패 빌드 시점 테스트 작업 일부는 shuttle과 turmoil 프로젝트로 오픈소스화됨
- 결정적 시뮬레이션 테스트는 분산 시스템을 단일 스레드 시뮬레이터에서 실행하고 모든 무작위성의 출처를 제어함
-
지속적 퍼징과 무작위 테스트 입력 생성
- 지속적 퍼징, 특히 커버리지 가이드 기반의 확장 가능한 테스트 입력 생성은 통합 시점의 시스템 정확성 테스트에 효과적임
- Amazon Aurora의 데이터 샤딩 기능인 Aurora Limitless Database 개발에서는 두 가지 핵심 속성 검증에 퍼징을 광범위하게 사용함
- SQL 쿼리와 전체 트랜잭션을 퍼징해 샤드에 걸친 SQL 실행 논리 분할이 올바른지 검증함
- 대량의 무작위 SQL 스키마, 데이터셋, 쿼리를 합성해 테스트 대상 엔진에서 실행하고, 샤딩되지 않은 엔진 기반 오라클과 결과를 비교함
- SQLancer가 개척한 접근 같은 다른 검증 방식도 함께 사용함
- 퍼징과 장애 주입 테스트의 결합은 데이터베이스의 원자성, 일관성, 격리성 같은 정확성 측면에도 유용함
- 트랜잭션을 자동 생성함
- 형식적으로 명세된 정확성 오라클로 올바른 동작을 정의함
- 트랜잭션과 트랜잭션 내부 문장의 가능한 인터리빙을 테스트 대상 시스템에 실행함
- Elle 같은 접근을 따라 격리성 같은 속성을 사후 검증함
Fault Injection Service와 장애 상황 검증
- AWS는 2021년 초 Fault Injection Service(FIS) 를 출시해 장애 주입 기반 테스트를 다양한 AWS 고객이 사용할 수 있게 함
- FIS는 AWS 인프라의 테스트 또는 프로덕션 배포에 시뮬레이션 장애를 주입할 수 있음
- API 오류
- I/O 일시 중지
- 실패한 인스턴스
- 장애 주입은 아키텍처에 구축된 복원력 메커니즘이 실제로 가용성을 개선하고, 새로운 정확성 문제를 만들지 않는지 확인하게 해줌
- 장애 조치
- 헬스 체크
- FIS 기반 장애 주입 테스트는 AWS 고객과 Amazon 내부에서 널리 사용됨
- Amazon.com은 Prime Day 2024 준비 과정에서 FIS 기반 장애 주입 실험 733건을 실행함
- 2014년 Yuan 등은 테스트한 분산 시스템의 치명적 장애 92%가 비치명적 오류의 잘못된 처리에서 촉발됐다고 분석함
- 정상 경로의 치명적 장애가 드문 이유는 정상 경로가 자주 실행되고, 더 잘 테스트되며, 오류 경로보다 훨씬 단순하기 때문임
- 장애 주입 테스트와 FIS는 장애와 실패 상황에서 시스템 동작을 더 쉽게 테스트하게 해 정상 경로와 오류 경로의 버그 밀도 격차를 줄임
- 장애 주입 자체는 형식 기법으로 간주되지 않지만 형식 명세와 결합될 수 있음
- 기대 동작을 형식 명세로 정의함
- 장애 주입 중과 이후 결과를 명세된 동작과 비교함
- 지표와 로그 오류만 확인하거나 사람이 육안으로 판단하는 방식보다 더 많은 버그를 잡을 수 있음
준안정성과 창발적 시스템 동작
- 최근 10년 동안 특정 부류의 시스템 실패인 준안정 실패(metastable failures) 에 대한 관심이 커짐
- 준안정 실패는 과부하나 캐시 비움 같은 트리거가 분산 시스템을 개입 없이는 회복하지 못하는 상태로 밀어 넣는 실패임
- 개입 예시는 부하를 정상보다 낮게 줄이는 것임
- 이 실패 부류는 클라우드 시스템의 비가용성에 중요한 기여 요인 중 하나임
- 일반적인 준안정 동작에서는 부하 증가에 따라 처음에는 goodput이 증가하다가 포화되고, 혼잡을 거쳐 goodput이 0 또는 0에 가까워짐
- 이후 시스템은 부하를 조금 줄이는 것만으로 건강한 상태로 돌아가지 못하며, 부하를 크게 줄여야 회복될 수 있음
- 이 동작은 단순한 시스템에서도 나타날 수 있고, 대부분의 시스템에서 타임아웃 후 재시도 클라이언트 로직으로도 촉발될 수 있음
- 전통적인 분산 시스템 형식 모델링은 보통 안전성(safety)과 활성성(liveness)에 초점을 맞추지만, 준안정 실패는 이 분류에 깔끔하게 들어가지 않는 동작이 있음을 보여줌
- AWS는 창발적 시스템 동작을 이해하기 위해 이산 사건 시뮬레이션을 더 많이 활용함
- 맞춤형 시스템 시뮬레이션에 투자함
- TLA+와 P 같은 언어로 만든 기존 시스템 모델을 시뮬레이션에 사용할 수 있는 도구에 투자함
- TLA+의 TLC 같은 완전 탐색 모델 검사기를 확률적 시뮬레이션으로 확장하면 사후 지연 분포 같은 통계 결과를 생성할 수 있음
- 이런 확장은 지연 시간 SLA 달성 가능성 이해 같은 작업에 모델 검사를 활용하게 함
형식 증명이 필요한 보안 경계
- 권한 부여와 가상화 같은 중요한 보안 경계에서는 앞서의 형식 기법만으로 충분하지 않을 수 있으며, 정확성 증명이 큰 투자 가치가 있음
-
Cedar 권한 정책 언어
- AWS는 2023년 세밀한 권한을 지정하는 정책 작성을 위한 Cedar 권한 정책 언어를 도입함
- Cedar는 자동 추론과 형식 증명을 고려해 설계됨
- 구현은 검증 친화적 프로그래밍 언어 Dafny로 구축됨
- Dafny를 통해 구현이 여러 보안 속성을 만족한다는 점을 증명함
- 이 증명은 테스트를 넘어서는 수학적 의미의 증명임
- 팀은 Dafny 코드를 정확성 오라클로 사용하는 차등 테스트도 적용해 프로덕션 준비가 된 Rust 구현의 정확성을 검증함
- Cedar 구현과 함께 Dafny 코드와 테스트 절차를 오픈소스로 공개해 사용자가 정확성 작업을 확인할 수 있게 함
-
Firecracker VMM
- Firecracker 가상 머신 모니터는 virtio라는 저수준 프로토콜을 사용해 네트워크 카드나 SSD 같은 에뮬레이션된 하드웨어 장치를 VM 내부 게스트 커널에 노출함
- 이 에뮬레이션 장치는 신뢰할 수 없는 게스트와 신뢰된 호스트 사이의 가장 복잡한 상호작용이므로 중요한 보안 경계임
- Firecracker 팀은 Rust 코드를 형식적으로 추론할 수 있는 Kani를 사용해 이 보안 경계의 핵심 속성을 증명함
- 이 증명은 게스트가 무엇을 시도하더라도 경계의 중요한 속성이 유지됨을 보장함
- AWS는 Kani, Dafny, Lean과 이를 구동하는 SMT solver 같은 기반 도구 개발을 지원함
- 형식 모델과 명세는 여러 방식으로 재사용됨
- 설계 시점 모델 검사
- 런타임 모니터링에서 정확성 오라클 역할
- 창발적 시스템 동작 시뮬레이션
- 핵심 속성의 증명 구축
정확성을 넘어선 성능과 비용 효과
- 형식 기법은 클라우드 시스템 성능을 안전하게 개선하는 데도 중요함
- Aurora 관계형 데이터베이스 엔진의 핵심 커밋 프로토콜을 P와 TLA+ 로 모델링한 결과, 안전성 속성을 희생하지 않고 분산 커밋 비용을 2 네트워크 왕복에서 1.5 네트워크 왕복으로 줄일 기회를 찾음
- 이런 성과는 형식 기법을 도입한 팀에서 흔함
- 분산 프로토콜을 깊게 생각하고 형식적으로 작성하는 과정이 구조화된 사고를 강제함
- 프로토콜 구조와 풀어야 할 문제에 대한 더 깊은 통찰을 줌
- 제안된 설계 최적화가 올바른지 형식적으로 확인하거나 증명할 수 있으면 분산 시스템 엔지니어가 위험을 늘리지 않고 더 과감한 설계를 선택할 수 있음
- 생산성과 비용 효과는 고수준 설계 최적화에만 국한되지 않음
- AWS 팀은 ARM 기반 Graviton 2 프로세서에서 RSA 공개키 암호화 구현 최적화를 찾아 처리량을 최대 94% 개선할 수 있었음
- HOL Light 대화형 정리 증명기를 사용해 이 최적화의 정확성을 증명함
- 클라우드 CPU 사이클의 높은 비율이 암호화에 쓰이므로 이런 최적화는 인프라 비용 절감, 지속가능성 지원, 고객이 체감하는 성능 개선에 기여할 수 있음
남은 과제와 향후 기회
- AWS는 지난 15년 동안 형식·준형식 테스트 방법을 확장하는 데 성공했지만, 산업적 채택에는 여전히 과제가 남아 있음
- 형식 기법 도구의 주요 장벽은 가파른 학습 곡선과 전문 도메인 지식 요구임
- 많은 도구가 여전히 학술적 성격을 갖고 있으며 사용자 친화적 인터페이스가 부족함
- 잘 정착된 준형식 접근도 채택 장벽이 남아 있음
- 결정적 시뮬레이션은 AWS와 FoundationDB 같은 프로젝트에서 성공적으로 쓰인 핵심 분산 시스템 테스트 기법이지만, AWS에 합류하는 숙련된 분산 시스템 개발자에게도 낯선 경우가 있음
- 장애 주입 테스트, 속성 기반 테스트, 퍼징 같은 검증된 방법론에서도 비슷한 격차가 존재함
- 분산 시스템 개발자에게 이런 테스트 방법과 도구를 교육하고, 엄밀한 사고 방식을 가르치는 일이 필요함
- 교육 격차는 학계 수준에서 시작됨
- 기본적인 형식 추론 접근도 드물게 가르쳐짐
- 상위 기관 졸업생도 이런 도구를 채택하기 어려움
- 형식 기법과 자동 추론은 산업 적용에 중요하지만 여전히 틈새 분야로 여겨짐
- 준안정성과 대규모 시스템의 다른 창발적 속성도 비슷한 인식 과제를 가진 중요한 연구 영역임
- “타임아웃 시 N번 재시도”처럼 준안정 시스템 동작을 유발할 수 있는 관행이 알려진 문제에도 계속 널리 권장됨
- 창발적 시스템 동작 이해를 위한 현재 도구와 기법은 초기 단계임
- 시스템 안정성 모델링은 비용이 많이 들고 복잡함
- AWS는 대형 언어 모델과 AI 어시스턴트가 형식 기법의 실무 채택 문제를 완화하는 데 크게 도움이 될 것으로 봄
- AI 보조 단위 테스트가 인기를 얻은 것처럼, 개발자가 형식 모델과 명세를 만드는 데 도움을 줄 수 있음
- 고급 기법이 더 넓은 개발자 커뮤니티에 접근 가능해질 수 있음
AWS가 계속 투자하는 정확성 체계
- 신뢰할 수 있고 안전한 소프트웨어를 만들려면 시스템 정확성을 추론하는 다양한 접근이 필요함
- AWS는 단위 테스트와 통합 테스트 같은 업계 표준 테스트와 함께 여러 기법을 채택함
- 모델 검사
- 퍼징
- 속성 기반 테스트
- 장애 주입 테스트
- 결정적 시뮬레이션
- 이벤트 기반 시뮬레이션
- 실행 추적의 런타임 검증
- 형식 명세는 AWS의 여러 테스트 관행에서 올바른 답을 제공하는 테스트 오라클로 중요한 역할을 함
- 정확성 테스트와 형식 기법은 이미 얻은 투자 수익을 바탕으로 AWS의 핵심 투자 영역으로 남아 있음