Phát hiện lỗi chưa từng được tài liệu hóa trong mã máy tính dẫn đường Apollo 11

• Một lỗi thiếu giải phóng khóa tài nguyên đã được phát hiện trong mã Apollo Guidance Computer (AGC), vốn được xem là gần như hoàn hảo suốt 57 năm
• Nhóm JUXT đã dùng ngôn ngữ đặc tả AI Allium và Claude để phân tích 130.000 dòng assembly, từ đó xác định một khiếm khuyết mà các phương pháp kiểm chứng trước đây không làm lộ ra
• Ở đường thoát bất thường (BADEND) của routine điều khiển con quay, khóa LGYRO không được giải phóng, tạo ra cấu trúc có thể khiến toàn bộ chức năng liên quan đến con quay về sau bị dừng lại
• Nếu trong nhiệm vụ thực tế ở quỹ đạo Mặt Trăng, công tắc Cage bị nhấn nhầm, thao tác căn chỉnh Program 52 có thể bị gián đoạn và Collins có thể hiểu nhầm đó là lỗi phần cứng
• Trường hợp này cho thấy phân tích dựa trên đặc tả hành vi là một phương pháp mạnh để tìm ra lỗi mới ngay cả trong mã cũ

---

Khiếm khuyết tiềm ẩn được phát hiện trong máy tính dẫn đường Apollo 11

• Apollo Guidance Computer (AGC) là một trong những codebase được xem xét kỹ lưỡng nhất trong lịch sử, đã được rất nhiều nhà phát triển và nhà nghiên cứu phân tích
  • Tuy vậy, một lỗi thiếu khóa tài nguyên chưa từng được phát hiện suốt 57 năm đã được xác nhận trong mã điều khiển con quay
  • Ở nhánh lỗi, khóa không được giải phóng, khiến chức năng căn chỉnh lại nền tảng dẫn đường bị vô hiệu hóa
• Nhóm JUXT đã dùng ngôn ngữ đặc tả dựa trên AI Allium và Claude để chuyển 130.000 dòng assembly của AGC thành 12.500 dòng đặc tả hành vi
  • Trích xuất đặc tả trực tiếp từ mã để mô hình hóa mọi đường đi của việc cấp phát và giải phóng tài nguyên
  • Trong quá trình này, một lỗi không lộ ra khi chỉ đọc mã hoặc mô phỏng đã được phát hiện

Cấu trúc mã và cách tiếp cận phân tích

• Mã nguồn AGC được công bố vào năm 2003 khi Ron Burkey và các tình nguyện viên chép tay lại bản in từ MIT Instrumentation Laboratory
  • Năm 2016, kho lưu trữ GitHub của Chris Garry được công khai, giúp các nhà phát triển toàn thế giới nghiên cứu mã assembly chạy trên RAM 2KB và CPU 1MHz
• Chương trình được lưu trong core rope memory dung lượng 74KB, nơi dây đồng được đan thủ công qua các lõi từ để biểu diễn 1 và 0
  • Những nữ kỹ thuật viên thực hiện công việc này được gọi là “Little Old Ladies”, và bộ nhớ này được đặt tên là LOL memory
• Cho đến nay, không có ghi nhận nào về việc AGC từng được áp dụng kiểm chứng hình thức, model checking hoặc phân tích tĩnh
  • Phần lớn việc kiểm chứng tập trung vào đọc mã, mô phỏng và xác nhận độ chính xác của bản chép lại
• JUXT đã viết đặc tả hành vi của phân hệ IMU (Inertial Measurement Unit) bằng Allium
  • Mô hình hóa thời điểm cấp phát và giải phóng của từng tài nguyên dùng chung để nhận diện lỗi

Thiếu giải phóng khóa trong routine điều khiển con quay

• AGC quản lý IMU bằng một khóa dùng chung có tên LGYRO
  • Khi tác động mô-men lên con quay, hệ thống lấy khóa, và chỉ giải phóng sau khi hoàn tất cả ba trục
  • Điều này ngăn hai routine thao tác phần cứng cùng lúc
