Software 100% livre de erros!

Software 100% livre de erros.
20/10/2009

É provável que estejamos frente a mais uma inovação revolucionária na área de software. 

Pesquisadores australianos relataram que, pela primeira vez, conseguiram provar com rigor matemático que o núcleo principal de um sistema operacional (kernel) está 100% livre de erros de programação (os famosos bugs).

Isto quer dizer que a parte principal do SO (sistema operacional) será imune a falhas, travamentos e nem a ataques que explorem falhas de segurança, (backdoors) que simplesmente não existem.

O avanço deverá ter implicações diretas no funcionamento e na segurança de computadores que controlam equipamentos que devem apresentar altíssima confiabilidade, como aparelhagens médicas robotizadas, sistemas aeroespaciais e servidores de informática . 

"Acredito que não é exagero afirmar que nosso sistema abre um mundo completamente novo no que diz respeito à construção de novos sistemas altamente confiáveis e seguros", diz o Dr. Gernot Heiser, que coordenou a equipe que desenvolveu a nova técnica nos laboratórios da Universidade Nova Gales do Sul, na Austrália.

Não se trata apenas de uma verificação intensiva do código contra erros específicos. O sistema de verificação garante que o kernel atende inteiramente a toda a sua especificação, não se desviando dela em todos os aspectos, incluindo a funcionalidade e a segurança Software livre de erros.

Uma regra no mundo do software - não-científica, mas largamente citada - é que existem 10 bugs para cada 1000 linhas de código de um programa.

Programas mais maduros e mantidos por grandes equipes certamente têm menos, mas nenhum engenheiro ou programador em bom juízo se arriscaria a dizer que seu sistema é 100% livre de erros.

Isto mostra o significado do feito alcançado pelos pesquisadores australianos, comprovando matematicamente a correção de um kernel desenvolvido em linguagem C por uma equipe de 6 pessoas ao longo de 6 anos.

Esta é a primeira vez que se demonstra de forma conclusiva que é possível construir programas de computador totalmente livres de erros. A correção do programa também significa que ele está imune a todos os tipos mais comuns de ataques, como os chamados buffer overflows, um forma de ataque na qual os crackers tomam controle dos programas injetando pequenas porções de código malicioso.

O usuário de computadores tradicionais deverá esperar um pouco antes de poder usufruir do acréscimo de segurança e confiabilidade oferecido por um sistema operacional livre de erros. 

O kernel 100% correto pertence a um sistema operacional do tipo embarcado (embedded system) que roda em computadores dedicados a tarefas específicas - seu nome é Secure Embedded L4 (seL4).

A nova técnica de verificação, contudo, poderá ser utilizada no desenvolvimento de qualquer outro programa, seja um sistema operacional ou outro aplicativo qualquer