Tìm thấy lỗi lập trình ẩn suốt 57 năm trong mã nguồn Apollo 11

Máy tính dẫn đường Apollo (Apollo Guidance Computer - AGC) sở hữu một trong những mã nguồn được kiểm duyệt kỹ lưỡng nhất trong lịch sử. Hàng nghìn lập trình viên đã đọc qua nó, các học giả đã công bố bài báo về độ tin cậy của nó, và các trình giả lập đã chạy từng lệnh mã một. Tuy nhiên, chúng tôi đã tìm thấy một lỗi đã bị bỏ lỡ suốt 57 năm: một khóa tài nguyên trong mã kiểm soát con quay hồi chuyển (gyro) bị rò rỉ trên đường dẫn lỗi, âm thầm vô hiệu hóa khả năng căn chỉnh lại 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ã hợp ngữ của AGC thành 12.500 dòng đặc tả. Các đặc tả này được derive trực tiếp từ mã nguồn và quy trình đã chỉ thẳng cho chúng ta thấy khiếm khuyết này.

Đánh dấu mã nguồn

Mã nguồn của AGC đã được công khai kể từ năm 2003, khi Ron Burkey và đội ngũ tình nguyện viên bắt đầu painstakingly chuyển thể nó thủ công từ các bản in tại Phòng thí nghiệm Công cụ MIT. Năm 2016, kho GitHub của cựu thực tập sinh NASA Chris Garry đã trở nên viral, dẫn đầu bảng xu hướng. Hàng nghìn nhà phát triển đã lướt qua ngôn ngữ hợp ngữ của một cỗ máy có 2KB RAM có thể xóa và đồng hồ 1MHz.

Các chương trình của AGC được lưu trữ trong 74KB bộ nhớ lõi dây (core rope): dây đồng được dệt thủ công qua các lõi từ tính nhỏ trong nhà máy (một sợi dây đi qua lõi là số 1, dây đi ngang qua là số 0). Những người phụ nữ dệt nó được gọi nội bộ là "Bà cụ già" (Little Old Ladies), và chính bộ nhớ này đượ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 từng cổng logic, 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 khôi phục từng byte một với các kết xuất lõi dây gốc.

Theo như chúng tôi tìm hiểu, chưa có bài kiểm toán hình thức, kiểm tra mô hình hay phân tích tĩnh nào được công bố trên mã nguồn chuyến bay này. Sự kiểm duyệt rất sâu sắc, nhưng đó là một loại kiểm duyệt cụ thể: đọc mã, giả lập mã, xác minh quá trình chuyển thể.

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

Nó đã làm nổi lên một khiếm khuyết mà việc đọc và giả lập đã bỏ sót.

Mất tham chiếu

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

Khóa được có được 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.

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

Khi việc tạo mômen hoàn thành bình thường, quy trình thoát qua STRTGYR2 và khóa LGYRO được xóa. Khi IMU bị kẹp hãm trong khi quá trình tạo mômen đang diễn ra, mã sẽ thoát qua một quy trình gọi là BADEND, quy trình này không xóa khóa. Đang thiếu hai hướng dẫn: CAF ZERO TS LGYRO

Bốn byte.

Một khi LGYRO bị kẹt, mọi nỗ lực tạo mô-men gyro sau đó đều thấy khóa đang được giữ, chờ đợi tín hiệu đánh thức sẽ không bao giờ đến, và treo. Căn chỉnh tinh, bù trôi, tạo mô-men gyro thủ công: tất cả đều bị chặn.

Sự im lặng của vô tuyế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 đang quay vòng một mình trong Mô-đun Lệnh Columbia. Mỗi hai giờ, ông biến mất phía sau mặt trăng, mất liên lạc vô tuyến với Trái Đất.

Trong mỗi lần bay qua, ông chạy Chương trình 52 (P52), một căn chỉnh quan sát ngôi sao giữ cho nền tảng dẫn đường hướng về đúng phía. Nếu nền tảng bị trôi, quá trình đốt động cơ để đưa ông về nhà sẽ hướng sai.

Dưới đây là cách lỗi này có thể biểu hiện.

Collins vừa hoàn thành việc quan sát ngôi sao tại trạm quang học và nhập các lệnh cuối cùng. Máy tính đang tạo mô-men cho các con quay để áp dụng điều chỉnh trên cả ba trục.

