Bug não documentado encontrado no código do computador de guiagem da Apollo 11

 (juxt.pro)
2 pontos por GN⁺ 22 일 전 | 1 comentários | Compartilhar no WhatsApp
  • Foi descoberto no código do Apollo Guidance Computer (AGC) um bug de liberação de recurso ausente que, por 57 anos, foi considerado quase perfeito
  • A equipe da JUXT analisou 130 mil linhas de assembly usando a linguagem de especificação de IA Allium e o Claude, identificando uma falha que não aparecia nos métodos tradicionais de verificação
  • No caminho de término anormal (BADEND) da rotina de controle do giroscópio, o bloqueio LGYRO não é liberado, o que pode fazer com que todas as funções relacionadas ao giroscópio parem em seguida
  • Se, durante a missão real, o interruptor Cage tivesse sido acionado por engano em órbita lunar, a operação de alinhamento do Program 52 poderia ter sido interrompida, e Collins poderia interpretar isso como uma falha de hardware
  • Este caso mostra que a análise baseada em especificação comportamental é um método poderoso para encontrar novas falhas mesmo em códigos antigos

Defeito potencial encontrado no computador de guiagem da Apollo 11

  • O Apollo Guidance Computer (AGC) é uma das bases de código mais minuciosamente revisadas da história, já analisada por inúmeros desenvolvedores e pesquisadores
    • Ainda assim, foi confirmado um bug de bloqueio de recurso não liberado no código de controle do giroscópio, que permaneceu oculto por 57 anos
    • O problema faz com que, em um caminho de erro, o bloqueio não seja liberado e a função de realinhamento da plataforma de guiagem seja desativada
  • A equipe da JUXT usou a linguagem de especificação baseada em IA Allium e o Claude para converter 130 mil linhas de assembly do AGC em 12,5 mil linhas de especificação comportamental
    • As especificações foram extraídas diretamente do código para modelar todos os caminhos de aquisição e liberação de recursos
    • Nesse processo, veio à tona uma falha que não aparecia com leitura de código ou emulação tradicionais

Estrutura do código e abordagem de análise

  • O código-fonte do AGC foi publicado em 2003, quando Ron Burkey e voluntários transcreveram manualmente as cópias impressas do MIT Instrumentation Laboratory
    • Em 2016, o repositório de Chris Garry no GitHub foi publicado, permitindo que desenvolvedores do mundo todo examinassem o código assembly de uma máquina com 2 KB de RAM e CPU de 1 MHz
  • O programa era armazenado em 74 KB de core rope memory, onde fios de cobre eram entrelaçados manualmente em núcleos magnéticos para representar 1s e 0s
    • As técnicas que faziam esse trabalho eram chamadas de “Little Old Ladies”, e a memória ficou conhecida como LOL memory
  • Até hoje, não havia registro de verificação formal, model checking ou análise estática aplicados ao AGC
    • A maior parte da verificação se concentrou em leitura de código, emulação e conferência da precisão da transcrição
  • A JUXT escreveu em Allium a especificação comportamental do subsistema IMU (Inertial Measurement Unit)
    • Ao modelar os momentos de aquisição e liberação de cada recurso compartilhado, conseguiu identificar o defeito

Falta de liberação do bloqueio na rotina de controle do giroscópio

  • O AGC gerencia a IMU com um bloqueio compartilhado chamado LGYRO
    • Ao aplicar torque nos giroscópios, o sistema adquire o bloqueio e o libera depois que os três eixos são concluídos
    • Isso impede que duas rotinas manipulem o hardware ao mesmo tempo
  • Porém, no caminho de término anormal, o bloqueio não é liberado
    • No encerramento normal, a rotina STRTGYR2 libera LGYRO, mas, se ocorrer “Caging” (travamento físico de proteção do giroscópio), o fluxo vai para a rotina BADEND
    • Em BADEND, faltam as duas instruções CAF ZERO e TS LGYRO (4 bytes no total), e o bloqueio permanece ativo
  • Se LGYRO não for liberado, todas as rotinas posteriores de torque do giroscópio ficam presas aguardando o bloqueio
    • Alinhamento fino, correção de deriva e torque manual: todas as funções relacionadas ao giroscópio são interrompidas

Impacto potencial no lado oculto da Lua

  • Em 21 de julho de 1969, Michael Collins executava periodicamente em órbita lunar o Program 52 (programa de alinhamento por observação estelar)
    • Se a plataforma sofresse deriva, haveria risco de direcionamento incorreto do motor de retorno
  • Se, durante uma operação de torque, o interruptor Cage tivesse sido pressionado por engano e o fluxo caísse no caminho BADEND, LGYRO poderia não ser liberado e todos os P52 seguintes poderiam travar
    • O DSKY (display e teclado) aceitaria entrada, mas não responderia
    • Como as outras funções continuariam normais, Collins poderia interpretar o problema como uma falha de hardware
  • Um reinício (hard reset) teria resolvido o problema, mas, por causa da experiência com o alarme 1202 durante o pouso lunar, decidir por um reset imediato provavelmente não teria sido simples

