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!
Novice » Operacijski sistemi » Prvi operacijski sistem brez programskih hroščev
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.
Seveda pa ne moreš pregledovati programa vrstico-po-vrstico; potrebno je obravnavati nekoliko večje sklope. lp, Matevžk
MrStein ::
On to v enem vikendu naredi... ;)
Motiti se je človeško.
Motiti se pogosto je neumno.
Vztrajati pri zmoti je... oh, pozdravljen!
Motiti se pogosto je neumno.
Vztrajati pri zmoti je... oh, pozdravljen!
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. 
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
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
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!
Č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 ()
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
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
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.
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.
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.
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:
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?
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?
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)?
Č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.
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. :)
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š.
. 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š.
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!
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
MrStein ::
Jernejl:
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 ;)
@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!
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
Boga roka ...
Vredno ogleda ...
| Tema | Ogledi | Zadnje sporočilo | |
|---|---|---|---|
| Tema | Ogledi | Zadnje sporočilo | |
| » | Del OpenSSL bo postal LibreSSLOddelek: Novice / Varnost | 9396 (7953) | LightBit |
| » | Previdno z Javo (spet) (strani: 1 2 )Oddelek: Novice / Varnost | 26600 (23277) | Grumf |
| » | Decaf potegavščinaOddelek: Novice / Zasebnost | 4023 (2749) | ABX |
| » | Prvi operacijski sistem brez programskih hroščevOddelek: Novice / Operacijski sistemi | 5089 (2646) | techfreak :) |
| » | IE in Outlook Lukenj™Oddelek: Novice / Varnost | 2076 (2076) | Ziga Dolhar |