» »

Prvi operacijski sistem brez programskih hroščev

Prvi operacijski sistem brez programskih hroščev

Schneier.com - Če ste bili do sedaj mnenja, da je v praksi nemogoče napisati kopleksnejši program, ki ne bi vseboval programskih hroščev, je skupina zbrana okrog profesorja Gernota Heiserja iz avstralske University of New South Wales dokazala nasprotno. Uspeli so namreč potolči prav vse programske hrošče v operacijskem sistemu in to tudi dokazati.

Njihov operacijski sitem je tako 100-odstotno varen pred napakami in sesutji. Žal pa ne gre za kakšen popularen operacijski sistem, pač pa za operacijski sistem seL4 microkernel.

Operacijski sistem vsebuje 7500 vrstic kode, pregled, ki ga je opravljalo šest ljudi, pa je trajal več kot pet let. V povprečju je tako en človek na leto pregledal 250 vrstic.

Po mnenju Heiserja ima povprečen program približno 10 hroščev na 1000 vrstic kode, pri zelo skrbno napisanih programih pa je število hroščev mogoče zmanjšati na 1 do 3. Glede na to, da imata operacijska sistema Linux in Windows okrog 50 milijonov vrstic kode, bi njun pregled zahteval vsaj 200.000 človek let, zelo verjetno pa še več, saj s številom vrstic kode, narašča tudi kompleksnost programa.

Glede na to, da je koda Linuxa odprta - kar veselo na delo!

49 komentarjev

Highlag ::

Ni ravno nek dosežek s katerim bi se pretirano hvalili. Pregled ene vrstice na dan?
Never trust a computer you can't throw out a window

Matevžk ::

Najbrž v teh 5 letih niso počeli samo tega. :) Seveda pa ne moreš pregledovati programa vrstico-po-vrstico; potrebno je obravnavati nekoliko večje sklope.
lp, Matevžk

SasoS ::

Gre za hitrost, ne dejanski pregled. Si kdaj delal formalne dokaze programov? :D

MrStein ::

On to v enem vikendu naredi... ;)
Motiti se je človeško.
Motiti se pogosto je neumno.
Vztrajati pri zmoti je... oh, pozdravljen!

denial ::

Akademiki so zabavni ljudje :D
SELECT finger FROM hand WHERE id=3;

borchi ::

pol pa naj uni tip, spender, al kaj je že, dokaže da so res zabavni...
l'jga

darkolord ::

Treba se je zavedati, da za takšno trditvijo stoji kar nekaj pomembnih predpostavk, ki v praksi velikokrat ne držijo...

mtosev ::

nic ni bug free. :D
Core i9 10900X, ASUS Prime X299 Edition 30, 32GB 4x8 3600Mhz G.skill, CM H500M,
ASUS ROG Strix RTX 2080 Super, Samsung 970 PRO, UltraSharp UP3017, Win 11 Pro,
Enermax Platimax 1700W | moj oče darko 1960-2016, moj labradorec max 2002-2013

WarpedGone ::

Če ste bili do sedaj mnenja

Še vedno sem tega mnenja.
100% bug-free software je možno dosečt edino deklerativno: We have no bugs, only features.
Zbogom in hvala za vse ribe

Mavrik ::

Treba se je zavedati, da za takšno trditvijo stoji kar nekaj pomembnih predpostavk, ki v praksi velikokrat ne držijo...


Če so prepostavke postavljene s skladu s teorijo pravilnosti, je tak program v praksi brez hroščev. Jasno pa je da se v praksi tole nikomur ne da delat niti za kritične in "nevarne" sklope kode. Se vsi raje zanašajo na nezanesljivo testiranje.
The truth is rarely pure and never simple.

Matevžk ::

nikomur ne da delat

Tudi če bi bilo strokovnjakov za to kot listja in trave, bi bilo za marsikateri kos kode to še vedno ekonomsko neupravičeno. :)
lp, Matevžk

Mavrik ::

