Estudo do Kernel Error-Free

Os matemáticos como sabemos não são apenas homenzinhos de óculos grossos com cara de nerds que dão aulas de matemática. Há uma miríade de aplicações para a matemática e algumas dessas aplicações são menos evidentes...

Uma das equipas que estuda algo que eu não sabia que se estudava desta forma é a do Dr. Gernot Heiser que é professor na   
School of Computer Science and Engineering da University of New South Wales (UNSW), Sydney, Australia.

O grupo que ele lidera dedica-se a Secure Embedded L4 Systems (SeL4) ou seja, ao estudo de sistemas informáticos protegidos embedded (não gosto da palavra embebidos... parece que levaram com uns shots de vodka moscovskaya). Traduzindo para linguagem corrente eles dedicam-se a estudar sistemas de processamento informático de alta segurança para tentarem eliminar as fragilidades do código dos sistemas operativos. É através de bugs que os hackers fazem os seus ataques a sistemas operativos e aplicações e se houver forma de elminiar esses bugs eliminamos os hackers. É lógico que estamos num campo um pouco utópico mas esta quimera parece ter tido desenvolvimentos. Precisamente os matemáticos deste grupo ocnseguiram provar que é possível construir um kernel (é o núcleo do SO) "error-free". Isto parece peanuts mas é mesmo um grande avanço.

Se bem que construir esse kernel ainda vá demorar alguns anos pelo menos o algoritmo desenvolvido para descobrir os erros num kernel já está operacional e pode ajudar ao desenvolvimento de código mais robusto mesmo para os sistemas de hoje.

Ora aqui está um exemplo de matemática ao serviço do consumidor geral que nem imagina de onde vem todos os gadgets a que temos acesso hoje em dia...

Abração error-free!!
I.