Chúng tôi đã tìm thấy một lỗi không có giấy tờ trong mã máy tính hướng dẫn Apollo 11

Apollo Guidance Computer (AGC) là một trong những cơ sở mã được xem xét kỹ lưỡng nhất trong lịch sử. Hàng nghìn lập trình viên đã đọc nó. Các học giả đã xuất bản các bài nghiên cứu về độ tin cậy của nó. Các trình giả lập chạy nó theo từng lệnh. Chúng tôi đã tìm thấy một lỗi trong đó mà đã bị bỏ sót suốt 57 năm qua: một khóa tài nguyên trong mã điều khiển con quay hồi chuyển bị rò rỉ trên đường dẫn lỗi, âm thầm vô hiệu hóa khả năng tái định hướng của nền tảng dẫn đường.

Chúng tôi đã sử dụng Claude và Allium, ngôn ngữ đặc tả hành vi mã nguồn mở của chúng tôi, để chắt lọc 130.000 dòng mã assembly của AGC thành 12.500 dòng đặc tả. Các thông số kỹ thuật được rút ra từ chính mã nguồn và quá trình này đã dẫn dắt chúng tôi trực tiếp đến khiếm khuyết đó.

Lập biểu đồ mã

Mã nguồn đã được công khai từ năm 2003, khi Ron Burkey và một nhóm tình nguyện viên bắt đầu công việc tỉ mỉ là chép tay nó từ các bản in tại Phòng thí nghiệm Thiết bị đo đạc MIT. Vào năm 2016, kho lưu trữ GitHub của cựu thực tập sinh NASA Chris Garry đã trở nên nổi tiếng, đứng đầu trang thịnh hành. Hàng nghìn lập trình viên đã lướt xem ngôn ngữ assembly của một cỗ máy với 2K RAM có thể xóa và xung nhịp 1MHz.

Các chương trình của AGC được lưu trữ trong 74KB bộ nhớ dây lõi (core rope): dây đồng được luồn thủ công qua các lõi từ nhỏ trong nhà máy (một sợi dây đi qua lõi là 1; một sợi dây đi vòng qua nó là 0). Những người phụ nữ dệt nên nó được gọi nội bộ là “Những quý bà già nhỏ bé” (Little Old Ladies), và chính bộ nhớ đó được gọi là bộ nhớ LOL. Chương trình được dệt vật lý vào phần cứng. Ken Shirriff đã phân tích nó xuống đến từng cổng logic riêng lẻ, và dự án Virtual AGC chạy phần mềm trong môi trường giả lập, đã xác nhận mã nguồn được phục hồi chính xác từng byte so với các bản sao bộ nhớ dây lõi gốc.

Theo những gì chúng tôi xác định được, chưa có xác minh chính thức, kiểm tra mô hình hay phân tích tĩnh nào được công bố đối với mã chuyến bay này. Sự xem xét kỹ lưỡng đã diễn ra sâu sắc, nhưng đó là một loại xem xét cụ thể: đọc mã, giả lập mã, xác minh bản chép tay.

Chúng tôi đã chọn một cách tiếp cận khác. Chúng tôi đã sử dụng Allium để chắt lọc đặc tả hành vi từ hệ thống con Đơn vị Đo lường Quán tính (IMU), nền tảng dựa trên con quay hồi chuyển cho biết tàu vũ trụ đang hướng về đâu. Đặc tả mô hình hóa vòng đời của mọi tài nguyên dùng chung: khi nào nó được chiếm dụng, khi nào nó phải được giải phóng và trên các đường dẫn nào.

Nó đã làm lộ ra một lỗ hổng mà việc đọc mã và giả lập trước đó đã bỏ lỡ.

Mất tham chiếu

AGC quản lý IMU thông qua một khóa tài nguyên dùng chung có tên là LGYRO. Khi máy tính cần tạo mô-men xoắn cho các con quay hồi chuyển (để điều chỉnh độ lệch nền tảng hoặc thực hiện căn chỉnh sao), nó sẽ chiếm dụng LGYRO ở bước bắt đầu và giải phóng nó khi cả ba trục đã được tạo mô-men xoắn. Khóa này ngăn chặn hai chương trình con tranh giành phần cứng con quay hồi chuyển cùng một lúc.

Khóa được chiếm dụng khi đi vào và giải phóng khi đi ra. Nhưng có một khả năng thứ ba, và nó không giải phóng khóa.

‘Caging’ là một biện pháp khẩn cấp: một kẹp vật lý khóa chặt các gimbal của IMU tại chỗ để bảo vệ con quay hồi chuyển khỏi bị hư hỏng. Phi hành đoàn có thể kích hoạt nó bằng một công tắc có bảo vệ trong buồng lái.