• Tuy nhiên, ở đường thoát bất thường, khóa lại không được giải phóng
  • Khi kết thúc bình thường, routine STRTGYR2 sẽ giải phóng LGYRO, nhưng nếu xảy ra “Caging” (khóa vật lý để bảo vệ con quay), luồng sẽ rẽ sang routine BADEND
  • Trong BADEND, thiếu hai lệnh CAF ZERO và TS LGYRO (tổng cộng 4 byte), nên khóa vẫn bị giữ lại
• Nếu LGYRO không được giải phóng, mọi routine mô-men con quay về sau sẽ bị treo ở trạng thái chờ khóa
  • Căn chỉnh tinh, bù trôi và mô-men thủ công, tức toàn bộ chức năng liên quan đến con quay, đều sẽ bị dừng

Tác động tiềm ẩn ở mặt khuất của Mặt Trăng

• Ngày 21/7/1969, Michael Collins đã định kỳ chạy Program 52 (chương trình căn chỉnh quan sát sao) khi ở quỹ đạo Mặt Trăng
  • Nếu nền tảng bị trôi, hướng của động cơ hồi quyển có thể bị sai lệch
• Nếu trong lúc tạo mô-men mà công tắc Cage bị nhấn nhầm và luồng rơi vào BADEND, LGYRO có thể không được giải phóng, khiến mọi lần chạy P52 sau đó bị treo
  • DSKY (màn hình và bàn phím) vẫn nhận đầu vào nhưng không phản hồi
  • Các chức năng khác vẫn hoạt động bình thường, nên Collins có thể hiểu nhầm là lỗi phần cứng
• Nếu thực hiện khởi động lại (hard reset), vấn đề có thể đã được giải quyết, nhưng với kinh nghiệm từ cảnh báo 1202 trong lúc hạ cánh xuống Mặt Trăng, việc quyết định reset ngay lập tức hẳn không dễ dàng

Thiết kế phòng thủ của hệ thống cũ và giới hạn của nó

• Nhóm MIT do Margaret Hamilton dẫn dắt đã đưa vào các khái niệm nền tảng của kỹ thuật phần mềm hiện đại như lập lịch ưu tiên, đa nhiệm bất đồng bộ và bảo vệ khi khởi động lại
  • Nhờ thiết kế đó, tàu vẫn có thể hạ cánh ngay cả khi xuất hiện cảnh báo 1202
• Phần lớn các lỗi lớn là lỗi đặc tả, và như trường hợp Don Eyles từng ghi lại, đã có lúc tải CPU tăng lên do thiếu đồng bộ pha giữa các phần cứng
• Khiếm khuyết lần này cũng có cấu trúc tương tự
  • BADEND là routine kết thúc chung cho chuyển đổi chế độ IMU, nên có giải phóng các tài nguyên dùng chung như MODECADR, nhưng không xử lý LGYRO
  • Vì logic khởi động lại có đặt lại LGYRO, lỗi được che giấu trong quá trình kiểm thử khi hệ thống phục hồi bình thường
• Tuy nhiên, trong tình huống thực tế không có khởi động lại, con quay có thể bị kẹt vĩnh viễn trong trạng thái khóa

Quá trình phát hiện lỗi bằng Allium

• Đặc tả Allium mô hình hóa vòng đời (lifecycle) của từng tài nguyên
  • Trường gyros_busy biểu diễn LGYRO, quy tắc GyroTorque định nghĩa việc lấy khóa, còn quy tắc GyroTorqueBusy định nghĩa trạng thái chờ khi khóa đã bị giữ
• Đặc tả nêu rõ nghĩa vụ rằng “khi khóa trở thành true thì cuối cùng phải quay về false”
  • Sau khi Claude lần theo mọi đường đi, kết quả cho thấy ở đường bình thường (STRTGYR2) khóa được giải phóng, nhưng ở đường lỗi (BADEND) thì bị bỏ sót
