• Home
  • Química
  • Astronomia
  • Energia
  • Natureza
  • Biologia
  • Física
  • Eletrônicos
  • A verificação matemática testa se o software é executado conforme anunciado
    p Crédito CC0:domínio público

    p Quando se trata de segurança, o que você não sabe pode te machucar. p A maioria das pessoas nunca pensa sobre a criptografia subjacente às atividades on-line seguras, incluindo serviços bancários, compras e comunicações. Mas todos dependem de programas de computador para gerar um número aleatório que serve como uma chave para desbloquear a comunicação criptografada. O problema é que pequenos erros de programação podem tornar esses sistemas vulneráveis, e essas vulnerabilidades muitas vezes podem ser muito difíceis de detectar.

    p "Sempre que você se conecta à Amazon para fornecer o número do seu cartão de crédito, sempre que você fizer login em algum lugar por meio de uma conexão segura, você depende de chaves criptográficas geradas aleatoriamente, "disse Andrew Appel, o professor Eugene Higgins de ciência da computação em Princeton. "E se o adversário, o espião que está tentando ler suas mensagens ou se passar por você, poderia adivinhar qual número aleatório seu computador estava usando, então, ele pode saber qual chave você vai usar e pode personificar seu tráfego e ler suas mensagens. "

    p A pesquisa de Appel há muito tempo se concentra na interseção da computação e das políticas públicas. Ele escreveu extensivamente sobre tecnologia de máquina de votação e testemunhou perante o Congresso sobre métodos para proteger o sistema eleitoral dos EUA. Em trabalho recente, sua pesquisa se concentrou na verificação formal, um conjunto de ferramentas "para especificar o que os programas devem fazer, para construir programas que estejam em conformidade com essas especificações, e para verificar se os programas se comportam exatamente como especificado, "de acordo com o site da DeepSpec, um projeto multi-institucional liderado por Appel.

    p Em um exemplo de verificação matemática da exatidão de uma função crítica, O grupo de Appel desenvolveu um método para verificar a força dos geradores de números aleatórios que formam a base da maioria dos sistemas de criptografia. Em um artigo desenvolvido a partir do trabalho de tese sênior de Katherine Ye '16, a equipe (que também incluiu pesquisadores da Johns Hopkins University e da Oracle) examinou um gerador de números aleatórios comumente usado e produziu uma prova abrangente e verificada por máquina de que o sistema é realmente seguro. Métodos convencionais, como testes exaustivos, não podem dizer se um gerador de números aleatórios é seguro.

    p Comentando sobre o trabalho, Eugene Spafford, líder em segurança e garantia da informação na Purdue University, disse que a pesquisa é um avanço significativo. "Como muitas outras pesquisas, pode não se aplicar diretamente à sua vida e à minha no momento, mas está construindo um conjunto de resultados que podem [levar a] resultados muito importantes no futuro. "


    © Ciência https://pt.scienceaq.com