F*: a linguagem orientada a provas que redefine a verificação formal de software
Conheça a linguagem F*, desenvolvida pela Microsoft Research e Inria para criar sistemas formalmente verificados executados na nuvem Azure e no Linux.
Camada de tradução Kakehashi roda utilitários Mach-O no Linux aarch64, oferecendo uma alternativa econômica para fluxos de CI/CD.
O projeto Kakehashi, disponibilizado sob a licença Apache License 2.0 no GitHub através do repositório wie-project/kakehashi, introduziu uma camada de tradução em espaço de usuário (userspace) que permite a execução direta de binários do macOS ARM64 no sistema operacional Linux aarch64. Sem recorrer a compilação Just-In-Time (JIT) ou à emulação de instruções de CPU, o software carrega binários Darwin Mach-O, mapeia uma versão própria da biblioteca de sistema (freestanding libSystem) e traduz chamadas de sistema (BSD syscalls) diretamente para o kernel Linux.
A execução em tempo real (live execution) do Kakehashi foi validada para a arquitetura Linux aarch64 em ambientes bare metal, máquinas virtuais via UTM e contêineres executados via Docker ou Colima. Para hosts baseados em outras arquiteturas ou sistemas operacionais, incluindo o próprio macOS, a ferramenta oferece o modo de inspeção estática (dry-load / inspect), permitindo analisar a estrutura de binários sem acionar a tradução de chamadas em tempo de execução.
Projetado com uma abordagem focada em linha de comando (CLI-first), o utilitário principal kh é capaz de carregar e rodar programas reais do macOS sobre o processador ARM64. O projeto já demonstra compatibilidade com ferramentas de produção, incluindo o compressor 7-Zip (7zz), o utilitário de transferência de dados curl, sondagens do Clang (clang probes) e rotinas multithreaded complexas.
A estrutura de código do Kakehashi foi dividida no repositório em quatro crates escritas na linguagem Rust, exigindo a versão Rust 1.88+ para compilação. A crate principal é a kakehashi, responsável por gerar o executável kh, instalado pelos usuários por meio do comando cargo install kakehashi ou via compilação local com cargo install --path crates/kh-cli --force.
A análise e a alocação de memória dos arquivos executáveis ficam a cargo da crate kh-loader, que faz o parsing do formato Mach-O do Darwin, mapeia suas seções e prepara a transferência do fluxo de controle. Em seguida, a crate kh-runtime assume a gestão de memória, tratamento de interrupções (traps), gerenciamento de **BSD syscalls** e a administração do ambiente isolado chamado de bottle.
Para prover os símbolos de sistema necessários para os executáveis do macOS, a kh-runtime traz embutida a biblioteca libSystem.B.dylib através da macro include_bytes!. O código-fonte dessa biblioteca é mantido na crate kh-libsystem, direcionada exclusivamente para o alvo aarch64-apple-darwin. Ao publicar a kh-runtime, a biblioteca compilada é incluída no binário, dispensando o download de dependências externas por parte do usuário.
A ordem de busca da biblioteca libSystem pelo binário kh obedece a uma ordem rigorosa de prioridade: sinalizador --libsystem, variável de ambiente KAKEHASHI_LIBSYSTEM, caminhos adjacentes ao executável kh, recursos da crate e, por fim, os bytes embutidos na kh-runtime. Para mantenedores do projeto que alteram a ABI da biblioteca, o script scripts/stage-libsystem.sh compila a kh-libsystem e move o artefato resultante para crates/kh-runtime/resources/libSystem.B.dylib.
O ambiente de execução isolado do Kakehashi, denominado bottle, é criado por padrão no diretório ~/.local/share/kakehashi/bottle/, caminho que pode ser alterado pelas variáveis de ambiente KAKEHASHI_DATA_DIR ou KAKEHASHI_ROOT. A estrutura inicial do ambiente é gerada ao executar o comando kh bottle ensure.
A bottle reproduz a hierarquia de diretórios esperada por binários compilados para o macOS. Ferramentas instaladas pelos comandos kh install 7zip e kh install curl têm seus binários posicionados no hospedeiro em …/usr/local/bin/7zz e …/usr/local/bin/curl, sendo expostos dentro do ambiente convidado como /usr/local/bin/7zz e /usr/local/bin/curl, acompanhados da biblioteca de sistema em /usr/lib/libSystem.B.dylib.
A integração entre o sistema de arquivos do hospedeiro Linux e a bottle ocorre através do ponto de montagem /Volumes/linux/, que mapeia a raiz do sistema (/) do hospedeiro. Dessa forma, um caminho convidado como /Volumes/linux/src/README.md é traduzido diretamente para o arquivo <repo>/README.md na máquina nativa.
Para requisições de rede com suporte a **TLS**, a **bottle** aloca os certificados em …/private/etc/ssl/cert.pem (acessível no ambiente convidado em /etc/ssl/cert.pem), utilizando a cadeia de **CA** do sistema hospedeiro ou o pacote fornecido pelo curl.se. Caso configurações opcionais do **OpenSSL** não sejam encontradas, o sistema pode registrar o aviso kh: open fail ENOENT(openat) path=/etc/ssl/openssl.cnf, sem comprometer a execução de conexões **HTTP** e **HTTPS**.
O utilitário de compactação 7-Zip (7zz) em sua versão nativa para **Darwin** é um dos principais softwares validados pela camada de tradução. O programa pode ser executado via kh com comandos como kh run 7zz -- --help ou para criar arquivos com kh run 7zz -- a demo.7z README.md, no qual os caminhos relativos de saída são resolvidos em relação ao diretório de trabalho atual (CWD) do processo kh.
A validação de chamadas concorrentes do Kakehashi é realizada por meio do teste multithreaded do 7-Zip com o comando kh run 7zz -- a -t7z -m0=lzma2 -mx=5 -mmt=4 mt.7z README.md. A instrução força a compressão utilizando quatro threads paralelas (-mmt=4) com o algoritmo LZMA2 no nível 5 de compactação, validando a integridade posterior do arquivo via kh run 7zz -- t mt.7z, que deve retornar o código de saída zero (exit 0) e a mensagem Everything is Ok.
O utilitário curl compilado para **macOS** passa por testes estruturados de rede, desde a validação do cabeçalho via kh run curl -- --version até requisições **HTTP GET** para download de arquivos usando kh run curl -- -sS -o .tmp/kh-out/body http://example.com/, gerando um arquivo de aproximadamente 559 bytes contendo a string Example Domain.
Para requisições seguras, o projeto valida conexões **HTTPS** via **OpenSSL** com o comando kh run curl -- -sS -o .tmp/kh-out/https-body https://example.com/. A integridade da verificação de segurança é confirmada por testes de falha intencional: ao tentar acessar certificados autoassinados inválidos com kh run curl -- -sS -o /dev/null https://self-signed.badssl.com/, o Kakehashi garante que a execução termine obrigatoriamente com um código de erro diferente de zero (rc ≠ 0).
O Kakehashi executa o código de instrução convidado nativamente na CPU ARM64, sem emular registradores ou instruções. O custo de desempenho existente deriva do overhead da fronteira das chamadas de sistema (syscall boundary), que inclui a alternância do armazenamento local de thread (TLS switch), troca para pilha alternativa (alt stack), preservação e restauração de registradores NEON e o despacho no runtime em **Rust**.
Em testes de desempenho conduzidos em uma máquina **Ubuntu aarch64 bare-metal** sob **UTM**, a compactação de uma árvore de arquivos com cerca de 8.000 itens e 240 MiB (utilizando os parâmetros -t7z -m0=lzma2 -mx=5 -mmt=4) apresentou os seguintes resultados comparativos:
Apesar da diferença de **×5,2** em cenários com grande volume de acessos ao sistema de arquivos (path walk), o relatório do projeto aponta que em amostras focadas estritamente em compressão pesada de poucos arquivos a desvantagem cai para a faixa de **×1,1** a **×1,2**. Isso confirma que o gargalo do sistema está na frequência de **syscalls** enviadas ao kernel, e não no processamento do algoritmo **LZMA**.
O recurso de **hypercall** é mantido ativo por padrão para todas as threads convidadas por meio de KAKEHASHI_HYPERCALL=1. A desativação dessa opção com KAKEHASHI_HYPERCALL=0 é recomendada apenas para sessões de depuração de sinais residuais SIGTRAP ou interrupções do tipo svc→brk.
A viabilidade técnica do **Kakehashi** sustenta-se na discrepância de custos de infraestrutura de integração contínua (CI) em provedores como o GitHub Actions. Os preços por minuto para diferentes tipos de executores hospedados revelam a seguinte estrutura tarifária:
Considerando que a tarifa do executor de **macOS** é de 10 a 12 vezes mais cara do que a de um runner **Linux arm64**, uma tarefa executada no **Kakehashi** que demore cinco vezes mais tempo para ser concluída no **Linux** ainda resulta em um custo financeiro final menor. Por exemplo, cinco minutos de execução em **Linux arm64** custam cerca de **$0,025** (5 × $0,005), valor significativamente inferior ao custo de **$0,062** por um único minuto em um executor **macOS** nativo.
O projeto ressalta que executores nativos de **macOS** continuam necessários para fluxos de trabalho que exigem compilação de interfaces gráficas (GUI), processos de assinatura e notarização de código (codesign/notarization) ou testes automatizados de UI no Xcode, escopos que não são cobertos pela **freestanding libSystem** do **Kakehashi**.
Para facilitar a execução em ambientes isolados, o projeto fornece um ecossistema de scripts auxiliares no diretório scripts/. A criação da imagem de desenvolvimento é feita com docker build -t kakehashi:dev -f Dockerfile.dev ., enquanto o script ./scripts/docker-smoke.sh executa a validação completa contendo análise estática com clippy, compilação do projeto e testes unitários via cargo test --workspace --exclude kh-libsystem.
O ecossistema Docker inclui utilitários específicos para teste e automação, tais como:
scripts/docker-7zz.sh: Executa a versão **Darwin** do **7-Zip** salvando artefatos em .tmp/kh-out/.scripts/docker-curl.sh e scripts/docker-curl-probe.sh: Tratam requisições de rede e registram logs de sondagem em .tmp/kh-curl-probe/.scripts/docker-git.sh: Executa a versão do **Apple git** obtida do **Command Line Tools (CLT)**, utilizando um cache local em .kh/data.scripts/bench-fair-local.sh: Roda comparações de desempenho entre binários nativos do Linux e versões Darwin sob o **Kakehashi**.No estágio atual de desenvolvimento, o **Kakehashi** não implementou suporte a funcionalidades avançadas do **curl** (como corpo de requisições **POST**, proxies e **HTTP/3**) nem bibliotecas nativas complexas da Apple, gerando alertas no terminal como WARN … skip dylib … Security/CoreFoundation. O próximo ciclo de expansão do projeto prevê o suporte ao git via kh install xcode-tools, conforme detalhado no documento docs/git.md.
O repositório enfatiza que a base de código do **Kakehashi** foi desenvolvida de forma independente, sem qualquer derivação do projeto **Darling** e sem incluir **blobs** ou **SDKs** proprietários da Apple. O software exige suporte a tamanhos de página de memória de **4 KiB** em contêineres padrão e **16 KiB** em arquiteturas da classe **Asahi Linux**, mantendo rigorosos critérios de validação de código executados por cargo clippy --workspace --exclude kh-libsystem --all-targets -- -D warnings.
Conheça a linguagem F*, desenvolvida pela Microsoft Research e Inria para criar sistemas formalmente verificados executados na nuvem Azure e no Linux.
Projeto de verificação de idade da UE exige atestação via hardware, gerando fortes críticas da comunidade de software livre no GitHub.
O sistema open-source Bor lança a versão 0.8.0 com suporte ao Thunderbird, Edge, Firewalld, nova interface em PatternFly 6 e segurança reforçada.