Nästan varje gång du öppnar en säker webbläsare Google Chrome, ett nytt MIT-utvecklat kryptografiskt system hjälper till att bättre skydda dina data.

I en artikel som presenterades vid det senaste IEEE-symposiet om säkerhet och integritet, MIT-forskare beskriver ett system som, för första gången, genererar automatiskt optimerad kryptografisk kod som vanligtvis skrivs för hand. Utplacerade i början av 2018, systemet används nu flitigt av Google och andra teknikföretag.

Uppsatsen visar nu för andra forskare inom området hur automatiserade metoder kan implementeras för att förhindra mänskliga misstag vid generering av kryptokod, och hur viktiga justeringar av komponenter i systemet kan bidra till att uppnå högre prestanda.

För att säkra onlinekommunikation, kryptografiska protokoll kör komplexa matematiska algoritmer som gör en del komplex aritmetik på stora tal. Bakom kulisserna, dock, en liten grupp experter skriver och skriver om dessa algoritmer för hand. För varje algoritm, de måste väga olika matematiska tekniker och chiparkitekturer för att optimera prestanda. När den underliggande matematiken eller arkitekturen förändras, de börjar i princip om från början. Förutom att vara arbetskrävande, denna manuella process kan producera icke-optimala algoritmer och introducerar ofta buggar som senare fångas upp och fixas.

Forskare från Computer Science and Artificial Intelligence Laboratory (CSAIL) designade istället "Fiat Cryptography, " ett system som automatiskt genererar – och samtidigt verifierar – optimerade kryptografiska algoritmer för alla hårdvaruplattformar. I tester, forskarna fann att deras system kan generera algoritmer som matchar prestandan för den bästa handskrivna koden, men mycket snabbare.

Forskarnas automatiskt genererade kod har fyllt i Googles BoringSSL, ett kryptografiskt bibliotek med öppen källkod. Google Chrome, Android-appar, och andra program använder BoringSSL för att generera de olika nycklar och certifikat som används för att kryptera och dekryptera data. Enligt forskarna, cirka 90 procent av den säkra Chrome-kommunikationen kör för närvarande sin kod.

"Kryptografi implementeras genom att göra aritmetik på stora tal. [Fiat Cryptography] gör det enklare att implementera de matematiska algoritmerna ... eftersom vi automatiserar konstruktionen av koden och ger bevis på att koden är korrekt, " säger pappersmedförfattaren Adam Chlipala, en CSAIL-forskare och docent i elektroteknik och datavetenskap och chef för gruppen programmeringsspråk och verifiering. "Det är i grunden som att ta en process som körde i mänskliga hjärnor och förstå den tillräckligt bra för att skriva kod som efterliknar den processen."

Jonathan Protzenko på Microsoft Research, en kryptografiexpert som inte var involverad i denna forskning, ser arbetet som ett skifte i branschtänkandet.

"Fiat Cryptography som används i BoringSSL gynnar hela [kryptografiska] gemenskapen, " säger han. "[Det är] ett tecken på att tiderna förändras och att stora programvaruprojekt inser att osäker kryptografi är en skuld, [och visar] att verifierad programvara är tillräckligt mogen för att komma in i mainstream. Det är min förhoppning att fler och fler etablerade mjukvaruprojekt ska göra övergången till verifierad kryptografi. Kanske inom de närmaste åren, verifierad programvara kommer att bli användbar inte bara för kryptografiska algoritmer, men också för andra applikationsdomäner."

Med Chlipala på tidningen är:första författaren Andres Erbsen och medförfattarna Jade Philipoom och Jason Gross, som alla är CSAIL-studenter; samt Robert Sloan MEng '17.

Dela bitarna

Kryptografiprotokoll använder matematiska algoritmer för att generera offentliga och privata nycklar, som i princip är en lång rad bitar. Algoritmer använder dessa nycklar för att tillhandahålla säkra kommunikationskanaler mellan en webbläsare och en server. En av de mest populära effektiva och säkra familjerna av kryptografiska algoritmer kallas elliptical curve cryptography (ECC). I grund och botten, den genererar nycklar av olika storlekar för användare genom att välja numeriska punkter slumpmässigt längs en numrerad kurvad linje på en graf.

De flesta marker kan inte lagra så stora antal på ett ställe, så de delar upp dem kort i mindre siffror som lagras på enheter som kallas register. Men antalet register och mängden lagring de tillhandahåller varierar från ett chip till ett annat. "Du måste dela upp bitarna på en massa olika platser, men det visar sig att hur du delar upp bitarna har olika prestandakonsekvenser, " säger Chlipala.

Traditionellt, experter som skriver ECC-algoritmer implementerar manuellt dessa bitdelningsbeslut i sin kod. I sitt arbete, MIT-forskarna utnyttjade dessa mänskliga beslut för att automatiskt generera ett bibliotek med optimerade ECC-algoritmer för vilken hårdvara som helst.

Deras forskare utforskade först befintliga implementeringar av handskrivna ECC-algoritmer, i programmerings- och assemblerspråken C, och överförde dessa tekniker till deras kodbibliotek. Detta genererar en lista över bäst presterande algoritmer för varje arkitektur. Sedan, den använder en kompilator – ett program som konverterar programmeringsspråk till kod som datorer förstår – som har bevisats korrekt med ett korrekturverktyg, kallas Coq. I grund och botten, all kod som produceras av den kompilatorn kommer alltid att verifieras matematiskt. Den simulerar sedan varje algoritm och väljer den bäst presterande algoritmen för varje chiparkitektur.

Nästa, forskarna arbetar på sätt att få sin kompilator att köra ännu snabbare när de söker efter optimerade algoritmer.

Optimerad kompilering

Det finns ytterligare en innovation som säkerställer att systemet snabbt väljer de bästa bitdelningsimplementeringarna. Forskarna utrustade sin Coq-baserade kompilator med en optimeringsteknik, kallad "delutvärdering, " som i princip förberäknar vissa variabler för att påskynda saker och ting under beräkningen.

I forskarnas system, den förberäknar alla bitdelningsmetoder. När du matchar dem med en given chiparkitektur, den kasserar omedelbart alla algoritmer som bara inte fungerar för den arkitekturen. Detta minskar dramatiskt tiden det tar att söka i biblioteket. Efter att systemet nollställt den optimala algoritmen, den avslutar kodkompileringen.

Från det, forskarna samlade sedan ihop ett bibliotek med de bästa sätten att dela ECC-algoritmer för en mängd olika chiparkitekturer. Det är nu implementerat i BoringSSL, så användarna hämtar mestadels från forskarnas kod. Biblioteket kan automatiskt uppdateras på liknande sätt för nya arkitekturer och nya typer av matematik.

"Vi har i princip skrivit ett bibliotek som, en gång för alla, är korrekt för alla sätt du kan dela siffror på, " säger Chlipala. "Du kan automatiskt utforska utrymmet för möjliga representationer av de stora talen, kompilera varje representation för att mäta prestandan, och ta den som springer snabbast för ett givet scenario."

Den här historien återpubliceras med tillstånd av MIT News (web.mit.edu/newsoffice/), en populär webbplats som täcker nyheter om MIT-forskning, innovation och undervisning.