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ć znaczenie 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 stopniu 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 najrozreglejszych matematycznych dowodów, które weryfikowano za pomocą maszyn.
To niezwykłe wydarzenia. 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.
Komentarze (2)
Zerivael, 17 sierpnia 2009, 16:26
niech wypuszcza ten kernel jako opensource to zaraz znajdzie się cwaniak, który pośle ich 200 000 linii dowodu matematycznego w kosmos
Eselix, 17 sierpnia 2009, 23:10
Ciekawe podejście do zagadnień bezpieczeństwa. Może taka będzie przyszłość tworzenia oprogramowania. Choć zauważam kilka luk w takim postępowaniu.
No właśnie, trzeba by wcześniej udowodnić, że specyfikacja zapewnia bezpieczeństwo. Raczej nikt nie przewidzi wszystkich możliwych scenariuszy jakie zastosują ewentualni hackerzy.
Po drugie programy składają się z wielu modułów, jeden robi to, drugi tamto. Zbadanie ich osobno może nie wykazywać żadnych błędów, ale mogą one na siebie wzajemnie oddziaływać i w specyficznych warunkach doprowadzić do błędnego działania. Tak jak w jednym z ostatnich błędów w Linuxie, gdzie narzędzie do zapewnienia bezpieczeństwa SELinux, w połączeniu z optymalizacją w jądrze, otwierało lukę dla hackerów.
No i jeszcze pozostaje najsłabsze ogniwo - człowiek. Jak ja słyszę, że jakiś menadżer projektu gry Half-Life zaraził swój komputer przez emaila i pozwolił hackerom na zdobycie kodu gry, oprogramowanie w wojsku jest nieaktualizowane od dziesiątków lat, sekretarki wyrzucają dane klientów, np numery kart kredytowych, na śmietnik albo jakieś inne tajne dokumenty ludzie zabierają sobie do domu - to żadne mikrojądro przed tym nie zabezpieczy.