▲

Amazon Web Services의 시스템 정확성 실천 사례

 (cacm.acm.org)
2P by GN⁺ 5일전 | ★ favorite | 댓글 1개
  • Amazon Web Services(AWS) 는 서비스의 정확성을 핵심 가치로 두고 여러 형태의 형식적 방법론을 개발 프로세스에 통합함
  • TLA+와 P 언어 등 형식 명세 도구를 통해 미묘한 버그를 조기에 발견하고, 대담한 최적화에도 신뢰성 확보 가능함
  • AWS는 경량화된 형식 방법론으로 속성 기반 테스트·결정적 시뮬레이션·지속적 퍼징 등도 폭넓게 운용함
  • Fault Injection Service 같은 실패 주입 도구를 통해 장애 발생 상황까지 포함한 신뢰성 검증을 자동화함
  • 교육적 장벽과 도구의 복잡성이 여전하지만, AI와 자동화 도구의 확산이 보급 확대에 기여할 전망임

AWS의 시스템 정확성 보장 전략

Amazon Web Services(AWS)는 고객이 완전히 신뢰할 수 있는 신뢰성 높은 서비스 제공을 목표로 함
이를 위해 보안성, 내구성, 무결성, 가용성 기준 유지를 추구하며, 그 중심에 시스템 정확성 개념을 배치함

2015년 Communications of the ACM에 소개된 AWS의 형식적 방법론 적용 사례 이후, 해당 접근법은 핵심 서비스의 성공적 운용에 중요한 역할을 해옴

중심에는 Leslie Lamport가 개발한 TLA+라는 형식 명세 언어가 있음
AWS의 TLA+ 도입 경험은 개발 초기 단계에서 기존 테스트로는 잡히지 않는 미세한 버그를 파악할 수 있게 해주었음
또한, 과감한 성능 최적화를 진행할 때도 형식적 검증을 통해 안정성과 신뢰성을 확보할 수 있었음

15년 전 AWS는 빌드 시점 단위 테스트, 제한된 통합 테스트 등 기본 수준에 머물렀지만, 이후로 형식적 접근과 준형식적 방법을 포괄적으로 도입함
이러한 변화는 정확성뿐 아니라 고수준 및 저수준 최적화 검증·개발 속도 향상·비용 절감에 기여함

AWS에서는 기존의 정형 증명, 모델 검증뿐만 아니라 속성 기반 테스트, 퍼징, 런타임 모니터링 등도 형식적 방법론의 범주로 수용함

P 프로그래밍 언어의 등장

초기에는 TLA+가 강력한 추상적 기술이라는 장점이 있었으나, 수많은 개발자 입장에서는 수학적 표기법 사용의 진입장벽이 컸음
그래서 AWS는 개발자가 익숙한 상태 기계 기반 접근을 제공하는 P 언어를 도입함

P 언어는 분산 시스템 설계 및 분석을 위해 상태 기계 모델링 방식을 제공함
마이크로서비스 기반 SOA 구조를 사용하는 Amazon 개발자들에게 친숙한 개념임
2019년부터 AWS에서 개발 및 전략적 오픈소스 프로젝트로 관리 중임
Amazon S3, EBS, DynamoDB, Aurora, EC2, IoT 등 주요 서비스팀이 P를 활용해 시스템 설계의 정확성 검증을 수행함

S3를 강력한 read-after-write 일관성으로 전환할 때, P로 프로토콜을 모델링 및 검증해, 설계 초기 단계에서 버그를 제거하고 최적화 사항도 안정적으로 반영함

2023년 AWS P 팀은 PObserve 툴을 개발해, 테스트와 실제 운영 환경 모두에서 분산 시스템의 정확성을 검증 가능하게 함
PObserve는 실행 로그를 추출해, 명세에 따라 올바른 동작이 이뤄졌는지 사후 검증이 가능하며, 설계 단계 명세와 실제 코드 구현을 효과적으로 연계해줌

경량 형식 방법론 확대

속성 기반 테스트

가장 대표적인 경량 형식 기법은 속성 기반 테스트임
예를 들어 S3의 ShardStore 개발팀은 개발 주기의 전 과정에서 속성 기반 테스트·코드 커버리지 기반 퍼징·실패주입·카운터 예제 최소화 등을 복합 사용함
이 방식은 개발자가 직접 작성하는 정확성 명세와 연동되고, 문제점 디버깅 효율도 크게 향상됨

