Oprogramowania idealne
Australijska organizacja NICTA ogłosiła powstanie pierwszego w historii jądra systemu operacyjnego, które nie tylko zostało w całości matematycznie opisane, ale również przeprowadzono matematyczne dowody na to, iż każda z linii kodu jest w pełni zgodna ze specyfikacją.
Oznacza to, że mikrojądro Secure Embedded L4 (seL4) jest wolne od zdecydowanej większości błędów, jest zatem odporne na większość ataków. Prace nad seL4 trwały przez cztery lata, a osiągnięciem Australijczyków zainteresowali się liczni specjaliści. Tak bezpieczne mikrojądro przyda się wojsku, służbom specjalnym, przedsiębiorstwom czy organizacjom rządowym.
- Trudno przecenić znacznie tego wydarzenia. Matematyczne udowodnienie bezbłędnego napisania 7500 linii kodu w języku C w jądrze systemu operacyjnego to coś wyjątkowego, co może prowadzić do powstania oprogramowania o niewyobrażalnej obecnie jakości - mówi profesor Lawrence C. Paulson, z laboratorium komputerowego Cambridge University.
- Formalne dowody jakości poszczególnych funkcji były przeprowadzana dla mniejszych jąder, a nam udało się przeprowadzić taki dowód dla ogólnych właściwości. Nikt wcześniej nie osiągnął tego samego dla tak wydajnego rozwiniętego kodu o takim stopni skomplikowania - stwierdził doktor Gerwin Klein z NICTA.
Matematyczny dowód na jakość jądra to również dowód na to, że jest ono całkowicie odporne na wiele typów ataków. Wiadomo na przykład, że seL4 jest całkowicie niewrażliwe na przepełnienie bufora.
Sam dowód jest znacznie bardziej rozległy, niż jądro, którego dotyczy. Składa się on bowiem z 200 000 linii. Prawdziwość dowodu została zweryfikowana za pomocą wyspecjalizowanego oprogramowania Isabelle stworzonego na politechnice w Monachium. To jednocześnie jeden z najrozleglejszych matematycznych dowodów, które weryfikowano za pomocą maszyn.
- To niezwykłe wydarzenie. Oznacza ono znaczący krok na drodze stworzenia systemu, który będzie w stanie w pełni weryfikować oprogramowanie w celu uzyskania rozsądnych gwarancji jego rzetelności - stwierdził profesor Zhong Shao z Yale University.
Prawa własności intelektualnej do stworzonej przez Australijczyków procedury zostaną przeniesione do należącej do NICTA firmy Open Kernel Labs.
Mariusz Błoński
