Bijna elke keer dat u een veilige Google Chrome-browser opent, een nieuw door MIT ontwikkeld cryptografisch systeem helpt uw ​​gegevens beter te beschermen.

In een paper gepresenteerd op het recente IEEE Symposium on Security and Privacy, MIT-onderzoekers beschrijven een systeem dat, Voor de eerste keer, genereert automatisch geoptimaliseerde cryptografiecode die meestal met de hand wordt geschreven. Ingezet begin 2018, het systeem wordt nu veel gebruikt door Google en andere technologiebedrijven.

De paper laat nu voor andere onderzoekers in het veld zien hoe geautomatiseerde methoden kunnen worden geïmplementeerd om door mensen gemaakte fouten bij het genereren van cryptocode te voorkomen, en hoe belangrijke aanpassingen aan componenten van het systeem kunnen helpen om betere prestaties te bereiken.

Om online communicatie te beveiligen, cryptografische protocollen voeren complexe wiskundige algoritmen uit die complexe berekeningen uitvoeren op grote aantallen. Achter de schermen, echter, een kleine groep experts schrijft en herschrijft die algoritmen met de hand. Voor elk algoritme, ze moeten verschillende wiskundige technieken en chiparchitecturen afwegen om te optimaliseren voor prestaties. Wanneer de onderliggende wiskunde of architectuur verandert, ze beginnen in wezen opnieuw vanaf nul. Behalve arbeidsintensief, dit handmatige proces kan niet-optimale algoritmen produceren en introduceert vaak bugs die later worden ontdekt en opgelost.

Onderzoekers van het Computer Science and Artificial Intelligence Laboratory (CSAIL) ontwierpen in plaats daarvan "Fiat Cryptography, " een systeem dat automatisch geoptimaliseerde cryptografische algoritmen genereert en tegelijkertijd verifieert voor alle hardwareplatforms. de onderzoekers ontdekten dat hun systeem algoritmen kan genereren die overeenkomen met de prestaties van de beste handgeschreven code, maar veel sneller.

De automatisch gegenereerde code van de onderzoekers heeft de BoringSSL van Google ingevuld, een open-source cryptografische bibliotheek. Google Chrome, Android-apps, en andere programma's gebruiken BoringSSL om de verschillende sleutels en certificaten te genereren die worden gebruikt om gegevens te coderen en te decoderen. Volgens de onderzoekers is ongeveer 90 procent van de beveiligde Chrome-communicatie voert momenteel hun code uit.

"Cryptografie wordt geïmplementeerd door met grote getallen te rekenen. [Fiat Cryptography] maakt het eenvoudiger om de wiskundige algoritmen te implementeren ... omdat we de constructie van de code automatiseren en bewijzen leveren dat de code correct is, " zegt mede-auteur Adam Chlipala, een CSAIL-onderzoeker en universitair hoofddocent elektrotechniek en informatica en hoofd van de groep Programmeertalen en Verificatie. "Het is eigenlijk alsof je een proces neemt dat in het menselijk brein loopt en het goed genoeg begrijpt om code te schrijven die dat proces nabootst."

Jonathan Protzenko van Microsoft Research, een cryptografie-expert die niet bij dit onderzoek betrokken was, ziet het werk als een verschuiving in het denken van de industrie.

"Fiat-cryptografie dat wordt gebruikt in BoringSSL komt de hele [cryptografische] gemeenschap ten goede, "zegt hij. "[Het is] een teken dat de tijden veranderen en dat grote softwareprojecten zich realiseren dat onveilige cryptografie een risico is, [en laat zien] dat geverifieerde software volwassen genoeg is om de mainstream te betreden. Ik hoop dat steeds meer gevestigde softwareprojecten de overstap zullen maken naar geverifieerde cryptografie. Misschien in de komende jaren, geverifieerde software wordt niet alleen bruikbaar voor cryptografische algoritmen, maar ook voor andere toepassingsdomeinen."

Deelnemen aan Chlipala op het papier zijn:eerste auteur Andres Erbsen en co-auteurs Jade Philipoom en Jason Gross, die allemaal CSAIL-afgestudeerde studenten zijn; evenals Robert Sloan MEng '17.