Zato pa nisem rekel "za vse" ampak za kritične dele, kateri niti po testiranju načeloma še ne delajo pravilno.
The truth is rarely pure and never simple.

filip007 ::

Linux se flika vsaj dan, Polkna pa na 3 leta in to je to, mikro kernel je samo kernel za kaj se ga pa uporablja je pa to druga stvar. Meni Nokia zašteka enkrat se na leto in pomeni da so napake povsod.
Trevor Philips Industries

win64 ::

Formalni dokaz programa: 3 vrstice ena stran A4?

ZaOstali ::

Narediš en über PRO OS, in ga nato pet let pofixxavaš vsaki dan. Tako dobiš isto sranje ven.
Če bi Linux pregledovalo 1000 ljudi, bi bil celoten OS pregledan v 200 dneh. Kar je dosti manj od nekega random OSja.
Je pa to samo gola teorija!

Zgodovina sprememb…

  • spremenilo: ZaOstali ()

hojnikb ::

Bolši met funkcionalen OS z bugi ko pa nek gol microkernel brez napak..:P
#brezpodpisa

win64 ::

Ne najdem nobenga primera uporabe tega kernela...

marvin42 ::


Če bi Linux pregledovalo 1000 ljudi, bi bil celoten OS pregledan v 200 dneh. Kar je dosti manj od nekega random OSja.
Je pa to samo gola teorija!


tvoja izjava tudi gole teorije ne preživi.
Mostly Harmless

l0g1t3ch ::

Nevem kaj ti koristi bug free kernel, ko pa niti hardware ni bug free.
Potem pa na vse to dodaš še na tisoče vrstic nepregledane kode in je že skoraj vseeno ali so v kernelu napake ali ne :D

ZaOstali ::


Če bi Linux pregledovalo 1000 ljudi, bi bil celoten OS pregledan v 200 dneh. Kar je dosti manj od nekega random OSja.
Je pa to samo gola teorija!


tvoja izjava tudi gole teorije ne preživi.

možno da sem se zmotil, saj sem računal po zgornjih podatkih. To pa že po defaultu (ja res je) ne drži.
Beri post MatevžkA

Zgodovina sprememb…

  • spremenilo: ZaOstali ()

pegasus ::

Nikjer ne vidim omenjeno, kakšne metode so uporabili pri teh njihovih matematičnih dokazih. Nekaj časa se namreč že spogledujem s spark ado in moram priznati, da je zadeva fascinantna.

rdecaluc ::

..bi njun pregled zahteval vsaj 200.000 človek let.. človeških?
Est modus in rebus. ,typos

PaX_MaN ::

Formalni dokaz programa: 3 vrstice ena stran A4?

Malo morgen:
They have successfully verified 7,500 lines of C code and proved over 10,000 intermediate theorems in over 200,000 lines of formal proof.

RejZoR ::

Wow, celih 7k vrstic in braganje o manjku hroščev. Če to primerjaš z Windowsi manjše napakice tu in tam izgledajo povsem nepomembne.
Angry Sheep Blog @ www.rejzor.com

LordJimy ::

Keri norci. Na svetu ne more obstajati program brez napake saj ga napiše človek (in noben človek ni brez napak). Je pa še bolj žalostno, da to omenjajo pri OSu (7500 vrstic kode). Ti so pa re smešni.

PaX_MaN ::

Na svetu ne more obstajati program brez napake saj ga napiše človek (in noben človek ni brez napak).

Formalno dokaži, pa ti bomo morda celo verjeli. :P

Looooooka ::

i call bullshit.
zihr niso v postev vzel dejstva, da ti lahko nekdo pred bootom gor kj nalozi in mal praska po memoryju.
...potem bo seveda izgovor, da tega niti niso hotl dat v kodo ker je prakticno nemogoce.
Upam, da jih ne bo prevec sram, ko bo zdele en kitajec v naprej narocil za 2 meseca junk fooda in jim dokazal nasprotno.

poweroff ::

Preden zabluzite si poglejte za kaj se ta mikrokernel sploh uporablja.
sudo poweroff

Utk ::

