1 · O que este serviço faz, e o que ele não afirma¶

Idiomas

O seletor entende turnos escritos em inglês. O português é a sua próxima gramática e ainda não foi lançado; até lá, um turno escrito em português não é lido como português.

A Stalwart constrói agentes que agem por uma empresa e verifica as regras sob as quais esses agentes agem. Este capítulo diz o que cada produto faz, em palavras simples, e depois as coisas que nenhum deles prova. Todo capítulo seguinte é escrito contra essa segunda metade.

Os produtos¶

O Construtor de Bots (Bot Builder) é como uma equipe constrói o seu próprio agente. A equipe declara o agente num único arquivo: as suas ferramentas, as suas regras, quais escritas desfazem quais, e a qual agente ele pode passar uma conversa. Um componente dentro dele, o seletor, lê cada turno e decide, por uma regra nomeada e sem chamar nenhum modelo, que ferramenta o turno pede, o que perguntar ao usuário, ou que o turno é recusado. Toda chamada de ferramenta é então verificada antes de rodar, seja quem for que a escolheu. A Parte I deste guia é o Construtor de Bots, e a Parte II é o seletor por baixo dele.

As ferramentas de segurança e teste verificam as regras em volta de um agente e os modelos de que ele depende:

A Verificação de Grafos de Agentes (Agent Graph Verification) verifica cada caminho de um agente antes de ele entrar no ar: cada ferramenta alcançada sem a sua verificação, a sua confirmação ou a sua regra de ordem é um achado, com o caminho que chega a ela (capítulo 47).
O Caçador de Bugs em Guardrails (Guardrail Bug Hunter) encontra cada caminho através dos guardrails de uma equipe até uma ação proibida, mostra cada um acontecendo e entrega à equipe uma correção que verificou varrendo de novo (capítulo 28).
A Verificação de Guardrails (Guardrail Verification) decide se uma ação pode disparar sem o seu contexto de segurança, ou uma tabela inteira dessas perguntas, e devolve um contraexemplo com um reparo, ou um certificado.
A Escrita de Guardrails (Guardrail Writing) redige uma política a partir de uma regra em prosa, no próprio modelo do cliente, e depois verifica e repara o rascunho (capítulo 13).
A Verificação de Random Forests (Random Forest Verification) verifica uma random forest treinada contra propriedades de robustez, monotonicidade, equidade e alcançabilidade (capítulo 14).

O caçador e o seletor são usados juntos. Um guardrail pode fazer toda ação de ferramenta esperar pela decisão do seletor; o caçador então prova que nenhum caminho chega a uma ferramenta sem essa decisão, e reprova o pull request que adicione um (capítulo 29).

O motor por baixo¶

Por baixo dos produtos de verificação há um único motor. Você nomeia um resultado que nunca pode acontecer, como uma transferência é executada para um usuário que não fez login, e o motor decide se a política deixa isso acontecer. Ele compila a política e a sua pergunta em equações sobre os dois valores 0 e 1, e pergunta se elas têm solução.

Se não têm nenhuma, o resultado é impossível em toda combinação de entradas de uma só vez, e não numa amostra, e o motor pode lhe entregar um certificado que o prova.
Se têm uma, o resultado é alcançável, e a solução nomeia a situação exata que chega a ele.
Em qualquer caso, quando o resultado é alcançável ou não pôde ser descartado, o motor propõe o reparo menos disruptivo que consegue encontrar, escrito como uma condição nas palavras da sua própria política, e prova que a política reparada fecha o buraco.

O caçador de bugs, a verificação de grafos de agentes e a escrita de guardrails fazem todos as suas perguntas a esse motor. O seletor não: ele é um leitor de linguagem com as suas próprias regras, e as suas decisões não são provas (capítulo 20).

O que ele não afirma¶

Quatro coisas que nada disso prova. Cada uma volta, sob um título próprio, no capítulo que faz a afirmação que ela limita.

Ele prova as perguntas que você fez, e nenhuma outra. Uma execução de verificação prova uma proposição: que esta ação não pode disparar sem aquele contexto, sob estas condições. Ela não diz nada sobre nenhuma outra ação, nenhum outro contexto, nem nenhum resultado que você não nomeou. Uma política só está verificada na medida em que a sua lista de resultados indesejados está completa, e fazer essa lista é um julgamento sobre o seu negócio, não um cálculo (capítulo 4).
Um certificado estabelece uma derivação, não que as suas premissas são a sua política. Conferir um certificado 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. Fechar esse segundo passo exige compilar a política de novo e comparar, o que um certificado não carrega (capítulo 7).
Um veredito sobre uma política com diagnósticos de análise não é um veredito. Uma linha que o compilador não conseguiu ler é uma regra que as equações não têm, e uma regra que falta parece um desvio, ou uma aprovação, que não significa nada. Um veredito desses é marcado como nulo e não pode ser citado (capítulo 6).
Um patch é provado fechar o buraco e, só às vezes, provado não bloquear demais. Todo reparo vem com uma prova de que a política reparada descarta o resultado. Se ele também recusa situações que a sua política deveria permitir é uma pergunta separada, com a sua própria resposta, e só um dos quatro valores dessa resposta, proved_free, diz que não (capítulo 8).

E uma sobre normas: uma correspondência com as listas Top 10 da OWASP ou com o NIST AI Risk Management Framework não é uma certificação, uma auditoria nem uma declaração de conformidade com nenhum dos dois. A cobertura OWASP do caçador é no nível da política: ela cobre a parte de cada risco que as regras escritas por uma equipe controlam, e nada sobre os pesos ou os dados de treinamento de um modelo (capítulo 39).

Nenhum dos produtos, nem o agente, é uma prova de que um agente é seguro. Cada um prova, ou verifica, a coisa específica que o seu capítulo diz, e o seu título de limites diz onde isso termina.