Os cientistas da computação podem provar que não há erros no programa com a mesma certeza que os matemáticos podem provar teoremas. Esses avanços são usados para aumentar a segurança em várias áreas, de drones à Internet.

Na primavera de 2015, uma equipe de hackers tentou invadir um helicóptero militar não tripulado chamado Little Bird ("Bird"). O helicóptero, semelhante à versão tripulada da aeronave favorita das forças especiais dos EUA, estava localizado na Boeing, no Arizona. Os hackers tiveram uma vantagem: no início de seu trabalho, eles tinham acesso a um dos subsistemas do computador de controle. Eles só podiam invadir o computador de bordo principal e obter o controle do UAV.

No início do projeto, a equipe de hackers da Equipe Vermelha poderia quebrar um sistema de helicóptero quase tão facilmente quanto o WiFi de sua casa. Nos meses seguintes, os engenheiros da DARPA implementaram um novo mecanismo de segurança, um sistema de software não sujeito a expropriação forçada. Os parâmetros-chave do sistema Little Bird não podem ser quebrados usando as tecnologias existentes, e seu código pode ser confiável como evidência matemática. E, embora a equipe tenha recebido seis semanas de acesso ao UAV e o acesso ao sistema de computador tenha excedido as capacidades de acesso de uma equipe real de hackers, eles não conseguiram quebrar a defesa do Bird.

"Eles não conseguiram decifrar ou interromper a operação", diz Kathleen Fisher, professor de ciência da computação na Universidade Tufts e gerente de projetos para sistemas militares cibernéticos de alta garantia (HACMS). "Como resultado, os representantes da DARPA se levantaram e disseram: Oh, meu Deus, você pode realmente usar essa tecnologia em sistemas importantes."

Os hackers que se opõem à tecnologia são um estilo de programação chamado confirmação formal . Diferentemente do código comum escrito informalmente e geralmente avaliado apenas por seu desempenho, o software formalmente verificado parece uma prova matemática: cada instrução segue logicamente a da anterior. Todo o programa pode ser verificado com a mesma certeza que um teorema matemático.

"Você escreve uma fórmula matemática que descreve o comportamento de um programa e usa uma ferramenta de prova de conceito que testa a validade dessa declaração", diz Brian Parno , pesquisador em confirmação e segurança formal da Microsoft Research.

O desejo de criar programas formalmente confirmados existia quase tanto quanto o próprio campo da ciência da computação. E por muito tempo isso permaneceu impossível, mas as realizações dos últimos dez anos no campo dos “métodos formais” aproximaram essa abordagem da prática convencional. Hoje, a confirmação formal de software está sendo estudada em grupos acadêmicos financiados, em projetos militares dos EUA e em empresas de tecnologia como Microsoft e Amazon.

O interesse está crescendo junto com um aumento no número de tarefas vitais passando on-line. Quando os computadores existiam isolados em residências e escritórios, os erros de programação eram apenas um incômodo. Agora, eles abrem brechas de segurança nas máquinas da rede, permitindo que qualquer pessoa com conhecimento penetre nos sistemas de computadores.

"No século 20, quando um programa cometeu um erro, foi ruim, poderia cair, bem, Deus a abençoe", disse Andrew Appel , professor de ciência da computação na Universidade de Princeton e líder em validação de programas. Mas no século 21, um erro pode abrir uma maneira de hackers ganharem o controle do programa e roubarem seus dados. Por um erro tolerável, tornou-se uma vulnerabilidade, o que é muito pior ”, diz ele.

Kathleen Fisher

Sonhos de programas perfeitos

Em outubro de 1973, Edsger Dijkstra teve a idéia de criar código sem erros. À noite, enquanto estava em um hotel em uma conferência, ele de repente pensou em como tornar a programação mais matemática. Explicando a ideia mais tarde, ele disse: "Com uma mente empolgada, saí da cama às 2:30 da manhã e escrevi por mais de uma hora". Esse material foi o início de seu frutuoso livro de 1976, The Discipline of Programming, que, juntamente com o trabalho de Charles Hoare (como Dijkstra, que recebeu o Prêmio Turing ), definiu pontos de vista sobre o uso da prova de correção nos programas de redação.

