Automatiseret kryptokodegenerator hjælper med at sikre internettet

Næsten hver gang du åbner en sikker Google Chrome-browser, et nyt MIT-udviklet kryptografisk system hjælper med at beskytte dine data bedre.

I en artikel præsenteret på det nylige IEEE-symposium om sikkerhed og privatliv, MIT-forskere beskriver et system, der for første gang, genererer automatisk optimeret kryptografikode, der normalt er skrevet i hånden. Indsat i begyndelsen af ​​2018, systemet bliver nu meget brugt af Google og andre teknologivirksomheder.

Artiklen demonstrerer nu for andre forskere på området, hvordan automatiserede metoder kan implementeres for at forhindre menneskeskabte fejl ved generering af kryptokode, og hvordan vigtige justeringer af komponenter i systemet kan hjælpe med at opnå højere ydeevne.

For at sikre online kommunikation, kryptografiske protokoller kører komplekse matematiske algoritmer, der udfører nogle komplekse regnestykker på store tal. Bag scenen, imidlertid, en lille gruppe eksperter skriver og omskriver disse algoritmer i hånden. For hver algoritme, de skal veje forskellige matematiske teknikker og chiparkitekturer for at optimere til ydeevne. Når den underliggende matematik eller arkitektur ændres, de starter i bund og grund forfra. Udover at være arbejdskrævende, denne manuelle proces kan producere ikke-optimale algoritmer og introducerer ofte fejl, der senere fanges og rettes.

Forskere fra Computer Science and Artificial Intelligence Laboratory (CSAIL) designede i stedet "Fiat Cryptography, " et system, der automatisk genererer - og samtidig verificerer - optimerede kryptografiske algoritmer til alle hardwareplatforme. I test, forskerne fandt ud af, at deres system kan generere algoritmer, der matcher ydeevnen af ​​den bedste håndskrevne kode, men meget hurtigere.

Forskernes automatisk genererede kode har udfyldt Googles BoringSSL, et open source kryptografisk bibliotek. Google Chrome, Android apps, og andre programmer bruger BoringSSL til at generere de forskellige nøgler og certifikater, der bruges til at kryptere og dekryptere data. Ifølge forskerne, omkring 90 procent af sikker Chrome-kommunikation kører i øjeblikket deres kode.

"Kryptografi implementeres ved at lave aritmetik på store tal. [Fiat Cryptography] gør det mere ligetil at implementere de matematiske algoritmer ... fordi vi automatiserer konstruktionen af ​​koden og giver beviser for, at koden er korrekt, " siger medforfatter Adam Chlipala, en CSAIL-forsker og lektor i elektroteknik og datalogi og leder af programmeringssprog og verifikationsgruppen. "Det er dybest set som at tage en proces, der kørte i menneskets hjerner og forstå den godt nok til at skrive kode, der efterligner den proces."

Jonathan Protzenko fra Microsoft Research, en kryptografiekspert, der ikke var involveret i denne forskning, ser arbejdet som et skift i branchetænkningen.

"Fiat Cryptography bliver brugt i BoringSSL til gavn for hele [kryptografiske] fællesskabet, " siger han. "[Det er] et tegn på, at tiderne ændrer sig, og at store softwareprojekter indser, at usikker kryptografi er en forpligtelse, [og viser] at verificeret software er moden nok til at komme ind i mainstream. Det er mit håb, at flere og flere etablerede softwareprojekter vil skifte til verificeret kryptografi. Måske inden for de næste par år, verificeret software vil blive anvendelig ikke kun til kryptografiske algoritmer, men også for andre applikationsdomæner."

Med Chlipala på papiret er:førsteforfatter Andres Erbsen og medforfattere Jade Philipoom og Jason Gross, som alle er CSAIL-kandidatstuderende; samt Robert Sloan MEng '17.

Opdeling af stumperne

Kryptografiprotokoller bruger matematiske algoritmer til at generere offentlige og private nøgler, som dybest set er en lang række af bits. Algoritmer bruger disse nøgler til at give sikre kommunikationskanaler mellem en browser og en server. En af de mest populære effektive og sikre familier af kryptografiske algoritmer kaldes elliptical curve cryptography (ECC). I bund og grund, den genererer nøgler af forskellige størrelser til brugere ved at vælge numeriske punkter tilfældigt langs en nummereret buet linje på en graf.

De fleste jetoner kan ikke gemme så store antal ét sted, så de opdeler dem kortvarigt i mindre cifre, der er gemt på enheder kaldet registre. Men antallet af registre og mængden af ​​lagerplads, de giver, varierer fra chip til chip. "Du er nødt til at dele stykkerne på en masse forskellige steder, men det viser sig, at den måde, du deler bitsene på, har forskellige præstationskonsekvenser, " siger Chlipala.

Traditionelt, eksperter, der skriver ECC-algoritmer, implementerer manuelt disse bitopdelingsbeslutninger i deres kode. I deres arbejde, MIT-forskerne udnyttede disse menneskelige beslutninger til automatisk at generere et bibliotek af optimerede ECC-algoritmer til enhver hardware.

Deres forskere udforskede først eksisterende implementeringer af håndskrevne ECC-algoritmer, i C-programmerings- og assemblersprogene, og overførte disse teknikker til deres kodebibliotek. Dette genererer en liste over bedst ydende algoritmer for hver arkitektur. Derefter, den bruger en compiler - et program, der konverterer programmeringssprog til kode, computere forstår - som er blevet bevist korrekt med et korrekturværktøj, kaldet Coq. I bund og grund, al kode produceret af den compiler vil altid være matematisk verificeret. Den simulerer derefter hver algoritme og vælger den bedst ydende for hver chiparkitektur.

Næste, forskerne arbejder på måder at få deres compiler til at køre endnu hurtigere i søgningen efter optimerede algoritmer.

Optimeret kompilering

Der er en yderligere innovation, der sikrer, at systemet hurtigt udvælger de bedste bit-splittende implementeringer. Forskerne udstyrede deres Coq-baserede compiler med en optimeringsteknik, kaldet "delevaluering, " som grundlæggende forudberegner visse variabler for at fremskynde tingene under beregningen.

I forskernes system den forudberegner alle bit-opdelingsmetoderne. Når du matcher dem til en given chiparkitektur, det kasserer med det samme alle algoritmer, der bare ikke vil fungere for den arkitektur. Dette reducerer dramatisk den tid, det tager at søge i biblioteket. Efter at systemet har nulstillet den optimale algoritme, det afslutter kodekompileringen.

Fra det, forskerne samlede derefter et bibliotek med de bedste måder at opdele ECC-algoritmer for en række forskellige chiparkitekturer. Det er nu implementeret i BoringSSL, så brugerne trækker for det meste fra forskernes kode. Biblioteket kan automatisk opdateres tilsvarende for nye arkitekturer og nye typer matematik.

"Vi har i det væsentlige skrevet et bibliotek, der én gang for alle, er korrekt for alle måder, du kan opdele tal på, " siger Chlipala. "Du kan automatisk udforske rummet af mulige repræsentationer af de store tal, kompiler hver repræsentation for at måle ydeevnen, og tag den, der løber hurtigst for et givet scenarie."

Denne historie er genudgivet med tilladelse fra MIT News (web.mit.edu/newsoffice/), et populært websted, der dækker nyheder om MIT-forskning, innovation og undervisning.