Nicta maakt 'veilige' SeL4-microkernel opensource

De organisatie Nicta en General Dynamics C4 Systems hebben deze week de SeL4-microkernel vrijgegeven als opensourcesoftware. Het gaat onder andere om de complete code van de kernel, tools, libraries en voorbeeldprogramma's.

SeL4, voluit de Secure Embedded L4-microkernel, kwam vijf jaar geleden in het nieuws nadat de programmatuur jarenlang uitvoerig was getest aan de hand van de analyse van wiskundige berekeningen. Daaruit bleek dat de relatief kleine kernel vrij was van bugs, wat volgens Nicta nu nog steeds het geval is. Ter ondersteuning van de claim heeft het ook de 'bewijzen' vrijgegeven aan de gemeenschap.

Volgens de SeL4-ontwikkelaars doorstaat de microkernel verschillende veelgebruikte aanvallen, zoals stack smashing, het misbruiken van exploits en return-oriented programming. "SeL4 tilt de betrouwbaarheid van software naar een nieuw niveau en zal de ontwikkeling van echte betrouwbare systemen ondersteunen", aldus Nicta.

De organisatie zegt dat belangrijke software tegenwoordig fundamentele tekortkomingen kent. Software waarbij dit onder meer het geval is, zijn volgens Nicta toepassingen in de industrie en in voertuigen, zoals auto's en vliegtuigen. "Wat is vrijgegeven is niet alleen de doorbraak die Nicta in 2009 bereikte, maar ook het complete werk dat daar de jaren daarna is bijgekomen."

Reacties (28)

Door veilige en bewijzen tussen aanhalingstekens te plaatsen lijkt het alsof je het met een korreltje zout moet nemen. Het is echter wel degelijk mogelijk om te bewijzen dat software zich precies gedraagt zoals gespecificeerd, en dat de software nooit in een onverwachte staat terecht zal komen. Oftewel, als je specificeert dat de kernel nooit in situatie X mag komen (een normale user die toegang heeft tot fysieke storage, bijvoorbeeld) dan is het te verifiëren dat dat inderdaad nooit kan gebeuren.

Het gaat hier wel om de software. Hardware kan ook bugs bevatten die weer uit te buiten zijn.

Ik kan me ook totaal niet vinden in die aanhalingstekens; het is veel (en redelijk saai) werk om een programma te bewijzen, zeker als het meer dan enkele tientallen regels lang is, maar het kán wel. En als je dat bewijs eenmaal hebt, dan is het ook net zo sterk als een wiskundig bewijs. Ter vergelijking: als je de Stelling van Pythagoras bewezen hebt, dan blijven mensen niet tot in het oneindige doorzeuren "ja, maar wat nou als, ...". Om de een of andere reden lijkt dat bij software waarvan de correctheid bewezen is juist wél altijd te gebeuren...!?

Eerlijkheidshalve: je moet nog wel belet zijn op "bugs" (onvolkomenheden) in de specificatie. Je kunt niet simpelweg bewijzen "hier zitten geen fouten in", je kunt alleen bewijzen "hier zit deze specifieke fout niet in". Stel dat je vergeet om te bewijzen dat er nooit deadlock optreedt, dan zijn alle bewijzen die je wel gegeven hebt nog steeds geldig (en die ándere fouten komen dan ook inderdaad niet voor), maar het is prima mogelijk dat er deadlock op kan treden. (Een veel realistischer vergissing is om afwezigheid van deadlock te bewijzen, maar te vergeten om afwezigheid van livelock te bewijzen.)

Tips om op te Googlen:

• correctness by construction
• hoare triple
• predicate transformers
• guarded command language

Door het voorbehoud dat je vanaf "Eerlijkheidshalve" in bouwt klinkt het heel erg alsof je zegt: alle bugs die wij konden bedenken zijn er uit (en dat is wetenschappelijk bewezen). Heel af en toe heb ik ook wel eens aan een projectje gewerkt waar alle bekende bugs weggewerkt waren (en natuurlijk hadden wij daar geen enkel wetenschappelijk bewijs voor) maar er werd altijd toch wel weer een hele nieuwe bug gevonden. Hoe is dat anders dan bij deze microkernel?

Valide vraag.

Het gebied dat zich bezig houdt met het 'bewijzen van software' heet "Formal Verification". De kernvraag in dit gebied is:
gegeven een programma P
gegeven een specificatie S
voldoet P aan S?

Een programma P voldoet aan een specificatie S indien voor alle mogelijke inputwaarden I voor P, P exact doet wat S specifieert dat P moet doen. M.a.w. voor alle I: P(I)=S(I). Een specificatie bevat typisch oa invarianten in je code.

Als je nu een bug specifieert als een mogelijke run van je programma waarbij iets onverwachts gebeurt, m.a.w. P(i)!=S(i), dan kan formal verification bewijzen dat er geen bug bestaat. Immers, als je kan bewijzen dat je programma P voldoet aan specificatie S, dan heb je bewezen dat er geen I bestaat waarvoor P(I)!=S(I), en bijgevolg dat er geen enkele bug is. Merk op dat een bug - zoals hier gedefinieerd - afhankelijk is je specificatie S. Dit is logisch, een bug hangt samen met wat je verwacht dat je programma doet.

Het enige wat nu nog fout kan gaan, is dat je specificatie niet volledig correct is. Dan heb je wel bewezen dat P(I)=S(I) voor alle I, maar als S toelaat dat een gebruiker root acces krijgt zonder admin-account, dan ben je natuurlijk nog steeds kwetsbaar. Niettemin bevat je programma dan geen bugs, uitgaande van specificatie S.

Als het nog fout kan lopen bij je specificatie, wat heb je dan gewonnen? Wel, specificaties schrijven is véél makkelijker dan programma's schrijven. Zeggen wát je programma moet doen, is makkelijker dan zeggen hóé het dat moet doen. Specificaties zijn typisch geschreven in logica, een veel leesbaarder taal dan C++ of <insert favoriete imperatieve taal>. Het is makkelijker voor mij om te zeggen: "een user zonder admin-account mag nooit root-access krijgen" dan om een programma te schrijven dat dit altijd garandeert. Die stap overbruggen is wat Formal Verification (of "het bewijzen van bug-vrijheid van programma's") doet.

Dus ja, je kan wiskundig bewezen bug-vrije programma's schrijven, gegeven een bepaalde specificatie van wat je programma moet doen. Ow, en gegeven een hele zak geld, want formal verification is lastig en duur

[Reactie gewijzigd door Dooievriend op 2 augustus 2014 19:00]

Maar dan heb je toch een ijzersterke nooit ambigue specificatie nodig. Zoiets wil ik wel eens zien, gewoon uit nieuwsgierigheid.

Ik ben er ook maar zijdelings bij betrokken, maar bvb. Alloy is een formele specificatietaal gebaseerd op relationele logica.

Zelf werk ik met eerste-orde-logica: inderdaad een taal die nooit ambigu is. In eerste orde logica kun je bvb schrijven: "er bestaat geen tijdstip waarop een gebruiker zonder adminrechten root-toegang heeft". Of "voor elke inputlijst geldt dat de outputlijst gesorteerd is".

Het probleem is dat perfect werkende software nog steeds misbruikt kan worden voor doeleinden waar het niet voor is bedoeld.
Software is niet veilig. Flexibiliteit is het grote voordeel van software. Het nadeel is dat het niet veilig is. Dat is de tradeoff. Het is goedkoper dan hardware, maar de prijs die je betaald is de opoffering van een deel veiligheid.

Software is goedkoper dan hardware ? Waar haal je dat ? Ik denk dat er meer manuren gaan in software dan in hardware. Maar ik kan verkeerd zijn.

Het aantal manuren noodzakelijk om software te ontwikkelen ligt lager dan om de hardware te ontwikkelen met dezelfde functie als die software.
Dat is het hele doel van software, daarom is het uitgevonden.

Ja als je het zo bekijkt dan heb je wel groot gelijk .

Totdat iemand aantoont dat die algoritmes niet kloppen. Geen garanties in de wetenschap. Alles is theorie totdat het tegendeel bewezen is

