Các thực hành về tính đúng đắn hệ thống tại Amazon Web Services

• AWS lấy tính đúng đắn của hệ thống làm nền tảng cốt lõi để bảo vệ bảo mật, độ bền, tính toàn vẹn và tính sẵn sàng, và đã mở rộng phạm vi áp dụng từ TLA+ ban đầu sang kiểm chứng mô hình, fuzzing, kiểm thử dựa trên thuộc tính, xác minh runtime và chứng minh hình thức
• TLA+ giúp loại bỏ sớm các lỗi khó phát hiện bằng kiểm thử truyền thống và mang lại sự tự tin cho các tối ưu hóa hiệu năng, nhưng để tăng khả năng tiếp cận cho nhà phát triển, các công cụ như ngôn ngữ lập trình P và PObserve cũng được đưa vào sử dụng
• Kiểm thử dựa trên thuộc tính của S3 ShardStore, mô phỏng tất định và fuzzing SQL của Aurora Limitless Database là những ví dụ đưa các kỹ thuật hình thức đến gần hơn với phát triển và kiểm thử tích hợp hằng ngày
• Fault Injection Service chèn các sự cố như lỗi API, tạm dừng I/O và lỗi instance để xác minh cơ chế phục hồi; trong quá trình chuẩn bị cho Prime Day 2024, Amazon.com đã chạy 733 thí nghiệm dựa trên FIS
• Trong các lĩnh vực mà ranh giới bảo mật và tối ưu hóa hiệu năng là quan trọng, như Cedar, Firecracker và tối ưu hóa RSA trên Graviton 2, chứng minh hình thức được sử dụng; đường cong học tập cao và khả năng tiếp cận công cụ vẫn là rào cản đối với việc áp dụng

---

Cách AWS xử lý tính đúng đắn của hệ thống

• Để cung cấp các dịch vụ mà khách hàng có thể tin cậy, AWS phải duy trì các tiêu chuẩn cao về bảo mật, độ bền, tính toàn vẹn và tính sẵn sàng, và tính đúng đắn của hệ thống là nền tảng hỗ trợ điều đó
• Bài viết “How Amazon Web Services Uses Formal Methods” trên CACM năm 2015 đã giới thiệu cách tiếp cận nhằm bảo đảm tính đúng đắn của các dịch vụ cốt lõi của AWS; kể từ đó, các dịch vụ này đã được khách hàng AWS sử dụng rộng rãi
• Công cụ trọng tâm ban đầu là ngôn ngữ đặc tả hình thức TLA+ do Leslie Lamport phát triển
  • Giúp phát hiện và loại bỏ sớm trong quá trình phát triển các lỗi tinh vi mà kiểm thử truyền thống có thể bỏ sót
  • Mang lại sự tự tin rằng có thể triển khai các tối ưu hóa hiệu năng mạnh tay trong khi vẫn duy trì tính đúng đắn của hệ thống
• 15 năm trước, thực hành kiểm thử của AWS chủ yếu dựa vào kiểm thử đơn vị tại thời điểm build và kiểm thử tích hợp hạn chế tại thời điểm triển khai
• Sau đó, AWS đã tích hợp các kỹ thuật hình thức và bán hình thức vào quy trình phát triển
  • Chứng minh định lý, xác minh diễn dịch, kiểm chứng mô hình
  • Kiểm thử dựa trên thuộc tính, fuzzing, giám sát runtime

Ngôn ngữ lập trình P và PObserve

• Khi AWS mở rộng các kỹ thuật hình thức ra ngoài các nhóm ban đầu vào đầu thập niên 2010, họ nhận thấy nhiều kỹ sư gặp khó khăn trong việc học TLA+ và đạt năng suất với nó
• Điểm mạnh của TLA+ là một ngôn ngữ trừu tượng cấp cao gần với toán học, nhưng điều này lại tạo rào cản tiếp cận cho các nhà phát triển quen với ngôn ngữ mệnh lệnh
• Ngôn ngữ P, dựa trên máy trạng thái để mô hình hóa và phân tích hệ thống phân tán, đóng vai trò thu hẹp khoảng cách này
  • Nhà phát triển mô hình hóa thiết kế hệ thống dưới dạng các máy trạng thái giao tiếp với nhau
  • Mô hình tư duy này quen thuộc với các nhà phát triển Amazon thường làm việc nhiều với microservice và kiến trúc hướng dịch vụ (SOA)
  • P được phát triển tại AWS từ năm 2019 và được duy trì như một dự án nguồn mở chiến lược