결정적 시뮬레이션

결정적 시뮬레이션 테스트는 단일 스레드 시뮬레이터에서 분산 시스템을 실행, 모든 난수 요소(스케줄링, 타이밍, 메시지 순서 등) 제어가 가능함
특정 오류 및 성공 시나리오에 대한 테스트, 버그 유발 순서 조정, 퍼징 확장 등 다양한 방식으로 적용됨
이로 인해 시스템의 지연, 실패 등 동작 검증을 빌드 단계에서 일찍 수행하고, 테스트 범위가 확대됨
AWS는 이러한 빌드 타임 테스트 코드를 shuttle, turmoil 오픈소스 프로젝트로 공개함

지속적 퍼징

지속적 퍼징, 특히 코드 커버리지 기반 대규모 입력 생성은 통합테스트 단계에서 시스템 정확성 검증에 효과적임
예를 들어 Aurora Limitless Database 개발시 SQL 쿼리와 트랜잭션을 퍼징해, 파티셔닝 논리의 정확성을 대량의 무작위 스키마·데이터셋·쿼리를 생성해 검증함
결과는 non-sharded 엔진의 동작 또는 SQLancer 등의 방식과 비교함
퍼징과 실패 주입 결합으로 원자성, 일관성, 격리성 등 데이터베이스의 핵심 속성을 검증함
자동 생성 트랜잭션, 격리성 등 일부 속성은 실행 이력 기반 사후 검증을 통해 보장함

Fault Injection Service를 통한 장애 주입

2021년 AWS는 Fault Injection Service(FIS) 를 출시해 고객도 API 오류, I/O 중단, 인스턴스 장애 등 다양한 결함 시나리오를 실제 또는 테스트 환경에 빠르게 실험할 수 있도록 함
이를 통해 아키텍처의 가용성 확보 및 장애 복원력 점검, 오류 케이스의 높은 버그 밀도 차이 해소, 가능성 높은 중대한 문제 사전 발견 등의 효과가 있음

FIS는 AWS 고객은 물론 Amazon 내부에서도 광범위하게 사용되고, 예를 들어 Prime Day 준비 과정에서만 733건의 실험이 진행됨

오류 주입은 형식 명세와 결합하면 더 효과적임
예상 동작을 형식 명세로 작성 후, 실제 결함 유발 결과를 이에 대조해 기존의 단순 로그·지표 점검보다 더 많은 오류를 잡을 수 있음

메타안정성과 시스템 발현 동작

분산 시스템에서 지나친 부하/캐시 소진 등 유발로 ‘자체적으로 복구 불가능’한 비정상(메타안정적) 상태에 빠지는 사례가 증가함
이 상태에선 단순 부하 감소만으로는 정상 복구되지 않고, 통상적인 오류 케이스보다 대응이 까다로움
대부분의 재시도-타임아웃 로직도 이런 현상의 원인이 됨

기존 형식 명세는 안전성과 진행성에 초점 두지만, 메타안정성은 그 이외의 다양한 발현 동작까지 고려해야 함
AWS는 TLA+, P 등의 명세 모델을 바탕으로 이산 이벤트 시뮬레이션을 진행, 성능 SLA 달성 가능성·지연 분포 산출 등 확률적 특성까지 체계적으로 분석함

형식 증명의 필요성

일부 보안 경계(권한·가상화 등) 에서는 단순 테스트 이상의, 수학적 수준의 증명이 필수적임

예를 들어 2023년 AWS가 도입한 Cedar 권한 정책 언어는 Dafny 기반으로 자동 증명과 형식적 검증에 최적화되며, 공개 코드와 정정 절차를 통해 전체 사용자도 직접 검증이 가능함
또 Firecracker VMM의 보안 경계(key property)는 Kani 등의 Rust 코드 분석 도구로 증명 작업 진행됨

이처럼 형식 모델과 명세를 다양한 시점(설계, 구현, 시행, 증명)에 폭넓게 활용함으로써 소프트웨어 정확성 확보와 기업·고객 가치 확대에 활용함

정확성을 넘어선 추가 효과

