- Ironclad é um kernel do tipo Unix com suporte a tempo real e baseado em verificação formal para ambientes gerais e embarcados
- Verificação formal (Formal verification): conjunto de processos e checagens pelos quais o código do kernel passa para garantir ausência de erros em tempo de execução (AoRTE, Absence of Runtime Errors) e a correção dos componentes
- Escrito em SPARK e Ada, e composto por 100% de software livre
- Suporta interface compatível com POSIX, multitarefa preemptiva, controle de acesso mandatório (MAC) e escalonamento hard real-time
- Distribuído sob a licença GPLv3, mantendo uma estrutura totalmente open source sem blobs de firmware
- Pode ser portado para várias plataformas e está expandindo seu ecossistema por meio de distribuições como Gloire
Visão geral do kernel do sistema operacional Ironclad
- Ironclad é um kernel do tipo UNIX com suporte a tempo real que aplica verificação formal (formal verification) parcialmente
- Projetado tanto para sistemas de propósito geral quanto embarcados
- Verificação formal (Formal verification): conjunto de processos e checagens pelos quais o código do kernel passa para garantir ausência de erros em tempo de execução (AoRTE, Absence of Runtime Errors) e a correção dos componentes
- Para isso, utiliza SPARK, um subconjunto de Ada
- Todo o código é composto por software livre
- O kernel fornece interface compatível com POSIX e oferece suporte a multitarefa preemptiva, controle de acesso mandatório (MAC) e escalonamento hard real-time
- Proporciona uma experiência de desenvolvimento semelhante à de ambientes UNIX tradicionais
- Estrutura adequada para sistemas que exigem controle em tempo real
Características como software livre
- Ironclad é distribuído como software totalmente open source sob a licença GPLv3
- O kernel não inclui blobs de firmware (firmware blobs)
- Todos os componentes da pilha são fornecidos em formato open source
Verificação formal (Formal Verification)
- Utiliza os recursos de verificação formal da linguagem SPARK para garantir a ausência de erros e a correção dos principais componentes
- O SPARK verifica matematicamente a consistência lógica do código ao especificar pré-condições (Pre), pós-condições (Post) e dependências (Depends) no código Ada
- Os alvos da verificação incluem módulos criptográficos, sistemas MAC e funções relacionadas à interface do usuário
Portabilidade e ambiente de desenvolvimento
- Ironclad foi portado para várias plataformas e placas, e foi projetado para facilitar ports adicionais
- Depende apenas do toolchain GNU, permitindo cross-compilation com facilidade
- Graças à compatibilidade com POSIX, portabilidade de software e desenvolvimento se tornam mais simples
Distribuições e ecossistema
- O projeto Ironclad fornece distribuições (distributions) para várias arquiteturas e placas
- A principal distribuição livre e open source é a Gloire
- Também oferece imagens de distribuição em formato tarball para download
Suporte ao projeto e continuidade
- Ironclad é mantido como um projeto livre para uso, pesquisa e modificação
- A operação do projeto depende de doações e subsídios
- Toda contribuição impacta diretamente a expansão e o desenvolvimento do projeto
1 comentários
Comentários no Hacker News
Projeto interessante. Fico curioso sobre os limites da verificação formal do worst-case execution time (WCET)
Existem outros kernels verificados, como seL4 e atmosphere, e também dá para empilhar uma camada de compatibilidade POSIX como no genode
Também há kernels totalmente compatíveis e maduros, como QNX e VxWorks, então a verificação completa talvez não agregue tanto valor assim
Mas quase nunca vi um caso que reunisse WCET + verificação formal + compatibilidade POSIX ao mesmo tempo
No estágio atual, não parece ter maturidade suficiente para ser usado imediatamente nos casos de uso em tempo real descritos na documentação
O seL4 é muito mais rápido que o Linux, mas este aqui parece que vai ser lento. POSIX é inerentemente falho, e MAC é complexo demais para ser usado na prática
Ada pertence à família das linguagens de Wirth (família do Pascal). Até hoje, o único kernel tipo Unix nessa família que eu conhecia era o TUNIS
O TUNIS foi implementado em Concurrent Euclid
Já o Sol, da INRIA nos anos 80, foi implementado em um dialeto de Pascal e fornecia um ambiente compatível com Unix, mais tarde evoluindo para o Chorus
Também existe uma empresa ligada a NDA chamada Ironclad. É bom tomar cuidado com questões de marca registrada
Mesmo assim, fico muito feliz de ver esse tipo de iniciativa. Mas, no mundo real, o elo mais fraco da segurança costuma ser a camada de firmware
Meu sonho é que hardwares como os computadores da Framework tenham firmware EFI verificado e firmware auditado por componente
Criar um novo OS é algo realmente ambicioso. Recentemente também apareceu o Radiant Computer; fico curioso se há outros projetos interessantes parecidos
Espero que um dia kernels totalmente formalmente verificados se popularizem
Verificar o Linux inteiro seria impossível, mas o seL4 talvez consiga encontrar espaço em mercados como o de smartphones
Olhando o roadmap de verificação deles, chamar isso de “verificação formal” parece exagero
Não há provas das propriedades centrais do kernel, e isso não chega ao nível de kernels como seL4 ou Tock
CuBit é outro OS escrito em SPARK/Ada
O código-fonte pode ser visto no GitHub
Do ponto de vista do usuário comum, só o kernel não serve para muita coisa
Um exemplo de OS que usa o kernel Ironclad é o Gloire
A documentação sobre MAC está bem organizada (Mandatory Access Control)
Vendo a frase “consulte preços” do SPARK, isso parece menos software livre e mais outro sentido de “free”