Uma metodologia formalizada para compilar C em Rust seguro

• Compilando C para Rust seguro

• A popularidade da linguagem Rust tem crescido rapidamente, mas muitas bases de código importantes ainda são escritas em C, e reescrevê-las manualmente não é viável na prática. Portanto, a tradução automática de C para Rust surge como uma alternativa atraente.

• Vários trabalhos anteriores vão na direção de cobrir progressivamente mais partes de C por meio de recursos do Rust (por exemplo, unsafe). No entanto, embora o cenário de automação seja atraente, gerar código que depende de unsafe invalida a garantia de segurança de memória fornecida pelo Rust, de modo que o benefício principal de portar uma base de código existente para uma linguagem com segurança de memória se perde.

• Nós exploramos um caminho alternativo para traduzir C para Rust seguro. Ou seja, gerar código que respeita o sistema de tipos do Rust, de modo a facilitar a garantia de segurança de memória.

• Nossa pesquisa inclui várias contribuições originais:

  • Tradução orientada a tipos de parte de C para Rust seguro
  • Uma nova análise estática baseada em "árvore de divisão" para expressar aritmética de ponteiros em C usando slices e operações de fatiamento do Rust
  • Uma análise para inferir precisamente quais empréstimos precisam ser mutáveis
  • Uma estratégia de compilação para tipos de struct de C compatível com a distinção do Rust entre alocação não proprietária e proprietária

• Aplicamos essa metodologia a bases de código C formalmente verificadas já existentes: a biblioteca criptográfica HACL* e o parser e serializador binário do EverParse. Demonstramos que o subconjunto de C suportado é suficiente para traduzir essas duas aplicações para Rust seguro.

• Os resultados da avaliação mostram que, para algumas partes que violam a disciplina de aliasing do Rust, uma reescrita cirúrgica automatizada é suficiente, e o impacto no desempenho dos poucos clones estratégicos inseridos é mínimo.

• Em particular, ao aplicar a abordagem ao HACL*, uma biblioteca criptográfica verificada de 80.000 linhas implementando todos os algoritmos modernos foi escrita em Rust puro. Este é o primeiro caso desse tipo.

[GN⁺]

Comentários do Hacker News

• Ao portar projetos para Rust, cheguei a algumas conclusões

  • Converter programas em C para Rust permite identificar bugs rapidamente graças às restrições rígidas do Rust
  • A conversão automática de C para Rust não é totalmente resolvida, porque os dois idiomas têm designs fundamentalmente diferentes
  • Em alguns casos, portar de C para Rust pode ser impossível, pois a insegurança é inerente ao próprio design
  • À medida que as ferramentas melhoram, o processo de portabilidade deve ficar mais fluido

• Um código-fonte C formalmente verificado e um código-fonte C de sistema comum não são a mesma coisa

• Em 2002, pesquisadores publicaram um paper sobre Cyclone, um dialeto seguro de C, e encontraram bugs de segurança ao portar código de C para Cyclone

  • Essa transformação, manual ou automática, pode aumentar a adoção de linguagens seguras e também descobrir bugs existentes

• Uma tradução direta para Rust pode gerar áreas seguras e inseguras, e o trabalho manual pode concentrar-se em validar a segurança das áreas inseguras

  • Mesmo que a parte insegura seja grande, pode haver benefícios

• Não espero que a abordagem de compilar apenas uma pequena parte do C funcione bem

  • Porque o modelo de propriedade do Rust é muito diferente do de um programa C real

• Curiosidade sobre a comparação com a conversão de C do Zig

  • O Zig compõe bem cenários com código novo e código C existente, e também pode ser usado como compilador C
  • Fico curioso sobre o motivo pelo qual os mantenedores do kernel Linux não consideram o Zig como substituto de C

• Pergunta sobre se C2Rust consegue gerar código formalmente correto

  • Não há nenhum link visível para o código-fonte que gera Rust

• Se uma biblioteca C funciona, pode valer a pena traduzir usando insegurança do Rust

  • Rust em geral ainda carece de bibliotecas

• Achei interessante que níveis de otimização mais altos não melhoram tanto a performance do Rust

  • Fiquei curioso sobre o quão bem funciona compilar C para Rust de uma vez no nível de otimização O3