Australiërs claimen geheel bugvrije kernel te hebben gebouwd

Australische onderzoekers aan de University of New South Wales en de firma Nicta claimen een kernel te hebben ontwikkeld die geheel bugvrij is. Dit zou mogelijk zijn dankzij een uitvoerige wiskundige verificatiemethode van de geschreven code.

De Secure Embedded L4 microkernel bestaat uit ongeveer 8700 regels C-code, en is daarmee relatief klein in omvang. De seL4-microkernel is door het verificatieprogramma Isabelle gedurende vier jaar uitvoerig getest aan de hand van de analyse van wiskundige berekeningen.

Uit de verificatieprocedure zou zijn gebleken dat de kernel vrij is van bugs, terwijl 'normale' code gemiddeld drie tot tien fouten bevat per duizend geschreven regels. De onderzoekers stellen ook dat de seL4-kernel geheel ongevoelig is voor buffer overflows, een populaire methode van hackers om toegang te verkrijgen tot besturingssystemen.

Volgens de onderzoekers blijkt uit het seL4-project dat het mogelijk is geworden om gegarandeerd bugvrije software te bouwen. Dit zou met name nuttig zijn voor de aansturing van embedded systemen, zoals de micro-elektronica in auto's en vliegtuigen. Verder zouden de kernel en de aanvullende testsoftware goed gebruikt kunnen worden bij de ontwikkeling van defensiesystemen. Nicta zal de uitkomsten van het onderzoek deels gebruiken in de producten van de spinoff Open Kernel Labs.

Reacties (160)

[Haan]

Voor de mensen die zich (net als ik ) afvragen wat het plaatje precies voorstelt: het is een 'function call graph' (zoals de alt-tag al zegt ), waarbij iedere stip een functie in de kernel voorstelt.
Een lijn tussen tweestippen geeft aan dat de twee functies elkaar aanroepen. Uit de wirwar van lijnen in het plaatje kan je dus opmaken dat er een hoge mate van onderlinge verbondenheid is tussen de functies, wat het geheel nogal complex maakt. De makers van de kernel geven zelf al aan dat je dit vaker ziet bij kernels die zijn geoptimaliseerd voor performance, terwijl een kernel die 'goed' ontworpen is meer 'eilandjes' zal hebben van groepen functies die onderling sterk verbonden zijn, met een paar lijnen die de eilandjes verbinden.
De groene stippen in het plaatje zijn functies die op het moment van het snapshot al geverifieerd waren (begin 2009).

Ook wel interessant om te melden is dat het mogelijk is om Linux te draaien op een port van de seL4 kernel naar x86 en dat ze ook een port voor Linux naar het ARM platform op de planning hebben staan.

En dan nog wat extra statistieken erbij:
-De kernel bestaat uit 7500 regels code en 1200 boot code + 600 regels assembly code
-Het test script bestaat uit 200.000 regels
-Er zijn 160 bugs gevonden

[Reactie gewijzigd door Haan op 23 juli 2024 06:16]

[nomennescio]

Het is knap werk, maar er zijn wat lelijke haken en ogen aan het bewijs:

• Wat precies de eigenschappen zijn die bewezen zijn, lijkt nergens te vinden. Ik vermoed dat het scheiding is tussen de domeinen (omdat het een micro kernel is, en dat zowat het enige is wat je zinnig kunt doen in die paar duizend regels code), maar dat is een gok.
• De assembly delen, het opstart deel, en alle afhankelijkheden op gedrag van de hardware zijn niet gecontroleerd.
• Alle tools zijn ook buiten beschouwing, in het bijzonder de C-compiler. Vooral bij zaken als wissen van geheugen voordat je het aan het andere domein geeft ("residual information protection") is dat nogal foutgevoelig door compilers die wisroutines wegoptimalizeren (doen immers niets functioneels, een memset gevolgd door een free) .
• Een aanvaller met physieke toegang maakt korte metten met zo'n systeem als ze niet veel meer in hardware beschermen (en ze willen het vooral in de telefoon / embedded markt verkopen lijkt het).
• Hun kosten claims zijn totaal idioot. Aan de ene kant kosten volgens hun al die Phd studenten en profs niets, aan de andere kant nemen ze voor de officiele Common Criteria-evaluatie getallen aan die nergens op slaan. Voor een kwart van die geclaimde prijs kun je een evaluatie lab opzetten, de evaluatie doen en nog asociaal veel winst maken.

Nogmaals zeer knap gedaan, maar neem het met een korreltje zout a.u.b..

[ZenTex]

Geheel bugvrij. Dat had ik nooit voor mogelijk gehouden, maar na 4 jaar testen?
Aan de andere kant, is de gebruikte verificatiesoftware wel bugvrij dan? En zijn de gebruikte wiskundige berekeningen wel geheel correct?

Het zou me niets verbazen als er na verloop van tijd tog een bugje in het hele proces ontdekt word. Want dit klinkt te mooi om waar te zijn.

[Verwijderd]

Docent van mij zegt altijd:

"Alleen de aanwezigheid van bugs kan aangetoond worden, de afwezigheid nooit"

Denk dat daar zeker waarheid in zit

[johnbetonschaar]

Je docent heeft gelijk. Automatische verificatie van software is onmogelijk, en het bewijs daarvoor de consensus daarover is waarschijnlijk heel wat waterdichter zekerder dan het bewijs dat deze kernel echt bugvrij is. Het is een NP-compleet of zelfs een NP-hard probleem, waar wiskundigen al heel wat jaren langer hun hoofd op breken en waarvan ondertussen wel voor 99.9999999% zeker is dat ze niet binnen polynomiaal begrensde tijd opgelost kunnen worden. Zie ook het halting probleem, een vereenvoudigde formulering van het probleem van automatische verificatie.

Wat natuurlijk wel kan is dat ze in de 4 jaar tijd handmatig formele bewijzen hebben afgeleid voor elk stukje code in deze kernel. Dus door middel van de wetten van logica en formele deductie bewezen hebben dat elke regel code zich zo gedraagt als dat bedoeld was. Maar ten eerste kunnen er zelfs dan nog 'bugs' in de code zitten als de onderzoekers niet elk mogelijke bron van exploitable fouten hebben onderzocht en afgedekt middels bewijzen, en ten tweede kost dat zoveel tijd en moeite dat het totaal niet interessant is voor 'echte' software ontwikkeling. In de tijd die nodig is om 1000 regels nieuwe code te verifieren kan je op heel veel andere manieren fouten opsporen.

Edit: laat ik dan ook even wat zorgvuldiger zijn in de terminologie want het is nog niet bewezen dat problemen uit de klasse NP niet binnen polynomiale tijd oplosbaar zijn.

[Reactie gewijzigd door johnbetonschaar op 23 juli 2024 06:16]

[RedLizard]

Automatische verificatie van software is onmogelijk, en de consensus daarover is waarschijnlijk heel wat zekerder dan het bewijs dat deze kernel echt bugvrij is.

Automatische verificatie van software is alleen onmogelijk in het algemene geval - ik kan geen programma schrijven dat alle ware uitspraken over een willekeurig programma kan opschrijven. Het is echter prima mogelijk om programma's te schrijven die een zekere verzameling ware uitspraken over een zekere verzameling van programma's kan doen.

Een voorbeeld: ik zou een programma kunnen schrijven dat controleert op afwezigheid van buffer overflows in alle programma's van een zekere vorm. Het programma zou bijvoorbeeld aannemen dat alle buffer-parameters worden gevolgd door een buffergrootte-parameter, om vervolgens de functieaanroepen en functieimplementatie te controleren op respectievelijk de correctheid van die parameter, en het binnen de grenzen van die parameter blijven. Hierbij heeft het programma waarschijnlijk nog wat meer aannames over de programmastructuur nodig.

Op deze manier kan je een programma maken dat correctheidsbewijzen levert voor alle programma's die op een specifieke manier geschreven zijn, en voor alle andere programma's tot de conclusie komt dat de correctheid niet gegarandeerd is. Vervolgens kun je je kernel zo schrijven dat hij kan worden gecontroleerd door je checker, en voila, een correct bewezen kernel.

[johnbetonschaar]

Dat is zeker waar maar daarmee beperk je de rijkwijdte van zo'n programma voor correctheidsbewijzen zo ver dat je niet echt meer van verificatie van het programma kan spreken maar slechts verificatie van bepaalde eigenschappen daarvan. Het voorbeeld wat je noemt is ook nog eens niet het beste voorbeeld: als alle buffer parameters gevolgd worden door een buffergrootte parameter dan zal je nog steeds op de een of andere manier moeten vaststellen welke waarden deze buffergrootte parameter allemaal kan aannemen in je programma. Tenzij dit een constante is, of tenzij je een programma hebt dat totaal vrij is van externe invoer, is dat dus onmogelijk binnen polynomiale tijd. Precies het soort dingen als bewijzen dat geen buffer-overruns kunnen optreden is een van de dingen die je niet geautomatiseerd kan doen voor het algemene geval.

Maar inderdaad, als je allerlei restricties aan je programma en de omgeving waarin het programma opereert gaat opleggen dan kan je steeds meer dingen geautomatiseerd bewijzen, alleen wordt de kracht en bruikbaarheid van je verificatietool natuurlijk ook steeds lager.

