Skocz do zawartości
Forum Kopalni Wiedzy

Rekomendowane odpowiedzi

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.

Udostępnij tę odpowiedź


Odnośnik do odpowiedzi
Udostępnij na innych stronach

niech wypuszcza ten kernel jako opensource to zaraz znajdzie się cwaniak, który pośle ich 200 000 linii dowodu matematycznego w kosmos :P

Udostępnij tę odpowiedź


Odnośnik do odpowiedzi
Udostępnij na innych stronach

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.

każda z linii kodu jest w pełni zgodna ze specyfikacją

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.

Udostępnij tę odpowiedź


Odnośnik do odpowiedzi
Udostępnij na innych stronach

Jeśli chcesz dodać odpowiedź, zaloguj się lub zarejestruj nowe konto

Jedynie zarejestrowani użytkownicy mogą komentować zawartość tej strony.

Zarejestruj nowe konto

Załóż nowe konto. To bardzo proste!

Zarejestruj się

Zaloguj się

Posiadasz już konto? Zaloguj się poniżej.

Zaloguj się

  • Podobna zawartość

    • przez KopalniaWiedzy.pl
      Naukowcy od dziesięcioleci spierają się o to, czy dochodzi do wymiany materiału pomiędzy jądrem Ziemi, a warstwami położonymi powyżej. Jądro jest niezwykle trudno badać, częściowo dlatego, że rozpoczyna się na głębokości 2900 kilometrów pod powierzchnią planety.
      Profesor Hanika Rizo z Carleton University, wykładowca na Queensland University of Technology David Murphy oraz profesor Denis Andrault z Universite Clermont Auvergne informują, że znaleźli dowody na wymianę materiału pomiędzy jądrem, a pozostałą częścią planety.
      Jądro wytwarza pole magnetyczne i chroni Ziemię przed szkodliwym promieniowaniem kosmicznym, umożliwiając istnienie życia. Jest najcieplejszym miejscem Ziemi, w którym temperatury przekraczają 5000 stopni Celsjusza. Prawdopodobnie odpowiada ono za 50% aktywności wulkanicznej naszej planety.
      Aktywność wulkaniczna to główny mechanizm, za pomocą którego Ziemia sie chłodzi. Zdaniem Rizo, Murphy'ego i Andraulta niektóre procesy wulkaniczne, np. te na Hawajach czy na Islandii, mogą brać swój początek w jądrze i transportować ciepło bezpośrednio z wnętrza planety. Twierdzą oni, że znaleźli dowód na to, iż do płaszcza ziemskiego trafia materiał z jądra.
      Odkrycia dokonano badając niewielkie zmiany w stosunku izotopów wolframu. Wiadomo, że jądro jest zbudowane głównie z żelaza i aluminium oraz z niewielkich ilości wolframu, platyny i złota rozpuszczonych w żelazno-aluminiowej mieszaninie. Wolfram ma wiele izotopów, w tym wolfram-182 i wolfram-184. Wiadomo też, że stosunek wolframu-182 do wolframu-184 jest w płaszczu znacznie wyższy niż w jądrze. Dzieje się tak dlatego, że hafn, który nie występuje w jądrze, posiada izotop hafn-182. Izotop ten występował w przeszłości w płaszczu, jednak obecnie już go nie ma, gdyż rozpadł się do wolframu-182. Właśnie dlatego stosunek wolframu-182 do wolframu-184 jest w płaszczu wyższy niż w jądrze.
      Uczeni postanowili więc zbadać stosunek izotopów wolframu, by przekonać się, czy na powierzchni występują skały zawierające taki skład wolframu, jaki odpowiada jądru. Problem w tym, że istnieje mniej niż 5 laboratoriów zdolnych do badania wolframu w ilościach nie przekraczających kilkudziesięciu części na miliard.
      Badania udało się jednak przeprowadzić. Wykazały one, że z czasem w płaszczu Ziemi doszło do znaczącej zmiany stosunku 182W/184W. W najstarszych skałach płaszcza stosunek ten jest znacznie wyższy niż w skałach młodych. Zespół badaczy uważa, że zmiana ta wskazuje, iż materiał z jądra przez długi czas trafiał do płaszcza ziemskiego. Co interesujące, na przestrzeni około 1,8 miliarda lat nie zauważono zmiany stosunku izotopów. To oznacza, że pomiędzy 4,3 a 2,7 miliarda lat temu do górnych warstw płaszcza materiał z jądra nie trafiał w ogóle lub trafiało go niewiele. Jednak 2,5 miliarda temu doszło do znaczącej zmiany stosunków izotopu wolframu w płaszczu. Uczeni uważają, że ma to związek z tektoniką płyt pod koniec archaiku.
      Jeśli materiał z jądra trafia do na powierzchnię, to oznacza, że materiał z powierzchni Ziemi musi trafiać głęboko do płaszcza. Proces subdukcji zabiera bogaty w tlen materiał w głąb planety. Eksperymenty zaś wykazały, że zwiększenie koncentracji tlenu na granicy płaszcza i jądra może spowodować, że wolfram oddzieli się od jądra i powędruje do płaszcza. Alternatywnie, proces zestalania wewnętrznej części jądro może prowadzić do zwiększenia koncentracji tlenu w części zewnętrznej. Jeśli uda się rozstrzygnąć, który z procesów zachodzi, będziemy mogli więcej powiedzieć o samym jądrze Ziemi.
      Jądro było w przeszłości całkowicie płynne. Z czasem stygło i jego wewnętrzna część skrystalizowała, stając się ciałem stałym. To właśnie obrót tej części jądra tworzy pole magnetyczne chroniące Ziemię przed promieniowaniem kosmicznym. Naukowcy chcieliby wiedzieć, jak przebiegał proces krystalizacji o określić jego ramy czasowe.

      « powrót do artykułu
    • przez KopalniaWiedzy.pl
      Microsoft zaprezentował materiał wideo, z którego wynika, iż system Windows 8 może uruchamiać się nawet w ciągu kilkunastu sekund. W porównaniu z Windows 7 czas startu nowego OS-u będzie krótszy - w zależności do konfiguracji - o 30-70 procent.
      Inżynierowie Microsoftu osiągnęli to stosując pewną sztuczkę. Otóż podczas zamykania systemu do pliku hibernacyjnego nie jest zapisywana cała zawartość pamięci. System zapisuje tylko sesje użytkownika oraz minimum informacji o stanie jądra. Sesja nie jest wyłączana, a hibernowana. Następnie podczas startu następuje dekompresja pliku i odczytanie z niego danych.
      Największe oszczędności osiągną użytkownicy interfejsu UEFI. Jest on bowiem nowocześniejszy od BIOS-u, a jego kod lepiej zoptymalizowano. Microsoft zapewnia, że nowy sposób startu będzie zauważalny dla użytkowników każdego komputera, a na maszyna z UEFI korzystających z szybkich dysków SSD różnica jest „dramatyczna".
       
      http://www.youtube.com/watch?v=9ia3zBs42cc
    • przez KopalniaWiedzy.pl
      Linus Torvalds zdecydował, że obecna wersja jądra Linuksa 3.1 zostanie opublikowana za pośrednictwem Github, a nie Kernel.org. Ten ostatni serwis padł bowiem ofiarą włamania i wciąż nie można uznać go za w pełni bezpieczny.
      Torvalds podkreśla, że jego decyzja nie oznacza rezygnacji z Kernel.org. Postanowił jedynie, że kolejne wersje jądra będą publikowane na bieżąco. Tymczasem administratorzy Kernel.org wciąż nie poradzili sobie z infekcją rootkitem Phalanx.
      Wszystko wskazuje na to, że ataku nie zauważono przez 17 dni. Obecnie trwają prace mające na celu oczyszczenie serwerów Kernel.org i ich zabezpieczenie.
    • przez KopalniaWiedzy.pl
      Serwis LWN.net, który regularnie bada kto i ile zmian wniósł do rozwoju jądra Linuksa informuje, że w pierwszej dziesiątce firm wprowadzających takie innowacje znajduje się... Microsoft. Koncern z Redmond jest na 7. miejscu listy z 361 zmianami w przygotowywanym jądrze 3.0. Dla porównania Red Hat wprowadził 1000 zmian, Intel jest autorem 839, a niezależni deweloperzy - 1085.
      Microsoft wprowadza bardzo niewielkie zmiany, obejmujące najczęściej kilka linijek kodu. W najnowszym jądrze firma Ballmera dokonała zmian w zaledwie 11564 liniach kodu, co stanowi zaledwie 1,3%. Tymczasem Intel zmienił aż 163 232 linie (18,1%). Większość zmian dokonanych przez Microsoft dotyczyła sterownika dla firmowej technologii wirtualizacji HyperV.
    • przez KopalniaWiedzy.pl
      Na Linux Kernel Mailing list ukazał się wpis Linusa Torvaldsa, w którym proponuje on zakończenie prac nad jądrem 2.6.x i przygotowanie jądra 2.8. Obecnie kończą się prace nad 40. już wersją jądra 2.6. PS. Głosy w mojej głowie mówią mi, że liczby są już zbyt duże. Może nazwiemy tą wersję 2.8.0. Mogę wam zagwarantować, że to Post Scriptum wywoła więcej dyskusji niż reszta mojego wpisu, ale gdy głosy do mnie mówią - słucham - czytamy w poście Torvaldsa.
      Jedyną poważną odpowiedź otrzymał Torvalds od Grega Kroaha-Hartmana, którego takie stanowisko twórcy Linuksa bardzo ucieszyło. Kroah-Hartman już w 2008 roku proponował porzucenie numeracji 2.6 i zastosowanie nowego schematu, jak np. 2009.0.0. Pozwalałby on bowiem na pierwszy rzut oka sprawdzić wiek danej wersji jądra.
      W późniejszym wpisie Torvalds zaproponował oznaczenie nowej wersji numerem 3.0.
  • Ostatnio przeglądający   0 użytkowników

    Brak zarejestrowanych użytkowników przeglądających tę stronę.

×
×
  • Dodaj nową pozycję...