Mas a ciência da computação não seguiu essa idéia, principalmente porque durante muitos anos pareceu impraticável, ou mesmo impossível, determinar a função de um programa usando as regras da lógica formal.

Uma definição formal é uma maneira de determinar o que um programa faz especificamente. A confirmação formal é uma maneira de provar, sem dúvida, que o código do programa se encaixa perfeitamente nessa definição. Imagine que você está escrevendo um programa para um robomóvel que o leva a um supermercado. No nível das operações, você determina os movimentos que o robomóvel tem para atingir a meta - ele pode girar, desacelerar ou acelerar, ligar ou desligar no início e no final do caminho. Seu programa consistirá dessas operações básicas, organizadas na ordem certa, para que você chegue à loja e não ao aeroporto.

A maneira tradicional de testar a saúde de um programa é através de testes. Os programadores fornecem ao programa muitos dados de entrada (testes de unidade) para garantir que ele se comporte da maneira que deveria. Se o seu programa definir um algoritmo para o movimento de um robomóvel, você poderá testar suas viagens entre muitos pontos diferentes. Esses testes garantem a operação correta dos programas na maioria dos casos, o que é suficiente para a maioria dos aplicativos. Mas os testes de unidade não garantem que o software sempre funcione corretamente - você não pode verificar o programa com todos os dados de entrada possíveis. Mesmo que o algoritmo funcione para todos os destinos, sempre existe a possibilidade de que ele se comporte de maneira diferente sob condições raras - ou, como se costuma dizer, em "condições de contorno" - e abra uma brecha na segurança. Em programas reais, esses erros podem ser simples, por exemplo, estouros de buffer,em que o programa copia um pouco mais de dados do que o necessário e substitui parte da memória do computador. Este erro aparentemente inofensivo é difícil de eliminar e fornece um buraco para um ataque de hackers - uma dobradiça de porta fraca que abre o caminho para o castelo.

“Um buraco em algum lugar do software, e isso é uma vulnerabilidade. É muito difícil verificar todos os caminhos para todas as entradas possíveis ", diz Parno.

Essas especificações são mais complicadas do que uma ida à loja. Os programadores, por exemplo, podem precisar de um programa com reconhecimento de firma e aposição da data de recebimento dos documentos na ordem em que foram recebidos. Nesse caso, a especificação deve indicar que o contador está sempre aumentando e que o programa nunca deve permitir que a chave usada para assinar vaze.

Na linguagem humana, isso é fácil de descrever. Transformar uma especificação em uma linguagem formal que um computador entende é muito mais difícil - o que explica o principal problema de escrever programas.

"Construir uma especificação formal compreensível para um computador é essencialmente difícil", diz Parno. "É fácil no nível superior dizer" não deixe a senha vazar ", mas você precisa pensar em como transformar isso em uma definição matemática."

Outro exemplo é um programa que classifica uma lista de números. Um programador na tentativa de formalizar uma especificação para ela pode vir com isso:

Para cada item j na lista, verifique se j ≤ j + 1

Mas mesmo nesta especificação formal - para garantir que cada elemento da lista seja menor ou igual ao próximo - há um erro. O programador assume que a saída conterá a entrada modificada. Se a lista for [7, 3, 5], ele espera que o programa retorne [3, 5, 7]. Mas a saída do programa [1, 2] satisfará as especificações - porque "também é uma lista classificada, mas não a lista que você provavelmente esperava", diz Parno.

