Telkens wanneer u iets op Amazon koopt, worden uw klantgegevens automatisch bijgewerkt en opgeslagen op duizenden virtuele machines in de cloud. Voor bedrijven als Amazon is het essentieel om de veiligheid en beveiliging van de gegevens van zijn miljoenen klanten te waarborgen. Dit geldt voor zowel grote als kleine organisaties. Maar tot nu toe was er geen manier om te garanderen dat een softwaresysteem beveiligd is tegen bugs, hackers en kwetsbaarheden.
Onderzoekers van Columbia Engineering hebben dit beveiligingsprobleem mogelijk opgelost. Ze hebben SeKVM ontwikkeld, het eerste systeem dat - door middel van wiskundig bewijs - de veiligheid van virtuele machines in de cloud garandeert. In een nieuw artikel dat op 26 mei 2021 wordt gepresenteerd, op het 42e IEEE-symposium over beveiliging en privacy, hopen de onderzoekers de basis te leggen voor toekomstige innovaties op het gebied van systeemsoftwareverificatie, wat leidt tot een nieuwe generatie cyberbestendige systeemsoftware.
SeKVM is het eerste officieel geverifieerde systeem voor cloud computing. Formele verificatie is een cruciale stap, omdat het het proces is om te bewijzen dat de software wiskundig correct is, dat de programmacode werkt zoals het hoort, en dat er geen verborgen beveiligingsbugs zijn om je zorgen over te maken.
"Dit is de eerste keer dat is aangetoond dat een real-world multiprocessor-softwaresysteem wiskundig correct en veilig is", zegt Jason Nieh, hoogleraar informatica en mededirecteur van het Software Systems Laboratory. "Dit betekent dat de gegevens van gebruikers correct worden beheerd door software die in de cloud wordt uitgevoerd en beschermd zijn tegen beveiligingsbugs en hackers."
De constructie van correcte en veilige systeemsoftware was een van de grootste uitdagingen van computers. | Nieh heeft aan verschillende aspecten van softwaresystemen gewerkt sinds hij in 1999 bij Columbia Engineering kwam. Toen Ronghui Gu, de Tang Family Assistant Professor of Computer Science en een expert in formele verificatie, in 2018 bij de afdeling informatica kwam, besloten hij en Nieh samen te werken. over het verkennen van formele verificatie van softwaresystemen.
Hun onderzoek heeft veel belangstelling gewekt: beide onderzoekers wonnen een Amazon Research Award, meerdere beurzen van de National Science Foundation, evenals een miljoenencontract van het Defense Advanced Research Projects Agency (DARPA) om de ontwikkeling van het SeKVM-project te bevorderen. Bovendien ontving Nieh voor dit werk een Guggenheim Fellowship.
In de afgelopen twaalf jaar is er veel aandacht besteed aan formele verificatie, inclusief werkzaamheden aan het verifiëren van multiprocessor-besturingssystemen. "Maar al dat onderzoek is uitgevoerd op kleine speelgoedachtige systemen die niemand in het echte leven gebruikt", zei Gu. "Het verifiëren van een commodity-systeem met meerdere processors, een systeem dat veel wordt gebruikt zoals Linux, werd min of meer onmogelijk geacht."
De exponentiële groei van cloud computing heeft bedrijven en gebruikers in staat gesteld hun gegevens en berekeningen off-site te verplaatsen naar virtuele machines die op hosts in de cloud draaien. Cloud computing-providers, zoals Amazon, zetten hypervisors in om deze virtuele machines te ondersteunen
Een hypervisor is het belangrijkste stuk software dat cloud computing mogelijk maakt. De beveiliging van de gegevens van de virtuele machine hangt af van de juistheid en betrouwbaarheid van de hypervisor. Ondanks hun belang zijn hypervisors gecompliceerd - ze kunnen een volledig Linux-besturingssysteem bevatten. Slechts een enkele zwakke schakel in de code - een die vrijwel onmogelijk te detecteren is via traditionele tests - kan een systeem kwetsbaar maken voor hackers. Zelfs als een hypervisor voor 99% correct is geschreven, kan een hacker nog steeds die specifieke 1% -configuratie binnensluipen en de controle over het systeem overnemen.
Het werk van Nieh en Gu is het eerste dat een commodity-systeem verifieert, met name de veelgebruikte KVM-hypervisor, die wordt gebruikt om virtuele machines te laten draaien door cloudproviders zoals Amazon. Ze bewezen dat SeKVM, wat KVM is met enkele kleine wijzigingen, veilig is en garandeert dat virtuele computers van elkaar zijn geïsoleerd.
"We hebben aangetoond dat ons systeem privégegevens en computers die naar de cloud zijn geüpload, met wiskundige garanties kan beschermen en beveiligen", aldus Xupeng Li, Gu's Ph.D. student en co-hoofdauteur van de paper. "Dit is nog nooit eerder gedaan."
SeKVM is geverifieerd met MicroV, een nieuw raamwerk voor het verifiëren van de beveiligingseigenschappen van grote systemen. Het is gebaseerd op de hypothese dat kleine wijzigingen in het systeem het aanzienlijk gemakkelijker kunnen maken om te verifiëren, een nieuwe techniek die de onderzoekers MICR-verificatie noemen. Deze nieuwe gelaagdheidstechniek past een bestaand systeem aan en extraheert de componenten die beveiliging afdwingen in een kleine kern die wordt geverifieerd en de beveiliging van het hele systeem garandeert.
De veranderingen die nodig zijn om een groot systeem achteraf aan te passen, zijn vrij bescheiden - de onderzoekers toonden aan dat als de kleine kern van het grotere systeem intact is, het systeem veilig is en er geen privégegevens zullen worden gelekt. Op deze manier konden ze een groot systeem zoals KVM verifiëren, wat voorheen als onmogelijk werd beschouwd.
'Denk aan een huis - een scheur in de gipsplaat betekent niet dat de integriteit van het huis in gevaar is,' legde Nieh uit. "Het is nog steeds structureel gezond en het belangrijkste structurele systeem is goed."
Shih-Wei Li, Nieh's Ph.D. student en co-hoofdauteur van de studie, voegde toe: "SeKVM zal dienen als een beveiliging in verschillende domeinen, van banksystemen en Internet of Things-apparaten tot autonome voertuigen en cryptocurrencies."
Als de eerste geverifieerde hypervisor voor grondstoffen, zou SeKVM de manier kunnen veranderen waarop cloudservices moeten worden ontworpen, ontwikkeld, geïmplementeerd en vertrouwd. In een wereld waar internetveiligheid is een groeiende zorg, er is veel vraag naar deze veerkracht. Grote cloudbedrijven onderzoeken al hoe ze SeKVM kunnen gebruiken om aan deze vraag te voldoen.