neprihlásený Utorok, 23. apríla 2019, dnes má meniny Vojtech   DonaskaKvetov.sk - donáška kvetov v SR a zahraničí Pošli kvety
Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti

DSL.sk, 15.8.2009


Austrálsky výskumný ústav Information and Communications Technology Centre of Excellence, Nicta, informoval tento týždeň o vyvinutí nového mikrokernelu, základu operačného systému, u ktorého autori zároveň matematicky dokázali jeho korektnosť a bezpečnosť.

Podľa Nicta je ich mikrokernel vôbec prvým všeobecnoúčelovým jadrom operačného systému s matematickým dôkazom o svojej korektnosti a bezchybnosti.

Mikrokernel Secure Embedded L4, seL4, má byť vhodný ako operačný systém do zariadení používaných v kritických nasadeniach napríklad v armáde, automobiloch, letectve.

Dôkaz podľa autorov dokázal, že seL4 napísaný v jazyku C funguje vždy v súlade so špecifikáciou a zároveň neobsahuje typické bezpečnostné chyby ako sú pretečenie buffera, rozličné chyby ukazovateľov a špeciálne použitie nulových ukazovateľov, úniky pamäte a aritmetické pretečenia a výnimky.

Dôkaz bol uskutočnený na úrovni jazyka C a je platný za predpokladu, že hardvér a prekladač z jazyka C do assemblera a strojového kódu fungujú správne.

Mikrokernel seL4 má celkom 8 700 riadkov kódu v jazyku C. Dôkaz bol uskutočnený pre 7 500 riadkov, pre zvyšných 1 200 riadkov zodpovedných za jednorazové bootovanie dôkaz uskutočnený nebol rovnako ako pre ďalších 600 riadkov assembler kódu. Dôkaz bol uskutočnený počítačovo softvérom Isabelle a má celkom 200 tisíc riadkov.

Podľa tlačovej správy Nicta tím vyvíjajúci seL4 vyvinul viacero nových techník a získal viacero poznatkov, ktoré výrazne uľahčia dokazovanie korektnosti a bezchybnosti aj ďalšieho softvéru.


      Zdieľaj na Twitteri



Najnovšie články:

Podľa Muska bude v 2020 na cestách milión samojazdiacich Tesla taxíkov
Vydané Ubuntu 19.04
Okná v kartách vo Windows 10 nakoniec zrejme nebudú - aktualizácia 1
Ďalšia smartfónová kauza Samsungu, zrušil spustenie predaja Galaxy Fold
Samsung ruší predstavenie Galaxy Fold vo viacerých krajinách
SpaceX mala vážne problémy pri teste lode pre ľudskú posádku
Identifikovaný prvý objekt nepochádzajúci z našej sústavy, ktorý narazil do Zeme
Pre .sk technicky spustená podpora bezpečného DNS, DNSSEC
Android ponúkne iné prehliadače a vyhľadávače, ako to bude vyzerať
NASA detekovala prvotnú molekulu vesmíru


Diskusia:
                               
 

Toto by mal kupit a pouzit microsoft vo windowse
Odpovedať Známka: 3.8 Hodnotiť:
 

numb3rs :D
Odpovedať Známka: 5.4 Hodnotiť:
 

A čo ak sa zle vyráta ten matematický dôkaz?
Odpovedať Známka: 8.3 Hodnotiť:
 

Ide asi o nieco na styl unit-testov.
Odpovedať Známka: -3.3 Hodnotiť:
 

Nie, unit-testy a klasicke testovanie su schopne okrem uplne trivialnych pripadov iba najst bug.

Formalna verifikacia ukaze , ze skumany software
vzhladom na formalizovanu specifikaciu bugy nema.

Navyse je medzi nimi v tom, ze formalna verifikacia
pracuje s formalnou semantikou daneho jazyka(funguje staticky), zatial co unit-test je kod v danom jazyku,
ktory sa spusta.




Odpovedať Známka: 10.0 Hodnotiť:
 

Zial, od jednoducheho mikrokernelu k nasadeniu v praxi, je velmi dlha plejada kniznic, poskytujuca neprieberne moznosti, vyskytu chyb:)