형식 방법론은 신뢰성과 성능 개선 모두에 중대한 역할을 함
예를 들어 Aurora의 commit 프로토콜을 P와 TLA+로 검증, 네트워크 소요 라운드트립을 줄이는 동시에 안전성도 보장함
RSA 암호화 알고리듬의 ARM Graviton 2 최적화 시, HOL Light에서 변환의 수학적 정확성을 증명해 성능·인프라 비용 동시 개선이라는 실질 효과를 거둠

미래의 도전과 기회

15년간 AWS는 형식/준형식 방법론의 산업 적용을 크게 확대했으나, 학습 곡선, 전문가 필요성, 도구의 학술적 특성 등 실질적 도입 장애 문제가 상존함
속성 기반 테스트, 결정적 시뮬레이션 등도 많은 개발자에겐 여전히 생소함
교육상의 진입장벽이 학부 과정부터 존재하므로, 도구·방법론의 보급과 실무 적용이 더디게 진행됨
메타안정성 등 대규모 시스템의 발현적 특성도 연구 초기 단계임

향후 AI/대형 언어 모델이 형식적 모델·명세 작성을 지원해, 실무자 접근성을 단기간 내 획기적으로 높여줄 것으로 기대됨

결론

견고하고 안전한 소프트웨어 구축에는 다양한 시스템 정확성 확보 수단이 필요함
AWS는 표준 테스트 기법 이외에도 모델체킹, 퍼징, 속성 기반 테스트, 장애 주입 테스트, 결정적/이벤트 기반 시뮬레이션, 실행 이력 검증 등을 포괄적으로 도입함
형식 명세와 방법론은 AWS의 개발 프로세스에서 중요한 시험 오라클 역할을 하며, 이미 실질적·경제적 효과 검증을 통해 투자 영역 중 하나로 자리잡고 있음