7000 vrstic ima najbrž malo bolj komplicirana pasjansa. Ki se mi ni še nikdar sesula. Big deal, res :)

poweroff ::

Če se sesuje pasjanja seveda ni problema. Če se železarna, so problemi večji.
sudo poweroff

Utk ::

Ja, ampak, prvič, 7000 vrstic dobro pretestirat, in že delat tako, da so res dobre, ni tako težko. In drugič, kaj ti pomaga 7000 popolnih vrstic, če imaš na njih še par milijonov "samo testiranih".

Mavrik ::

Ja, ampak, prvič, 7000 vrstic dobro pretestirat, in že delat tako, da so res dobre, ni tako težko


Kaj ti ni jasno? Tole NI bilo pretestirano. To je bilo dokazano da dela. Testiranje ne dokaže odsotnosti hroščov.
The truth is rarely pure and never simple.

Utk ::

Kaj tebi ni jasno, mi ni jasno. Jasno, da testiranje ne dokaže nič, pa vseeno niso šli tega dokazovat iz praktičnih razlogov, ampak čisto akademskih. 250 vrstic na človeka na leto...kaj če bi software od neke banke tako pregledovali, bi uporaba Klika stala najmanj 10,000 evrov na mesec.

poweroff ::

Ja. Korist tele raziskave je (med drugim) točno v tem, da sedaj lahko ocenimo koliko bi stal razvoj bug free spletnega bančništva... Morda pa se bo dalo razviti tudi kakšne avtomatizirane teste...
sudo poweroff

VolkD ::

In potem se bo stvar sesula.....
To o bug free je samo pravljica. Človek je pač zmotljivo bitje. V povprečno 40-ih besedah se zmoti vsaj pri eni za eno črko.

Ne verjamete?

Poglejte si citat prvega stavka te novice:
Če ste bili do sedaj mnenja, da je v praksi nemogoče napisati kopleksnejši program, ki ne bi vseboval programskih hroščev, je skupina zbrana okrog profesorja Gernota Heiserja iz avstralske University of New South Wales dokazala nasprotno.
Preden zaspiš zapri oči. Preden zapreš oči, ustavi avto.

poweroff ::

No, napisano je tako zato, ker "Hello world" bug free programa ni ravno težko napisati...
sudo poweroff

BigWhale ::

No, napisano je tako zato, ker "Hello world" bug free programa ni ravno težko napisati...


Ja ga je, ker ga moras napisati v assemblerju (pa se to ni povsem dovolj). Cim uporabis kakrsnokoli drugo knjiznjico zraven obstaja moznost, da bos kje na kak bug naletel.

jernejl ::

Ker tukaj sodelujete tudi ljudje, ki se malo bolje spoznate tudi na pravo, me zanima naslednje.

Kako je v pravnem vidiku zaščiten avtor (programer) neke programske opreme pred neposrednimi in posrednimi posledicami nenamernih napak (bug-ov) v programski opremi?

Vemo namreč, da je praktično nemogoče narediti bug-free software, posledice pa so lahko tudi katastrofalne.
Ali (in kdaj) lahko podjetje od avtorja zahteva povračilo nastalih stroškov, ki so nastali kot posledica hrošča?

poweroff ::

Z EULO... :D
sudo poweroff

WarpedGone ::

Morda pa se bo dalo razviti tudi kakšne avtomatizirane teste...

Katerih pravilnost bo seveda potrebno dokazati ročno.
Goedlu ne pobegneš.
Zbogom in hvala za vse ribe

jernejl ::

@Matthai:

Če prav razumem, je torej besedilo v EULA "sveto" - torej ne obstaja posebna zakonodaja, ki bi določala / omejevala pravice in dolžnosti obeh stani (avtorja in uporabnika-kupca)?

Zgodovina sprememb…

  • spremenil: jernejl ()

poweroff ::

WarpedOne - da, vendar ti avtomatizirani testi lahko precej olajšajo delo. Za buffer overflowe že obstajajo...

