Une équipe de chercheur du NICTA (Australia's Information and Communications Technology Centre of Excellence) a écrit un micro-noyau de système d'exploitation orienté système embarqué dont la sécurité face à plusieurs types de failles a été prouvé formellement (typiquement, des buffers overflow).

L'écriture des 7500 lignes de code a nécessité 4 ans, la preuve est composé de 10.000 théorèmes et de 200.000 lignes de preuves.

L'utilité de ceci est d'être sûr que certaines failles classiques ne peuvent être exploités.


Vous en pensez-quoi ?

Plus de détails sur le projet : http://www.ertos.nicta.com.au/research/sel4/