Bug não documentado encontrado no código do computador de orientação da Apollo 11 usando IA e linguagem de especificação

Encontrando um bug em um dos códigos mais examinados da história

O código do Computador de Orientação Apollo (AGC) está disponível publicamente desde 2003, transcrito de listagens impressas do Laboratório de Instrumentação do MIT. Em 2016, o repositório GitHub de Chris Garry viralizou, e milhares de desenvolvedores examinaram esse código assembly rodando em hardware com 2K de RAM apagável e um clock de 1MHz. Apesar desse escrutínio, nenhuma verificação formal, verificação de modelo ou análise estática havia sido publicada contra o código de voo até agora.

O bug: Um vazamento de bloqueio de recurso no controle do giroscópio

O bug está no subsistema da Unidade de Medição Inercial (IMU), que gerencia a plataforma baseada em giroscópio que informa à espaçonave para que direção ela está apontando. O AGC gerencia a IMU através de um bloqueio de recurso compartilhado chamado LGYRO. Quando o computador precisa aplicar torque aos giroscópios (para corrigir deriva da plataforma ou realizar alinhamento estelar), ele adquire LGYRO no início e o libera quando todos os três eixos foram torquedos.

O problema ocorre durante o 'engaiolamento' - uma medida de emergência onde uma braçadeira física trava os gimbals da IMU no lugar para proteger os giroscópios de danos. Quando o torque é concluído normalmente, a rotina sai via STRTGYR2 e o bloqueio LGYRO é liberado. Mas quando a IMU é engaiolada enquanto um torque está em andamento, o código sai por uma rotina chamada BADEND, que não libera o bloqueio.

Duas instruções estão faltando: CAF ZERO TS LGYRO - apenas quatro bytes. Uma vez que LGYRO fica travado, toda tentativa subsequente de aplicar torque aos giroscópios encontra o bloqueio mantido, dorme esperando por um sinal de despertar que nunca virá, e trava. Isso desabilitaria o alinhamento fino, a compensação de deriva e o torque manual do giroscópio.

Como foi encontrado: IA e especificações comportamentais

Os pesquisadores usaram Claude e Allium, sua linguagem de especificação comportamental de código aberto, para destilar 130.000 linhas de assembly do AGC em 12.500 linhas de especificações. A especificação modela o ciclo de vida de cada recurso compartilhado: quando é adquirido, quando deve ser liberado e em quais caminhos. Essa abordagem revelou uma falha que a leitura e emulação haviam perdido.

As especificações foram derivadas do próprio código, e o processo apontou diretamente para o defeito. Isso representa uma abordagem diferente do escrutínio anterior, que se concentrava em ler o código, emular o código e verificar a transcrição.

Contexto histórico e impacto potencial

Em 21 de julho de 1969, enquanto Neil Armstrong e Buzz Aldrin caminhavam na superfície lunar, Michael Collins orbitava sozinho no Módulo de Comando Columbia. A cada duas horas ele desaparecia atrás da Lua, fora do contato de rádio com a Terra. Durante cada passagem ele executava o Programa 52, um alinhamento por observação estelar que mantinha a plataforma de orientação apontada na direção correta. Se a plataforma derivasse, a queima do motor para trazê-lo para casa apontaria para o lado errado.

O bug poderia ter se manifestado se Collins acidentalmente acionasse o interruptor de engaiolamento enquanto o computador estava aplicando torque aos giroscópios. O código lidaria com isso graciosamente detectando o engaiolamento, abandonando o torque e saindo - mas o alinhamento P52 falharia, e a plataforma de orientação poderia perder sua referência.