jernejl - ne, EULA ni sveto besedilo. Načeloma velja, da če ni drugače določeno v pogodbi, odgovarjaš kvečjemu za malomarnost. Če se programer potrudi po svojih močeh (in spoštuje industry standarde), ni odgovoren za napake.
sudo poweroff

dfajt ::

BugFree. To me spominja na eno resnično prigodo izpred kakšnih 10-15 let.
Kolega napiše program in trdi, da je totalno bug-free. Vpišeš dva datuma in program ti izračuna razliko in izpiše v dnevih.
Pa pri datumih upošteva mesece (nepravilno število dni), prestopna leta, prverja ali je prvi datum večji od drugega... Mi našteva 10 minut, kaj se vse preverja. Nato pa pride en mulec in v prvi datum vpiše aa.aa.aaaa, pa program pogrne. :)

Mavrik ::

A je kolega formalno dokazal pravilnost programa?
The truth is rarely pure and never simple.

dfajt ::

Meni ne :). Dokazat pravilnost programa z 100 vrsticami najbrž ni nek problem. Zakomplicira se pri n*1000 vrsticah in vseh možnih variantah vhodov in izhodov.
Mislim, da je kaj takšnega praktično nemogoče (OK, v teoriji je izvedljivo, a se porabi preveč časa).
En profesor je nekoč dejal, da programi brez hroščev ne obstajajo. Obstajajo zgolj tisti, ki jih imajo malo in tisti, ki jih imajo veliko. In pa, da če v nekem programu odkriješ in popraviš ogromno hroščev, to še ne pomeni, da si odpravil vse - pomeni zgolj, da si jih ogromno spregledal - več kot jih najdeš, večja gostota jih je in več jih spregledaš. :D

desperados ::

Zame je to vse le dokaz, da formalni preskusi za programsko opremo niso ekonomsko upravičeni. Tudi če potem z hudo dobro pogodbo SW prodaš uporabniku. Jaz ne vem za nobenega proizvajalca strojne opreme, ki bi bil pripravljen storiti kaj podobnega, torej smo v paradoksu, saj celoten sistem ni formalno preverjen!
No ja mogoče je kaka 486 ka formalno preverjena ampak tudi to dvomim.

Zdi pa se mi, da bi bila to dobra praksa za FW v raznih kritično pomembnih sistemih v realnem času!

SoulReaver ::

jaz sem pripravljen dat roko v ogenj, da moj prastari HP kalkulator ima OS brez hrošča :P

MrStein ::

Jernejl:
@Matthai:

Če prav razumem, je torej besedilo v EULA "sveto" - torej ne obstaja posebna zakonodaja, ki bi določala / omejevala pravice in dolžnosti obeh stani (avtorja in uporabnika-kupca)?

Seveda obstaja. Celo objavljena je : www.uradni-list.si , http://zakonodaja.gov.si/

Za mnenja pa vprašaj odvetnika, ne nekoga "moj stric je v mladosti gledal Matlocka, zato se na stvar poznam" s foruma ;)
Motiti se je človeško.
Motiti se pogosto je neumno.
Vztrajati pri zmoti je... oh, pozdravljen!

techfreak :) ::

jaz sem pripravljen dat roko v ogenj, da moj prastari HP kalkulator ima OS brez hrošča :P

Boga roka ...


Vredno ogleda ...

TemaSporočilaOglediZadnje sporočilo
TemaSporočilaOglediZadnje sporočilo
»

Del OpenSSL bo postal LibreSSL

Oddelek: Novice / Varnost
169367 (7924) LightBit
»

Previdno z Javo (spet) (strani: 1 2 )

Oddelek: Novice / Varnost
7426513 (23190) Grumf
»

Decaf potegavščina

Oddelek: Novice / Zasebnost
204016 (2742) ABX
»

Prvi operacijski sistem brez programskih hroščev

Oddelek: Novice / Operacijski sistemi
495082 (2639) techfreak :)
»

IE in Outlook Lukenj™

Oddelek: Novice / Varnost
192069 (2069) Ziga Dolhar

Več podobnih tem