Skocz do zawartości
Forum Kopalni Wiedzy

Znajdź zawartość

Wyświetlanie wyników dla tagów 'Isabelle' .



Więcej opcji wyszukiwania

  • Wyszukaj za pomocą tagów

    Wpisz tagi, oddzielając je przecinkami.
  • Wyszukaj przy użyciu nazwy użytkownika

Typ zawartości


Forum

  • Nasza społeczność
    • Sprawy administracyjne i inne
    • Luźne gatki
  • Komentarze do wiadomości
    • Medycyna
    • Technologia
    • Psychologia
    • Zdrowie i uroda
    • Bezpieczeństwo IT
    • Nauki przyrodnicze
    • Astronomia i fizyka
    • Humanistyka
    • Ciekawostki
  • Artykuły
    • Artykuły
  • Inne
    • Wywiady
    • Książki

Szukaj wyników w...

Znajdź wyniki, które zawierają...


Data utworzenia

  • Od tej daty

    Do tej daty


Ostatnia aktualizacja

  • Od tej daty

    Do tej daty


Filtruj po ilości...

Dołączył

  • Od tej daty

    Do tej daty


Grupa podstawowa


Adres URL


Skype


ICQ


Jabber


MSN


AIM


Yahoo


Lokalizacja


Zainteresowania

Znaleziono 1 wynik

  1. 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.
×
×
  • Dodaj nową pozycję...