Diariamente somos confrontados com actualizações de segurança que vêm corrigir bugs e vulnerabilidades que parecem nunca acabar; com a verificação formal, poderemos estar prestes a conseguir garantir a produção de código sem erros à prova de hackers.
Se durante muito tempo os erros de software eram algo que se associava a um crash inesperado que, nos piores casos, poderia obrigar a reiniciar a máquina; actualmente são coisas que mais se associam à potencial infecção por malware que pode deixar um sistema comprometido e sob controlo de um atacante. Se isso é algo preocupante num computador ou smartphone, ainda mais o é num mundo em que a internet se vai alastrando a dispositivos físicos, que vai dos electrodomésticos aos próprios automóveis.
Seria catastrófico que hackers conseguissem controlar remotamente automóveis ou, pior ainda, drones militares com potencial de devastação muito superior - e daí a necessidade de criar sistemas que garantam a produção de software à prova de hackers. Algo que a "verificação formal" parece conseguir garantir.
A ideia é tentar demonstrar que um programa é totalmente à prova de erros de forma idêntica à que é utilizada para comprovar teoremas matemáticos. Para isso há que criar definições matemáticas sobre as funções que o programa deve cumprir - o que nem sempre é fácil - mas que, quando é bem sucedido, permitirá garantir, com certeza quase absoluta, que se trata de código 100% à prova de erros e à prova de hackers. E os resultados até à data parecem estar a comprová-lo, com uma equipa de hackers a não ter conseguido ganhar controlo sobre o sistema de controlo de um drone verificado usando esta técnica.
... Talvez um dia o mesmo venha a poder ser aplicado às apps que usamos no nosso dia a dia, e fazer com que os recorrentes "bug fixes" desapareçam da descrição das actualizações, permitindo que as mesmas só aconteçam quando há algum funcionalidade nova a acrescentar à app. ;)
Sem comentários:
Enviar um comentário (problemas a comentar?)