De bits splitsen

Cryptografieprotocollen gebruiken wiskundige algoritmen om openbare en privésleutels te genereren, die in feite een lange reeks bits zijn. Algoritmen gebruiken deze sleutels om veilige communicatiekanalen tussen een browser en een server te bieden. Een van de meest populaire efficiënte en veilige families van cryptografische algoritmen wordt elliptische kromme cryptografie (ECC) genoemd. In principe, het genereert sleutels van verschillende groottes voor gebruikers door willekeurig numerieke punten te kiezen langs een genummerde gebogen lijn in een grafiek.

De meeste chips kunnen zulke grote aantallen niet op één plek opslaan, dus splitsen ze ze kort op in kleinere cijfers die worden opgeslagen in eenheden die registers worden genoemd. Maar het aantal registers en de hoeveelheid opslagruimte die ze bieden, verschilt van chip tot chip. "Je moet de stukjes over een heleboel verschillende plaatsen verdelen, maar het blijkt dat de manier waarop je de bits splitst verschillende gevolgen heeft voor de prestaties, ' zegt Chlipala.

traditioneel, experts die ECC-algoritmen schrijven, implementeren die bitsplitsingsbeslissingen handmatig in hun code. In hun werk, de MIT-onderzoekers maakten gebruik van die menselijke beslissingen om automatisch een bibliotheek met geoptimaliseerde ECC-algoritmen voor alle hardware te genereren.

Hun onderzoekers verkenden eerst bestaande implementaties van handgeschreven ECC-algoritmen, in de programmeer- en assembleertalen C, en bracht die technieken over naar hun codebibliotheek. Dit genereert een lijst met best presterende algoritmen voor elke architectuur. Vervolgens, het gebruikt een compiler - een programma dat programmeertalen omzet in code die computers begrijpen - waarvan is bewezen dat het correct is met een proofingtool, genaamd Coq. In principe, alle code die door die compiler wordt geproduceerd, wordt altijd wiskundig geverifieerd. Het simuleert vervolgens elk algoritme en selecteert het best presterende voor elke chiparchitectuur.

Volgende, de onderzoekers werken aan manieren om hun compiler nog sneller te laten werken bij het zoeken naar geoptimaliseerde algoritmen.

Geoptimaliseerd compileren

Er is nog een extra innovatie die ervoor zorgt dat het systeem snel de beste bitsplitsingsimplementaties selecteert. De onderzoekers rustten hun op Coq gebaseerde compiler uit met een optimalisatietechniek, genaamd "gedeeltelijke evaluatie, " die in feite bepaalde variabelen voorberekent om dingen tijdens de berekening te versnellen.

In het systeem van de onderzoekers het berekent vooraf alle bit-splitsingsmethoden. Wanneer ze worden gekoppeld aan een bepaalde chiparchitectuur, het verwijdert onmiddellijk alle algoritmen die gewoon niet werken voor die architectuur. Dit vermindert de tijd die nodig is om de bibliotheek te doorzoeken aanzienlijk. Nadat het systeem op het optimale algoritme is ingesteld, het voltooit het compileren van de code.

Van dat, de onderzoekers verzamelden vervolgens een bibliotheek met de beste manieren om ECC-algoritmen te splitsen voor verschillende chiparchitecturen. Het is nu geïmplementeerd in BoringSSL, dus gebruikers putten meestal uit de code van de onderzoekers. De bibliotheek kan op dezelfde manier automatisch worden bijgewerkt voor nieuwe architecturen en nieuwe soorten wiskunde.

"We hebben in wezen een bibliotheek geschreven die, voor eens en altijd, correct is voor elke manier waarop u getallen kunt splitsen, " zegt Chlipala. "Je kunt automatisch de ruimte verkennen van mogelijke representaties van de grote getallen, compileer elke representatie om de prestaties te meten, en neem degene die het snelst loopt voor een bepaald scenario."

Dit verhaal is opnieuw gepubliceerd met dank aan MIT News (web.mit.edu/newsoffice/), een populaire site met nieuws over MIT-onderzoek, innovatie en onderwijs.