Alexander Dax (afb: Helmholtz/CISPA)

Onlangs werd in een bekend internetprotocol, HTTP, een kwetsbaarheid ontdekt, waardoor massa-aanvallen makkelijker zouden zijn geworden. Dat probleem is niet met een ‘pleistertje’ op te lossen zoals lekken in een programma of besturingssysteem. Onderzoekers pleiten voor een automatische controle van internetprotocollen (pdf-bestand) om dergelijke problemen in de toekomst voor te zijn.
Om het (steeds minder) wereldwijde web te laten functioneren zijn bepaalde ‘afspraken’ (protocollen) nodig. Die regelen het in principe wereldwijde webverkeer. Zo hebben we (dus) HTTP (het hypertext transfer protocol) of het minder bekende TLS-protocol dat zorgt dat dat verkeer veilig verloopt door, onder meer, versleuteling en er geen ongenode gasten kunnen ‘meekijken’.
“Vrijwel elk beveiligingsprotocol gebruikt zogeheten hashfuncties”, zegt Alexander Dax van het Helmholtzcentrum voor informatiebeveiliging CISPA. Daarmee maak je een soort digitale vingerafdruk. Daarmee kun je nagaan of er onderweg op internet met de informatie geknoeid is. “Deze functies nemen elke waarde aan, ongeacht de grootte en maken er een kleinere waarde van met een vaste grootte”, legt hij uit.
Daar kun je nog niet zoveel mee. De ​​functies moeten ook bepaalde eigenschappen hebben. “Dit betekent dat een bepaald gegeven, zoals een wachtwoord, altijd dezelfde waarde moet opleveren als het wordt berekend met dezelfde hashfunctie. Omgekeerd mag het niet mogelijk zijn om uit de hashwaarde conclusies te trekken over de (meegestuurde; as) inhoud.”
Een andere belangrijke eigenschap van hashfuncties is dat verschillende originele gegevens niet naar dezelfde hashwaarde mogen worden omgezet. “We praten over botsingen als dat gebeurt”, zegt Dax.

Daar staan theorie en praktijk elkaar in de weg. “Er zijn geen perfecte hashfuncties”, zegt de informaticus. “Het is altijd slechts een kwestie van tijd voordat er botsingen plaatsvinden. Bovendien is de stand van de techniek veranderd. Met oude hashfuncties is het nu met voldoende rekenkracht mogelijk om verschillende waarden uit te proberen totdat de oorspronkelijke waarde voor een hashwaarde gevonden is. Dat heet een brute-krachtaanval”, zegt Dax.

Automatisch

Zulke aanvallen op moderne hashfuncties zijn duur en daarom nog geen gemeengoed, maar de techniek ontwikkelt zich razendsnel en het web (en andere netwerken) moeten ook in de toekomst veilig en bedrijfszeker zijn. Dax en zijn medeonderzoekers zien daarbij een belangrijke taak weggelegd voor automatische analyses van protocollen. “Het is niet voldoende ervan uit te gaan dat protocollen veilig zijn. We moeten dat ook formeel bewijzen. Dat doen we met met nauwkeurige, wiskundige definities om te achterhalen hoe veilig dat protocol is.”

“Het vervelende is dat deze analysemethoden tot nu toe meestal werken met modeltoewijzingen van hashfuncties die perfect zijn in deze vorm, maar we weten dat dat in de praktijk vaak niet zo is.” Dat is de eerste stap in de richting van het verbeteren van instrumenten. Dat heeft nog een bijkomend voordeel, stelt Dax: “We hebben verschillende varianten van zwakke hashfuncties gemodelleerd en deze in de Tamarin Prover en in Proverif (veiligheidstesters; as) ingebouwd. We willen ook ontdekken hoe groot de invloed van verschillende kwetsbaarheden in de hashfuncties is op de algehele veiligheid van het protocol.”
Die formele veiligheidsbewijzen van protocollen zijn geen abberaties van beveiligingsidioten, maar harde noodzaak. “Veel grote bedrijven zoals Google hebben cryptografen in dienst om te controleren hoe veilig de protocollen zijn die zij gebruiken”, zegt de Helmholtzonderzoeker. “Dat is zeer tijdrovend om handmatig te doen en zelfs het controleren van geautomatiseerde beveiligingsanalyses vergt momenteel veel inspanning. We willen de analysemiddelen zo goed maken dat er in de toekomst aanzienlijk minder personeel en inspanning nodig zullen zijn en dat geautomatiseerde controle ook werkelijk protocolveiligheid kan waarborgen.”

Dax werkt CISPA in de groep van Cas Cremers en en houdt zich al jaren bezig met geautomatiseerd controleren van protocollen. Een paar jaar geleden ontwikkelden Cremers en collega’s Tamarin Prover, dat wordt gebruikt door bedrijven als Mozilla en Amazon. “Mijn onderzoek maakt deel uit van een groter project om geautomatiseerde beveiligingsanalyses te verbeteren”, zegt Dax.

Bron: idw-online.de