• Nhiều nhóm sản phẩm tiêu biểu của AWS sử dụng P để rà soát tính đúng đắn trong thiết kế hệ thống
  • Lưu trữ: Amazon S3, EBS
  • Cơ sở dữ liệu: Amazon DynamoDB, MemoryDB, Aurora
  • Điện toán: EC2, IoT
• S3 đã sử dụng P trong quá trình chuyển từ eventual consistency sang strong read-after-write consistency
  • Phân hệ chỉ mục của S3 là kho lưu trữ metadata đối tượng cho phép tra cứu dữ liệu nhanh
  • Để đạt được tính nhất quán mạnh, cần nhiều thay đổi không tầm thường trong stack giao thức chỉ mục của S3
  • P cho phép mô hình hóa và xác minh hình thức thiết kế giao thức, loại bỏ sớm các lỗi ở cấp thiết kế và dùng kiểm chứng mô hình để xác nhận các tối ưu hóa rủi ro
• Năm 2023, nhóm AWS P xây dựng PObserve
  • Sử dụng log có cấu trúc sinh ra từ quá trình thực thi hệ thống phân tán
  • Xác minh hậu nghiệm rằng log khớp với các hành vi được đặc tả P hình thức của hệ thống cho phép
  • Thu hẹp khoảng cách giữa triển khai production viết bằng các ngôn ngữ như Rust hoặc Java và đặc tả P tại thời điểm thiết kế
  • Kết nối xác minh tại thời điểm thiết kế với giám sát runtime của triển khai, qua đó tăng giá trị đầu tư vào đặc tả hình thức

Cách gắn các kỹ thuật hình thức nhẹ vào luồng phát triển

• AWS đưa vào các kỹ thuật hình thức nhẹ để đưa kỹ thuật hình thức đến gần hơn với luồng phát triển và kiểm thử của các nhóm kỹ thuật

• Kiểm thử dựa trên thuộc tính

  • ShardStore của Amazon S3 sử dụng kiểm thử dựa trên thuộc tính trong suốt chu kỳ phát triển để kiểm thử tính đúng đắn và cải thiện tốc độ phát triển
  • Kết hợp nhiều kỹ thuật để con người đặc tả hành vi kỳ vọng, còn kiểm thử tự động khám phá nhiều đầu vào và điều kiện lỗi hơn
    • Đặc tả tính đúng đắn do nhà phát triển cung cấp
    • Fuzzing có hướng dẫn bằng độ bao phủ, dùng chỉ số code coverage để dẫn dắt phân phối đầu vào
    • Chèn lỗi để mô phỏng lỗi phần cứng và các lỗi hệ thống khác trong quá trình kiểm thử
    • Thu nhỏ tự động các phản ví dụ để con người dễ debug hơn

• Mô phỏng tất định

  • Kiểm thử bằng mô phỏng tất định chạy hệ thống phân tán trong trình mô phỏng đơn luồng và kiểm soát mọi nguồn ngẫu nhiên
    • Lập lịch thread
    • Timing
    • Thứ tự truyền thông điệp
  • Nhà phát triển có thể viết các kịch bản thất bại/thành công cụ thể, chẳng hạn một participant bị lỗi ở một giai đoạn cụ thể của giao thức phân tán
  • Vì framework kiểm thử kiểm soát tính bất định, có thể chỉ định các thứ tự thực thi thú vị, như thứ tự từng gây ra lỗi trong quá khứ
  • Scheduler có thể được mở rộng sang fuzzing thứ tự hoặc khám phá mọi thứ tự có thể
  • Đưa kiểm thử thuộc tính hệ thống trong các tình huống trễ và lỗi đến gần thời điểm build hơn so với kiểm thử tích hợp, giúp tăng tốc phát triển và mở rộng độ bao phủ hành vi
  • Một phần công việc kiểm thử tại thời điểm build của AWS về thứ tự thread và lỗi hệ thống đã được mở nguồn dưới dạng các dự án shuttle và turmoil

