O que uma prova pode prometer

Em geral, confia-se em um software porque ele foi testado. Alguém pensou nas formas como ele poderia falhar, experimentou cada uma e viu como ele se saía. Isso funciona bem, até chegar o caso em que ninguém pensou.

Uma prova começa pela outra ponta. Ela não experimenta casos. Ela mostra, com matemática, que uma afirmação vale para todos.

Todos os casos, não só os que testamos

Tome uma promessa pequena: este código nunca lê além do fim do seu buffer. Um teste pode lhe dar mil entradas, ou um bilhão, e relatar que nenhuma o fez falhar. Uma prova diz algo de outra natureza: não há entrada que o faça falhar. Nenhuma foi encontrada, e nenhuma existe.

O preço é o rigor. Uma prova precisa de um enunciado exato do que o código deve fazer, a sua especificação, e de um argumento que ligue cada linha do código a ele. Em software de verdade, esse argumento é longo demais para uma pessoa conferir a olho. Então um computador confere.

Verificada por máquina

É isso que “verificada por máquina” quer dizer. A prova é escrita por inteiro, em uma linguagem que um programa chamado assistente de provas consegue ler, e o programa confere cada passo com as regras da lógica. Ele não se cansa na página novecentos, e não aceita a palavra de ninguém.

As provas do seL4 são verificadas assim, em um assistente de provas chamado Isabelle/HOL. Elas são públicas, e qualquer pessoa pode executá-las de novo.

O que dizem as provas do seL4

O seL4 é o kernel sobre o qual todo sistema NoWayOS roda: cerca de 10.000 linhas de código, e o único código com controle total do dispositivo. O tamanho é o ponto. Um argumento sobre dez mil linhas pode ser concluído. Um argumento sobre dezenas de milhões, ainda não.

A seL4 Foundation apresenta as provas em camadas:

• O código faz o que a especificação diz, e nada mais. Disso decorre uma lista de coisas que o kernel não pode fazer: estourar um buffer, seguir um ponteiro nulo, vazar memória, dividir por zero.
• O programa que roda corresponde ao código que foi provado. Há um compilador entre os dois, então outra prova confere a saída dele.
• O kernel consegue manter separadas as partes de um sistema. Uma parte não pode alterar os dados de outra, nem lê-los, nem tomar os recursos de que ela precisa, a menos que tenha recebido esse direito.
• Um sistema pode iniciar no estado para o qual foi projetado, com exatamente as concessões que a sua descrição lista.

Nem toda camada está concluída para todo processador e toda configuração. Isso importa, e voltaremos ao assunto.

O que uma prova toma como dado

Uma prova tem exatamente o alcance do seu enunciado, e se apoia nas suas premissas. O seL4 registra as dele por escrito: que o hardware se comporta como o seu modelo diz, que algumas centenas de linhas do código de mais baixo nível estão certas, que o código que roda antes de o kernel iniciar fez o seu trabalho. A prova de confidencialidade não cobre os tempos de execução.

Ela não diz nada sobre se a especificação pede a coisa certa, nem sobre o software acima do kernel. Um kernel provado vai isolar fielmente um programa que tem um defeito. O defeito continua lá. Ele só não consegue alcançar mais nada.

Isso não é uma fraqueza das provas. É o que faz delas algo que vale a pena ter: elas dizem com precisão o que cobrem, e assim você sabe com precisão o que sobra.

Onde o NoWayOS está

Esta é a posição, sem rodeios. O NoWayOS roda sobre o seL4, mas nenhuma imagem do NoWayOS está hoje dentro das provas concluídas do seL4. O NoWayOS usa a configuração de criticidade mista do seL4, cujas provas para os nossos processadores estão em andamento. E as provas do seL4 nunca cobriram o código do próprio NoWayOS. Por isso não chamamos o NoWayOS de “formalmente verificado”, e não vamos chamar.

Cada imagem diz onde está. Um arquivo ao lado dela lista a configuração do seu kernel, opção por opção, ao lado daquela que o seL4 provou. A página Segurança mostra um de verdade.

Provas menores, as nossas

O código do NoWayOS obtém a sua garantia por outro caminho: Rust, isolamento, revisão, testes e provas de um tipo mais modesto.

Cada decodificador das mensagens que passam entre as partes de um sistema tem provas limitadas, feitas com um verificador de modelos chamado Kani. Uma prova limitada cobre toda entrada até um tamanho declarado, aqui o registro mais longo que um decodificador aceita. Dentro desse limite, ela é uma prova de verdade: nenhuma entrada faz o decodificador entrar em pânico, estourar ou ler fora dos limites. Além do limite, ela não diz nada, e é por isso que o limite é a entrada mais longa que existe.

Depois quebramos os decodificadores de propósito, para ter certeza de que as provas percebem. Uma prova que não pode falhar não é melhor do que um teste que não pode.

O tamanho real disso

Uma prova não torna nada “inhackeável”. Ela torna uma afirmação verdadeira, em todos os casos, sob premissas que você pode ler. Conheça a afirmação e as premissas, e você sabe o que tem.

É por isso que o NoWayOS é construído sobre o kernel que tem essas provas, e por isso ele diz a você, imagem por imagem, até onde elas vão.