◇ OpenCyber Academy
Graduação · Capítulo 1 · Português

Capítulo 1 — Raciocínio matemático

Ensino gratuito e aberto para quem deseja proteger pessoas e tecnologias. Não é preciso criar uma conta para estudar ou consultar as respostas.

Capítulo 1 — Raciocínio matemático

Mapa da aula

Aula 01 publicada. Mapa, exemplo, EX001.

flowchart TD
  N0["1.1 Enunciados e quantificadores"]
  N1["1.2 Técnicas de prova"]
  N2["1.3 Funções e vetores"]
  N3["1.4 Otimização"]
  N4["Síntese"]
  N0 --> N1 --> N2 --> N3 --> N4
  N4 --> EX["Exemplo resolvido"]
  EX --> Q["Exercício EX001"]

Desenho lógico

flowchart LR
  N0["1.1 Enunciados e quantificadores"]
  N1["1.2 Técnicas de prova"]
  N2["1.3 Funções e vetores"]
  N3["1.4 Otimização"]
  N4["Síntese"]
  N0 --> N1 --> N2 --> N3 --> N4 --> Q["EX001"]

[1.1 Enunciados e quantificadores]
    |
    v
[1.2 Técnicas de prova]
    |
    v
[1.3 Funções e vetores]
    |
    v
[1.4 Otimização]
    |
    v
[Síntese]
    |
    v
[Exemplo resolvido] --> [Exercício EX001]

Objetivos de aprendizagem

Você vai (1) ler e escrever enunciados matemáticos precisos; (2) usar técnicas de prova (direta, por contradição, por contraexemplo) para raciocinar sobre afirmações de segurança; (3) trabalhar com funções, vetores e otimização simples; e (4) ver por que um único contraexemplo derruba uma afirmação universal de segurança.

1.1 Enunciados e quantificadores

Afirmações de segurança são enunciados matemáticos disfarçados. "O Ask Lumen nunca revela a consulta de outro paciente" significa: para todas as entradas e para todos os usuários, a saída não contém dados de outro paciente. Um enunciado universal ("para todo") é refutado por um contraexemplo; um enunciado existencial ("existe um ataque") é provado exibindo-se um. Essa assimetria explica por que os atacantes levam vantagem: precisam de uma entrada que funcione, enquanto os defensores precisam cobrir todas. Escrever a afirmação por extenso expõe o que precisa ser verificado: cada usuário, cada entrada, cada caminho pelo qual os dados chegam à saída, incluindo documentos recuperados e resultados de ferramentas.

1.2 Técnicas de prova

A prova direta deduz a conclusão a partir das hipóteses. A prova por contradição supõe o contrário e deduz uma impossibilidade. A prova por contraexemplo refuta uma afirmação universal. Em segurança de IA, provas são raras para sistemas inteiros, mas comuns para componentes: "se o serviço de políticas nega toda chamada de ferramenta sem um token válido, então nenhuma marcação não autenticada ocorre" é uma prova direta a partir de uma propriedade do projeto. A prova baseada na propriedade do projeto vale tanto quanto sua hipótese: se algum caminho chega ao sistema de agendamento sem passar pelo serviço de políticas, a conclusão falha. Verificar essa hipótese é uma tarefa de arquitetura, que capítulos posteriores automatizam com busca em grafos.

1.3 Funções e vetores

Um modelo é uma função das entradas para as saídas. Entradas como imagens ou registros de atributos são vetores; a distância entre vetores (por exemplo, a distância euclidiana ou a maior diferença absoluta) formaliza a ideia de "pequena mudança". Muitos ataques procuram um vetor próximo que produza uma saída diferente (Szegedy et al., arXiv:1312.6199). A escolha da distância importa. Sob a maior diferença absoluta, todos os atributos podem mudar ao mesmo tempo até um valor fixo; sob a distância euclidiana, uma grande mudança num único atributo consome todo o orçamento. O laboratório de evasão, mais adiante, usa o primeiro tipo, de modo que o tamanho da perturbação eps limita separadamente a mudança em cada coordenada. Uma afirmação de robustez não significa nada até que a distância e seu tamanho sejam declarados.

1.4 Otimização

O treinamento minimiza uma função de perda; os ataques a maximizam (ou minimizam a distância sujeita a uma saída alterada). Ambos são problemas de otimização, e é por isso que as mesmas ferramentas matemáticas — gradientes, restrições, busca — aparecem dos dois lados. O laboratório de evasão mostra os dois lados em poucas linhas. O treinamento ajusta os pesos no sentido oposto ao gradiente da perda para reduzir o erro; o ataque move cada ponto de teste no sentido do sinal do mesmo gradiente em relação à entrada para aumentar o erro. Com eps de 0.5, a acurácia do modelo de brinquedo cai de 0.985 para 0.840, o que mostra quão pouco esforço uma busca guiada pelo gradiente exige quando o modelo é simples.

1.5 Exemplo resolvido (caso sintético da LCH)

O fornecedor da LCH afirmou: "O NoShow não pode ser manipulado por pacientes." Rina reescreveu isso como um enunciado universal: para todos os pacientes e todos os valores dos campos que os pacientes controlam (preferências de contato, motivo declarado da consulta), a previsão não muda num sentido que o paciente prefira. Em seguida, encontrou um contraexemplo num registro sintético: mudar o "motivo" de "retorno" para "urgente" baixou o risco previsto de falta de 0.42 para 0.18, o que poderia fazer um paciente subir numa lista de lembretes. A afirmação, tal como foi feita, era falsa; o fornecedor a revisou.

1.6 Erros e limites

Três erros são comuns: aceitar afirmações universais testadas em poucos exemplos; confundir "nenhum ataque encontrado" com "nenhum ataque existe"; e noções vagas de "pequena mudança", sem medida de distância. O exemplo do NoShow mostra os três. A afirmação do fornecedor foi testada apenas em registros comuns; ninguém havia procurado uma mudança num campo que os pacientes controlam; e "manipulado" não tinha medida declarada. O contraexemplo de Rina, uma mudança de 0.42 para 0.18 causada por um único campo, resolveu a questão de imediato. Uma afirmação revisada nomearia os campos, o tamanho de mudança considerado aceitável e a forma como foi testada.

Exercícios

Síntese

O raciocínio matemático torna precisas as afirmações de segurança. Afirmações universais exigem evidências fortes; um contraexemplo basta para refutá-las; "pequeno" exige uma distância.

Continue estudando — capítulo 01 de 40

← Página do curso · Índice de capítulos do curso · Capítulo 02 (rascunho) →