• Fuzzing liên tục và sinh đầu vào kiểm thử ngẫu nhiên

  • Fuzzing liên tục, đặc biệt là sinh đầu vào kiểm thử có khả năng mở rộng dựa trên hướng dẫn độ bao phủ, rất hiệu quả cho kiểm thử tính đúng đắn của hệ thống tại thời điểm tích hợp
  • Trong quá trình phát triển Aurora Limitless Database, tính năng sharding dữ liệu của Amazon Aurora, fuzzing được sử dụng rộng rãi để xác minh hai thuộc tính cốt lõi
  • Fuzzing các truy vấn SQL và toàn bộ giao dịch để xác minh logic phân tách thực thi SQL trên các shard là đúng
  • Tổng hợp lượng lớn schema SQL, dataset và truy vấn ngẫu nhiên để chạy trên engine cần kiểm thử, rồi so sánh kết quả với oracle dựa trên engine không sharding
  • Cũng sử dụng các phương pháp xác minh khác như cách tiếp cận do SQLancer tiên phong
  • Sự kết hợp giữa fuzzing và kiểm thử chèn lỗi cũng hữu ích cho các khía cạnh đúng đắn của cơ sở dữ liệu như tính nguyên tử, tính nhất quán và tính cô lập
    • Tự động sinh giao dịch
    • Định nghĩa hành vi đúng bằng oracle tính đúng đắn được đặc tả hình thức
    • Thực thi trên hệ thống cần kiểm thử các khả năng interleaving của giao dịch và các câu lệnh bên trong giao dịch
    • Xác minh hậu nghiệm các thuộc tính như tính cô lập theo các cách tiếp cận như Elle

Fault Injection Service và xác minh tình huống sự cố

• Đầu năm 2021, AWS ra mắt Fault Injection Service(FIS), đưa kiểm thử dựa trên chèn lỗi đến với nhiều khách hàng AWS
• FIS có thể chèn các sự cố mô phỏng vào các deployment kiểm thử hoặc production trên hạ tầng AWS
  • Lỗi API
  • Tạm dừng I/O
  • Instance bị lỗi
• Chèn lỗi giúp xác nhận rằng các cơ chế phục hồi được xây dựng trong kiến trúc thực sự cải thiện tính sẵn sàng và không tạo ra vấn đề đúng đắn mới
  • Failover
  • Health check
• Kiểm thử chèn lỗi dựa trên FIS được sử dụng rộng rãi bởi khách hàng AWS và trong nội bộ Amazon
• Trong quá trình chuẩn bị cho Prime Day 2024, Amazon.com đã chạy 733 thí nghiệm chèn lỗi dựa trên FIS
• Năm 2014, Yuan và cộng sự phân tích rằng 92% sự cố nghiêm trọng trong các hệ thống phân tán được kiểm thử bắt nguồn từ việc xử lý sai các lỗi không nghiêm trọng
• Lý do sự cố nghiêm trọng trên đường đi bình thường hiếm gặp là đường đi bình thường được thực thi thường xuyên, được kiểm thử tốt hơn và đơn giản hơn nhiều so với đường đi lỗi
• Kiểm thử chèn lỗi và FIS giúp dễ kiểm thử hơn hành vi hệ thống trong các tình huống sự cố và thất bại, qua đó thu hẹp khoảng cách mật độ lỗi giữa đường đi bình thường và đường đi lỗi
• Bản thân chèn lỗi không được xem là kỹ thuật hình thức, nhưng có thể kết hợp với đặc tả hình thức
  • Định nghĩa hành vi kỳ vọng bằng đặc tả hình thức
  • So sánh kết quả trong và sau khi chèn lỗi với hành vi đã đặc tả
  • Có thể bắt được nhiều lỗi hơn so với chỉ kiểm tra chỉ số, lỗi log hoặc để con người đánh giá bằng mắt

Tính bán ổn định và hành vi hệ thống nổi lên

• Trong 10 năm gần đây, sự quan tâm đến một lớp lỗi hệ thống cụ thể là lỗi bán ổn định (metastable failures) đã tăng lên
• Lỗi bán ổn định là loại lỗi trong đó một tác nhân kích hoạt như quá tải hoặc xóa sạch cache đẩy hệ thống phân tán vào trạng thái không thể phục hồi nếu không có can thiệp
  • Ví dụ can thiệp là giảm tải xuống thấp hơn mức bình thường
• Lớp lỗi này là một trong những yếu tố đóng góp quan trọng vào tình trạng không sẵn sàng của hệ thống cloud
• Trong hành vi bán ổn định điển hình, khi tải tăng, goodput ban đầu tăng rồi bão hòa, sau đó đi qua trạng thái tắc nghẽn và goodput giảm về 0 hoặc gần 0
• Sau đó, hệ thống không thể quay lại trạng thái khỏe mạnh chỉ bằng cách giảm tải một chút; cần giảm tải rất mạnh để phục hồi
• Hành vi này có thể xuất hiện ngay cả trong các hệ thống đơn giản, và trong hầu hết hệ thống cũng có thể bị kích hoạt bởi logic client retry sau timeout
• Mô hình hóa hình thức hệ thống phân tán truyền thống thường tập trung vào safety và liveness, nhưng lỗi bán ổn định cho thấy có những hành vi không nằm gọn trong phân loại này
• AWS sử dụng ngày càng nhiều mô phỏng sự kiện rời rạc để hiểu hành vi hệ thống nổi lên
  • Đầu tư vào mô phỏng hệ thống tùy chỉnh
  • Đầu tư vào các công cụ có thể dùng các mô hình hệ thống hiện có được tạo bằng các ngôn ngữ như TLA+ và P cho mô phỏng