Projeto defensivo do sistema existente e seus limites

  • A equipe do MIT liderada por Margaret Hamilton introduziu conceitos fundamentais da engenharia de software moderna, como escalonamento por prioridade, multitarefa assíncrona e proteção contra reinicialização
    • Graças a esse projeto, o pouso foi possível mesmo durante o alarme 1202
  • A maioria dos defeitos importantes estava ligada a erros de especificação; como documentado por Don Eyles, houve casos em que a ausência de sincronização de fase entre hardwares aumentou a carga da CPU
  • Este defeito atual tem estrutura semelhante
    • BADEND é uma rotina geral de término para transições de modo da IMU e libera recursos comuns como MODECADR, mas não trata LGYRO
    • Como a lógica de reinicialização inicializa LGYRO, o problema se recuperava sem dificuldade nos testes e acabou ficando oculto
  • Porém, em uma situação real sem reinicialização, o giroscópio poderia permanecer travado permanentemente

Como a falha foi descoberta com Allium

  • A especificação em Allium modela o ciclo de vida (lifecycle) de cada recurso
    • O campo gyros_busy representa LGYRO, a regra GyroTorque define a aquisição do bloqueio e a regra GyroTorqueBusy define o estado de espera quando ele já está ocupado
  • A especificação declara a obrigação de que “se o bloqueio virar true, ele deve obrigatoriamente voltar para false”
    • Depois que o Claude rastreou todos os caminhos, ficou claro que a liberação acontece no caminho normal (STRTGYR2), mas falta no caminho de erro (BADEND)
  • A abordagem baseada em especificação verifica não o que o código faz, mas o que ele deveria fazer
    • Testes confirmam o comportamento atual do código; especificações validam o comportamento pretendido
  • As especificações em Allium e o código de reprodução do bug foram publicados no GitHub

Implicações modernas e lições

  • Na época, os programadores precisavam liberar manualmente o bloqueio com as instruções CAF ZERO e TS LGYRO
    • Era necessário lembrar de todos os caminhos e inserir manualmente o código de liberação
  • Linguagens modernas evitam estruturalmente esse tipo de falha de recurso não liberado
    • Recursos como defer do Go, try-with-resources do Java, with do Python e o sistema de ownership do Rust garantem liberação automática
  • Mesmo assim, falhas do tipo CWE-772 (liberação ausente de recurso) continuam existindo
    • Conexões de banco de dados, bloqueios distribuídos, file handles e a ordem de desligamento de infraestrutura ainda continuam sendo responsabilidade do programador
  • Todas as missões Apollo retornaram com sucesso, mas esse defeito permaneceu sem correção e foi herdado também pelo software COMANCHE (módulo de comando) e LUMINARY (módulo lunar)
  • A falha, escondida por 57 anos, mostra a importância da análise baseada em especificação comportamental

Leituras relacionadas