Daar op aansluitend @johanw910:
Niet in polynomiale tijd oplosbaar betekent in praktische gevallen altijd niet oplosbaar, het probleem is zogezegd 'intractable'. De rekentijd die voor typische NP-complete problemen nodig is loopt zo gigantisch hard op dat je binnen de kortste keren al meer rekenkracht nodig hebt dan op aarde beschikbaar, en dan al net zo lang nodig hebt als de leeftijd van het universum. Enkel NP-complete problemen waar je alleen maar geinteresseerd bent in de aller eenvoudigste instantiatie van het probleem zijn nog houdbaar, maar het bewijzen van een programma van 8000+ regels valt daar echt niet onder, dan moet je denken aan programma's met een 10-tal statements met enkele 10-tallen verschillende mogelijke inputs.

[RedLizard]

Dat is zeker waar maar daarmee beperk je de rijkwijdte van zo'n programma voor correctheidsbewijzen zo ver dat je niet echt meer van verificatie van het programma kan spreken maar slechts verificatie van bepaalde eigenschappen daarvan.

Als je als te bewijzen eigenschap kiest "het programma voldoet aan de specificatie" dan ben je er toch? De techniek is echt niet alleen van toepassing op buffer overflows hoor.

Het voorbeeld wat je noemt is ook nog eens niet het beste voorbeeld: als alle buffer parameters gevolgd worden door een buffergrootte parameter dan zal je nog steeds op de een of andere manier moeten vaststellen welke waarden deze buffergrootte parameter allemaal kan aannemen in je programma.

Nee hoor. Als mijn programma eerst een buffer alloceert van grootte X en hem vervolgens doorgeeft aan een functie met als grootte-parameter X dan maakt het mij helemaal niet uit wat precies de waarde van X is.

Dit is weliswaar maar een van de vele manieren om de functie in kwestie te gebruiken, maar wel de manier die in het overgrote deel van de gevallen in de praktijk gebruikt wordt. Als ik mijn programma nou de restrictie opleg dat dit het enige toegestane gebruik van buffers is, dan kan ik bewijzen dat mijn programma overflow-vrij is - zonder een grote aanslag op de programmeermoeite te plegen, omdat het overgrote deel toch al van die vorm was.

alleen wordt de kracht en bruikbaarheid van je verificatietool natuurlijk ook steeds lager.

Daarom heeft het ook vier jaar gekost om dit toe te passen op een klein stukje software

[MSalters]

Precies het soort dingen als bewijzen dat geen buffer-overruns kunnen optreden is een van de dingen die je niet geautomatiseerd kan doen voor het algemene geval.

Grappig. Ben je bekend met PREfast? Microsoft heeft een dergelijk programma.

De vraag is uiteraard wat je precies onder "het algemene geval" laat vallen. Als we de volgende code in gedachten nemen:

1. Roep functie Foo() aan
2. Overflow buffer.

dan is het triviaal dat je het halting probleem voor Foo() moet oplossen om te bepalen of er hier een buffer overflow optreedt. Definieer "algemeen" echter in het probleemdomein, en dan is er (vziw) voor elk programma een equivalent programma dat hetzelfde probleem oplost maar bewijsbaar vrij is van buuferoverflows.

[Verwijderd]

Edit: laat ik dan ook even wat zorgvuldiger zijn in de terminologie want het is nog niet bewezen dat problemen uit de klasse NP niet binnen polynomiale tijd oplosbaar zijn.

Zo'n formele kijk is niet eens nodig: niet binnen polynominale tijd oplosbaar betekent niet onoplosbaar, het kan bij grote systemen alleen lang duren. In dit geval was de tijd blijkbaar nog binnen de perken te houden (nou ja, 4 jaar voor een kernel...).

[Verwijderd]

Is het nu NP-Compleet of NP-hard?

[sirdupre]

Dan citeert je docent Dijkstra toch behoorlijk slordig.

Het daadwerkelijke citaat luidt: "Program testing can be used to show the presence of bugs, but never to show their absence! " (Uit EWD294: http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF - onderaan pagina 11)

Dijkstra heeft het hier specifiek over het testen van programma's. Een test is namelijk gewoon empirisch bewijs. Dijkstra was zelf juist voorstander van een formelere, wiskundige aanpak waarbij je bewijst dat je programma aan je specificatie voldoet (dat dit eigenlijk zelfs essentiëel is) en zou een aanpak als deze vermoedelijk wel als een goede aanpak zien (in elk geval beter dan het gewone testen).

[Cergorach]

Dat is zeer zeker niet waar, zie het als een potje schaken, alle mogelijke zetten zijn bekend. Hetzelfde geld voor software, alle opties zijn bekend, alleen is het extreem veel werk om al die zetten te controleren.

Omdat het zoveel werk is, probeert men er wiskundige formules voor te bedenken, het probleem is dat deze wel eens niet geheel juist zou kunnen zijn.

En dat de kernel bug vrij is betekent nog niet dat de processor bug vrij is en er voor kan zorgen dat de kernel niet werkt zoals deze is ontworpen (en dus nieuwe 'bugs' of beveiliging lekken creëert).

[johnbetonschaar]

Het uitvoeren van een computerprogramma is niet hetzelfde als een potje schaken, want een computer programma heeft doorgaans ook nog externe invoer die niet van te voren bekend is.

Lees anders even het wikipedia verhaaltje over het halting probleem wat ik hieronder al gepost heb, elke universitair opgeleide informaticus kent dit probleem omdat het een van de hoofd onderwerpen van de formele informatica en bewijstheorie is. Kort samengevat is het bewijsbaar onmogelijk om een computerprogramma te maken dat zelfs alleen maar bepaalt of een stukje code termineert of oneindig door blijft lopen voor alle mogelijke invoer.

[sirdupre]

Toch is het niet zo zwart/wit als jij stelt. In veel gevallen kun je best een specificatie opstellen voor de invoer die je toestaat, zodat de mogelijke invoer niet meer oneindig groot is, maar beperkt is, of wel oneindig is en aan bepaalde eigenschappen voldoet. Het kan best zijn dat je door dergelijke condities te stellen minder snel bij de onbeslisbare haltingproblemen uitkomt. Ik denk dat het Halting Probleem wat dat betreft ook sterk gerelateerd is aan Gödels onvolledigheidsstellingen. Het feit dat er oneindig veel ware uitspraken zijn in een eindig axiomatisch systeem dat minstens de kracht van de Peano rekenkunde heeft die niet bewezen kunnen worden, tenzij dat systeem incosistent (en dus waardeloos is), betekent natuurlijk niet dat er geen stellingen bestaan die bewezen kunnen worden binnen dat systeem.

Hetzelfde geldt natuurlijk voor programmatuur. Dat er oneindig veel programma's bestaan waarvan we niet kunnen bewijzen of ze ooit zullen termineren gegeven alle mogelijke invoer betekent niet dat er geen programma's bestaan waarvan we niet kunnen bewijzen dat ze zullen termineren. Ik durf er namelijk best mijn hand voor in het vuur te steken dat een programma dat de input negeert en verder ook niets doet, zal termineren (dat lijkt me zelfs een axiomatisch gegeven als je halting problemen gaat oplossen).

Je hebt het dan ook niet helemaal begrepen: het is best mogelijk om een computerprogramma te maken dat bepaalt of een stukje code termineert. Het is alleen niet mogelijk om een computerprogramma te maken dat voor elk stukje code bepaalt of het termineert.

[johnbetonschaar]

Godels onvolledigheidsstelling beschrijft exact hetzelfde fenomeen als het halting probleem, het kan zelfs gebruikt worden als bewijs dat het halting probleem onoplosbaar is. Dat je van subsets van alle mogelijke programma's kunt vaststellen of ze termineren is natuurlijk evident, als ik een programma schrijf met 1 statement 'halt' (bij wijze van spreken) dan heb je dat voor het triviale geval al bewezen. Dus tot zover zijn we het eens.

Echter, ging het er hier niet om of je sommige eigenschappen van sommige programma's kunt bewijzen, dan ben je namelijk alleen bezig om te bewijzen dat je programma aan bepaalde gestelde (formele of informele) specificaties voldoet. Deze formele specificaties kunnen best verifieerbaar zijn, maar zijn verschillend voor elk programma, en dus niet toepasbaar op het algemene geval. En dat was de vraag hier, kan je een programma schrijven dat bewijst of een ander programma geen bugs bevat. Het antwoord blijft 'nee', tenzij je bereid bent om je definitie van 'bugvrij' te verdunnen tot 'vrij van de door ons vastgestelde subset van mogelijke bugs'.

Ik heb trouwens ook nergens beweerd dat je geen programma kunt maken dat voor bepaalde gevallen vaststelt of een programma termineert of niet, dus laten we maar even in het midden houden hoe veel ik er wel of niet van begrepen heb. Laat ik het maar even herformuleren naar: het is onmogelijk om in het algemene geval geautomatiseerd vast te stellen dat een stuk code bugvrij is, dus ook niet van een computer kernel. Overigens staat ook nergens in het artikel dat de onderzoekers beweren dat ze het bewijs via een computerprogramma hebben verkregen.