Khi quá trình tạo mô-men xoắn hoàn tất bình thường, chương trình con thoát qua STRTGYR2 và khóa LGYRO được xóa. Khi IMU bị khóa (caged) trong khi quá trình tạo mô-men xoắn đang diễn ra, mã sẽ thoát qua một chương trình con gọi là BADEND, vốn không xóa khóa. Hai lệnh đã bị thiếu:

        CAF  ZERO
        TS   LGYRO

Bốn byte.

Một khi LGYRO bị kẹt, mọi nỗ lực tiếp theo để tạo mô-men xoắn cho con quay hồi chuyển đều thấy khóa vẫn bị giữ, chuyển sang trạng thái ngủ chờ đợi tín hiệu đánh thức sẽ không bao giờ đến, và bị treo. Căn chỉnh tinh vi, bù trôi, tạo mô-men xoắn con quay thủ công: tất cả đều bị chặn.

Vào ngày 21 tháng 7 năm 1969, trong khi Neil Armstrong và Buzz Aldrin đi bộ trên bề mặt Mặt Trăng, Michael Collins bay một mình trên Mô-đun Chỉ huy Columbia. Cứ mỗi hai giờ, anh ấy lại biến mất sau Mặt Trăng, mất liên lạc vô tuyến với Trái Đất. “Bây giờ tôi chỉ có một mình, thực sự cô độc và hoàn toàn bị cô lập khỏi bất kỳ sự sống nào được biết đến. Tôi là duy nhất,” anh viết trong cuốn Carrying the Fire. “Nếu tính số người, kết quả sẽ là ba tỷ cộng với hai người ở phía bên kia Mặt Trăng, và một cộng với Chúa mới biết là ai ở phía bên này.”

Trong mỗi lần đi qua, anh thực hiện Chương trình 52, một phép căn chỉnh định vị sao giúp nền tảng dẫn đường luôn hướng theo đúng hướng. Nếu nền tảng bị lệch, động cơ đẩy để đưa anh trở về nhà sẽ hướng sai cách.

Im lặng vô tuyến

Dưới đây là cách lỗi có thể đã xảy ra.

Collins vừa hoàn thành các phép quan sát sao tại trạm quang học ở khoang thiết bị bên dưới và nhập các lệnh cuối cùng. Máy tính đang tạo mô-men xoắn cho các con quay hồi chuyển để áp dụng hiệu chỉnh trên cả ba trục.

Anh di chuyển trở lại bảng điều khiển chính trong một buồng lái chật hẹp, đi ngang qua một công tắc khóa (cage switch) được bảo vệ bởi một nắp lật. Một khuỷu tay vướng vào nắp và huých vào công tắc. Mã xử lý việc này khá mượt mà: một chương trình con gọi là CAGETEST phát hiện trạng thái khóa, hủy bỏ việc tạo mô-men xoắn và thoát. P52 thất bại, và anh hiểu lý do: việc khóa đã làm gián đoạn hiệu chỉnh. Anh mở khóa IMU và quay lại trạm quang học để căn chỉnh lại.

Anh bắt đầu một chương trình P52 mới. Chương trình bị treo.

Không có báo động, không có đèn chương trình. DSKY (hiển thị và bàn phím, giao diện duy nhất của anh với máy tính) chấp nhận dữ liệu nhập nhưng không làm gì cả. Anh thử V41, lệnh tạo mô-men xoắn con quay thủ công. Kết quả tương tự. Mọi thứ khác trên máy tính vẫn hoạt động. Chỉ có các hoạt động liên quan đến con quay hồi chuyển là bị tê liệt.

Lần thất bại đầu tiên trông có vẻ bình thường: một sự kiện khóa trong khi căn chỉnh, với phương pháp khôi phục đã biết. Lần thứ hai không cho thấy manh mối nào về những gì đang xảy ra. Phản ứng được huấn luyện cho trường hợp vô tình khóa là mở khóa và căn chỉnh lại. Collins đã được huấn luyện để khởi động lại máy tính, nhưng không có gì về lỗi này gợi ý rằng anh cần phải làm vậy. Các lệnh được chấp nhận, mọi thứ khác đều hoạt động. Nó sẽ trông giống như phần cứng bị lỗi, chứ không phải là một chiếc khóa bị kẹt.

“Nỗi kinh hoàng thầm kín của tôi trong sáu tháng qua là bỏ mặc họ trên Mặt Trăng và một mình quay trở lại Trái Đất”, Collins sau này đã viết về cuộc hội ngộ. Một hệ thống con quay hồi chuyển bị hỏng ở phía sau Mặt Trăng, với Armstrong và Aldrin đang ở trên bề mặt chờ đợi một thao tác đốt động cơ để hội ngộ, vốn phụ thuộc vào một nền tảng mà ông không còn có thể căn chỉnh được nữa, chính xác là viễn cảnh đó.