Em outras palavras, é difícil transformar a idéia do que um programa deve fazer em uma especificação formal que exclua qualquer interpretação incorreta do que você deseja do programa. E o exemplo dado descreve o programa de classificação mais simples. Agora imagine uma descrição de algo muito mais abstrato, como proteção por senha. “O que isso significa matematicamente? Para essa definição, pode ser necessário escrever uma descrição matemática do que significa "manter um segredo" ou o que significa que o algoritmo de criptografia é seguro ", diz Parno. "Consideramos todas essas questões e avançamos em seus estudos, mas elas podem ser extremamente difíceis de implementar."

Bloquear a segurança

De fato, é necessário escrever especificações e comentários adicionais necessários para que o software tire conclusões sobre o código. Um programa, incluindo sua confirmação formal, pode ter cinco vezes o tamanho de um programa regular escrito para o mesmo objetivo.

Esse fardo pode ser aliviado um pouco com ferramentas adequadas - linguagens de programação e programas auxiliares que ajudam os programadores a criar programas à prova de balas. Mas na década de 1970 eles não existiam. "Muitos aspectos da ciência e da tecnologia não cresceram o suficiente, então, na década de 1980, muitas áreas da ciência da computação perderam o interesse nisso", diz Appel, pesquisador principal do DeepSpec, um grupo de sistemas de computadores formalmente validado.

Apesar do aprimoramento das ferramentas, surgiu outra barreira para confirmar os programas: não havia certeza de que isso fosse necessário. Embora os entusiastas do método tenham dito que pequenos erros podem levar a grandes problemas, o restante chamou a atenção para o fato de que basicamente os programas de computador funcionam muito bem. Às vezes eles falham, sim - mas perder um pouco de dados não salvos ou às vezes reiniciar o sistema parece ser um preço pequeno a pagar por não ter que traduzir meticulosamente cada parte do programa para a linguagem da lógica formal. Com o tempo, mesmo aqueles que estavam na origem da confirmação do programa começaram a duvidar de seus benefícios. Nos anos 90, mesmo Hoar reconheceu que as especificações poderiam ser uma solução demorada para um problema inexistente. Em 1995, ele escreveu:

( ) , … , , .

Depois veio a Internet, que fez o mesmo com erros no código que as viagens aéreas fizeram para infecções: quando todos os computadores estão conectados, erros desconfortáveis, mas tolerantes, podem levar a problemas de segurança crescentes.

"Não entendemos completamente", diz Appel. "Existem programas abertos a todos os hackers da Internet e, se houver um erro nesse programa, ele poderá se tornar uma vulnerabilidade".

Quando os pesquisadores começaram a entender a seriedade das ameaças à segurança colocadas pela Internet, a confirmação do programa estava prestes a retornar. Para começar, os pesquisadores fizeram progressos nas partes fundamentais dos métodos formais. Isso é uma melhoria em programas auxiliares como Coq e Isabelle; desenvolvimento de sistemas lógicos ( teoria dos tipos dependentes) fornecer uma plataforma de desenvolvimento que ajude os computadores a avaliar o código; "Semântica operacional" é uma linguagem que possui as palavras certas para expressar o que é exigido do programa.

"Começando com a especificação na linguagem humana, você encontrou ambigüidades", diz Janette Wing , vice-presidente da Microsoft Research. - Qualquer linguagem natural contém ambiguidades. Na especificação formal, você escreve uma descrição exata com base na matemática para explicar o que deseja do programa. ”

Janette Wing da Microsoft Research

Além disso, os pesquisadores formais de métodos redefiniram seus objetivos. Nas décadas de 1970 e 1980, eles queriam criar sistemas de computador totalmente testados, de circuitos eletrônicos a programas. Hoje, a maioria dos pesquisadores trabalha em partes pequenas, mas mais críticas ou vulneráveis, de sistemas - por exemplo, sistemas operacionais ou protocolos criptográficos.

"Não estamos dizendo que provaremos que todo o sistema está 100% correto, até os circuitos eletrônicos", diz Wing. - Tais declarações são ridículas. Somos precisos no que podemos ou não podemos fazer. ”

