heh.pl
Kanał informacyjny Heh.pl


Piątek 29 marca 2024 r.

artykuły | abc komputera (archiwum) | forum dyskusyjne | redakcja


Poniedziałek, 17 sierpnia 2009, 17:04

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 najrozreglejszych matematycznych dowodów, które weryfikowano za pomocą maszyn.

Mariusz Błoński


Wersja do druku
Poleć znajomym: Udostępnij

Podobne tematy


Starsze

17.08.2009 r.

Litografia i DNA, 17:01

Lenovo wymienia wadliwe baterie w ThinkPadach, 17:00


Nowsze

17.08.2009 r.

Rewolucyjny spaser, 17:08

Samsung: Komórka dla niewidomych, 17:10


Redakcja nie ponosi odpowiedzialności za wypowiedzi Internautów opublikowane na stronach serwisu oraz zastrzega sobie prawo do redagowania, skracania bądź usuwania komentarzy zawierających treści zabronione przez prawo, uznawane za obraźliwie lub naruszające zasady współżycia społecznego.


Brak komentarzy. Może warto dodać swój własny?



Autor:  










Copyright © 2002-2024 | Prywatność | Load: 1.43 | SQL: 13 | Uptime: 328 days, 4:21 h:m | Wszelkie uwagi prosimy zgłaszać pod adresem eddy@heh.pl