• Cách tiếp cận dựa trên đặc tả kiểm chứng không phải mã đang làm gì, mà là đáng lẽ phải làm gì
  • Kiểm thử xác nhận hành vi hiện tại của mã, còn đặc tả kiểm chứng hành vi dự định
• Đặc tả Allium và mã tái hiện lỗi đã được công bố trên GitHub

Hàm ý hiện đại và bài học rút ra

• Khi đó, các lập trình viên phải giải phóng khóa thủ công bằng các lệnh CAF ZERO và TS LGYRO
  • Họ phải nhớ mọi đường đi và tự chèn mã giải phóng trên từng nhánh
• Các ngôn ngữ hiện đại ngăn chặn dạng rò rỉ tài nguyên này theo cách có cấu trúc
  • defer của Go, try-with-resources của Java, with của Python và hệ thống ownership của Rust đều bảo đảm việc giải phóng tự động
• Dù vậy, lỗi kiểu CWE-772 (thiếu giải phóng tài nguyên) vẫn tiếp tục tồn tại
  • Kết nối cơ sở dữ liệu, khóa phân tán, file handle và thứ tự shutdown của hạ tầng vẫn là trách nhiệm của lập trình viên
• Dù mọi nhiệm vụ Apollo đều quay về thành công, khiếm khuyết này vẫn tiếp tục tồn tại nguyên vẹn trong phần mềm COMANCHE (tàu chỉ huy) và LUMINARY (tàu đổ bộ Mặt Trăng) về sau mà không được sửa
• Lỗi bị che giấu suốt 57 năm này là một ví dụ cho thấy tầm quan trọng của phân tích dựa trên đặc tả hành vi

[GN⁺]

Ý kiến trên Hacker News

• Tôi là Mike Stewart, người dẫn dắt dự án phục dựng AGC trên kênh CuriousMarc và là đồng quản trị viên của VirtualAGC
  Lỗi được nhắc đến lần này đúng là một khiếm khuyết trong phần mềm AGC từng tồn tại ngoài đời thực. Tuy nhiên, nó không bị bỏ mặc suốt toàn bộ vòng đời chương trình. Nó được phát hiện trong giai đoạn thử nghiệm 3 của SATANCHE, được ghi nhận là L-1D-02, và đã được sửa trong khoảng giữa Apollo 14 và 15
  Có thể xem các báo cáo liên quan tại tài liệu ibiblio 1 và tài liệu 2
  Bản sửa không chỉ đơn giản là thêm hai dòng đặt LGYRO về 0, mà còn bao gồm cả tái cấu trúc mã và logic đánh thức các tác vụ đang chờ. Nếu so sánh mã của Apollo 14 và 15 (mã Apollo 14, mã Apollo 15) thì có thể thấy sự khác biệt
  Đây cũng không phải là kiểu lỗi âm thầm xảy ra như bài báo mô tả. LGYRO còn được khởi tạo trong STARTSB2, và đoạn này chạy mỗi lần chuyển chương trình nên sẽ tự động giải quyết vấn đề. Vì vậy, trên thực tế nó chỉ hiếm khi xảy ra khi thực hiện thao tác torque trong BADEND
  Nếu lỗi kéo dài, nhiều tác vụ sẽ chồng chất lên nhau và cuối cùng gây ra lỗi 31202 (phiên bản tiếp theo của 1202). Vấn đề này đã được phát hiện trước chuyến bay Apollo 14, và quy trình khôi phục đã được thêm vào Apollo 14 Program Notes
  Ngoài ra, dù Ken Shirriff được nói là đã phân tích ở mức cổng logic, trên thực tế phần lớn công việc đó là do tôi thực hiện
  Virtual AGC mới chỉ hoàn tất xác minh khớp từng byte với bản dump core rope gốc cho một số chương trình; với toàn bộ chương trình thì hiện vẫn chưa thể. Phần lớn mã nguồn được phục dựng từ bản in hoặc checksum
  Margaret Hamilton là “rope mother” của Comanche (phần mềm module chỉ huy), còn Luminary (module đổ bộ Mặt Trăng) do Jim Kernan phụ trách. Có thể xác nhận điều này trong sơ đồ tổ chức năm 1969
  Vào thời điểm báo động 1202, AGC không được thiết kế để loại bỏ các tác vụ ưu tiên thấp. Ngược lại, dẫn đường hạ cánh lại là tác vụ có ưu tiên thấp nhất, còn điều khiển ăng-ten và cập nhật hiển thị có ưu tiên cao hơn. Tài liệu này có tổng hợp mức ưu tiên của từng tác vụ
  Cuối cùng, nguyên nhân của báo động 1202 không phải là chênh lệch pha mà là chênh lệch điện áp (28V so với 15V), điều đã được xác nhận qua thử nghiệm phần cứng thực tế. Có thể xem video thí nghiệm liên quan tại liên kết YouTube

  • Tôi đã chờ bình luận của bạn. Cảm ơn vì đã chia sẻ những chi tiết lịch sử thực sự đáng kinh ngạc
  • Trang chủ đã chuyển sang chủ đề khác rồi, nhưng nội dung này thật sự là kho thông tin quý giá. Cảm ơn bạn đã dành thời gian