O projeto HACMS mostra como você pode obter grandes garantias de segurança descrevendo uma pequena parte de um sistema de computador. O primeiro objetivo do projeto era criar um quadrocopter inquebrável para entretenimento. O software que acompanhava o quadriculado era monolítico - ou seja, ao obter acesso a uma parte dele, o hacker obteve acesso a todas as outras. Por dois anos, a equipe do HACMS dividiu o código no computador de controle em partes.

A equipe reescreveu a arquitetura do software usando o que Fisher chama de "blocos de construção de alta confiança" - ferramentas que permitem ao programador provar a pureza do código. Um deles fornece evidências de que, tendo obtido acesso a uma das unidades, não é possível escalar privilégios para alcançar as outras.

Mais tarde, os programadores instalaram esse software no "Bird". No teste com a equipe vermelha, ela recebeu acesso a uma das partes do sistema que controlava parte do helicóptero, por exemplo, a câmera - mas não as principais funções. O fracasso dos hackers foi matematicamente garantido. "Eles provaram de uma maneira verificável por máquinas que os hackers não podem ir além da partição do sistema, então isso não é surpreendente", diz Fisher. "Isso é consistente com o teorema, mas é sempre útil realizar um teste."

No ano seguinte à auditoria, a DARPA aplicou as ferramentas e tecnologias do projeto em outras áreas da tecnologia militar, por exemplo, satélites e caminhões automáticos. Novas iniciativas coincidem com a forma como a confirmação formal se espalhou nos últimos dez anos: cada projeto bem-sucedido incentiva o próximo. "Desculpas sobre a complexidade desse princípio não funcionam mais", diz Fisher.

Verifique a internet

Segurança e confiabilidade são dois dos principais objetivos que inspiram métodos formais. Todos os dias, a necessidade de melhorias está se tornando cada vez mais óbvia. Em 2014, um pequeno erro de software, que uma descrição formal detectaria, abriu caminho para um erro do Heartbleed que ameaçava quebrar a Internet. Um ano depois, alguns hackers "legais" confirmaram os piores temores sobre carros conectados à Internet, ganhando controle remoto sobre o Jeep Cherokee .

Com taxas mais altas, os pesquisadores formais de métodos estabelecem metas cada vez mais ambiciosas. A equipe do DeepSpec, liderada por Appel (que também trabalha no HACMS), está tentando criar um sistema tão complexo e totalmente testado como um servidor da web. Se for bem-sucedido, o projeto, que recebeu uma doação da Fundação de Ciências do Estado de US $ 10 milhões, reunirá muitos projetos bem-sucedidos menores da última década. Os pesquisadores criaram vários componentes seguros comprovados, como o kernel do sistema operacional. "O que não foi feito até agora é a integração desses componentes em interfaces específicas de especificações", diz Appel.

Na Microsoft Research, os programadores têm dois projetos ambiciosos. O primeiro, o Everest, visa criar uma versão validada do HTTPS, um protocolo para proteger navegadores da web que o Wing chama de "calcanhar de Aquiles da Internet".

O segundo é a criação de especificações confirmadas para sistemas ciber-físicos complexos, como UAVs. O projeto tem dificuldades significativas. Enquanto os programas convencionais trabalham com etapas separadas e inequívocas, os programas de controle por drone usam o aprendizado de máquina para tomar decisões probabilísticas com base em um fluxo contínuo de dados ambientais. Está longe de ser óbvio como as decisões lógicas podem ser tomadas com esse grau de imprecisão ou descritas como uma especificação formal. Mas apenas nos últimos dez anos, os métodos formais avançaram bastante, e Wing, gerenciando o projeto, acredita otimista que os pesquisadores serão capazes de resolver todos esses problemas.

Existe um código ininterrupto

Sonhos de programas perfeitos

Bloquear a segurança

Verifique a internet

More articles: