UT-onderzoeker ontwikkelt algoritme voor controleren parallel draaiende software

Tri Minh Ngo, onderzoeker aan de Universiteit Twente, heeft een algoritme ontwikkeld waarmee parallel draaiende software gecontroleerd kan worden op het mogelijk lekken van gevoelige gegevens. Daarmee zijn lekken in programma's gemakkelijker op te sporen.

Het kan bij parallel geprogrammeerde software, waarbij simultane berekeningen uitgevoerd worden, een uitdaging zijn om te achterhalen of de diverse parallelle taken geen informatie lekken. Zo moet een individuele gebruiker geen informatie over privégegevens kunnen afleiden door naar de openbare gegevens te kijken. Marieke Huisman, associate professor aan de Universiteit Twente, geeft als voorbeeld software voor salarisadministratie. Normaliter zijn de salarisgegevens van individuele werknemers privé, maar op basis van andere informatie, zoals het aantal werknemers en het totaalbedrag aan salarissen, zou mogelijk toch iets te zeggen zijn over de salarissen van individuele werknemers.

Onderzoeker Ngo heeft een algoritme ontwikkeld dat de controle op lekken zou vergemakkelijken. Zo zou zijn software kunnen aangeven hoe informatie gelekt wordt en er zou een schatting gemaakt kunnen worden hoeveel informatie er uitlekt. Op basis daarvan kunnen twee verschillende software-implementaties met elkaar vergeleken worden. Uiteindelijk zou het algoritme van Ngo parellelle software veiliger kunnen maken. Ngo zal op 17 april binnen de vakgroep Formal Methods and Tools van onderzoeksinstituut CTIT aan de Universiteit Twente promoveren op zijn proefschrift 'kwantitatieve en kwalitatieve informatie Flow Analysis voor multi-threaded programma's'.

Reacties (24)

Het lijkt mij iets wat elke internet gebruiker zou willen zien op zijn pc, smartphone or whatever hij ook gebruikt om online te gaan.
Een programma dat elke poging tot misbruik van de ontwikkelaars, al dan niet bedoelt,
Aan banden kan leggen, of in ieder geval zichtbaar kan maken.
Met een firewall lukt dat natuurlijk al aardig, maar sommige programma,s hebben zoveel connecties tegelijk dat het onoverzichtelijk word welke wel en welke niet "absoluut" noodzakelijk zijn.
Ik weet dat dit programma hier niet specifiek voor is ontwikkeld, maar dat lijkt mij nou wel de moeite waard om er een programma voor te maken.
misschien wel een doorontwikkeling van dit "parallel geprogrammeerde software" sniffer of hoe moet ik het noemen?!

???? Waar gaat dit nu over???

Waarom deze kortzichtige reactie, Jules Verne. Werd in zijn tijd als fantast gezien.
Onverlet dat werd hij na zijn dood als een soort van ziener gezien.
Damocles werd als tovenaar neergezet in zijn tijd, had echter achteraf vaak wel gelijk.
Alleen geef ik aan dat, met veel minder inzicht of fantasie er een alternatief programma geschreven zou kunnen worden dat totale inzicht in je netwerk verkeer zou geven!
Wat is nou het probleem???
Als jij dat niet wilt, goed. Ik wel!

[Reactie gewijzigd door Rev-anche op 17 april 2014 00:49]

Dat is er al lang, wireshark, ot tcpdump, maar dan encrypt je de traffic die je ongewenst naar buiten stuurt toch gewoon? Of gooi je het ergens anders het internet op, waar al verkeer heen loopt.

Dus, als je dat wilt, installeer die tools, de developer tools, en speur je geheugen af, kijk naar de broncode, compileer zelf je programma's en inspecteer geregeld je netwerkverkeer. De tools zijn er, jouw wens ook, nu alleen jouw inzet nog.

Goed zo. Er wordt veel te weinig met formele methoden gewerkt. Software wordt maar in elkaar geknutseld, en dan wordt er gekeken of het een beetje functioneert, en dan krijgt het al snel het stempel "OK". Dit gebeurt zelfs bij de grote bedrijven zoals Apple en Google. Wat formele methoden betreft zitten we nog in de dark-ages volgens mij, want software blijft maar crashen en lekken.

Tja, probleem is ook dat software niet enkel geproduceerd wordt door afgestudeerde WO beta's. Iedereen denkt wel ff te kunnen ontwerpen/programmeren. En het gaat vaak ook wel goed..
Bedenk wel dat echte vaklui die de formele methoden (behoorlijke dosis wiskunde / logica / abstract kunnen denken) kunnen snappen en toepassen heel duur zijn, en de software dus ook..

Handig voor de klassieke voorbeelden van kerncentrale, hartlongmachine, stormvloedkering.. maar voor smartphones? Daar is time-to-market vele malen belangrijker dan 100% foutloos..

Je hebt gelijk dat economische motieven meespelen, maar die economische motieven zijn ondoorzichtelijker dan je denkt. Zo ken ik iemand die bij Qualcomm de gedragingen van de basebandprocessor formeel specificeert en checkt (toevallig een oud-collega van deze Huisman). Binnen smartphones zijn er genoeg toepassingen die om formele methoden vragen, het zijn niet alleen Snapchatmachines.

Bedenk wel dat echte vaklui die de formele methoden kunnen snappen en toepassen heel duur zijn, en de software dus ook..

Als ik zo'n dure iPhone koop, dan verwacht ik wel dat er capabele mensen aan hebben gewerkt, natuurlijk.

Dat kun je niet verwachten want je betaalt alleen voor de HARDWARE, zoals je zelf aangeeft. Je betaalt niet voor de SOFTWARE.

Vandaar dat al die software totale crap is en vooral van apple (getyped vanaf apple macbookpro overigens).

Je bedoeld de "echte" vaklui die software voor Ariane 5 geschreven hebben met een zodanige fout dat de raket ontplofte ?

bedoelT ja
Ik heb even kort de achtergrond van de Ariane 5 crash opgezocht: http://www.around.com/ariane.html

Daaruit blijkt dat het om een foute aanname / requirement ging. Dat gaan formele methoden niet automatisch voor je oplossen..

Static typing zou hier al heel veel hebben geholpen. En voor die andere ruimtebug, waar men met voet werkte ipv meters (of iets dergelijks) was gemakkelijk vermeden met Dimension typing.

Zolang de klanten blijven vragen om meer features, lagere kosten en sneller af, zullen developers altijd grijpen naar de oplossingen die dit mogelijk maken. Wat inderdaad vaak betekend dat dingen niet goed getest zijn, niet 100% af zijn, of balkanization veroorzaken door van standaarden af te wijken om zo een voordeel te hebben.

Er is net zo goed geen enkele ontwikkeling zo hard gegaan als de software ontwikkeling waarbij ook nog eens ongekend veel mensen er profijt van hebben en er toch eigenlijk veelal zonder al te grote problemen mee in aanraking komen.

Ach nee joh - in de security wereld zijn het de systeembeheerders die altijd programmeren en DUS dingen uitbrengen.

Een wiskundig bewijs van dat iets correct werkt wordt nooit gegeven noch om gevraagd door de klant.

Sterker nog - dat zou niet mogen van de overheid.

Stel je eens voor dat je computer NIET automatisch door de 100 officiele inlichtingendiensten getapt kon worden. Dat zou een schokgolf geven in Den Haag, waarbij ze in staat zijn je te verbieden een computer te mogen gebruiken.

Ik herinner me dat wij in een of andere informatica-cursus ooit bewezen (als in wiskundig waterdicht) hebben dat een algoritme correct werkte. Voor een eenvoudig als-het-licht-aan-is-gaat-het-uit-en-omgekeerd algoritme was dat toch al een bladzijde bewijs. Ik zou dat niet graag doen voor een praktisch nuttig programma tenzij er wat nieuwe technieken of hulpmiddelen beschikbaar zijn.

Dit is in elk geval een stap in de goede richting, zelfs als het nog niet "wiskundig waterdicht" bewijst dat de software doet wat ie moet doen.

simpel is het inderdaad niet , maar op dit moment is het zo dat vrijwel elke driver het hele systeem kan hacken.

Met virtualisatie probeert men dit ingewikkelder te maken, maar is er ook geen sprake van formele bewijzen dat het systeem an sich klopt. Wel zien we hoe ontzettend veel meer RAM je dan ineens nodig hebt op het moment dat je virtualiseert.

Xen begint pas bij 4GB ram en heeft eigenlijk nog heel wat meer nodig.

An sich is dat wel op dit moment zo'n beetje enige wapen dat je goedkoop kunt installeren en een beetje werkt tegen de vele hacks die via je browser plaatsvinden.

Natuurlijk zit je altijd dan nog met de hardware hacks - waartegen geen enkele beveiliging werkt. Wie de hardware maakt kan je ALTIJD hacken.
Dan zit je echter op nivootje (chinese) NSA en die verzinnen toch wel een manier om je te hacken...

Parallel is alles nog een slag ingewikkelder omdat je dan ook moet bewijzen dat je niet gehacked kunt worden door de gebruikelijke race bugs.

Overigens in geval van linux zijn er voorbeelden van ontzettend knullige bugs. Bijvoorbeeld al versies lang werkt Debian van geen meter op veel machines omdat er een racebug in 1 van de eerste scripts zit waarmee je opstart

[Reactie gewijzigd door hardwareaddict op 16 april 2014 20:23]

Je verkondigd helaas heel wat onzin in dit comment:

Xen heeft geen 4gb nodig, en ook niet eigenlijk nog meer. De hypervisor heeft wat ram nodig voor zn boekhouding, en daarna heeft de vm wat ram nodig. Beide kunnen prima in een half gb.

Geheugenpages die de zelfde inhoudt hebben kunnen tussen vm's gedeeld worden waardoor je dus helemaal niet enorm veel meer geheugen nodig hebt.

Parallels is niets anders dan virtualisatie zoals xen en kvm dat ook doen. Wat je precies bedoeld met "racebug"'s waarmee je gehackt kan worden is me onduidelijk. Je doelt vast op race-conditions, maar die zijn nergens meer gevaarlijk dan andere bugs, en er is nergens een regel die zegt dat je voor parallels beter je best moet doen en moet kunnen bewijzen dat je code veilig is. Parallels mapt gewoon de hardware door naar de VM, net als elke andere VM waarna daarbinnen je gewoon windows/linux of iets anders kunt draaien ongeacht of parallels het daar mee eens is of niet.

Waar je op doelt met de "racebug" in debian ontgaat me volledig, een linkje naar een bugreport, of een forum thread of iets iig zou helpen. Versies lang in debian betekend namelijk letterlijk jaren, en er is ondertussen zo veel aan debian veranderd, inc alle opstart scripts dat het me ontzettend sterk lijkt dat er een bug in zit die op "veel machines" de boel voor "geen meter" laat werken.

@twop : Linus Thorvalds heeft glashelder aangegeven ook niet de kernel te willen herschrijven naar iets wat stuk veiliger in elkaar zit.

D'r zijn 2 overwegingen.

a) de kernel wordt trager
b) het is al zo lastig om goede device drivers te krijgen en als je via een device driver niet meer de hele computer totaal kunt plathacken, dan brengt bijna geen "bedrijf" meer device drivers uit, omdat d'r daar niks te halen valt voor ze dan.

referentie naar b) zou welkom zijn.

"Zo moet een individuele gebruiker geen informatie over privégegevens kunnen afleiden door naar de openbare gegevens te kijken." Kan iemand mij uitleggen wat hier nou precies het voordeel van is ten opzichte van wat de NSA heeft ontwikkeld en open source heeft vrijgegeven als Apache Accumulo

Klinkt leuk voor beveiliging, maar kan dus ook andersom gebruik worden. Ook zie ik zoets nog wel gebruikt worden voor drm.

snelle suikers man... bubbel en poof it's gone
met een holle kies tot gevolg
lol, ik weet dat je "zoiets" bedoelde maar vind "zoets" net zo doeltreffend xD

demand/solution bubbles

[Reactie gewijzigd door Anoniem: 500749 op 17 april 2014 12:31]