Nechcem nijak znizovat ich vyskumnu pracu, automaticka analyza sw je vskutku zasluzna vec, ale zrovna v pripade mikrokernelu to s tou (ne)bezpecnostou a chybovostou az tak nehori. Vsak mk su od podstaty navrhnute tak, aby boli male a aby poskytovali iba zakladnu funkcionalitu a abstrakciu nad HW. Mnozstvo kodu v mikrokerneli byva na takej urovni, ze sa da skontrolovat aj manualne...
Odpovedať Známka: 8.9 Hodnotiť:
 

Asi tak nejako. Pravdepodobnost vyskytu chyby rastie s mnozstvom kodu, ale nie linearne. Preto bezchybny soft dnes prakticky neexistuje.
Odpovedať Známka: 6.7 Hodnotiť:
 

ale OpenBSD ma k tomu velmi blizko...
Odpovedať Známka: -3.3 Hodnotiť:
 

Preco chces za kazdu cenu robit Flame?
Odpovedať Známka: 4.7 Hodnotiť:
 

Ak by si vedel, ze svetlo sviecky je plamen, jedlo by uz bolo davno uvarene ;)
Odpovedať Známka: 4.5 Hodnotiť:
 

Kód o 8000 riadkoch pre celý kolektív je nič a kernel s toľkými riadkami určite nič nedokáže, je to proste blaf, kernel nič nevie a nemá sa na čom kusnúť, nech spravia druhý Linux s podporov tisícov zariadení, bezpečnostnou politikou, multiužívateľský a potom sa môžeme baviť bugoch, blaf, blaf, blaf.
Odpovedať Známka: -2.2 Hodnotiť:
 

Na mikrokernel to aj bude stacit. Tam nie je potrebne mat implementovane vsetko a so zameranim na automobily a ine samostatne zariadenia uz vobec nie multiuzivatelske prostredie ;)
Odpovedať Známka: 10.0 Hodnotiť:
 

http://tinyurl.com/m3ttjt
Odpovedať Hodnotiť:
 

A nema k tomu OpenBSD blizko ? :P
Odpovedať Známka: -6.8 Hodnotiť:
 

k vyvrcholeniu
Odpovedať Známka: 6.4 Hodnotiť:
 

OpenBSD nepouziva mikrokernel
Odpovedať Známka: 10.0 Hodnotiť:
 

Prave rozdiel medzi mikrokernelom a monolitickym kernelom je v tom, ze je maly, preto aj matematicky dokaz korektnosti bude "maly" (velkost dokazu exponencialne vzrasta). Vsetko ostatne su samostatne nezavisle moduly, ktore sa budu verifikovat samostatne. Takze je mozne overit vsetky sucasti samostatne a potom vyhlasit celok za korektny.

Na mnozstve kodu nezalezi, aj v parriadkovom kode mozes spravit chybu, ktoru si manualnou verifikaciou nevsimnes ;)
Odpovedať Známka: 5.6 Hodnotiť:
 

To nie je pravda. Nedá sa s určitosťou povedať, že ak objekty
bezchybne otestujem jednotlicvé časti a tie následne pospájam do celku, že ten bude v praxi rovnako bezchybné.
Moje poznatky sú také, že sa vyskytnú nové a podstatne zložitejšie problémy. Na mnohé z nich sa prakticky ani nedá naraziť ak testujete objek samostatne, teda nie ako celok...
Odpovedať Známka: 8.0 Hodnotiť:
 

Ak sa otestuje, teda skor verifikuje, samostatny modul a dokaze sa, ze na dany vstup da vzdy korektny vystup, tak druhy objekt, ktory pracuje s tymto modulom uz nie je potrebne verifikovat spolu s tymto modulom, ale len vzhladom k vystupom ake generuje ten dany modul.

Velmi zjednoduseny priklad: ak mam stroj, ktory niekolko dni nieco spracovava a jeho jedine 2 vystupy su "Success", "Error" (true/false) a nejaky softver, ktory dany stroj kontroluje, nemusim pri verifikacii softveru zaroven verifikovat aj stroj, pretoze ten uz verifikaciou presiel a bolo dokazane, ze iny vystup produkovat nebude.
Odpovedať Známka: 0.0 Hodnotiť:
 

Nemas pravdu, toto casto neplati napriklad pri paralelnom kode, kde sa mozu vyskytovat liviness/starvation/deadlock chyby (napriklad sa tvoje 2 stroje mozu dostat do deadlocku).
Odpovedať Známka: 6.0 Hodnotiť:
 