• Nếu bạn quan tâm đến Apollo AGC thì rất nên xem kênh YouTube CuriousMarc. Một đội ngũ cực kỳ giỏi về kỹ thuật đã ghi lại quá trình phục dựng và phân tích nhiều thành phần của AGC
  Phần đặc biệt thú vị là cách diễn giải lại báo động 1202 khét tiếng. Thường thì nó được biết đến như một lỗi cảm biến có thể bỏ qua, nhưng trên thực tế trong một số điều kiện nhất định nó có thể cực kỳ nghiêm trọng

  • Vì thế có thể nói rằng ngày nay việc thử lại cùng một cuộc hạ cánh đó sẽ khó hơn hoặc dễ hơn. Bởi vì giờ chúng ta biết nhiều chế độ lỗi hơn rất nhiều so với khi ấy
  • “Điều được giải thích cho công chúng” và “điều thực sự được hiểu” là khác nhau. Có rất nhiều lời giải thích giản lược, nhưng trong giới chuyên môn thì đây vốn đã là hiện tượng được hiểu khá rõ
  • Cuộc thảo luận của nhóm CuriousMarc về việc phục dựng AGC cũng tiếp tục trong chuỗi này

• Đoạn mã tôi thích nhất là thế này

  TC  BANKCALL  # TEMPORARY, I HOPE HOPE HOPE
  CADR STOPRATE  # TEMPORARY, I HOPE HOPE HOPE
  TC  DOWNFLAG  # PERMIT X-AXIS OVERRIDE
  

  Liên kết GitHub

  • Đoạn mã này cũng được nhắc đến trong The Codeless Code
  • Ở đây CADR không liên quan đến hàm cadr của Lisp
  • Có ai có thể giải thích vì sao đoạn mã này lại thú vị không?
  • Tôi nhớ là trước đây từng thấy một bài thơ trên XKCD về đoạn mã này, dù có thể là tôi nhớ nhầm

• Tôi tò mò không biết lỗi này đã từng được kiểm chứng là thực sự tồn tại hay chưa. AI mạnh ở kiểu phân tích thăm dò như thế này, nhưng vẫn có tỷ lệ dương tính giả cao
  Tùy ngữ cảnh mà nó có thể quan trọng hoặc không. Cũng có rất nhiều lỗi mà AI không tìm ra
  Tôi không đủ chuyên môn để tự xác minh, nhưng thấy rất thú vị

  • Thực ra cũng chưa rõ liệu AI có thật sự tìm ra lỗi hay không. Bài chỉ nói rằng họ “mô hình hóa bằng ngôn ngữ native của AI”
    Dù vậy, phần mô tả việc giành lock và các kịch bản lỗi nghe khá thuyết phục