1 comentários

 
GN⁺ 22 일 전
Comentários no Hacker News

  • Sou Mike Stewart, liderei o projeto de restauração do AGC no canal CuriousMarc e sou coadministrador do VirtualAGC
    O bug mencionado desta vez era de fato uma falha real no software do AGC. Mas ele não ficou abandonado durante todo o período do programa. Foi descoberto durante o teste de estágio 3 do SATANCHE, registrado como L-1D-02, e corrigido entre a Apollo 14 e a 15
    Os relatórios relacionados podem ser consultados em documento 1 do ibiblio e documento 2
    A correção não foi simplesmente adicionar duas linhas para zerar o LGYRO, mas incluiu também uma reestruturação da arquitetura do código e a lógica para despertar tarefas em espera. Comparando o código da Apollo 14 e da 15 (código da Apollo 14, código da Apollo 15), dá para ver a diferença
    Não era um bug silencioso como descrito no artigo. O LGYRO também é inicializado em STARTSB2, que é executado sempre que há troca de programa, resolvendo o problema automaticamente. Portanto, na prática, ele só ocorria raramente ao executar o movimento de torque durante BADEND
    Se o bug persistisse, várias tarefas se acumulariam e acabariam provocando o erro 31202 (uma versão posterior do 1202). Esse problema foi descoberto antes do voo da Apollo 14, e um procedimento de recuperação foi adicionado nas Apollo 14 Program Notes
    Além disso, embora se diga que Ken Shirriff fez a análise em nível de portas lógicas, na prática fui eu quem fez a maior parte
    O Virtual AGC concluiu a verificação de correspondência byte a byte com dumps originais de core rope apenas para alguns programas; para o conjunto completo isso ainda não é possível. A maior parte do código-fonte foi restaurada a partir de impressos ou checksums
    Margaret Hamilton foi a ‘rope mother’ do Comanche (software do módulo de comando), enquanto o Luminary (módulo lunar) ficou a cargo de Jim Kernan. Isso pode ser confirmado no organograma de 1969
    No momento do alarme 1202, o AGC não havia sido projetado para remover tarefas de baixa prioridade. Na verdade, a orientação de pouso era a tarefa de prioridade mais baixa, enquanto o controle da antena e a atualização do display tinham prioridade maior. Este documento resume a prioridade de cada tarefa
    Por fim, testes com o hardware real confirmaram que a causa do alarme 1202 não era diferença de fase, mas sim diferença de tensão (28V vs 15V). O experimento relacionado pode ser visto neste link do YouTube

    • Eu estava esperando o seu comentário. Obrigado por compartilhar detalhes históricos realmente incríveis
    • A página principal já seguiu para outros assuntos, mas isso aqui é realmente uma informação preciosa. Agradeço por ter dedicado seu tempo

  • Se você tem interesse no Apollo AGC, recomendo muito o canal do YouTube CuriousMarc. Uma equipe tecnicamente brilhante documenta o processo de restaurar e analisar vários componentes do AGC
    A parte especialmente interessante é a reinterpretação do infame alarme 1202. Em geral ele é apresentado como um erro de sensor que podia ser ignorado, mas na prática poderia ter sido extremamente crítico em certas condições

    • Então dá para dizer que hoje seria mais difícil ou mais fácil repetir o mesmo pouso. Sabemos muito mais sobre os modos de falha do que naquela época
    • O que é “explicado para o público” e o que é “de fato compreendido” são coisas diferentes. Há muitas explicações simplificadas, mas entre especialistas isso já é bem entendido
    • A discussão da equipe do CuriousMarc sobre a restauração do AGC continua neste tópico

  • Meu trecho de código favorito é o seguinte

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

    Link no GitHub

    • Esse código também é citado em The Codeless Code
    • Aqui, CADR não tem relação com a função cadr do Lisp
    • Alguém consegue explicar por que esse código é engraçado?
    • Lembro de ter visto há muito tempo um poema no XKCD sobre esse código, mas talvez eu esteja confundindo

  • Fico curioso se já verificaram se esse bug realmente existe. A IA é boa nesse tipo de análise exploratória, mas ainda tem alta taxa de falso positivo
    Dependendo do contexto, pode ser importante ou não. Também há muitos bugs que a IA não encontra
    Eu não tenho a especialização para validar por conta própria, mas acho isso muito interessante

    • Na verdade, nem está claro se foi a IA que encontrou o bug. O texto só diz que “foi modelado em uma linguagem nativa de IA”
      Ainda assim, a descrição da aquisição do lock e do cenário de falha pareceu bastante convincente

  • É interessante que eles tenham encontrado um bug real. Mas a encenação dramática do texto é quase fictícia
    Coisas como bater num interruptor com o cotovelo ou exagerar um problema que seria resolvido com reset. Isso deixou o texto mais chamativo, mas menos confiável. Além disso, o estilo parece escrito por IA, o que incomoda ainda mais

    • Claro, era um interruptor com tampa de proteção.
      Mas para explicar um bug sutil ao leitor comum, algum nível de narrativa é necessário. Se ficar técnico demais, perde o interesse; se ficar dramático demais, os especialistas criticam. Acho difícil encontrar esse equilíbrio

  • Eu mesmo executei o código de reprodução (repro) incluído no artigo
    Link no GitHub
    Ele roda, mas a Fase 5 (demonstração de deadlock) é completamente saída falsa. Em vez de rodar o emulador de verdade, ela só imprime o resultado esperado
    Então enviei este PR, corrigindo para que funcione de fato no emulador, e também verifiquei se o patch de duas linhas realmente resolve o bug

    • Vejo esse tipo de “código de IA” com frequência. Ele imita desenvolvimento orientado a testes, mas na prática entrega código falso que só faz os testes passarem
      Código gerado por IA tende a parar no “agora está perfeito!”, e as pessoas que acreditam nisso acabam publicando assim mesmo. Esse é o verdadeiro problema

  • O texto em si é interessante, mas passa uma sensação artificial de algo escrito por LLM

    • Para mim não teve nenhum cheiro de LLM. Acho que é mais um estilo de artigo científico
    • A Juxt já escreve textos excelentes há muito tempo e tem expertise suficiente. Por isso, acho improvável que este artigo tenha sido escrito por IA
    • Aliás, segundo esta análise do Pangram, o texto foi classificado como escrito por humano
    • Mas um outro texto da Juxt realmente declara ter sido escrito pelo Claude. Isso é dito no último parágrafo deste artigo
    • Além disso, a parte sobre Rust e locks está factualmente incorreta. Isso é apontado neste comentário

  • O fato de que até o software que levou seres humanos à Lua com apenas 4 KB de memória ainda tenha bugs não descobertos mostra como a complexidade pode se esconder até em código pequeno

    • Quanto menor a memória, mais fraca é a correlação entre tamanho do código e taxa de bugs. Na verdade, a tentativa de comprimir a complexidade acaba aumentando os bugs
    • Isso soa apenas como um clichê vazio

  • Dizer que “derivaram a especificação a partir do código” está errado. Vale a pena rever o significado de specification

    • Na verdade, isso só quer dizer engenharia reversa

  • Tanto o artigo quanto o repositório são trabalhos descuidados (sloppy)
    Se você olhar o link do repositório, a suposta “reprodução” nem executa o bug real, apenas lista mensagens de saída dizendo “isso aconteceria”