[Verwijderd]

En hoe zit het dan met zogenaamde radicalen (ik denk toch dat het zo wordt genoemd), een geheel van regels code die op een onvoorspelde manier iets nieuws bewerkstelligen (of is dit nog niet van toepassing in huidige programma's, is dit nog te sci-fi?) ? Dit kan volgens mij niet bekend zijn en kan dus problematisch zijn.

[Reactie gewijzigd door Verwijderd op 23 juli 2024 06:16]

[koelpasta]

volgens mij is dit meer 'fi' dan 'sci' ....

[MSalters]

Maakt niet uit. lees hierboven maar een over het "Halting probleem". Zelfs een elementaire eigenschap als "stopt dit programma ooit" kan al niet voorspeld worden. Nog complexere eigenschappen zijn evenzeer onvoorspelbaar. Dat maakt niet uit. Deze kernel zorgt er alleen voor dat die onvoorspelbare software binnen de opgelegde grenzen onvoorspelbaar blijft. Alleen die grenzen zijn nu 100% zeker getrokken, binnen de grenzen is alles nog steeds mogelijk.

[Bacchus]

Dat ligt er een beetje aan waar je vanuitgaat: Het is goed mogelijk aan te tonen dat een stuk software zijn technische specificatie implementeert en niets meer dan dat, maar of je dat nou moet verstaan onder bugvrije code..

[berend_engelbrecht]

Een probleem is dat de "bugs" die door klanten gemeld worden vaak helemaal geen bugs zijn in de implementatie, maar missers in de specificatie. De software doet dan wat gespecificeerd was, maar niet wat veel van de klanten er van verwachten. Dit soort softwarefouten komen minstens zo vaak voor als simpele programmeerfouten.

Ik denk dat iedereen die wel eens een nieuw stuk software voor de eerste keer aan de opdrachtgever gepresenteerd heeft, de ervaring heeft dat je daarna vaak voor belangrijke delen van je mooie nieuwe product back to the drawingboard moet. Mensen kunnen zich vaak niet voldoende voorstellen wat een softwareproduct zal gaan doen aan de hand van een specificatie, maar zien wel meteen dat het niet doet wat ze willen als ze de software in handen hebben.

Zeker als je te lang gewacht hebt met het betrekken van je toekomstige gebruikers bij je ontwikkelwerk, loop je in zo'n situatie het risico dat je om de boel te redden last minute changes gaat aanbrengen, er geen tijd meer is dat die de hele testmolen opnieuw doorlopen, en je daarmee bugs introduceert ...

[Reactie gewijzigd door berend_engelbrecht op 23 juli 2024 06:16]

[demonite]

Mee eens dat de 'klant' vaak incompleet wat betreft zijn specificaties, maarja zeg nou zelf, dat is toch ook enorm lastig? Zoveel dingen liggen vaak voor de hand (in de ogen van persoon A, maar niet voor persoon B )

Het is aan de developer (naar mijn mening) om er voor te zorgen dat alle mogelijke 'paden' door de code naar behoren functioneren en ook robuust zijn tegen alle mogelijke inputs. Vaak wordt alleen maar getest tijdens ontwikkeling tegen de specificaties, alle andere mogelijkheden worden dan vergeten... Meest voorkomende voorbeeld is het invoeren van getallen.. Hoe vaak daar wel niet wordt vergeten om de input van text te blokkeren / correct af te handelen...

Alles af dekken is trouwens net zo lastig als een 'complete' specificatie aan leveren..

[Reactie gewijzigd door demonite op 23 juli 2024 06:16]

[berend_engelbrecht]

zeg nou zelf, dat is toch ook enorm lastig?

Dat is het inderdaad, en daarom zal je ook in een "bugvrij" systeem nog altijd dit soort problemen aantreffen als het voor een real-world taak gebruikt wordt. Je kan dat de klant zeker niet aanrekenen, maar je moet bij de ontwikkeling rekening houden met (dus openstaan en tijd reserveren voor) dit soort onvoorziene wijzigingen in je specificaties.

Meest voorkomende voorbeeld is het invoeren van getallen..

Inderdaad, dat hebben wij ook wel eens aan den lijve ervaren. Laatst nog: ergens werden getallen >= 0 geaccepteerd terwijl dat > 0 had moeten zijn. Gebruikers vinden het niet zo leuk als ze elke 0 weken een periodieke e-mail ontvangen, kan ik je vertellen

[Reactie gewijzigd door berend_engelbrecht op 23 juli 2024 06:16]

[latka]

Inderdaad. En dat is precies wat ze hier gedaan hebben. Ze hebben bewezen dat:

"The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more."

En ze nemen aan dat er geen bugs in de toolchain zitten (compiler, linker, CPU etc.)

Het leek me ook nogal sterk. Heb dit zelf ook gedaan voor software en het je kunt de aanwezigheid van bugs aantonen, de afwezigheid niet.

Een ander probleem van het bewijs is dat ze bewezen hebben dat software overeenkomt met de specs. Dat geloof ik wel, maar als er in de SPECs staat: crash eens in de 10 dagen dan zal de software dat ook gegarandeerd doen......

[Haan]

Dat is zeker waar, en wordt door de makers zelf ook benoemd. Ze stellen dat de code gegarandeerd bugvrij is, mits de gemaakte aannames in het testscript kloppen en er geen onvoorziene omstandigheden opduiken.

[TheGhostInc]

Je moet het ook meer vergelijken met het oplossen van een SuDoKu:
Elke regel kan elk getal maar 1* bevatten
Elke kolom kan elk getal maar 1* bevatten
Elk vak kan elk getal maar 1* bevatten

Mocht je een van de aannames vergeten toe te passen dan kom je misschien in een impasse terecht, waar je dan onderzoek naar gaat doen. Pas je een aanname aan, dan kloppen de andere 2 mogelijk niet meer en ben je weer even terug bij af. Voeg je een extra aanname toe dan kom je sommige situaties niet meer tegen, maar krijg je ook geen oplossing.

Op deze manier hoeft je testsoftware helemaal niet zozeer perfect te zijn, maar elke keer komt er een set informatie vrij die bestudeerd moet worden waarom die test die output geeft. Vandaar dat het een wiskundige aangelegenheid is en eigenlijk minder een programmeerprobleem.

Als ICT-er zou je denken aan:
"Run test" ... (wacht 4 jaar) ... "0 errors"
De wiskundige zal de benadering hebben:
"Test 341 zou 6501 resultaten moeten geven naar aanleiding van test 340"... (wacht 5 minuten) ... "6502 resultaten" ... (1 maand onderzoek naar de reden) ...

[elmuerte]

Jou docent was Edsger Dijkstra?

[Reactie gewijzigd door elmuerte op 23 juli 2024 06:16]

[flamingworm]

In men opleiding heb ik allesinds wiskundige methodes gezien waarmee ik kon bewijzen dat een code (20-50 regels) bugvrij was

[ATS]

Het probleem is dat je daarmee alleen controleert of je code doet wat in de formele specificatie staat. Niet of die specificatie beschrijft wat je écht wil dat er gebeurt in alle gevallen. En dat is natuurlijk ook een bug.

[Reactie gewijzigd door ATS op 23 juli 2024 06:16]

[MorosMyrddin]

Maar zoals het artikel aangeeft, in een normale kernel 3 tot 10 fouten per 1000 regels.

dus op dat 1 foutje dat ze mss ooit als het kan zullen vinden komt het dan niet direct é.

4 jaar testen en maar 8700 regels code, het zou moeten kunnen dan er dan nog een fout in zit.
nuja hackers zijn vindingrijk é zij zullen wel ergens een omweg vinden. maar dat zal toch ook minimum 2 jaar duren en met welke middelen ?

Dit is een zeer mooie vooruitgang !!

[Sibylle]

Het gaat niet zozeer om hackers, die hebben geen bug in de kernell nodig maar proberen 'features/bugs' in de omringende software te gebruiken.

Bugvrije systemen zijn gewild in kitische systemen die vaak niet eens gevoelig zijn voor hackers. Denk daarbij aan een boordcomputer van een helicopter (gevechts of reddings), een bug kan daar heel vervelend uitpakken!

Het mooiste is dat er nu geen code ontwikkeld hoeft te worden die een bug voorspelt en opvangt/omzeild. De software in zo'n kritisch systeem is dus minder lomp en ook nog eens bugvrij NICE!

[SPee]

Het systeem zal dan wel goed werken (doet het nu ook al).
Maar dan zit je nog met de menselijke factor (de piloot), de omgeving en de rest van de techniek.

De meeste vliegtuigen zijn niet gecrasht enkel vanwege softwarebugs.
Denk b.v. aan;

• kortsluiting in de tank (ja, daar gaan met strenge regels datakabels door)
• (losse) moertjes, buitjes, rubbertjes
• onoplettendheid en foutief gebruik van de boordcomputer/automatische piloot
• en nog veel meer om er een lange lijst van te maken

[koelpasta]

Maar je kan ook verder denken.
Ruimteschepen zijn in grote mate afhankelijk van computers.
Luchtverkeerstorens ook.

Verder gaan we steeds meer richting een wereld met volledig autonome machines.
Auto's die zichzelf besturen bijvoorbeeld.

Er zijn tal van toepassingen waarbij je wit dat de software in princiepe bugvrij is.

[fdm391]

Nou, als 'dat ene foutje' in de implementatie van de wiskundige algoritmes zit, dan kan het dus best zo zijn dat er in de code die gecheckt wordt (van de kernel dus) meer dan 1 fouten zitten die niet gevonden worden...

De onderzoekers zijn er vanuit gegaan dat die implementatie klopt, omdat de core hiervan relatief simpel en klein is:

Q: How do you know the theorem prover is correct? Have you verified it?
A: We have not formally verified the theorem prover (you could, but note the potential for an infinite conversation if we said yes here). It is a so-called LCF-system that constrains any correctness-critical problems to a very small part of the prover. We have strong confidence in this small core.

[Yakotb]

Het idee van een wiskundige methode is dat onomstotelijk bewezen is dat de methode werkt, want zo werkt wiskunde.

[koelpasta]

Je beschrijft een recursief probleem.
Want hoe bepaal je of het gereedschap waarmee je iets onomstotelijk probeert te bewijzen zelf wel onomstotelijk correkt is?

[MSalters]

Niet: je hebt axioma's. Zo heb je het axioma dat een bit 0 of 1 is. Je kunt niet bewijzen dat dat de enige mogelijk waarden zijn. Maar je kunt wel bewijzen dat het gevolg is dat twee bits de waarden 00, 01, 10 en 11 kunnen hebben.

[bbob]

idd mooie vooruitgang maar de vraag is eerder wat kan deze kernel. Met 8700 regels aan code heb je normaal dus maximaal 87 fouten. Deze moet je er normaal ook binnen een paar jaar uithalen.

Wat als de kernel ineesn 87000 regels heeft werkt dit systeem dan nog.

[YopY]

nuja hackers zijn vindingrijk é zij zullen wel ergens een omweg vinden. maar dat zal toch ook minimum 2 jaar duren en met welke middelen ?

Ligt eraan of hackers een bug moeten misbruiken of gewoon een feature gebruiken. Als je als 'hacker' gewoon het wachtwoord van een gebruiker raadt, dan is dat géén fout in de software. Hacken en bugs in de software zijn vaak, maar niet verplicht of altijd met elkaar gerelateerd.

[Verwijderd]

Inderdaad, men zal nooit 100% halen, dat is zelfs een wiskundig gegeven, 99,99 % zal mogelijk zijn maar altijd zal er 0,01% onzekerheid overblijven en meestal slaat daar de wet van Murphy toe. want denk maar aan b.v. de Pentium bug, stelde niets voor maar daar zou dan de bugvrije software van de kernel nu juist mee kunnen crashen omdat men toch nog te veel variabelen heeft.

[Reactie gewijzigd door Verwijderd op 23 juli 2024 06:16]

[bwerg]

Ja, maar als het crasht door falende hardware zit er nog geen bug in de software .

Hiervoor heeft het team in kwestie zich wel ingedekt, door te zeggen dat er geen onvoorziene omstandigheden moeten zijn. Bij falende hardware is die er wel.

[leuk_he]

Bugvrij betekend enkel dat het precies doet wat het moet doen volgens de specificaties. Maar wiskundig bewijzen dat de code correct is een bekende techniek, en ook een helse klus.

[JivZ]

het is m.i. ook te mooi, want zoals je zelf al aangaf: is de verificatiesoftware zelf wel 100% op bugvrij zijn geverifieerd (en waarmee dan? Ook met geverifieerde software?).
En ook: de code kan dan wel bugvrij zijn, is de compiler waarmee de kernel gecompiled is wel bugvrij, is de hardware wel bugvrij? En hoe wordt dat gecontroleerd.

Nee, dit is een mooie ontwikkeling maar de claim dat er gegarandeerd bugvrije software mee ontwikkeld kan worden lijkt me niet terecht.

[Het.Draakje]

De verificatie is niet zozeer gedaan met een programma maar met een wiskundig algoritme. Dat begint met het bewijzen van het algoritme zelf. (Als het met een computerprogramma uitgevoerd wordt, moet dus ook eerst de correctheid van het programma bewezen worden).

Vier jaar testen op "slechts" 8700 regels. Dat is precies de reden waarom het economisch niet verantwoord is om software bugvrij op te leveren.

(Tenminste als je windows als maatstaf neemt : enige miljoen regels)

[Remco Kramer]

Sorry, maar ben ik de enige die 8700 regels code in een ontwikkel/test tijd van minimaal 5 jaar (aangezien het 4 jaar getest is neem ik aan dat daarvoor ook enige jaren aan ontwikkel tijd aan vooraf ging) erg weinig en niet echt een prestatie?

quote: psychoclown

Vraag me alleen af of dit de stimulans kan zijn tot een echte windows/mac os killer..

Als hun minimaal 5 jaar over 8700 regels doen, vraag ik mij af hoelang zij over 50.000.000 regels code gaan doen. Windows Vista heeft namelijk veel meer dan 50 miljoen regels code... Windows XP zat tegen de 50 miljoen aan. Een Desktop OS killer zullen ze dus nooit worden lijkt mij. Waarschijnlijk zal dat ook nooit hun bedoeling zijn.

The L4.verified project demonstrates that such contracts and proofs can be done for real-world software. Software of limited size, but real and critical.

[Reactie gewijzigd door Remco Kramer op 23 juli 2024 06:16]

[army]

Ja, men ontwikkelt methoden om software te valideren. Dus design op papier versus implementatie in C. En als je kijkt naar projecten zoals Coverity dan is de tijd redelijk. Zeker als "pilot"-project.

En 50 miljoen regels voor een hybrid OS zoals Windows is een beetje veel eigenlijk, maar dezelfde problemen komen nu ook al bij projecten zoals Linux. Gelukkig maakt de techniek vooruitgang en komen microkernels gelukkig steeds dichterbij en kunnen van monolistische hopelijk over zeg 10 a 20 jaar vaarwel zeggen.

Misschien wel de meest bekenste L4-kernel is Hurd en na z'n 24 jaar zijn ze nog steeds bezig om de materie onder de knie te krijgen, maar ook problemen op te lossen. De grap is dat andere oplossing ook langzaam die kant op gaan. KMS in Linux is misschien wel de belangrijkste stap van deze tijd waarmee ze Windows volgen door zo min mogelijk grafische activiteiten in kernelspace te doen, maar in userspace.

Wordt dit een desktop os killer? Ja, maar niet zoals mensen verwachten en ook niet op korte termijn. Dit is gewoon evolutie en projecten waarbij validatie en analyse wordt gedaan horen daarbij. Er zijn al voldoende projecten zoals PostgreSQL die de optie bieden om te controleren of alles correct werkt na compilatie en of er regressies optreden. Linux doet zelf tegenwoordig aan performance meeting om te controleren of veranderingen geen verslechteringen opleveren.

Dus hoe lang zal het duren? Kijk naar bv OpenBSD wat sinds versie 3.0 auditing doet en steeds nieuwe punten oplost. Vergeet ook niet Microsoft die sinds begin 2007 actief code is gaan nalopen en we beginnen daar nu langzaam de vruchten daarvan te plukken. Het grootste probleem zal zijn om oude code uit de wereld te krijgen en de problemen daarvan op te lossen.

[MSalters]

Misschien wel de meest bekenste L4-kernel is Hurd...

Nee. Hurd is een afgeleide van de Mach microkernel. L4 is een alternatief voor de Mach architectuur.

Het grote verschil is dat L4 fundamenteel heeft erkend dat performance relevant is. Dat maakt het tot een relevante kernel voor serieuze research naar praktische microkernels. Voor academisch onderzoek kunnen de Mach kernels soms nog relevant zijn. Maar Hurd is een doodlopend pad, omdat ze proberen om een fundamenteel ongeschikte architectuur praktisch toe te passen.

[Havocnl]

Het blijft door mensen gebouwd, dus kan ook door mensen ongedaan maken.
Echte bugloze software bestaat niet... Alleen software die tot dan toe geen bugs kent, dat wel.

[pe1dnn]

"Echte bugloze software bestaat niet" is een misvatting, die bestaat wel. Simpel voorbeeld:

#include <stdlib.h>
#include <stdio.h>

int main(int argc, char *argv())
{
printf("Hello world!\n");
return 0;
}

Nu kun je zeggen, dat telt niet maar dit is nu precies waar het om gaat. Hoe bewijs je dat de bovenstaande code bug vrij is. Bij elke regel die je toevoegt wordt het moeilijker. Maar dat wil niet zeggen dat het niet kan.

Je kan bewijzen dat code goed is als de code onder alle omstandigheden de voorgedefinieerde paden doorloopt. Dit is mathematisch te bewijzen is door *alle* mogelijke states te controleren op een juiste uitvoering. Dus als je 2 16 bit getallen optelt heb je 65536 * 65536 = 4.294.967.296 mogelijkheden, als je die allemaal getest hebt kun je met zekerheid zeggen dat deze optelling bug vrij is. Voor een praktisch systeem is dat dus behoorlijk moeilijk, vandaar dat dit het nieuws haalt.

Men zegt dat je niet kan bewijzen dat code goed is omdat je dan alle mogelijkheden zou moeten testen, maar wat als je inderdaad alle mogelijkheden test?

Waar ik echter een probleem zie is of de code ook doet wat het zou moeten doen. Als je een optelling programmeert waar je eigenlijk had moeten vermenigvuldigen dan is de code correct maar doet de code niet wat je wil. Dat blijft natuurlijk een probleem want wat je had bedoeld kan geen wiskundig algoritme doorrekenen. Dus de kernel is misschien bug vrij, maar of het ook werkt zoals je gewild had dat een kernel werkt is een andere vraag. Hij zal in elk geval geen onverwachte dingen doen, want dat is wat je hebt bewezen.

[robvanwijk]

Dus als je 2 16 bit getallen optelt heb je 65536 * 65536 = 4.294.967.296 mogelijkheden, als je die allemaal getest hebt kun je met zekerheid zeggen dat deze optelling bug vrij is.

Ehm ja, met als extra probleem dat je vier miljard testen mag gaan verifiëren... Persoonlijk zou ik liever de code van mijn optel-functie (okee, in dit geval is dat redelijk zinloos, aangezien dat hardware is, maar het gaat even om het idee) erbij pakken en die code regel voor regel bewijzen. Zodra die functie bewezen is mag ik de code

{ b en c zijn geïnitaliseerd }
a := TelOp ( b, c )
{ a = b+c, b = b', c = c' }

simpelweg bewijzen met de claim "specificatie TelOp". b = b' betekent "de huidige waarde van b is gelijk aan de waarde van b voordat deze regel code werd uitgevoerd". Een vaak triviaal (en vaak vergeten) bewijs, maar absoluut cruciaal!

Als je een optelling programmeert waar je eigenlijk had moeten vermenigvuldigen dan is de code correct maar doet de code niet wat je wil.

Je bedoelt "als je een optelling specificeert waar je eigenlijk had moeten vermenigvuldigen". Dit wordt overigens afgevangen door je bewijs (automatisch) te laten verifiëren. De volgende stap van het bewijs gaat met zo'n fout namelijk niet lukken.
Je hebt gelijk dat er een fout in de specificatie kan zitten, maar aangezien die op veel hoger niveau wordt geschreven is het veel begrijpelijker voor een mens en vallen fouten dus veel sneller op dan in je programma-code. Bovendien, dit is mensenwerk (en dat bedoel ik voor de verandering als iets goeds ), ook al heb je net het correctheidsbewijs geleverd, toch test je het nog even uit door het programma te draaien. Blunders in de specificatie vallen dan vaak snel op.

[Reactie gewijzigd door robvanwijk op 23 juli 2024 06:16]

[Munters]

Jij beweert nu wel dat bovenstaande Hello World bugvrij is. Maar weet jij welke libraries meegelinkt worden? Daar kunnen zomaar bugs inzitten hoor. Als je een bugvrije kernel wilt claimen zul je de libraries ook moeten bewijzen.
En dan nog de compiler natuurlijk. Als je een wiskundig bewijs claimt, zul je de compiler ook moeten bewijzen, zeker met optimalisatie aan. Of niet de source, maar de machinecode bewijzen natuurlijk.

[pe1dnn]

Daar heb je gelijk in. Bovendien is er nog een tijds aspect, bijvoorbeeld:

if(vrijdag_de_dertiende == TRUE) {
c = 13
} else {
c = a + b
}

Dit is normaal gesproken een perfecte optelling, tenzij je het toevallig uitvoert op vrijdag de 13e. Dus als je op een willekeurige dag bewezen hebt dat de procedure altijd de som van a en b oplevert dan heb je op vrijdag de 13e een onverklaarbare bug.

Maar daarmee is nog niet bewezen dat bug vrije code niet bestaat, maar alleen dat het heel moeilijk is, zelfs voor een simpel Hello world! programma. Het is in praktisch onmogelijk maar daarom nog niet per definitie onmogelijk.

[koelpasta]

Een goede test zou testen voor zowel vrijdag_de_dertiende = TRUE als vrijdag_de_dertiende = FALSE ...

[MSalters]

Je haalt nu "bewijs" en "test" door elkaar. Een bewijs zou aantonen dat er een vertakking (branch) is, en de correctheid van beide takken aantonen. Omdat de eerste tak niet correct is, faalt het bewijs voor de hele functie. Juist deze vertakkingen zorgen ervoor dat bewijzen meer werk is dan testen. Een nog grotere complexiteit ontstaat namelijk als je meerdere vertakkingen hebt; soms moet je niet aleen de correctheid van alle takken maar zelfs van alle mogelijke paden bewijzen. Dat is het verschil tussen 2+2+2+2 en 2*2*2*2

[n4m3l355]

Niet lullig bedoelt.. je bent zelf een Msc maar dan zou ik toch wel meer verwachten qua reactie zijnde. Je mag er wel vanuit gaan een project als deze hebben meerdere uiterst knappe koppen aan gewerkt die naar alle waarschijnlijkheid wel weten waar ze het over hebben. Immers zij zijn volledig begaan na 4 jaar met hun project en indien dit gepubliceerd is, is het pas correct bevonden nadat andere partijen dit ook getoetst hebben. Ik kan me moeilijk voorstellen dat ze iets wereldwijd publiceren als dit dan ook niet het geval zou zijn. Niet alleen hangt je geloofwaardigheid als universiteit sterk hier vanaf maar ook je sponsors. Dus... als ze denken dat deze kernel bugvrij is mag je er wel vanuit gaan dat dit daadwerkelijk het geval is.
Nu... 4 jaar controleren op een kleine 8700 regeltjes code lijkt me wel erg lang. Als je bedenkt dat de hedendaagse linux kernel een kleine 2,4 miljoen lines aan code kent zou deze (indien je lineair werkt) 1100 jaar duren om te controleren. Ik weet niet hoe het zit met andere stukken software die ook critical zijn waar men het hierover heeft maar dit lijkt me toch wel een erg trage methode voor practisch te kunnen functioneren.

[Reactie gewijzigd door n4m3l355 op 23 juli 2024 06:16]

[johnbetonschaar]

Aan de TU/e waar ik afgestudeerd ben zijn al 10-tallen jaren hele groepen mensen er stellig van overtuigd dat ze software formeel kunnen bewijzen, de helft van het curriculum was in mijn tijd nog ingericht voor dit soort methodes. Maar veel verder dan wat eenvouidige loopjes of zoekalgoritmes bewijzen kom je niet, omdat het bewijsproces niet te automatiseren is, en de bewijslast explosief stijgt als je het aantal regels code of het aantal interacties tussen variabelen vergroot. Bovendien zijn sommige constructies zelfs tot nu toe fundamenteel onbewijsbaar gebleken, zoals non-deterministische parallele uitvoering van code (bijvoorbeeld multithreading in een modern OS, I/O parallelisme, user input, etc).

Al dit onderzoek aan de TU/e, die er echt jarenlang voorloper in is geweest, heeft nog nooit tot praktische resultaten geleid. Nu wil ik absoluut niet zeggen dat de mensen die aan universiteiten bezig zijn met dit soort dingen niet heel erg slim zijn, maar het blijven wel academici, die zich soms zo in een bepaald onderzoeksgebied storten dat ze op het gegeven moment te ver van de praktische realiteit afdwalen dat het onderzoek steeds minder nuttig wordt. Zo moet het ook zijn trouwens, anders zullen er nooit meer grote doorbraken die altijd onmogelijk leken worden behaald, maar dat wil niet zeggen dat alles wat aan universiteiten gebeurt altijd zinvol of nuttig is omdat er zulke slimme mensen rondlopen.

[latka]

Zat zelf op de TUD met dit soort onderzoek en het kan weldegelijk praktisch nuttig zijn. Bijvoorbeeld I2C protocol doorgetest en race-condities vinden of een software algoritme voor multiple-reader, single-writer locking mechanisme toetsen en fouten in vinden.
Ik geef toe, het is geen OS of tekstverwerker, maar je software/oplossing is zo sterk als de zwakste schakel. Als je fundamenten al fout zijn wordt het huisje wat je erop bouwt niet veel beter.

[robvanwijk]

Maar veel verder dan wat eenvouidige loopjes of zoekalgoritmes bewijzen kom je niet, omdat het bewijsproces niet te automatiseren is, en de bewijslast explosief stijgt als je het aantal regels code of het aantal interacties tussen variabelen vergroot.

Nou haal je twee dingen door elkaar. Je kunt weliswaar geen algorithme schrijven dat volledig automatisch en gegarandeerd binnen eindige tijd een bewijsverplichting bewijst of weerlegt, maar je kunt wel een algorithme schrijven dat het overgrote deel van de bewijsverplichtingen automatisch afwerkt. En dan doe je de laatste paar met de hand. Vervelend werkje, ik weet het, maar zeer zeker wel mogelijk.
Die explosieve groei aan bewijsverplichtingen zijn voor het grootste deel trouwens triviale dingetjes, die je automatische checker allemaal voor je doet.

Bovendien zijn sommige constructies zelfs tot nu toe fundamenteel onbewijsbaar gebleken, zoals non-deterministische parallele uitvoering van code (bijvoorbeeld multithreading in een modern OS, I/O parallelisme, user input, etc).

Als je aan de TU/e afgestudeerd bent in de tijd dat er nog veel van dit soort vakken gegeven werden, dan moet je ook "Parallelle en Gedistribueerde Algorithmen" gedaan hebben, dat hier juist specifiek over gaat...
Bij parallellisme blaast het aantal bewijsverplichtingen pas echt op, maar daar heb je juist je synchronisatie voor om het enigszins binnen de perken te houden, zodat simpele sommetjes zelfs nog met de hand te maken zijn. En het is hoe dan ook niet "fundamenteel onbewijsbaar"!

[RedLizard]

Maar veel verder dan wat eenvouidige loopjes of zoekalgoritmes bewijzen kom je niet, omdat het bewijsproces niet te automatiseren is.

Dat is dus precies waar zoveel onderzoek naar wordt gedaan. Grote delen van het bewijsproces zijn wel degelijk te automatiseren, middels technieken als model checking.

Bovendien zijn sommige constructies zelfs tot nu toe fundamenteel onbewijsbaar gebleken, zoals non-deterministische parallele uitvoering van code (bijvoorbeeld multithreading in een modern OS, I/O parallelisme, user input, etc).

Bron? Ik kan parallele programma's probleemloos correct bewijzen.

Al dit onderzoek aan de TU/e, die er echt jarenlang voorloper in is geweest, heeft nog nooit tot praktische resultaten geleid.

Voor bepaalde waarden van praktisch misschien niet.

maar dat wil niet zeggen dat alles wat aan universiteiten gebeurt altijd zinvol of nuttig is omdat er zulke slimme mensen rondlopen.

Tja, met fundamenteel onderzoek weet je nooit van tevoren of het iets gaat opleveren. Maar in de praktijk bestaat er vrijwel geen fundamenteel onderzoek waar men op de lange termijn niks aan heeft. Kun je me een stukje fundamenteel onderzoek van ouder dan 200 jaar aanwijzen wat bij nader inzien volstrekt zinloos was? (Onderzoek of iets mogelijk is met de conclusie dat het niet mogelijk is telt niet als zinloos)

(edit: typo)

[Reactie gewijzigd door RedLizard op 23 juli 2024 06:16]

[fdm391]

Ik denk dat je er niet zomaar vanuit moet gaan dat de 'controletijd' lineair oploopt. De linux kernel bugvrij maken zou grappig zijn, maar niet écht nodig.
Het onderzoek hier heeft betrekking op kritische embedded systemen met een kleine kernel. Bovendien gaan ze er ook vanuit dat de hardware goed werkt, dit is op zich niet erg, maar om de techniek dus toe te passen op bijv. de linux kernel die op eindeloos veel soorten hardware kan draaien is nog vele malen moeilijker om te testen omdat de de hardware makkelijk fouten kan bevatten.

[Herko_ter_Horst]

Heb je het nu over beveiliging of bugvrije software? 100% waterdichte beveiliging bestaat inderdaad niet (zeker niet als er ook nog met het systeem gewerkt moet worden).

Van software kan wiskundig bewezen worden dat het bugvrij is. Of dat hier ook echt gebeurd is, laat ik in het midden, maar het kan wel.

De lange doorlooptijd van de tests, gekoppeld aan de relatief geringen omvang/complexiteit van de code, geeft overigens wel aan waarom de meeste software nog steeds bugs bevat: het is te duur en het duurt te lang om software bugvrij te maken.

[koelpasta]

"Van software kan wiskundig bewezen worden dat het bugvrij is. Of dat hier ook echt gebeurd is, laat ik in het midden, maar het kan wel."

Eeh, nee dus,
Van software in zn algemeenheid kun je niet bewijzen dat het bugvrij is.
Hooguit van bepaalde soorten/stukken software.

[Verwijderd]

Wooow o.O als dat echt zo is, knap gedaan!

[Verwijderd]

Mijn ervaring is dat de software om te testen net zoveel fouten bevat als de te testen code zelf.

En hoe weten ze of hun specificaties wel bugvrij zijn?

Dat er weinig bugs in zitten geloof ik meteen, maar gegarandeerd bugvrij? Nee, sorry...

[TheekAzzaBreek]

Maar dit is dan ook niet zomaar een test suite. Hier gaat het om wiskundig bewijs dat de code foutvrij is, niet om testen of je fout gedrag kunt waarnemen. Daar wordt al veel langer over getheoretiseerd, maar dit is de eerste keer dat ik hoor over een echte praktische toepassing. Heel erg praktisch is het overigens nog niet, vier jaar verificatie voor 8700 regels code schiet niet op, maar voor kleine kritische systemen met een heeel lange releasecycle we een doorbraak.

[robvanwijk]

Hier gaat het om wiskundig bewijs dat de code foutvrij is, niet om testen of je fout gedrag kunt waarnemen. Daar wordt al veel langer over getheoretiseerd, maar dit is de eerste keer dat ik hoor over een echte praktische toepassing.

Dat kon in '68 al, toen de groep van Dijkstra het multiprogramming system maakte. Lees deze paper maar eens:

quote: EWD196

We have found it is possible to design a refined multiprogramming system in such a way that its logical soundness can be proved a priori and that its implementation admits exhaustive testing. The only errors that showed up during testing were trivial coding errors (occurring with a density of only one error per 500 instructions), each of them located with 10 minutes (classical) inspection at the machine and each of them correspondingly easy to remedy.

Of er tussen 1968 en 2009 ook nog andere bewezen-foutvrije kernels gemaakt zijn weet ik niet.

Heel erg praktisch is het overigens nog niet, vier jaar verificatie voor 8700 regels code schiet niet op

Hou er rekening mee dat het niet vier jaar kostte om het bewijs te leveren; het kostte vier jaar om te proberen het bewijs te leveren en telkens eerst de code te moeten fixen en dan weer proberen het bewijs rond te krijgen. Ik heb indertijd nog wel sommetjes mogen maken "schrijf code die een binary search uitvoert en bewijs de correctheid"; nog geen tien regels aan code, maar een paar pagina's aan bewijs en je was er al snel een uur mee bezig.

[Verwijderd]

Uhm, daar zit nogal een groot verschil in.

Dijkstra deed een beetje aan hand-waving met informele bewijzen. Dit is pure formele logica die door een machine wordt gecontroleerd. Het is dus zeker niet "hetzelfde".

Dan nog iets over het "bewijzen". Het is inderdaad niet 100% zeker dat wat er geclaimd wordt in dit artikel ook bewezen wordt, maar dat is alleen als je aanneemt dat de personen die het bewezen hebben geen idee hadden wat ze aan het doen waren.

Formele bewijzen schrijven is redelijk lastig. Het verkeerde bewijzen en dit niet weten is redelijk onwaarschijnlijk in mijn ervaring.

[Verwijderd]

Interesant stukje artikel, maar dit in 8000 regels code is helemaal te gek minix was volgens mij 3000 regels, ik zou toch niet met een windows willen vliegen dan komt een blauw scherm toch wel heel er dicht bij de dood.

[Aikon]

Het gaat om iets wat ze denken 'wiskundig bewijs' te zijn. Nu weet ik niet alles van de methode (of eigenlijk niks), maar eerst moet je zeker weten dat de testsoftware 100% bugvrij is natuurlijk, en hoe test je dat? Daar heb je je vicieuze cirkel al.

En bovendien is dit soort dingen sowieso lastig te bewijzen, in de trant van, hoe bewijs je dat er geen theepot rond de aarde cirkelt?

[Verwijderd]

Ga je maar eens inlezen in de materie dan dat is echt het enige dat ik je kan aanraden gezien het feit dat je wel graag een mening hierover deelt

[i-chat]

nooit erg opgelet dus - een beetje nadenken en wiskundig inzicht - zegt je direct
dat die tenminste plausibel is, - natuurlijk moet je oppassen met wat jij zegt voor die vicieuze circel - maar denk maar niet dat als jij daar op komt zij dat niet al lang hadden gedaan...

bovendien willen ze die gaan verwerken in openkernel projecten- er zouden best nog denk en rekenfouten kunnen worden achterhaald, - of NOG betere bugvrije oplossingen te bedenken zijn, - maar stellen dat het niet kan, is net zo dom als roepen dat de aarde plat is (gewoon omdat jij de ronding niet kunt zien) ...

[Aikon]

Ik weet niet of het op mij slaat, maar ik stel iig niet dat het niet kan, enkel dat het lastig is.

Maar ik hoor graag waarom het dan wel mogelijk is om met 100% zekerheid te zeggen dat eea bugvrij is ipv een 'aan zekerheid grenzende waarschijnlijkheid'.

[koelpasta]

En wie zegt dat de wiskunde die ze gebruiken bug vrij is?

[MSalters]

Die wiskunde is gebasserd op een beperkt aantal regels; dan moet je eerder aan 10 regels denken. Juist daarom kun je de correctheid daarvan bewijzen. Vervolgens heb je inderdaad de toepassing van die regels, maar dat is met "Isabelle" automatisch toegepast.

De enige overgebleven vraag is nu of er in Isabelle fouten zitten die toevallig precies een fout in se4L verhullen. Dat is bijzonder onwaarschijnlijk; een bug in Isabelle leidt vrij waarschijnlijk tot het falen van het bewijs, niet tot een onjuist bewijs. Vergelijk het met de automatische piloot van een vliegtuig: een bug daarin leidt veel sneller tot een crash dan een landing op een verkeerd vliegveld.

[Verwijderd]

Tja, dat krijg je met unit tests en dergelijke. Maar dit gaat niet om unit tests. Dit gaat om een formeel wiskundig bewijs. Door de code achter de proof checkers en de verzameling gebruikte axioma's zo klein mogelijk te houden weet je ook vrij zeker dat er geen fouten in je testsoftware zit, en de enige fouten die je dan kunt hebben zitten in de vertaling van de code naar de formele wiskundige uitdrukking.

En voor de mensen die roepen dat het bewijzen helemaal niet kan, omdat het stopprobleem onbeslisbaar is: we hebben het hier slechts over één programma, dus het haltingprobleem is irrelevant.

[J.J.J. Bokma]

Het "stop probleem" heeft niks met het aantal programma's te maken. Het zegt slechts dat een extern programma (in dit geval het verificatieprogramma) niet kan beslissen of een ander programma ooit stopt of niet.

En ik ben inderdaad nieuwsgierig hoe dit wiskundige bewijsprogramma om het halting problem heen gewerkt heeft. Misschien door nergens in de code zo'n situatie te plaatsen?

[robvanwijk]

Correctie, het "stop probleem" (beter bekend als "halting problem") kan niet voor alle programma's zeggen "deze stopt" of "deze stopt niet". Als je echter drie mogelijke antwoorden toestaat: "deze stopt", "deze stopt niet" of "ik weet het niet", dan kun je wel degelijk een programma schrijven dat in veel (maar dus niet alle) gevallen verteld of het programma stopt of niet.
Dat het bewijsprogramma dus van een flink aantal stukken code heeft gezegd "dit stopt ooit" betekent absoluut niet dat het halting problem is opgelost en is niet strijdig met het feit dat het halting problem onoplosbaar is.
Het is niet mogelijk om alle priemgetallen te geven, maar dat houdt niemand tegen om een heleboel priemgetallen te geven. De reden dat je niet alle priemgetallen kunt geven (het zijn er oneindig veel) heeft overigens niks te maken met de reden dat het halting problem onoplosbaar is (niet eenvoudig uit te leggen).

Voor wie meer wil lezen, het Wikipedia artikel over het halting problem is behoorlijk uitgebreid en duidelijk. De volgende paragraaf vat het mooi samen:

quote: http://en.wikipedia.org/wiki/Halting_problem

While Turing's proof shows that there can be no general method or algorithm to determine whether algorithms halt, individual instances of that problem may very well be susceptible to attack. Given a specific algorithm, one can often show that it must halt for any input, and in fact computer scientists often do just that as part of a correctness proof. But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt. However, there are some heuristics that can be used in an automated fashion to attempt to construct a proof, which succeed frequently on typical programs. This field of research is known as automated termination analysis.

Hier staat ook een uitleg over hoe je kunt bewijzen dat het halting problem onoplosbaar is.

[hello123456]

Zeker, 8700 regels code is ook wel zeer weinig voor een kernel, maar als ze hier bug-vrij-blijvend op verder kunnen bouwen heeft dit zeker toekomst.

[Pixeltje]

Ze zeggen vier jaar uitvoerig getest te hebben met allerlei wiskundige speeltjes; ik neem aan dat als ze nu nieuwe code toevoegen (of code aanpassen) dat ze die weer testen.

Ik hoop alleen dat het relatief snel kan, anders blijf je als ontwikkelaar achter de feiten aanlopen. Tegen de tijd dat je code dan goed en wel in de kernel staat, werkt en bugvrij is, issie alweer oud

[Verwijderd]

Mijn vermoeden is dat ze niet veel meer zullen veranderen aan de kernel, nu hij helemaal getest is en bugvrij bevonden is. Het is een micro-kernel, dus uitbreiding zal voornamelijk gebeuren door middel van modules die in user-space zullen draaien. Die modules kunnen dan natuurlijk nog wel bugs bevatten, maar dat is in dat geval minder erg omdat die modules in elk geval niet draaien met alle rechten van de kernel, zodat een eventuele exploit of crash van een module minder grote gevolgen heeft.

Ik weet nog niet het fijne van deze specifieke kernel, maar bij bijvoorbeeld Minix is het de bedoeling dat als een bepaalde module crasht, deze gewoon herstart kan worden zonder dat het hele besturingssysteem er last van hoeft te hebben. Ik neem aan dat dit project soortgelijke "stabiliteitsdoelstellingen" heeft, alleen hebben ze bij dit project geprobeerd te bewijzen dat de kernel foutloos is en bij Minix voor zover ik weet niet.

[Peregrine]

Op PC gebied zal het misschien belangrijk zijn om de 'nieuwste' software te draaien, maar

voor de aansturing van embedded systemen, zoals de micro-elektronica in auto's en vliegtuigen

is het belangrijker dat het foutvrij is.

Vooral deze systemen draaien op 'oude' software omdat deze juist door het lange gebruik 'bewezen' hebben goed te werken. Of, anders gezegd, deze systemen hebben bewezen dat de fouten die er nog in zitten niet vaak genoeg voorkomen om op te vallen, wat ook acceptabel is.

Hoewel ik betwijfel of dit project in eerste instantie is opgezet om een product op te leveren vraag ik mij af, ik vermoed dat het vooral een 'proof-of-concept' is. Maar dat neemt niet weg dat als het de juiste functionaliteit heeft, dat dit, vooral voor de medische, luchtvaart en ruimtevaart industrie, super goed toepasbaar zal zijn.

[dasiro]

ik noem dat niet knap gedaan. Voor zo'n kleine programmacode is het zelfs relatief simpel om bugs op te sporen en eruit te programmeren.

Echter 4 jaar testen is enorm lang. Als je weet dat de Windows en linux kernels uit enkele miljoenen regels code zijn opgebouwd, dan zou je dus ruwweg een paar duizend jaar moeten testen om alle bugs eruit te krijgen (ff lineair doorgerekend)

[MatthiasDS]

De bedoeling was dan ook niet om van de windows en linux kernel te bewijzen dat ze foutvrij zijn. De bedoeling was om hun eigen kernel te maken en dit volledig bugvrij. Dat is gelukt, en dat is een stevige basis om verder op te borduren voor software zoals genoemd in het artikel: "micro-elektronica in auto's en vliegtuigen".

[OddesE]

Ze hebben dus niet getest. Dat is juist het mooie aan deze methode, testen hoeft niet want je hebt wiskundig aangetoond dat het bugvrij is. Alles testen is onmogelijk, van bepaalde problemen kun je echter wel het bewijs leveren. (er zijn problemen die niet te bewijzen zijn).

Verder is vier jaar ook weer niet zoveel. Had MS maar 4 gewerkt om wiskundig aan te tonen dat de kernel van NT 1 vrij van bugs is. Eenmaal goed kan die code tientallen jaren mee en ik vraag me ook af hoeveel test effort er nu steeds in gaat zitten

[Verwijderd]

Goh, en wie ben jij om te zeggen dat dit niet "knap" is?

Hoeveel kernels heb jij geverifieerd? Ik zeg niet dat het knap is, maar ook niet dat het niet knap is, maar als je er de ballen verstand van hebt, zeg dan niets.

[Verwijderd]

De code is geschreven in C. Dus al niet rechtstreeks in assembler. Dat betekent dat er een stuk software de code omzet. Is die code bugvrij ? Waarin is de controlesoftware geschreven ? Is die controlesoftware wel bugvrij ? Wat is de kans dat er een fout zit in de wiskundige principes die zijn toegepast ? Dan is er nog het "brown-out" fenomeen, de kans dat een computer een spontane fout maakt.

Kennelijk weten deze mensen het beter dan Murpy maar volgens mij gelden zijn wetten nog steeds.

[psychoclown]

Wat een geweldige ontwikkeling!
Vraag me alleen af of dit de stimulans kan zijn tot een echte windows/mac os killer..
Evenals of dit ook gebruikt kan worden in het bugvrij maken van bijv. games want de laatste jaren komen er maar weinig games uit met vrijwel geen bugs

[BastiaanCM]

Zou een applicatie een ingame bug zien als een bug ?

Stel, een kleur is anders weergegeven. Dat mag een bug zijn, maar in principe is ergens een kleur foutief aangegeven. De game laat het kleurtje gewoon zien, zoals de bedoeling was in de code. Misschien niet die van de makers.

Ik denk zelf dat er wel meer gecompliceerde voorbeelden zijn, echter wil ik geen verkeerde uitspraken doen Iets met collision detection o.i.d. het lijkt me ZEER lastig om bugs in games te ontdekken. Vooral omdat in games geen (vaak niet) foutcodes zijn, dingen gebeuren gewoon anders, of worden anders weergegeven.

[psychoclown]

Daar heb je een goed punt maar er zijn ook bugs qua instabiliteit.
Bugs die een spel laten crashen bijvoorbeeld, lijkt me dat dat wel een fout in de code is en zoals ik het lees kan deze verificatiemethode dit eruit filteren.

Als dit ook zo geschreven kan worden dat het ook voor games werkt die specifiek dat soort bugs eruit filtert kan dit bijv. erg veel tijd schelen voor de ontwikkelaars.
Maarja dat zal wel toekomst muziek zijn..

[bwerg]

en zoals ik het lees kan deze verificatiemethode dit eruit filteren.

Niet erg realistisch. Kijk eens hoeveel code er achter een game zit en op hoeveel drivers en hardware een game moet kunnen draaien. Als het al kan met deze methode, ben je niet binnen een triljard jaar klaar met testen...

[TD-er]

Ik denk zelf dat er wel meer gecompliceerde voorbeelden zijn, echter wil ik geen verkeerde uitspraken doen Iets met collision detection o.i.d. het lijkt me ZEER lastig om bugs in games te ontdekken. Vooral omdat in games geen (vaak niet) foutcodes zijn, dingen gebeuren gewoon anders, of worden anders weergegeven.

Bij collision detection achtige algoritmen wordt vaak een versimpelde representatie van de werkelijkheid gemaakt, die dusdanig veel simpeler is, dat het heel veel rekentijd scheelt. Nadeel is wel dat het ontwerp bewust ontworpen is met foutjes, alleen dan wel met de afwijkingen dusdanig gekozen dat het resultaat zo weinig mogelijk afwijkt van de werkelijkheid.

Een collision-object bestaat vrijwel altijd uit een sphere, of een sphere-swept object, zoals een capsule (het volume wat je krijgt als je een bol beweegt over een lijn)
Hierdoor hoef je alleen maar de afstand te berekenen tussen 2 punten (sphere-sphere) of punt en lijn-segment (sphere-capsule) of 2 lijn-segmenten (capsule-capsule) en van die afstand beide radii af te trekken.
Het is wel duidelijk wat de foutjes zijn in het ontwerp, tussen een auto en een reeks spheres en capsules.

Kortom, collision detection en andere "foutjes" in spellen kunnen niet met dit soort bewijzers verbeterd of geverifieerd worden, omdat er bewust fouten in het ontwerp worden toegelaten.

[robvanwijk]

Kortom, collision detection en andere "foutjes" in spellen kunnen niet met dit soort bewijzers verbeterd of geverifieerd worden, omdat er bewust fouten in het ontwerp worden toegelaten.

Maar dan kun je nog steeds wel bewijzen dat de code correct je sphere-collisions uitrekent! Waarmee je bijvoorbeeld een bug kan vinden die het onder (zeer specfieke en/of zeldzame omstandigheden) toestaat om dwars door een muur heen te lopen. Gewoon testen kan dat missen, een formele verificatie niet.
Los hiervan: deze methoden zijn velen malen te arbeids-intensief (en dus te duur) om te gebruiken voor een spel. Zou jij duizenden euro's neertellen voor "Yet another FPS, maar dan gegarandeerd zonder bugs"? Nee, ik ook niet. En als het niet net zo goed verkoopt als een normale FPS dan wordt de prijs per exemplaar alleen maar hoger.

[Niosus]

je hebt bugs en glitches. Een glitch is eigenlijk jouw voorbeeld: De game blijft draaien maar ergens is er iets wat er niet zou mogen zijn. Bij (échte) bugs loopt het spel meestal vast of daalt de FPS aanzienlijk. Omdat er hier berekingen worden gedaan die gewoon niet kloppen. Dit zouden ze wel kunnen vinden door in een testrun de hoeveelheid berekingen per seconde een bepaalde "event" nodig heeft, en als die plots enorm stijgt om dan te gaan zoeken naar waar gaat het fout.


Tegenwoordig zijn er niet heel veel bugs meer in games, er zijn er nog, maar DirectX is een platform dat redelijk stabiel is en de meeste crashes kan opvangen. Glitches komen echter steeds meer voor. Omdat er steeds meer physics worden gebruikt en je meer vrijheid krijg gebeurt het regelmatig dat je door een physics glitch voor 10 minuten lang in de lucht geslingerd wordt of dat er 2 objecten in elkaar vastzitten en hun collision sound blijven uitzenden, voor tientallen keren per seconde... Ook bij free roaming games kan je last hebben van de AI die plots niets meer wilt doen. Of objectives die niet gecomplete willen geraken, dan zit je daarop te springen en te doen op elke mogelijke manier maar nog steeds ziet de game het niet.

[bwerg]

Tegenwoordig zijn er niet heel veel bugs meer in games

Nou, helaas wel, er zijn genoeg games die na tien keer patchen nog steeds op willekeurige momenten crashen...

Daar heeft dit kernel-verhaal echter niks mee te maken, wiskundig bewijzen dat een game op àlle drivers en hardware kan is onmogelijk. De enige manier om deze bugs op te lossen is door het gewoon uitvoeriger te testen, wat helaas lang niet altijd gebeurd.

[Verwijderd]

Kijk, daar hebben we consoles voor uitgevonden.

Helaas zijn Console games vaak ook niet bugvrij..

[SirNobax]

Vraag me alleen af of dit de stimulans kan zijn tot een echte windows/mac os killer..

Ik denk weet zeker dat er (gigantisch veel) meer te verdienen is met de embedded markt, dan een simpel OS'je voor consumenten. Dit zal je dan ook enkel maar terug zien in Pinautomaten of beveiligingsinstallaties bijvoorbeeld.

[StefanTs]

Pinautomaten werken gewoon op Windows

[willyb]

Helaas wel ja... zelfs kassa's starten nog op met 'Himem is bezig met het testen...'.

[Verwijderd]

Waarom zou je voor zulke dingen een nieuw OS gaan ontwikkelen als er al OSen zijn? Dat die overkill zijn voor de toepassing is geen bezwaar, de benodigde generieke hardware waar het nog op draaid kost toch niet veel. Je kunt best een embedded 486 bordje maken waar een geldautomaat of kaartjesautomaat op draait, maar dat is veel duurder dan een goedkope standaard PC met win2000.

[vDorst]

Dit is dan exclusief de drivers en geheugen variablen?

Lijk me niet dat de verificatie van drivers mee kan nemen. Want dan zal je alle hardware ook als model mee moeten nemen.

Of ik nu txpower nu 10 of 100mW laat uitzenden. Qua functionaliteit blijft het hetzelfde maar radio protocol zou dit niet mogen en is dat een bug.

[Haan]

Er zitten geen drivers voor filesystem, netwerkstack etc. in deze microkernel Dus dat hebben ze inderdaad niet geverifieerd.

[Adion]

8700 regels code bugvrij krijgen in 4 jaar lijkt me nu ook weer niet zo bijzonder.
Ik snap overigens ook niet wat die verificatiesoftware nu exact gedaan heeft in die 4 jaar?
Het lijkt me sterk dat het zoeken naar een wiskundige verificatie van 8700 regels code echt 4 jaar rekenwerk vraagt?

Hoe dan ook, als het 4 jaar duurt om zo'n klein stukje van het geheel bewezen bugvrij te maken dan vrees ik dat het in de praktijk maar zeer beperkt nuttig is. (En bijna zeker nutteloos voor een gemiddeld desktop OS, waar je constant nieuwe hardware wilt kunnen benutten, nieuwe programma's wilt kunnen draaien/maken en wat je constant wilt verbeteren.

[Verwijderd]

Maar het kan wel de eerste stap zijn naar het ontwikkelen van software die dit sneller en effecienter kan. Stel je voor dat we binnen enkele jaren software hebben die code kan controleren op alle gekende bugs in bv. enkele dagen/uren. Dan zal het mogelijk zijn dat de frabrikant van het OS zegt dat iedere driver/programma voor dat OS moet gecertificeerd zijn door hun validatieprogramma. Zo kunnen we zeker zijn dat de software zal doen wat we ervan verwachten met een minimum beveiligingsrisico.

[CH4OS]

En heeft men ook getest door middel van proberen een buffer overflow te creëren?
Anders ben je nooit zeker dat een kernel er vatbaar voor is of niet.

[robvanwijk]

En heeft men ook getest door middel van proberen een buffer overflow te creëren?
Anders ben je nooit zeker dat een kernel er vatbaar voor is of niet.

Nee, precies andersom! Je kunt vier jaar langs non-stop testen en dan weet je nog niet zeker of je niet een testgeval vergeten bent. Met een wiskundig bewijs heb je zekerheid. Nee, niet 99,99..9937 procent, echt 100 procent!
Lees even de post hier een klein beetje boven van pvcholten die Dijkstra quote.

[Verwijderd]

Als ze zeggen in het artikel (en hu publicatie) dat de kernel ongevoelig is voor buffer overflows, zal dat wel zeker...