Neviem presne o aky druh verifikacie slo v tomto pripade, ale jednoduchy (spin) model checking je urceny na verifikaciu programov, ci uz single thread/process, ale aj paralelnych a distribuovanych systemov ;)
Tato verifikacia okrem liviness/starvation/deadlock chyb zistuje, ci je dany system (ne)schopny dosiahnut urcity stav/konfiguraciu a presne urcit akym sposobom tento stav nastal. Takze ti presne popise pripady ako k deadlocku doslo a nepotrebujes ziadny debug :)

A ak narazas cisto na moj zjednoduseny priklad, tak s deadlockom 2 strojov by mal pocitat ten softver. Ale kedze deadlock nemoze nastat (formalne dokazane) bude treba osetrit iny pripad, teda uplne vyradenie strojov z cinnosti, najjednoduchsie nejakym timeoutom na danu ulohu - ale to uz je ina vec (ktora sa taktiez da odchytit formalnou verifikaciou ;)
Odpovedať Hodnotiť:
 

toto slo cez refinement z abstraktneho modelu na C-implementaciu v systeme Isabelle/HOL..

Mne islo o to, ze ked mas paralelny kod v komponentach,
tak musis uvazovat aj ine behavioralne vlastnosti ako
vstupne a vystupne podmienky pri imperativnom programovani...


Odpovedať Hodnotiť:
 

Ked mas samostatnu jednotku, vedies dokaz voci tomu, ze je korektna ako samostatna jednotka.

Ak mas vsak komponenty, ktore su zavisle jedna od druhej, tak musis dokazat, ze su korektne aj v takom spojeni v akom sa budu pouzivat. Ale aj tam sa da dokaz zjednodusit, pretoze nie je nutne verifikovat interne vypocty danej komponenty v celku, ale len komunikaciu s okolim.

A ake ine vlastnosti mas na mysli?
Odpovedať Hodnotiť:
 

uz spomenute deadlock/livines/starvation, ale tych vlastnosti
moze byt viac, zavisi od specifikacie(napriklad cez formuly v modalnom mu-calcule)
Ale myslim, ze uz si v principe rozumieme("...musis dokazat, ze su korektne aj v takom spojeni v akom sa budu pouzivat.")..:)
Odpovedať Hodnotiť:
 

Ty si dnes asi šňupol tabáčika-chytráčika, fšagáno???
Odpovedať Hodnotiť:
 

Murphyho zákony platia vždy a všade.
Odpovedať Známka: 9.1 Hodnotiť:
 

tj ked murphyho zakon nemusi aspon v jednom pripade fungovat, tak nebude? :D
Odpovedať Známka: 4.3 Hodnotiť:
 

Toto ma obrovsku buducnost.
Odpovedať Známka: 1.4 Hodnotiť:
 

Co ak je ten dokaz mylny? Clanok sa mal volat radsej:

Vyšinutý operačný systém s matematickým dôkazom o svojej nebezpečnosti
Odpovedať Známka: 1.4 Hodnotiť:
 

potom treba dokaz o spravnosti dokazu, dokaz o spravnosti dokazu dokazu, dokaz o spravnosti dokazu dokazu dokazu, dokaz o spravnosti dokazu dokazu dokazu dokazu ...
Odpovedať Známka: 10.0 Hodnotiť:
 

Poznam jedneho velkeho programatora, ktory programoval sam svoj vlastny OS, teda stale na nom pracuje.
pre viac info www.zexos.org
Odpovedať Hodnotiť:
 

Nuz, ked ho teda poznas, tak mu odkaz, ze cim skor ho to prestane bavit, tym lepsie. Mohol by svoj talent investovat do niecoho prospesnejsieho...

...a inak serial, ktory pise pre root.cz, je vcelku fajn.
Odpovedať Hodnotiť:
 

nech si robi svoj OS, nie vsetko co clovek robi musi byt prospesne... ja som si OS robil, ked som mal 14 rokov, ale na druhu stranu, teraz si skladam lego :)
Odpovedať Hodnotiť:
 

a kde je dokaz o spravnosti dokazu?

Odpovedať Hodnotiť:
 

neviete kedy bude vlna overovania pravosti windows7?????????,,
Odpovedať Hodnotiť:

Pridať komentár