Ông di chuyển trở lại bảng điều khiển chính trong buồng lái chật hẹp, đi qua một công tắc kẹp được bảo vệ bởi nắp gập. Khuỷu tay va vào nắp và làm đẩy công tắc. Mã xử lý việc này một cách nhẹ nhàng: một quy trình gọi là CAGETEST phát hiện việc kẹp, bỏ qua việc tạo mô-men và thoát. P52 thất bại, và ông hiểu tại sao: việc kẹp đã làm gián đoạn điều chỉnh. Ông bỏ kẹp IMU và quay lại trạm quang học để căn chỉnh lại.

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

Không có báo động, không có đèn chương trình. DSKY (màn hình và bàn phím, giao diện duy nhất của ông với máy tính) chấp nhận đầu vào và không làm gì cả. Ông thử V41, lệnh tạo mô-men gyro 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 thao tác gyro là chết.

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

Một khởi động lại cứng (hard reset) sẽ xóa nó. Nhưng các báo động 1202 trong quá trình hạ cánh xuống mặt trăng đã đủ căng thẳng với Trung tâm Kiểm soát Mission Control trên đường dây và Steve Bales phải đưa ra quyết định nhanh chóng về việc hủy bỏ hay tiếp tục.

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

Các mốc đã biết

Margaret Hamilton (với tư cách là "người mẹ 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 vào bộ nhớ lõi dây. Đội ngũ của bà tại Phòng thí nghiệm MIT đã tiên phong các khái niệm mà chúng ta hiện nay coi là đương 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. Chính bà là người đặt ra thuật ngữ "kỹ thuật phần mềm" (software engineering).

Việc lập lịch ưu tiên của họ đã cứu cuộc hạ cánh Apollo 11 khi các báo động 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 dưới tải chính xác như được thiết kế. Hầu hết các hệ thống hiện đại không xử lý quá tải một cách khéo léo như vậy.

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

Khiếm khuyết này có hình dạng tương tự. BADEND là một quy trình chấm dứt mục đích chung được chia sẻ bởi tất cả các thao tác chuyển đổi chế độ IMU. Nó xóa MODECADR (thanh ghi giữ), đánh thức các công việc đang ngủ, và thoát. Nhưng LGYRO là một khóa dành riêng cho gyro, chỉ có được bởi mã tạo mô-men xung 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 đi qua BADEND, nó xử lý các tài nguyên chung một cách chính xác, nhưng không xử lý khóa dành riêng cho gyro.

AGC được viết một cách phòng thủ đến mức các lỗi tiềm ẩn như thế này sẽ được sửa âm thầm bởi logic khởi động lại, vốn 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 liền mạch.

Việc lập trình phòng thủ đã che giấu vấn đề, nhưng không loại bỏ nó. Một sự kiện kẹp không có khởi động lại tiếp theo sẽ vẫn để các gyro 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 giải pháp.

Quan sát ngôi sao

Chúng tôi đã tìm thấy khiếm khuyết này bằng cách chắt lọc một đặ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ả mô hình hóa từng tài nguyên chia sẻ như một thực thể có vòng đời: có được, giữ, 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 chi phối nó:

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

Với nghĩa vụ đó được ghi lại, Claude đã theo dõi từng đườ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 bởi kẹp (BADEND) thì không. MODECADR, tài nguyên chia sẻ khác, được xóa đúng cách trong BADEND: LGYRO bị thiếu.

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

Đặc tả tiếp cận theo hướng ngược lại: bắt đầu từ LGYRO và hỏi xem是否有 bất kỳ đường dẫn nào thất bại trong việc xóa nó.

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

Một đặc tả được chắt lọc bởi Allium mô hình hóa các 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à sự tái tạo của lỗi trên GitHub.

Sửa chữa lộ trình

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

Các ngôn ngữ hiện đại đã cố gắng làm cho việc 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, hệ thống quyền sở hữu của Rust làm cho lỗi rò rỉ khóa trở thành lỗi thời gian biên dịch.

Tuy nhiên, lỗi 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 vòng đời hiệu quả", và đánh giá khả năng khai thác của nó là cao. Không phải tất cả tài nguyên đều được quản lý bởi thời gian chạy ngôn ngữ. Các kết nối cơ sở dữ liệu, khóa phân tán, tay cầm tệp trong tập lệnh shell, cơ sở hạ tầng phải được tháo dỡ theo đúng thứ tự: những thứ nà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, cùng một lỗi đó đang chờ đợi.

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

Một lỗi 57 năm ẩn trong hợp ngữ đã được chứng thực bởi chuyến bay. Đang có gì ẩn trong mã của bạn? Hãy cùng thảo luận.