In de wiskunde zijn er wel degelijk garanties te geven, in de vorm van sluitende bewijzen. Er is dan nooit meer een speld tussen te krijgen. Er zijn dan geen uitzonderingen meer. De algoritmes voor dit soort model checking software zijn ongetwijfeld ook bewezen.

Ja, voor de stelling van Piet misschien, maar ik zie niemand 100% garantie geven dat software 100% foutvrij is. Waarom stopte de NASA anders 5 (2+2 en een 'scheidsrecher') identieke boordcomputers in de Shuttle, die door 3 verschillende fabrikanten volgens dezelfde specs zijn gemaakt? Omdat er zulke mooie algoritmes zijn om aan te tonen dat het ok is? Kweenie, maar volgens mij kun je dat voor software gewoon nooit garanderen. Een programma is geen stelling van pythagoras...

[edit]
Ah! Ik zie dat meneer hieronder het beter verwoord:

je kunt alleen bewijzen "hier zit deze specifieke fout niet in".

Ergo: 100% foutvrij is gewoon niet te bewijzen. Nu is alleen bewezen dat de nu bekende manieren niet onderuit te halen is. Bedenken we wel weer een nieuwe.
Net zoiets als zeggen dat er dit jaar in de Tour geen doping is gebruikt...het is alleen niet ontdekt

[Reactie gewijzigd door mphilipp op 2 augustus 2014 11:11]

De reden om redundante hardware te gebruiken is dat: redundantie. Als er één uitvalt of onjuiste meetwaardes geeft, dan kunnen de andere het overnemen resp. overriden. Zeker in de ruimte moet je ook nog rekening houden met veel hogere stralingsniveaus dan op aarde, waardoor er letterlijk bits geflipt kunnen worden in RAM/CPU. Dat staat los van de software.

Maar correct me if I'm wrong, je lijkt niet te willen geloven dat het niet mogelijk is om foutloze software te schrijven. Met formele specificaties en controles kan dat wel degelijk. De software doet dan exact wat gespecificeerd is. De wiskunde erachter is feilloos. De clou is dat je het wel goed moet specificeren. Je zou nog kunnen twisten of de specificatie onderdeel is van de software of niet.

Dan moeten ze het maar eens wat vaker toepassen. Ik geloof iets pas wanneer ik het zie. Theorie zegt mij in zoverre niets dat als het in de praktijk niet haalbaar blijkt het zinloos is. Voorlopig wmelen allerlei programma's nog steeds van de fouten. Dus ofwel de wiskundige manier zorgt ervoor dat het allemaal idioot veel langer duurt, of het laat toch nog ruimte voor fouten.

Dus inderdaad: ik wil het niet geloven Theorie heb je in het gewone leven niet zo heel veel aan. Het moet wérken.

De theorie is zeker haalbaar in de praktijk. Maar het is complex en daarmee kostbaar. Meestal loont het de moeite niet om van iets dat waarschijnlijk goed werkt (en zo niet dan fixen we de bug wel even) naar iets dat gegarandeerd goed werkt te gaan.

Komt bij dat bij veel software de aantal mogelijke toestanden gewoon te groot is om door te rekenen. Om GTA V op die manier te specificeren en valideren gaat voorlopig niet lukken ben ik bang.

Maar met kernels en mission critical stukjes software kan het wel. Een bekend voorbeeld is de besturing van onze eigen Maeslantkering waarvan de software op die manier gecontroleerd is (en ja, daardoor zijn er fouten aan het licht gekomen - en gerepareerd).

De technieken die deze meneer gebruikt heeft bewijzen dat zijn software equivalent is aan de specificatie ervan. Dus als daar een foutje (of onvolkomendheid) in zit dan kan het nog net zo makkelijk misgaan.

Idem als de onderliggende CPU een probleem heeft (denk aan de oude FDIV bug). Kortom, leuk dat hij het 'bewezen' heeft maar je moet wel de waarde van dat bewijs begrijpen. Dat het 'wiskundig' is zegt werkelijk niets.

Als je het zo omschrijft klinkt het net als unit-testing eigenlijk. Leuk, maar niet de heilige graal. Dat bepaalt ook of je software voldoet aan de specificaties, zoals deze uitgewerkt is in de unit tests. Hoe is dit anders?

Het probleem zit hem in het feit, wat gebeurt er als ik de software _niet_ volgens de specificaties gebruik.

Want dat is wat er meestal gebeurt. Onkundige gebruikers die software gebruiken voor een doel waar het niet voor is ontworpen, of op een manier die niet is voorzien.

Prima dat een unit test een procedure controleert op het ontbreken van kwetsbaarheden, maar wat gebeurt er als ik 2 of meer van die procedures combineer? Werkt het dan nog steeds naar behoren?

Software installeren is een perfect valide functie, maar als het een trojan is, dan is dat toch zeer onwenselijk en oneigenlijk gebruik van een perfect functionerende functionaliteit.

Het is ook niet de heilige graal.

Wat je hier anders doet is een equivalentie bewijzen dmv. transformatie regels. Dus je draait de code niet, zoals bij een unit-test, maar je bewijst hem gelijk aan een eerdere specificatie. Zeg maar, zoals je in de wiskunde de equivalentie van twee formules kan (proberen te) bewijzen, kun je hier de equivalentie van specificaties en code bewijzen.

Het is alleen pokkemoeilijk om te doen, en met een handjevol (minder dan tien) regels source kun je makkelijk een paar uur bezig zijn. En het wordt in hoog tempo moeilijker naarmate er meer code is.

Misschien is de state of the art inmiddels beter, ik leerde hier twintig jaar geleden op de universiteit over en heb er daarna niet veel aandacht meer aan besteed...

Bewijzen dat software werkt zoals gespecificeerd is eigenlijk niet zo lastig. Het klinkt als een unittest, maar wat ze doen is eigenlijk meer een analyse van de code. Zo wordt er onder andere op buffer overflows gecontroleerd..

De SeL4 micro kernel (net als elke ander micro kernel) heeft out-of-the-box maar beperkte functionaliteit. Zij hebben meer theorien (10.000) getest dan de kernel uit regels (7.500) bestaat.

Als het SeL4 team de tools voor het test suite van de theorieen ook vrij geeft, dan kunnen ook afgeleide projecten worden getoetst dan zal een dergelijke OS een zeer hoge betrouwbaarheid en veiligheidsniveau hebben. Autonome auto's worden steeds meer realiteit en dan is het wel prettig te weten dat de meeste basale fouten niet zijn gemaakt..

Bewijzen dat software werkt zoals gespecificeerd is slechts voor kleine projecten echt makkelijk. Voor de meeste projecten is dat al een hele uitdaging. Maar hier ging het er om dat de software bug-vrij zou zijn, dat legt de lat een stuk hoger voor de specificatie en dat zal dus ook aan de kant van de testen wel een invloed hebben op de complexiteit.

Overigens heb ik zelden unit testen geschreven die je zomaar kunt oppakken en hergebruiken voor een ander project, eigenlijk nooit, denk ik. Waarschijnlijk heeft een ander project ook een andere specificatie, dus dan heeft dat ook niet zoveel zin.

Als je even doorklikt, dan zul je de source code op github vinden: SeL4 Even een handigheidje

[Reactie gewijzigd door Feanathiel op 1 augustus 2014 23:57]

Tsja, dit soort zaken worden toch veelal gebruikt op plaatsen waar je de computer niet fysiek kan bewaken. Zoals eerder genoemd zijn technieken als Side-Channel attaca's te gebruiken.

Daarnaast is dit alleen het OS. Daarbovenop komt nog een applicatie. Die programmeur zal ook fouten kunnen maken

Maar: mooi werk om te programmeren vanuit security. Wordt veels te weinig gedaan...

Totdat iemand input waarden geeft waar niemand eerder aan gedacht heeft...

Het ding is net, dat de er maar heel beperkt aantal input waarden zijn .... net daardoor kun je ook voor iedere input bewijzen dat het doet wat het moet. Er zit een hele wetenschap achter zo'n systemen.