7 · Certificados¶

Um certificado é a parte de um veredito que você pode entregar a alguém que não confia em nós. Ele registra por que as equações de uma pergunta não têm solução, em passos simples o bastante para serem conferidos com uma página de código. Este capítulo diz o que um certificado prova e o que não prova, como ele é construído, os dois caminhos para reproduzi-lo e a que pergunta cada um responde, e como citá-lo.

O que um certificado prova¶

Um certificado vem com um veredito UNSAT: a obrigação vale. Ele estabelece que as equações de que parte, as suas premissas, não têm solução em comum. As premissas são a política compilada, os pins da pergunta, um patch se houver, e nada mais: todo outro ponto de partida no documento é marcado como algo afirmado em vez de derivado, e o procedimento que o afirmou é nomeado.

Sob o perfil fast não há certificado nenhum; sob patch e proof, há (capítulo 10). Um reparo sempre traz o seu próprio: o certificado de que a política mais esse reparo descarta o resultado (capítulo 8).

O que ele não prova¶

Um certificado estabelece uma derivação, não que as suas premissas são a sua política. Conferi-lo mostra que as equações de que ele parte não têm solução em comum. Não mostra que essas equações são uma compilação fiel do seu arquivo de política: um defeito do compilador que descartasse uma regra produziria premissas coerentes entre si e erradas sobre a sua política, e o certificado seria conferido sem erro. O certificado nomeia a política de que foi compilado, com o seu SHA-256, para que o arquivo possa ser compilado de novo e comparado; fazer isso é um segundo passo, que o certificado não carrega.

E ele não prova nada sobre uma pergunta que você não fez. É um certificado para uma obrigação, sob os seus pins (capítulo 4). Nenhum relatório de um verificador diz, e nenhum leitor pode concluir de um, que uma política é segura.

Como um certificado é construído¶

Cada passo que o motor algébrico dá para eliminar o impossível é uma operação de linha sobre os dois valores 0 e 1, e o motor registra de onde veio cada linha em que se apoia. Esse registro é um grafo acíclico dirigido de três tipos de passo:

INSERT traz uma premissa: uma equação do sistema, citada como é.
ADD soma duas linhas anteriores: os seus termos são combinados, e um termo presente nas duas se cancela.
MULTIPLY multiplica uma linha anterior por uma variável.

Quando o motor encontra a contradição, a linha que diz 0 = 1, ele escreve a ancestralidade dessa linha e nada mais, em pós-ordem em profundidade, para que toda linha que um passo usa apareça antes do passo. Um certificado é, portanto, pequeno: dezenas de passos para uma política de tamanho realista, um objeto que um revisor consegue ler, e não um que só uma máquina consegue auditar.

O último passo é retido de propósito. As operations do certificado param um passo antes da contradição, e o passo que a completa é dado separadamente como final_step. Reproduzir operations não pode produzir 0 = 1; aplicar final_step tem de produzir. Assim, quem confere um certificado produz a contradição por si mesmo, em vez de recebê-la pronta.

Essa forma é a assimetria em que todo o produto se apoia: encontrar a derivação foi caro, e conferi-la é barato. Cada passo é a soma de duas linhas esparsas, ou uma linha vezes uma variável, sem busca, sem heurística e sem solver. É por isso que podemos entregar a conferência sem entregar o motor.

Os dois tipos, e o que confere cada um¶

certificate_type diz que parte do motor refutou o sistema, e origin_class diz como a refutação pode ser conferida:

`certificate_type`	`origin_class`	`status`	Conferido por
`algebraic`	`derived`	`verified_unsat`	reprodução: rodar `operations`, aplicar `final_step`, chegar a `0 = 1`
`algebraic`	`exhaustion`	`verified_unsat`	o registro de refutação: o motor reduziu a pergunta a um conjunto finito de soluções candidatas, provou que o conjunto está completo e mostrou que toda candidata falha
`phase0`	`external_proof`	`proof_unsat`	um verificador de provas: a prova FRAT do solver SAT, conferida pelo `frat-rs`, sobre um CNF que o verificador de referência decodifica de volta para as equações
`phase0`	`external_oracle`	`oracle_unsat`	nada no documento: o solver SAT o afirmou, e confirmá-lo significa rodar um solver de novo

Três campos dizem que tipo de afirmação o documento faz, e um leitor cuidadoso os lê antes de qualquer outra coisa:

self_contained é true quando o documento sozinho resolve a questão: nada externo foi afirmado, toda premissa é legível e o registro de uma exaustão está completo. false é honesto, não uma falha.
oracle_dependent é true quando a refutação depende de um procedimento de decisão externo, o solver SAT. Ele é relatado ao lado do certificado, no veredito, então está lá mesmo para uma execução que não construiu certificado.
origin_class diz qual das quatro linhas acima o documento é. Uma refutação que depende de um oráculo não pode ser reproduzida passo a passo: operations está vazio e final_step é a afirmação do oráculo.

Uma prova FRAT de uma refutação da Fase 0: `external_proof`¶

Sob os perfis padrão, uma refutação a que o solver SAT chega é uma afirmação dele. Peça frat_proof num job guardrail ou batch e, para cada refutação que a Fase 0 decide, o solver SAT roda de novo com o registro de prova ligado, e dois arquivos voltam como artefatos proof: o CNF que ele refutou e um registro FRAT da refutação. O proof_log do certificado nomeia os dois, com os seus digests SHA-256.

O que essa prova estabelece é que o CNF não tem atribuição que o satisfaça. O que liga o CNF às suas equações é a verificação da codificação: o CNF entregue ao solver se decodifica, cláusula por cláusula, de volta para as equações que o certificado carrega como phase0_system, e o próprio verificador de referência faz essa decodificação. Com as duas, a confiança no oráculo é substituída pela confiança em dois verificadores que você pode rodar: o verificador de referência, para a decodificação, e o frat-rs, para a prova. O frat-rs passa, portanto, a fazer parte daquilo em que um leitor confia. A classe não é derived, porque os três passos de uma reprodução não conseguem expressar a resolução de cláusulas: é uma quarta classe, e self_contained continua false.

result = client.verify_guardrail("transfers.co", "execute_transfer_funds", "is_authenticated",
                                 profile="proof", frat_proof=True)
print(result.status, result.verdict["origin_class"])
for artefact in result.artifacts:
    if artefact.role in ("certificate", "proof"):
        print(artefact.role, artefact.filename)
        artefact.save(artefact.filename)       # checked against its digest as it is written

A prova não custa nada a menos que você a peça. Pedida, ela acrescenta uma segunda resolução de uma refutação a que a Fase 0 já chegou; nas refutações de referência isso leva milissegundos, e os arquivos têm quilobytes, mas isso não é um limite garantido (capítulo 10). Quando o serviço descarta uma prova, porque ela falhou na própria verificação frat-rs do worker ou excederia o max_proof_bytes da chave, o certificado volta a external_oracle e oracle_unsat, e diz o porquê em proof_log_omitted.

Os blocos de proveniência¶

Todo certificado traz três blocos que dizem em que as suas premissas se apoiam. Eles não participam da conferência, e são indexados pelos índices das variáveis (x12), nunca por nomes:

provenance: qual sistema de registro afirma cada controle que a refutação cita, onde a implantação os declarou, e todo controle que ninguém declarou, em undeclared;
control_integrity: se as próprias palavras de quem faz o pedido podem chegar a um controle por meio de um classificador, o que deixaria a pessoa contra quem o controle protege defini-lo;
detection: se a obrigação depende de um detector reconhecer algo e, nesse caso, o limite de quantas vezes uma classificação errada poderia deixar a ação passar, com o corpus sobre o qual esse limite foi medido.

Cada bloco lista os seus próprios limites no documento. Uma fonte declarada pode ser falsa; um resolvedor pode transformar um argumento numa leitura; um limite de detecção só é tão bom quanto o seu corpus.

Conferindo um certificado você mesmo¶

Há dois caminhos de reprodução, e eles respondem a perguntas diferentes.

	O verificador de referência	A reprodução do serviço
A pergunta que responde	consigo confirmar isto sem confiar no fornecedor?	este certificado se reproduz no produto que eu estou rodando?
Em que você confia	na sua própria leitura de um arquivo curto, ou na sua própria implementação da especificação	no nosso serviço
Do que precisa	Python, um arquivo, nenhuma chave, nenhuma rede	uma chave, e o modo `replay_certificate`
O que trata	os certificados que uma política produz	qualquer certificado que o motor emite
O que relata	o resultado e o seu motivo	o resultado, com os diagnósticos de conformidade do próprio motor, completos
Use quando	você é uma segunda linha, um auditor, ou recebeu um certificado e nada mais	você opera o serviço e quer saber se o artefato de uma execução está correto

