Já é ruim perder uma hora de trabalho quando seu computador trava, mas em ambientes como saúde e aviação, falhas de software podem ter consequências muito mais sérias. Em um caso notório, um bug de computador fez com que pacientes com câncer recebessem overdoses letais de uma máquina de radioterapia; em manchetes mais recentes, software defeituoso foi responsabilizado por acidentes de avião na Etiópia e na Indonésia.

Agora, pesquisadores do Stevens Institute of Technology, em colaboração com a Yale University, estão desenvolvendo ferramentas que podem tornar muito menos prováveis ​​acidentes catastróficos com computadores. Liderado por Eric Koskinen, professor assistente de ciência da computação na Stevens, o trabalho não visa apenas garantir que os programas funcionem corretamente em situações específicas, mas também usa algoritmos para determinar se é logicamente possível, em qualquer circunstância, para que o software produza resultados indesejados.

"O que pretendemos é uma garantia de 100 por cento de que você nunca encontrará um bug, "disse Koskinen.

A equipe de Koskinen, apoiado por mais de US $ 2,5 milhões do Office of Naval Research, modela diferenças entre duas versões de um programa. Isso é útil porque os programadores geralmente trabalham com base no software existente, em vez de escrever código do zero, e bugs podem ser introduzidos de uma versão para a próxima. Essa abordagem é especialmente valiosa para os militares, uma vez que as agências de defesa freqüentemente compram software de empreiteiros privados, em seguida, faça alterações internamente antes de implantá-los em situações de missão crítica.

"Eles precisam de uma forma de confirmar que fizeram as alterações corretamente internamente, e não introduziu novos problemas, "Koskinen disse.

Para provar matematicamente que um programa de computador nunca poderia ter qualquer tipo de bug, não importa as circunstâncias, antecipado ou não imaginado, A equipe de Koskinen usa uma estratégia chamada lógica temporal. Em vez de examinar linhas individuais de código para procurar diferenças sintáticas, O time, incluindo o professor assistente Jun Xu, um especialista em análise binária na Stevens, examina como um programa se comporta ao longo do tempo. A ideia é provar que não importa quanto tempo o programa rode, não há uma maneira lógica de retornar um resultado indesejado.

Modelar a estrutura e o comportamento de um programa, em vez de se debruçar sobre linhas individuais de código, é importante porque as mesmas linhas de código podem ter efeitos diferentes em contextos diferentes, assim como linhas de código que parecem muito diferentes podem realizar a mesma coisa. É como estudar um documento legal, Koskinen explica:mudar uma única palavra pode parecer trivial, mas pode mudar todo o significado do documento. A lógica temporal ajuda a modelar o potencial de um programa, obtendo insights poderosos sobre os recursos do mundo real do programa.

A abordagem da equipe também permite eliminar bugs em software comercial de prateleira para o qual o código-fonte não está disponível. Sem o código-fonte, a equipe precisa comparar os programas de computador usando a versão binária do código-fonte. "É difícil ver se a vulnerabilidade foi realmente eliminada se você não puder ver o código-fonte, "disse ele." As técnicas que estamos construindo farão isso:se você tiver uma versão do software em que confia, nossas técnicas serão capazes de ajudá-lo a detectar mudanças - vulnerabilidades em atualizações de software ou malware inserido em programas executáveis ​​- e decidir se confia na nova versão. "

A equipe de Koskinen também está desenvolvendo um kit de ferramentas que outros pesquisadores e membros do público poderão usar para testar software - e estão ampliando sua abordagem para trabalhar com programas maiores e falhas mais complexas. "Esses são grandes problemas que assolam os sistemas de computadores modernos, "disse Koskinen." Essas questões só vão se tornar mais críticas - em áreas como saúde, aviação, veículos autônomos, e muitos mais - portanto, é vital desenvolvermos técnicas práticas para tornar os sistemas controlados por computador livres de bugs e seguros para uso. "