Stel je het internet en onze mobiele telefoons voor als een enorme, bruisende stad waar miljarden berichten elke seconde tussen gebouwen heen en weer zoeven. Om deze stad draaiende te houden, hebben deze berichten een universele taal nodig, zodat een telefoon in New York met een mast in Tokio kan communiceren zonder in de war te raken. Deze taal wordt ASN.1 genoemd, en het is als de grammatica en woordenschat die computers precies vertellen hoe ze informatie in piepkleine, efficiënte digitale doosjes moeten verpakken. Maar hier komt het lastige gedeelte bij: om ruimte te besparen en de snelheid te verhogen, zijn deze doosjes zo strak verpakt dat ze zelfs niet zijn uitgelijnd op nette rijen bytes (zoals standaard computerwoorden); in plaats daarvan zijn ze verpakt tot op het allerlaatste bit, het kleinste stofje aan data. Deze specifieke, superstrakke verpakkingmethode wordt UPER genoemd.

Het probleem is dat het schrijven van een vertaler (of "parser") om deze piepkleine, bit-gebaseerde doosjes uit te pakken ontzettend moeilijk is. Als de vertaler zelfs maar een kleine fout maakt — zoals het verkeerd lezen van een enkel bitje of het vergeten van een regel over hoe nieuwe, onbekende informatie moet worden afgehandeld — kan dit het hele systeem laten crashen, geheimen laten lekken of hackers de kans geven om binnen te sluipen. Jarenlang hebben ingenieurs geprobeerd deze fouten op te lossen door de vertalers te testen met miljoenen willekeurige berichten, in de hoop bugs te vangen. Maar dit is als proberen een naald in een hooiberg te vinden door simpelweg de hooiberg te schudden; je vindt misschien wat naalden, maar je kunt nooit zeker weten of je er alle hebt gevonden, of dat de exemplaren die je hebt gevonden wel de echte zijn.

Ontmoet VUPER, een nieuwe tool ontwikkeld door onderzoekers van Penn State die het spel verandert. In plaats van alleen de hooiberg te schudden, bouwt VUPER een mathematisch perfecte vertaler vanaf de basis. Denk aan het creëren van een "gouden standaard" woordenboek en grammaticaboek dat door een computerwiskundige is bewezen 100% correct te zijn. De onderzoekers gebruikten deze perfecte vertaler om 11 andere populaire parsers te testen die worden gebruikt in echte 5G-netwerken en voertuigcommunicatiesystemen. Ze ontdekten dat veel van deze breed gebruikte vertalers eigenlijk behoorlijk niet-conform waren, waarbij ze 20 verschillende soorten regels misten. In sommige gevallen maakte deze niet-conformiteit het mogelijk voor hackers om telefoons te laten crashen of netwerken te misleiden om ongeëncrypteerde berichten te verzenden. VUPER bewijst dat, hoewel we de vertalers die we nu hebben misschien niet altijd kunnen vertrouwen, we nu vertalers kunnen bouwen die wiskundig gegarandeerd veilig zijn, en ze kunnen gebruiken om de kapotte versies te repareren.

Het Verhaal van VUPER: Het Bouwen van de Perfecte Vertaler

In de wereld van computernetwerken is data als een lange stroom water die door pijpen stroomt. Om een bericht te verzenden, "serialiseert" een computer het bericht, waarbij de data wordt samengeperst in een compacte stroom van bits. Om het te ontvangen, "parst" een andere computer de stroom, waarbij de bits weer worden samengeperst tot een leesbaar bericht. In de risicovolle wereld van 5G-cellulaire netwerken en vehicle-to-everything (V2X) communicatie, gebruikt dit proces een specifieke set regels genaamd UPER (Unaligned Packed Encoding Rules). Het wordt "unaligned" genoemd omdat het niet geeft om nette byte-grenzen; het verpakt data zo compact mogelijk, bit voor bit, om bandbreedte te besparen.

De uitdaging is dat het officiële regelboek voor UPER geschreven is in dicht, beschrijvend tekst, niet in code. Dit laat ingenieurs over aan het gissen hoe de regels moeten worden geïmplementeerd, wat leidt tot subtiele fouten. De onderzoekers achter VUPER besloten te stoppen met gissen. Ze bouwden een framework dat de parser formeel bewijst te zijn. Ze hebben niet alleen code geschreven en gehoopt dat het werkt; ze gebruikten een krachtige wiskundige tool genaamd de Rocq prover om elke stap van de logica te verifiëren.

De "Round-Trip" Test

Om te begrijpen hoe VUPER werkt, stel je voor dat je een magische vertaler hebt die een boek in een geheime code verandert en weer terug. Een "round-trip" test betekent dat je een zin neemt, deze in code verandert, en de code vervolgens weer terugvertaalt naar een zin. Als je exact dezelfde zin terugkrijgt, werkt de vertaler.

Echter, UPER heeft een speciale twist: extensions (uitbreidingen). Naarmate de technologie evolueert (zoals de overgang van 4G naar 5G), worden er nieuwe functies aan de berichten toegevoegd. Een oude vertaler moet in staat zijn om een nieuw bericht te lezen, de nieuwe delen die hij niet begrijpt te negeren, en toch de oude delen begrijpelijk te houden. Dit wordt forward compatibility genoemd. VUPER handelt dit af door twee dingen te bewijzen:

1. Strict Round-Trip: Als het bericht uit dezelfde versie komt, moet de vertaler het terugveranderen in het exact zelfde bitpatroon. Geen extra bits, geen ontbrekende bits.
2. Weak Round-Trip: Als een bericht nieuwe, onbekende uitbreidingen bevat, kan de vertaler deze overslaan, maar moet hij nog steeds in staat zijn om de bekende delen terug te veranderen in een geldig bericht. Het hoeft niet bit-voor-bit overeen te komen met het origineel (omdat de onbekende delen weg zijn), maar het mag de rest niet corrumperen.

De Bugs Vinden

De onderzoekers bouwden een "trusted oracle"—een perfecte parser gegenereerd door VUPER—en gebruikten deze om 11 andere parsers te testen. Deze bevatten 7 open-source tools (zoals asn1c en pycrate) en 4 commerciële parsers die worden gebruikt in echte 4G en 5G basisstations (de hardware die jouw telefoon met het netwerk verbindt).

Ze stuurden niet alleen willekeurige troep; ze gebruikten een slimme "fuzzer" die de structuur van de berichten begreep om miljoenen lastige testgevallen te creëren. Toen ze de resultaten vergeleken, vonden ze 20 verschillende soorten inconsistenties in de andere parsers.

Hier zijn enkele van de meest interessante bevindingen:

• Het "Te Lang" Probleem: Sommige parsers accepteerden getallen die te groot waren voor de toegewezen ruimte, of lengtes die niet overeenkwamen met de data. Dit is alsoals een postbode die een brief accepteert die zegt "Ik heb 5 pagina's", maar eigenlijk 100 pagina's bevat, waardoor de brievenbus overloopt en crasht.
• De "Onbekende Uitbreiding" Verwarring: Wanneer een bericht nieuwe functies had die de oude parser niet kende, raakten sommige parsers in de war en begonnen ze het verkeerde deel van het bericht te lezen, denkend dat het iets heel anders was. Dit is als een vertaler die een nieuw woord in een vreemde taal ziet, in de war raakt, en vervolgens de rest van de zin onjuist vertaalt.
• De "Default Waarde" Fout: De regels zeggen dat als een waarde de "default" is, deze helemaal niet verzonden moet worden om ruimte te besparen. Maar sommige parsers verzonden deze nog steeds, of herkendenen niet wanneer deze ontbrak.

Het Gevaar in de Praktijk

Het paper vond niet alleen theoretische bugs; het toonde aan hoe deze geëxploiteerd konden worden. De onderzoekers demonstreerden vier concrete aanvallen:

1. Een Telefoon Crashen: Door een bericht te sturen met een lijst van netwerk-ID's die net iets te lang was (een schending van een beperking), veroorzaakten ze dat de software van een telefoon crashte, wat leidde tot een Denial of Service (DoS).
2. Een Mast Crashen: Een gecompromitteerde zendmast zou een foutief bericht naar een andere mast kunnen sturen, waardoor de tweede mast crasht tijdens het verwerken ervan.
3. Geheime Lekken: Als een parser een bericht verkeerd interpreteert door een onbekende uitbreiding, kan hij denken dat een beveiligingsinstelling "uit" staat, terwijl deze eigenlijk "aan" staat, of andersom. Dit kan leiden tot een situatie waarin een telefoon denkt dat hij veilig communiceert, terwijl het netwerk in werkelijkheid data in plat tekst stuurt, waardoor afluisteraars de gegevens kunnen lezen.
4. Device Fingerprinting: Omdat verschillende parsers anders omgaan met fouten, kan een hacker specifieke "truikberichten" sturen en kijken hoe een apparaat reageert. Als een apparaat een vreemd bericht accepteert, weet de hacker dat het een specifieke merk hardware gebruikt (zoals een Samsung baseband), waardoor hij dat specifieke apparaat met bekende exploits kan targeten.

Prestaties en de Toekomst

De onderzoekers geven toe dat hun perfecte, wiskundig geverifieerde parser niet de snelste is die er is. Hij is ongeveer 4 keer langzamer dan de hoog geoptimaliseerde C-libraries die momenteel in de industrie worden gebruikt. Echter, hij is 4 keer sneller dan Python-gebaseerde parsers.

Het doel van VUPER is niet om de snelle parsers onmiddellijk te vervangen, maar om te dienen als een referentie-implementatie. Net zoals een meesterkok een gerecht kan proeven en je precies kan vertellen wat er mis is met het recept, kan VUPER ingenieurs precies vertellen waar hun parsers falen. De onderzoekers hopen dat ze door VUPER te gebruiken om deze bugs te vinden en op te lossen, de industrie uiteindelijk parsers kan laten bouwen die zowel snel als wiskundig gegarandeerd veilig zijn.

Uiteindelijk laat VUPER zien dat in de complexe, hogesnelheidswereld van 5G en daarna, we niet langer kunnen vertrouwen op "goed genoeg" testen. We hebben wiskundig bewezen vertalers nodig om onze digitale stad veilig, beveiligd en soepel draaiende te houden.