• Nếu mở rộng trình kiểm chứng mô hình duyệt toàn bộ như TLC của TLA+ thành mô phỏng xác suất, có thể tạo ra các kết quả thống kê như phân phối độ trễ hậu nghiệm
• Các mở rộng như vậy cho phép tận dụng kiểm chứng mô hình cho những việc như hiểu khả năng đạt SLA về độ trễ

Ranh giới bảo mật cần chứng minh hình thức

• Với các ranh giới bảo mật quan trọng như phân quyền và ảo hóa, các kỹ thuật hình thức nêu trên có thể chưa đủ; chứng minh tính đúng đắn có giá trị đầu tư lớn

• Ngôn ngữ chính sách phân quyền Cedar

  • Năm 2023, AWS giới thiệu ngôn ngữ chính sách phân quyền Cedar để viết các chính sách chỉ định quyền chi tiết
  • Cedar được thiết kế với suy luận tự động và chứng minh hình thức trong tâm trí
  • Phần triển khai được xây dựng bằng ngôn ngữ lập trình thân thiện với xác minh Dafny
  • Thông qua Dafny, nhóm chứng minh rằng triển khai thỏa mãn nhiều thuộc tính bảo mật
  • Chứng minh này là chứng minh theo nghĩa toán học, vượt xa kiểm thử
  • Nhóm cũng áp dụng kiểm thử vi sai, dùng mã Dafny làm oracle tính đúng đắn để xác minh tính đúng đắn của triển khai Rust sẵn sàng cho production
  • Cùng với triển khai Cedar, mã Dafny và quy trình kiểm thử được công bố mã nguồn mở để người dùng có thể kiểm tra công việc về tính đúng đắn

• Firecracker VMM

  • Trình giám sát máy ảo Firecracker sử dụng giao thức cấp thấp virtio để phơi bày các thiết bị phần cứng được giả lập như card mạng hoặc SSD cho kernel khách bên trong VM
  • Các thiết bị giả lập này là tương tác phức tạp nhất giữa guest không đáng tin cậy và host được tin cậy, nên là ranh giới bảo mật quan trọng
  • Nhóm Firecracker dùng Kani, công cụ có thể suy luận hình thức về mã Rust, để chứng minh các thuộc tính cốt lõi của ranh giới bảo mật này
  • Chứng minh này bảo đảm rằng bất kể guest cố gắng làm gì, các thuộc tính quan trọng của ranh giới vẫn được duy trì
  • AWS hỗ trợ phát triển các công cụ nền tảng như Kani, Dafny, Lean và các SMT solver vận hành chúng
  • Mô hình và đặc tả hình thức được tái sử dụng theo nhiều cách
    • Kiểm chứng mô hình tại thời điểm thiết kế
    • Đóng vai trò oracle tính đúng đắn trong giám sát runtime
    • Mô phỏng hành vi hệ thống nổi lên
    • Xây dựng chứng minh cho các thuộc tính cốt lõi

Hiệu năng và hiệu quả chi phí vượt ra ngoài tính đúng đắn

• Kỹ thuật hình thức cũng quan trọng trong việc cải thiện hiệu năng hệ thống cloud một cách an toàn
• Khi mô hình hóa giao thức commit cốt lõi của engine cơ sở dữ liệu quan hệ Aurora bằng P và TLA+, nhóm tìm thấy cơ hội giảm chi phí commit phân tán từ 2 lượt khứ hồi mạng xuống 1,5 lượt khứ hồi mạng mà không hy sinh các thuộc tính an toàn
• Những kết quả như vậy thường gặp ở các nhóm áp dụng kỹ thuật hình thức
  • Quá trình suy nghĩ sâu về giao thức phân tán và viết nó một cách hình thức buộc tư duy phải có cấu trúc
  • Mang lại hiểu biết sâu hơn về cấu trúc giao thức và vấn đề cần giải quyết
  • Khi có thể xác nhận hoặc chứng minh hình thức rằng một tối ưu hóa thiết kế được đề xuất là đúng, kỹ sư hệ thống phân tán có thể chọn các thiết kế táo bạo hơn mà không tăng rủi ro