• Việc họ thực sự tìm ra một lỗi có thật là điều thú vị. Nhưng cách dàn dựng kịch tính của bài viết thì gần như hư cấu
  Kiểu như vô tình gạt công tắc bằng khuỷu tay, hay phóng đại một vấn đề vốn có thể giải quyết bằng reset. Những điểm đó khiến bài viết giật gân hơn nhưng cũng kém đáng tin hơn. Thêm nữa, nó còn mang văn phong như do AI viết, nên càng khó chịu

  • Tất nhiên đó là công tắc có nắp bảo vệ.
    Nhưng để giải thích một lỗi tinh vi cho độc giả phổ thông thì cũng cần một mức độ kể chuyện nhất định. Quá kỹ thuật thì họ sẽ mất hứng, còn quá kịch tính thì chuyên gia sẽ chỉ trích. Theo tôi, rất khó để giữ được sự cân bằng đó

• Tôi đã tự chạy mã tái hiện lỗi (repro) được đưa trong bài
  Liên kết GitHub
  Nó có chạy, nhưng Phase 5 (minh họa deadlock) hoàn toàn là đầu ra giả. Nó không chạy trình giả lập thật mà chỉ in ra kết quả dự kiến
  Vì vậy tôi đã gửi một PR tự sửa, để nó thực sự hoạt động trên trình giả lập và cũng xác minh rằng bản vá hai dòng đúng là sửa được lỗi

  • Tôi thường xuyên thấy kiểu “mã AI” như thế này. Nó bắt chước phát triển hướng kiểm thử, nhưng thực chất lại tạo ra mã giả chỉ để vượt qua test
    Mã do AI sinh ra có xu hướng dừng lại ở câu “giờ thì hoàn hảo rồi!”, và có người tin như vậy rồi đem phát hành nguyên xi. Đó mới là vấn đề thật sự

• Bản thân bài viết thì thú vị, nhưng có cảm giác nhân tạo như do LLM viết rất rõ

  • Với tôi thì hoàn toàn không có cảm giác LLM. Chắc là vì nó mang phong cách bài báo khoa học
  • Juxt từ trước đến nay vẫn viết rất tốt và có chuyên môn đủ sâu. Vì vậy tôi cho rằng khả năng bài này do AI viết là thấp
  • Tham khảo phân tích Pangram, bài này được đánh giá là do con người viết
  • Nhưng một bài khác của Juxt thì thực sự có ghi rõ là do Claude viết. Họ nói điều đó ở đoạn cuối của bài này
  • Hơn nữa, phần nói về Rust và lock cũng không đúng với thực tế. Điều này được chỉ ra trong bình luận này

• Việc ngay cả phần mềm đưa con người lên Mặt Trăng chỉ với 4KB bộ nhớ mà vẫn còn lỗi chưa được phát hiện cho thấy ngay cả mã nhỏ cũng có thể ẩn chứa độ phức tạp

  • Càng ít bộ nhớ thì mối tương quan giữa độ dài mã và tỷ lệ lỗi càng yếu. Thậm chí, việc cố nén độ phức tạp còn có thể làm tăng số lỗi
  • Câu đó nghe chỉ như một sáo ngữ rỗng tuếch

• Cách nói “rút ra đặc tả từ mã” là sai. Có lẽ cần tra lại ý nghĩa của specification

  • Thực ra đó đơn giản chỉ là reverse engineering

• Cả bài viết lẫn kho chứa đều là sản phẩm chất lượng thấp, làm cẩu thả
  Nhìn vào liên kết kho chứa, cái gọi là “tái hiện” thực ra không chạy lỗi thật mà chỉ liệt kê ra các dòng đầu ra kiểu “nó sẽ thế này”