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.




Najnovšie články:



Diskusia:

Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti Od: Leonard555 | Pridané: 15.8.2009 8:28 Toto by mal kupit a pouzit microsoft vo windowse Odpovedať Známka: 3.8 Hodnotiť:

Re: Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti Od: charlie charlie | Pridané: 15.8.2009 10:35 numb3rs :D Odpovedať Známka: 5.4 Hodnotiť:

Re: Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti Od reg.: Eagle | Pridané: 15.8.2009 15:43 A čo ak sa zle vyráta ten matematický dôkaz? Odpovedať Známka: 8.3 Hodnotiť:

Re: Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti Od: Deer | Pridané: 15.8.2009 19:07 Ide asi o nieco na styl unit-testov. Odpovedať Známka: -3.3 Hodnotiť:

Re: Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti Od: xman | Pridané: 16.8.2009 11:24 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 reg.: x x l l | Pridané: 15.8.2009 8:42 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ť:

Re: Zial... Od: fotograf | Pridané: 15.8.2009 9:48 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ť:

Re: Zial... Od: ufc | Pridané: 15.8.2009 10:25 ale OpenBSD ma k tomu velmi blizko... Odpovedať Známka: -3.3 Hodnotiť:

Re: Zial... Od: BigLama-nepr | Pridané: 15.8.2009 11:12 Preco chces za kazdu cenu robit Flame? Odpovedať Známka: 4.7 Hodnotiť:

Re: Zial... Od reg.: still | Pridané: 15.8.2009 11:33 Ak by si vedel, ze svetlo sviecky je plamen, jedlo by uz bolo davno uvarene ;) Odpovedať Známka: 4.5 Hodnotiť:

Re: Zial... Od: Bedňa | Pridané: 15.8.2009 12:10 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ť:

Re: Zial... Od reg.: still | Pridané: 15.8.2009 13:23 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ť:

Re: Zial... Od reg.: x x l l | Pridané: 15.8.2009 22:58 http://tinyurl.com/m3ttjt Odpovedať Hodnotiť:

Re: Zial... Od: ufc | Pridané: 15.8.2009 12:05 A nema k tomu OpenBSD blizko ? :P Odpovedať Známka: -6.8 Hodnotiť:

Re: Zial... Od: NTI Student | Pridané: 15.8.2009 13:12 k vyvrcholeniu Odpovedať Známka: 6.4 Hodnotiť:

Re: Zial... Od reg.: x x l l | Pridané: 15.8.2009 23:04 OpenBSD nepouziva mikrokernel Odpovedať Známka: 10.0 Hodnotiť:

Re: Zial... Od reg.: still | Pridané: 15.8.2009 10:47 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ť:

Re: Zial... Od: Hatatitlaa | Pridané: 15.8.2009 20:59 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ť:

Re: Zial... Od reg.: still | Pridané: 15.8.2009 22:00 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ť:

Re: Zial... Od: xman | Pridané: 16.8.2009 11:06 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ť:

Re: Zial... Od reg.: still | Pridané: 16.8.2009 11:47 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ť:

Re: Zial... Od: xman | Pridané: 16.8.2009 12:08 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ť:

Re: Zial... Od reg.: still | Pridané: 16.8.2009 12:54 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ť:

Re: Zial... Od: xman | Pridané: 16.8.2009 13:11 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ť:

Re: Zial... Od: ooo | Pridané: 16.8.2009 15:09 Ty si dnes asi šňupol tabáčika-chytráčika, fšagáno??? Odpovedať Hodnotiť:

všetko čo sa môže pokaziť, sa aj pokazí Od: dalen | Pridané: 15.8.2009 12:14 Murphyho zákony platia vždy a všade. Odpovedať Známka: 9.1 Hodnotiť:

Re: všetko čo sa môže pokaziť, sa aj pokazí Od: claudius | Pridané: 15.8.2009 17:33 tj ked murphyho zakon nemusi aspon v jednom pripade fungovat, tak nebude? :D Odpovedať Známka: 4.3 Hodnotiť:

Super Od: ... | Pridané: 15.8.2009 18:17 Toto ma obrovsku buducnost. Odpovedať Známka: 1.4 Hodnotiť:

mylny dokaz? Od reg.: Zmurko | Pridané: 15.8.2009 18:37 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ť:

Re: mylny dokaz? Od reg.: Pjetro de | Pridané: 16.8.2009 12:38 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ť:

ZeXOS Od: Axwellx64 | Pridané: 16.8.2009 15:29 Poznam jedneho velkeho programatora, ktory programoval sam svoj vlastny OS, teda stale na nom pracuje. pre viac info www.zexos.org Odpovedať Hodnotiť:

Re: ZeXOS Od reg.: x x l l | Pridané: 16.8.2009 17:41 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ť:

Re: ZeXOS Od: suxi | Pridané: 17.8.2009 8:12 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ť:

dokaz Od reg.: mdl.. | Pridané: 17.8.2009 8:46 a kde je dokaz o spravnosti dokazu? Odpovedať Hodnotiť:

Windows7 Od: Windows7 | Pridané: 18.8.2009 16:02 neviete kedy bude vlna overovania pravosti windows7?????????,, Odpovedať Hodnotiť:

Pridať komentár