• Năng suất và hiệu quả chi phí không chỉ giới hạn ở tối ưu hóa thiết kế cấp cao
• Nhóm AWS đã tìm ra tối ưu hóa cho triển khai mã hóa khóa công khai RSA trên bộ xử lý ARM Graviton 2, cải thiện throughput tới 94%
• Họ dùng trình chứng minh định lý tương tác HOL Light để chứng minh tính đúng đắn của tối ưu hóa này
• Vì một tỷ lệ lớn chu kỳ CPU trên cloud được dùng cho mã hóa, các tối ưu hóa như vậy có thể góp phần giảm chi phí hạ tầng, hỗ trợ tính bền vững và cải thiện hiệu năng mà khách hàng cảm nhận được

Các thách thức còn lại và cơ hội tương lai

• Trong 15 năm qua, AWS đã thành công trong việc mở rộng các phương pháp kiểm thử hình thức và bán hình thức, nhưng việc áp dụng trong công nghiệp vẫn còn nhiều thách thức
• Rào cản chính của các công cụ kỹ thuật hình thức là đường cong học tập dốc và yêu cầu kiến thức miền chuyên sâu
• Nhiều công cụ vẫn mang tính học thuật và thiếu giao diện thân thiện với người dùng
• Ngay cả các cách tiếp cận bán hình thức đã ổn định cũng vẫn có rào cản áp dụng
  • Mô phỏng tất định là kỹ thuật kiểm thử hệ thống phân tán cốt lõi đã được dùng thành công tại AWS và các dự án như FoundationDB, nhưng đôi khi vẫn xa lạ ngay cả với các nhà phát triển hệ thống phân tán giàu kinh nghiệm khi gia nhập AWS
  • Khoảng cách tương tự cũng tồn tại trong các phương pháp luận đã được chứng minh như kiểm thử chèn lỗi, kiểm thử dựa trên thuộc tính và fuzzing
• Cần đào tạo các nhà phát triển hệ thống phân tán về những phương pháp và công cụ kiểm thử này, đồng thời dạy cách tư duy nghiêm ngặt
• Khoảng cách giáo dục bắt đầu từ cấp học thuật
  • Ngay cả các cách tiếp cận suy luận hình thức cơ bản cũng hiếm khi được giảng dạy
  • Ngay cả sinh viên tốt nghiệp từ các cơ sở hàng đầu cũng gặp khó khi áp dụng những công cụ này
  • Kỹ thuật hình thức và suy luận tự động quan trọng đối với ứng dụng công nghiệp, nhưng vẫn bị xem là lĩnh vực ngách
• Tính bán ổn định và các thuộc tính nổi lên khác của hệ thống quy mô lớn cũng là lĩnh vực nghiên cứu quan trọng với thách thức nhận thức tương tự
  • Các thực hành có thể gây ra hành vi hệ thống bán ổn định, như “retry N lần khi timeout”, vẫn tiếp tục được khuyến nghị rộng rãi dù vấn đề đã được biết đến
  • Các công cụ và kỹ thuật hiện nay để hiểu hành vi hệ thống nổi lên vẫn ở giai đoạn đầu
  • Mô hình hóa độ ổn định hệ thống tốn kém và phức tạp
• AWS cho rằng mô hình ngôn ngữ lớn và AI assistant sẽ giúp đáng kể trong việc giảm bớt vấn đề áp dụng kỹ thuật hình thức vào thực tế
  • Tương tự như kiểm thử đơn vị có AI hỗ trợ đang trở nên phổ biến, chúng có thể giúp nhà phát triển tạo mô hình và đặc tả hình thức
  • Các kỹ thuật nâng cao có thể trở nên dễ tiếp cận hơn với cộng đồng nhà phát triển rộng lớn hơn

Hệ thống tính đúng đắn mà AWS tiếp tục đầu tư

• Để xây dựng phần mềm đáng tin cậy và an toàn, cần nhiều cách tiếp cận khác nhau để suy luận về tính đúng đắn của hệ thống
• AWS áp dụng nhiều kỹ thuật cùng với các kiểm thử tiêu chuẩn trong ngành như kiểm thử đơn vị và kiểm thử tích hợp
  • Kiểm chứng mô hình
  • Fuzzing
  • Kiểm thử dựa trên thuộc tính
  • Kiểm thử chèn lỗi
  • Mô phỏng tất định
  • Mô phỏng dựa trên sự kiện
  • Xác minh runtime của dấu vết thực thi
• Đặc tả hình thức đóng vai trò quan trọng như test oracle cung cấp câu trả lời đúng trong nhiều thực hành kiểm thử của AWS
• Kiểm thử tính đúng đắn và kỹ thuật hình thức vẫn là lĩnh vực đầu tư cốt lõi của AWS, dựa trên lợi tức đầu tư đã đạt được