Một cú hard reset lẽ ra đã giải quyết được vấn đề. Nhưng các cảnh báo 1202 trong quá trình hạ cánh xuống Mặt Trăng đã đủ gây căng thẳng với bộ phận Kiểm soát Sứ mệnh đang trực tuyến và Steve Bales phải đưa ra một quyết định hủy bỏ hay tiếp tục ngay tức khắc.

Ở phía sau Mặt Trăng, đơn độc, với một chiếc máy tính chỉ chấp nhận lệnh mà không thực hiện gì cả, Collins sẽ phải tự mình đưa ra quyết định đó.

Các cột mốc đã biết

Margaret Hamilton (với vai trò “mẹ đẻ của bộ nhớ dây” cho LUMINARY) đã phê duyệt các chương trình bay cuối cùng trước khi chúng được dệt thành bộ nhớ lõi dây (core rope memory). Nhóm của bà tại Phòng thí nghiệm Thiết bị đo đạc MIT đã tiên phong trong những khái niệm mà ngày nay chúng ta coi là điều hiển nhiên: lập lịch ưu tiên, đa nhiệm không đồng bộ, bảo vệ khởi động lại và khôi phục lỗi dựa trên phần mềm. Ngay cả thuật ngữ ‘kỹ thuật phần mềm’ cũng là do bà đặt ra.

Khả năng lập lịch ưu tiên của họ đã cứu cuộc đổ bộ của Apollo 11 khi các cảnh báo 1202 kích hoạt trong quá trình hạ cánh, loại bỏ các tác vụ ưu tiên thấp khi hệ thống bị quá tải đúng như thiết kế. Hầu hết các hệ thống hiện đại không xử lý tình trạng quá tải một cách khéo léo như vậy.

Những lỗi nghiêm trọng nhất xuất hiện thực ra là lỗi đặc tả kỹ thuật, không phải lỗi lập trình. Don Eyles, người đã viết mã hướng dẫn hạ cánh lên Mặt Trăng, đã ghi lại một vài trường hợp. Ví dụ, tài liệu ICD cho radar hội ngộ quy định rằng hai bộ nguồn 800 Hz sẽ được khóa tần số nhưng không đề cập gì đến việc đồng bộ hóa pha. Độ lệch pha tạo ra khiến ăng-ten dường như bị rung, tạo ra khoảng 6.400 ngắt giả mỗi giây trên mỗi góc và tiêu tốn khoảng 13% công suất máy tính trong quá trình hạ cánh của Apollo 11. Đây là nguyên nhân sâu xa dẫn đến các cảnh báo 1202.

Lỗi này cũng có bản chất tương tự. BADEND là một quy trình kết thúc đa năng được chia sẻ bởi tất cả các thao tác chuyển đổi chế độ IMU. Nó xóa MODECADR (thanh ghi chờ), đánh thức các công việc đang tạm dừng và thoát. Nhưng LGYRO là một khóa dành riêng cho con quay hồi chuyển, chỉ được lấy bởi mã tạo xung (pulse-torquing) và chỉ được giải phóng bởi đường dẫn hoàn thành bình thường trong STRTGYR2. Khi đường dẫn lỗi chuyển qua BADEND, nó xử lý các tài nguyên chung một cách chính xác, nhưng lại không xử lý khóa dành riêng cho con quay hồi chuyển.

AGC được viết theo cách phòng thủ đến mức các lỗi tiềm ẩn như thế này sẽ âm thầm được sửa chữa bởi logic khởi động lại, vốn sẽ xóa LGYRO như một tác dụng phụ của việc khởi tạo toàn bộ bộ nhớ có thể xóa. Bất kỳ bài kiểm tra nào tình cờ kích hoạt khởi động lại sau lỗi đó sẽ thấy hệ thống phục hồi một cách liền mạch.

Cách lập trình phòng thủ đã che giấu vấn đề, nhưng không loại bỏ được nó. Một sự kiện khóa (cage event) mà không có khởi động lại theo sau vẫn sẽ để các con quay hồi chuyển bị khóa. Collins sẽ không có cách nào để căn chỉnh lại nền tảng dẫn đường và không có manh mối chẩn đoán nào chỉ ra cách khắc phục.

Quan sát các ngôi sao

Chúng tôi đã tìm thấy lỗi này bằng cách chắt lọc đặc tả hành vi của hệ thống con IMU sử dụng Allium, một ngôn ngữ đặc tả hành vi gốc AI. Đặc tả này mô hình hóa mỗi tài nguyên dùng chung như một thực thể với vòng đời: được lấy, đang giữ, được giải phóng.

Thực thể IMU khai báo một trường gyros_busy mô hình hóa LGYRO. Hai quy tắc quản lý nó:

rule GyroTorque {
    -- Sends gyro torquing pulse commands. Reserves the gyros,
    -- enables power supply, and dispatches pulses per axis.
    when: GyroTorque(command: GyroTorqueCommand)
    requires:
        imu.mode != caged
        imu.gyros_busy = false
    ensures:
        imu.gyros_busy = true
        GyroTorqueStarted()
}
rule GyroTorqueBusy {
    -- Gyros already reserved by another torquing operation.
    -- Caller sleeps until LGYRO is cleared.
    when: GyroTorque(command: GyroTorqueCommand)
    requires: imu.gyros_busy = true
    ensures:
        JobSleep(job: calling_job())
}

GyroTorque yêu cầu gyros_busy = false và đảm bảo gyros_busy = true: khóa được lấy. Ở đâu đó, trên mọi đường dẫn theo sau, khóa phải được giải phóng. Đặc tả không chỉ ra nơi nào trong mã lệnh diễn ra việc giải phóng, nhưng nó làm cho nghĩa vụ này trở nên rõ ràng: nếu gyros_busy chuyển sang true, thứ gì đó phải đặt nó trở lại thành false.

Với nghĩa vụ đó được ghi lại, Claude đã truy vết mọi đường dẫn chạy sau khi gyros_busy được đặt thành true. Đường dẫn hoàn thành bình thường (STRTGYR2) xóa nó. Đường dẫn bị gián đoạn do khóa (BADEND) thì không. MODECADR, tài nguyên dùng chung còn lại, được xóa chính xác trong BADEND: nhưng LGYRO thì bị thiếu.

Đặc tả ép buộc câu hỏi này trên mọi đường dẫn thông qua mã chuyển đổi chế độ IMU. Một người đánh giá kiểm tra BADEND sẽ thấy việc dọn dẹp chính xác, đầy đủ cho mọi tài nguyên mà BADEND được thiết kế để xử lý.

Đặc tả tiếp cận từ hướng ngược lại: bắt đầu từ LGYRO và đặt câu hỏi liệu có đường dẫn nào không xóa được nó hay không.

Các bài kiểm tra xác minh mã lệnh như đã viết; một đặc tả hành vi đặt câu hỏi mã lệnh đó dùng để làm gì.

Một đặc tả được chắt lọc bởi Allium mô hình hóa vòng đời tài nguyên trên tất cả các đường dẫn, bao gồm cả những đường dẫn mà không ai nghĩ đến việc kiểm tra. Bạn có thể xem các đặc tả Allium và bản tái tạo lỗi trên GitHub.

Điều chỉnh lộ trình

Nhóm của Hamilton đã giải phóng tài nguyên bằng cách tải hằng số 0 vào thanh ghi tích lũy (accumulator) (CAF ZERO) và lưu nó vào thanh ghi khóa (TS LGYRO). Mỗi lần giải phóng đều được đặt thủ công bởi một lập trình viên, người phải ghi nhớ mọi đường dẫn có thể dẫn đến điểm đó.

Các ngôn ngữ hiện đại đã cố gắng làm cho rò rỉ khóa trở nên bất khả thi về mặt cấu trúc: Go có defer, Java có try-with-resources, Python có with, và hệ thống sở hữu của Rust khiến lỗi rò rỉ khóa trở thành lỗi biên dịch.

Tuy nhiên, tình trạng rò rỉ khóa vẫn tồn tại. MITRE phân loại mô hình này là CWE-772: “Thiếu giải phóng tài nguyên sau khi kết thúc vòng đời hiệu dụng”, và đánh giá khả năng bị khai thác ở mức cao. Không phải tất cả tài nguyên đều được quản lý bởi runtime của ngôn ngữ. Các kết nối cơ sở dữ liệu, khóa phân tán, file handle trong tập lệnh shell, hạ tầng cần được gỡ bỏ theo đúng thứ tự: đây vẫn thường là trách nhiệm của lập trình viên. Bất cứ nơi nào lập trình viên chịu trách nhiệm viết mã dọn dẹp, lỗi tương tự vẫn luôn chực chờ.

Mọi phi hành đoàn Apollo đều trở về an toàn. Nhưng các quy trình chuyển đổi chế độ IMU đã được chuyển tiếp qua các sứ mệnh trong cả phần mềm Mô-đun Chỉ huy (COMANCHE) và phần mềm Mô-đun Mặt trăng (LUMINARY). Lỗi này chưa bao giờ bị phát hiện và cũng chưa bao giờ được khắc phục.

Một lỗi tồn tại năm mươi bảy năm đã ẩn mình trong phần mã assembly đã được kiểm chứng qua các chuyến bay. Còn những gì đang ẩn giấu trong mã của bạn? Hãy cùng thảo luận.

Cảm ơn Farzad “Fuzz” Pezeshkpour vì đã độc lập tái hiện lỗi này, và cảm ơn Danny Smith cùng Prashant Gandhi vì đã xem xét các bản thảo đầu tiên của bài viết này.