▲
GN⁺ 5일전  [-]
Hacker News 의견

  • 결정론적 시뮬레이션 테스트 방식에 대해 이야기하고 싶음. AWS에서는 분산 시스템을 단일 스레드 시뮬레이터에서 실행하면서 스레드 스케줄링, 타이밍, 메시지 전달 순서 등 모든 비결정적인 요소들을 제어함. 그런 다음 특정 실패나 성공 시나리오에 맞춘 테스트를 작성하며, 시스템 내 비결정성은 테스트 프레임워크가 제어함. 개발자는 과거에 버그를 유발했던 특정 순서를 지정할 수 있음. 스케줄러는 순서에 대한 퍼징이나 가능한 모든 순서 탐색까지 확장 가능함. 이런 것을 언어와 무관하게 오픈소스로 구현해둔 라이브러리가 있는지 궁금함. 컨테이너 내에서 네트워킹, 스토리지 등도 테스트 시점에 "결정적"으로 만드는 미들웨어 도구가 필요하다는 아이디어임. antithesis는 거의 이와 같은 역할을 하지만, 아직 오픈소스에서 못 봤음. 테스트를 잘 짜면 I/O 같은 걸 스텁 처리해서 어느 정도 해결할 수 있지만, 다들 테스트를 잘 짠다는 보장은 없음. 애플리케이션 위에 더 높은 계층에서 결정성을 제공하면 좋다고 생각함. 한편으로 AI가 테스트에서 제대로 빛을 발할 수 있을 거라 기대함. 프롬프트(요구사항)-테스트 구현-AI-실행 코드 이 세 축이 이상적으로 맞물릴 수 있음. AI가 형식 검증을 더 손쉽게 해서 소프트웨어 세계를 한층 엄밀하게 만들어줬으면 하는 기대가 있음

    • 결정론적 시뮬레이션 테스트(DST) 기술 확산에는 두 가지 어려움 존재. 첫째, 기존에는 모든 시스템을 특정 시뮬레이션 프레임워크 위에 직접 올려서 다른 의존성이 없어야 했음. 둘째, 입력 생성 및 탐색이 약하면 테스트가 전부 성공하는 척 보이면서 실질적 검증이 안 됨. antithesis가 이 둘을 모두 해결하려 노력하고 있지만 아직 어려움 많음. 결정성을 아무 소프트웨어에나 적용하는 확실한 방법을 지닌 곳은 잘 없음. Facebook의 Hermit 프로젝트도 결정론적 Linux 유저스페이스로 시도했지만 끝내 중단됨. 결정론적 컴퓨터는 테스트 외에도 매우 유용한 기술적 기반이고, 언젠가는 누군가 오픈소스로 공개할 것이라는 생각임

    • QEMU를 100% 에뮬레이션 모드에서 단일 쓰레드로 돌리며 결정론적 머신을 얻는 건 비교적 쉬운 편이라 생각함. 다만 진짜로 원하는 건 '제어된' 결정적 실행이고, 이건 훨씬 어려움. 여러 프로세스를 지정한 시나리오로 동작하게 만들려면 특히 CPU 및 OS 스케줄러 레벨에서 난이도가 매우 높음. 언어에 구애받지 않는 환경 자체를 만들기도 힘들고, 세세한 부분에 휘둘리기도 쉬움. 나도 JVM 쓰레드 여러 개를 특정 동작 시점에서 락스텝(lockstep)으로 동작시키는 간단한 시스템을 만든 적 있는데, I/O와 시스템 타임을 스텁과 제어로 처리함. 그래서 비동기 컴포넌트들 간의 다양한 상호작용, I/O 장애, 재시도 등도 테스트해보고 프로덕션 가기 전에 골치 아픈 버그를 잡음. 단, 전체 시스템을 제어하기보다는 특정 동기화 지점만 단순화해서 가능했음. 동기화 실수로 인한 일반적인 데이터 레이스는 이 방식으론 잡기 어려움

    • FoundationDB의 테스트 방법 공식 문서 및 유튜브 발표 영상 공유

    • gdb로 디버깅 가능한 언어라면 https://rr-project.org/ 프로젝트 추천

    • Joe Armstrong이 property testing을 활용해 Dropbox를 테스트한 발표를 예전에 본 기억이 있음

  • S3는 지금까지 본 소프트웨어 중 가장 멋진 것 중 하나라 생각함. 몇 년 전 S3 전체 시스템에 강력한 읽기-쓰기 일관성을 추가한 것도 진짜 소프트웨어 엔지니어링의 극치라 생각함 블로그 포스팅 링크

    • S3의 라이프사이클 담당으로 직접 일한 적이 있는데, 그때 인덱스 팀이 이 일관성 제공을 위한 구조를 새로 설계하던 시기와 겹침. 외부에서 봐도 S3는 대단하지만, 내부적으로는 구현 및 조직 구조 모두 상상을 뛰어넘을 정도로 인상적임

    • Google Cloud Storage는 오히려 S3보다 훨씬 이전부터 이 기능(강력한 일관성)을 갖추고 있었음. 전반적으로 GCS가 좀 더 체계적이고 제대로 만들어진 제품 같다는 인상임

  • 92% 수치(클러스터 장애의 대부분이 사소한 실패에서 시작됨)에 공감함. 화려한 대형 사고가 아니라 "별거 아닌" 재시도가 상태 누적으로 이어지다가, 결국 새벽 2시에 대규모 장애로 터진 경우가 대부분임. 눈에 안 띄는 실패에 더 많은 엔지니어링 시간을 할당하는 것이 중요함

    • 이건 살아남은 문제만 보게 되는 '생존 편향' 효과일 수도 있음. 큰 문제는 이미 해결되어 두 번 다시 발생하지 않고, 덜 위험해 보이는 사소한 문제들이 때때로 큰 장애를 일으킴

  • 정말 흥미로운 글이라 생각함. 인프라 컨트롤 플레인 구축에 상태 기계 사용은 필수임. 꼭 P가 필요했을지는 모르겠음. 우리도 13년 넘게 Ruby로 인프라 컨트롤 플레인을 만들었고, 아주 훌륭하게 동작함 관련 경험 공유 블로그

  • P 언어에 대해 궁금한 점 있었음. 예전엔 Microsoft에서 Windows USB 스택 런타임 용도로 P로 C코드 생성해서 실제로 사용한 것 같은데, 지금은 더 이상 운영 코드 생성에 쓰지 않는 것 같음. 관련 질문을 Hacker News에도 남긴 적 있음 질문 링크. 커널에까지 생성된 코드가 들어갈 수 있다면 훨씬 완화된 조건의 클라우드 환경에도 분명히 쓸 수 있을 듯

  • AWS 출신이 아니고 TLA+나 P에 익숙하지 않은 입장에선 "헬로월드"쯤의 예제라도 있었으면 그나마 이해가 쉬웠을 것 같음. 글만 보면 그냥 고통스러운 과정처럼 느껴지기도 하고, 좋은 설계와 테스트만으로 충분히 잡을 수 있는 문제 아닌가라는 생각이 듦. 간단 예제가 있었다면 실제로 뭘 하는지 판단에 더 도움이 됐을 것

    • 내가 좋아하는 TLA+의 빠른 데모 예제가 있음 gist 링크. 여러 스레드가 공유된 카운터를 서로 원자적이지 않게 증가시키는 모델인데, 속성 검증시 race condition이 잡힘. 실제로 이런 버그를 테스트만으로 발견하기 무척 어려움. 대부분의 TLA+ 명세는 훨씬 더 복잡하지만, 단순 오류를 포착하는 데 이 예제가 좋음

    • 직접 TLA를 써봤는데, 그래픽 도구가 튜토리얼과 잘 맞지 않아 실망스러웠던 경험 있음. TLA 자체는 쓰고 싶었고 Lamport의 작업(LaTeX~논문까지)을 예전부터 좋아해 왔음

    • 형식 기법(formal methods)을 쓰는 전제가 결국 테스트만으로 절대 모든 문제를 잡을 수 없다는 데 있음

    • 공식 TLA+ Examples 깃허브 저장소 추천. DieHard 문제 같은 단순한 것부터 시작하는 걸 권장함

    • 테스트는 문제의 특정 인스턴스에 대해 구현의 옳음을 증명하지만, 형식 검증은 전체 범주에 대해 증명함. 예를 들어 아나그램을 반환하는 함수의 경우, 테스트는 일부 단어쌍만으로 확인하지만, 전체 단어쌍에 대해 옳음을 증명하려면 formal verification이 필요함. undefined behavior나 라이브러리 버그 같은 사례도 formal verification 과정에서만 잡히는 경우 많음

  • "프러퍼티 기반 테스트, 퍼징, 런타임 모니터링 같은 경량 준형식 기법" 언급에, property-based testing과 fuzzing은 형식 기법의 하위 집합이 맞지만, runtime monitoring까지 준형식 기법에 포함하는 건 다소 과하다고 느낌

    • PObserve 같은 도구를 활용한 런타임 모니터링이라면 충분히 준형식 기법이라 볼 수 있음. 단순 알람이나 메트릭 체계와 구분 필요함

  • 예전에 Leslie Lamport와 Buridan's Principle 관련 논문 등으로 교류한 적 있음. 오늘 그의 홈페이지에서 TLA+와 PlusCal에 대해 많이 알게 됨 Peterson 예제 페이지. 수학을 프로그래밍에 끌고 오고, 동시성 시스템 분야의 시초격인 분이 시스템 설계 언어(TLA+)를 만들고, AWS 등에서 쓰인다는 점이 너무나 자연스러움. 분산 시스템 구축하는 사람들이 Lamport가 만든 걸 더 많이 썼으면 하는 바람이 있음. 대규모 시스템에선 옳음 증명이 매우 중요함

    • 기존 코드에서 TLA+ 사양 변환은 Claude Opus(Extended Thinking)가 아주 쓸만함. Rust 프로젝트나 C++ 핵심 컴포넌트 검증에도 여러 버그를 찾은 경험이 있음. 다른 모델은 구문 및 스펙 논리에서 자주 막히는 반면 Opus는 훨씬 매끄럽게 작동함

    • 대규모 시스템뿐 아니라 SSH, 터미널 같은 작지만 중요한(전세계에서 많이 쓰는) 유틸리티에도 옳음 증명은 굉장히 유익함

    • "시스템의 옳음 증명"이라는 발언에, 실제로 전부 증명하는 건 불가함. 모델 체커는 한정된 상태 공간 내에서 명시한 스펙이 속성을 만족한다고만 알려줄 수 있음

  • 개인적으로 FIS를 분산 서비스 실험에 써본 경험 있는지 궁금함. 도입 고려 중이지만 직접 대규모 실험을 해본 경험은 없음

  • Promela와 SPIN이 글에서 다루는 것보다 더 상위 수준 언어인지 궁금함

    • Promela로 분산 시스템 작업도 해봤던 입장인데, 이 분야에 딱 맞는 느낌은 아님. 독특한 아이디어는 있지만, 다시 살펴볼 여지는 있음
답변달기