Nenhum substitui o outro. Uma reprodução feita pelo nosso serviço não é uma verificação independente: ela estabelece que o nosso software concorda consigo mesmo. Isso é útil para quem opera, e não vale nada para um auditor, e uma equipe que confunde os dois não fez uma auditoria.

O verificador de referência¶

O verificador de referência é um único arquivo Python, só com a biblioteca padrão, sob a licença MIT, publicado com o seu digest. Ele relata um de três resultados, verified, not_self_contained ou failed, e sai com 0, 2 ou 1, respectivamente. O que ele imprime está em inglês, como ele o escreve:

$ python qls-check.py FCA-01a/patch.certificate.json
qls-check: verified
replayed 105 operation(s), and the withheld final step yields 0 = 1
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
0

$ python qls-check.py FCA-01a/proof.certificate.json
qls-check: not_self_contained
the contradiction rests on rows asserted by cryptominisat-phase0, which nothing in the certificate checks
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
2

O mesmo arquivo vai dentro do pacote stalwart-agents, como stalwart check certificate.json, que não precisa de chave; stalwart check --print-source o escreve para ser comparado com o publicado. Para construir o seu próprio verificador, a especificação do certificado é normativa e completa, e o corpus lhe dá certificados para testá-lo, cada um com o resultado que um verificador correto relata.

A reprodução do serviço¶

O modo replay_certificate reproduz um certificado que você tem, ou um dos seus artefatos pelo seu id, com o reprodutor do próprio motor. replay é replayed, failed ou out_of_scope: fora do escopo é uma refutação correta de um tipo que a reprodução não confere (uma exaustão, ou a afirmação de um oráculo), não um erro.

replayed = client.replay_certificate("certificate.json")
print(replayed.replay)                   # replayed, failed or out_of_scope

checked = check_certificate("certificate.json")   # the reference checker, here, offline
print(checked.outcome, checked.reason)

Conformidade não é reprodução¶

Duas verificações separadas são feitas sobre um certificado, e passar numa não implica passar na outra:

A conformidade é o formato do documento: todo INSERT sem equação está marcado como afirmado, certificate_type concorda com final_step, um documento derived não se apoia em nenhuma linha afirmada, e nenhuma equação de um documento autocontido tem uma coluna que ninguém consegue decodificar. Um certificado válido pelo esquema ainda pode falhar na reprodução.
A reprodução é a aritmética: as operações, e depois o passo final, chegam a 0 = 1. Um certificado pode se reproduzir e ainda declarar self_contained: false, porque se apoia em algo afirmado.

Os dois verificadores fazem as duas verificações e as relatam separadamente. As duas produzem um resultado verde, e é por isso que confundi-las é a leitura errada contra a qual mais vale a pena se proteger.

Citando um certificado¶

Um certificado continua conferível por alguém que não estava lá, então cite o que permite conferi-lo:

o id do job e o id do artefato de onde ele foi baixado, e o seu SHA-256 (o registro do artefato o traz, e o download é conferido contra ele durante a transferência);
o arquivo de política que ele nomeia e o SHA-256 desse arquivo, que o certificado registra em policy;
a pergunta: a ação, o contexto e cada pin, todos registrados em question;
o perfil, do bloco run do job.

Duas execuções da mesma pergunta podem produzir certificados diferentes, com números de passos diferentes: a busca do motor é paralela e encontra a derivação válida a que chegar primeiro. Isso não é uma discrepância. Cada certificado é uma prova válida do mesmo fato, conferível nos seus próprios termos, e a pergunta que um auditor faz é se o certificado que você arquivou é conferido sem erro, não se uma nova execução o reproduz byte a byte.

Os limites¶

Um certificado estabelece que as suas premissas não têm solução em comum, não que as premissas são a sua política.
Ele prova uma obrigação, sob os seus pins, e nada sobre nenhuma outra pergunta.
self_contained: false significa que o documento sozinho não resolve a questão: confia-se na afirmação de um oráculo, ou, para external_proof, no frat-rs.
Uma reprodução pelo nosso serviço não é uma verificação independente.
Conformidade e reprodução são verificações separadas; passar numa não implica passar na outra.