Setiap kali anda membeli sesuatu di Amazon, data pelanggan anda secara automatik dikemas kini dan disimpan di ribuan mesin maya di awan. Untuk perniagaan seperti Amazon, memastikan keselamatan dan keselamatan data berjuta-juta pelanggannya adalah mustahak. Ini berlaku untuk organisasi besar dan kecil. Tetapi sampai sekarang, belum ada cara untuk menjamin bahawa sistem perisian aman dari bug, penggodam, dan kerentanan.
Penyelidik Columbia Engineering mungkin telah menyelesaikan masalah keselamatan ini. Mereka telah mengembangkan SeKVM, sistem pertama yang menjamin - melalui bukti matematik - keselamatan mesin maya di awan. Dalam makalah baru yang akan dibentangkan pada 26 Mei 2021, di Simposium IEEE ke-42 mengenai Keselamatan & Privasi, para penyelidik berharap dapat meletakkan landasan untuk inovasi masa depan dalam pengesahan perisian sistem, yang mengarah pada generasi baru perisian sistem tahan siber.
SeKVM adalah sistem pertama yang disahkan secara formal untuk pengkomputeran awan. Pengesahan formal adalah langkah penting kerana proses membuktikan bahawa perisian itu betul secara matematik, kod program berfungsi sebagaimana mestinya, dan tidak ada bug keselamatan tersembunyi yang perlu dikhawatirkan.
"Ini adalah pertama kalinya sistem perisian multiprosesor dunia nyata terbukti betul dan selamat secara matematik," kata Jason Nieh, profesor sains komputer dan pengarah bersama Makmal Sistem Perisian. "Ini bermaksud bahawa data pengguna dikelola dengan betul oleh perisian yang berjalan di cloud dan selamat dari bug keselamatan dan penggodam."
Pembinaan perisian sistem yang betul dan selamat telah menjadi salah satu cabaran utama pengkomputeran. | Nieh telah mengusahakan pelbagai aspek sistem perisian sejak bergabung dengan Columbia Engineering pada tahun 1999. Ketika Ronghui Gu, Penolong Profesor Sains Komputer Keluarga Tang dan pakar dalam pengesahan formal, bergabung dengan jabatan sains komputer pada tahun 2018, dia dan Nieh memutuskan untuk bekerjasama untuk meneroka pengesahan formal sistem perisian.
Penyelidikan mereka telah mendapat minat utama: kedua-dua penyelidik memenangi Anugerah Penyelidikan Amazon, banyak geran dari National Science Foundation, serta kontrak Agensi Projek Penyelidikan Lanjutan Pertahanan (DARPA) berjuta-juta dolar untuk memajukan pengembangan projek SeKVM. Sebagai tambahan, Nieh dianugerahkan Guggenheim Fellowship untuk karya ini.
Selama belasan tahun yang lalu, ada banyak perhatian yang diberikan kepada pengesahan formal, termasuk pekerjaan untuk mengesahkan sistem operasi multiprosesor. "Tetapi semua penyelidikan itu dilakukan pada sistem seperti mainan kecil yang tidak ada yang digunakan dalam kehidupan nyata," kata Gu. "Mengesahkan sistem komoditi multiprosesor, sistem yang digunakan secara meluas seperti Linux, dianggap tidak mungkin."
Pertumbuhan eksponensial pengkomputeran awan telah membolehkan syarikat dan pengguna memindahkan data dan pengiraan mereka di luar laman web menjadi mesin maya yang berjalan di host di cloud. Penyedia pengkomputeran awan, seperti Amazon, menggunakan hypervisors untuk menyokong mesin maya ini
Seorang hypervisor adalah perisian utama yang memungkinkan pengkomputeran awan dilakukan. Keselamatan data mesin maya bergantung pada kebenaran dan kebolehpercayaan penyelia. Walaupun penting, hypervisors rumit — mereka boleh merangkumi keseluruhan sistem operasi Linux. Hanya satu pautan lemah dalam kod - yang hampir mustahil untuk dikesan melalui ujian tradisional - dapat menjadikan sistem rentan terhadap penggodam. Walaupun hypervisor ditulis 99% dengan betul, penggodam masih dapat menyelinap ke dalam penyediaan 1% tertentu dan mengendalikan sistem.
Karya Nieh dan Gu adalah yang pertama untuk mengesahkan sistem komoditi, khususnya hypervisor KVM yang banyak digunakan, yang digunakan untuk menjalankan mesin maya oleh penyedia awan seperti Amazon. Mereka membuktikan bahawa SeKVM, yang merupakan KVM dengan beberapa perubahan kecil, adalah selamat dan menjamin bahawa komputer maya terasing antara satu sama lain.
"Kami telah menunjukkan bahawa sistem kami dapat melindungi dan mengamankan data peribadi dan pengkomputeran yang dimuat naik ke awan dengan jaminan matematik," kata Xupeng Li, Gu's Ph.D. pelajar dan pengarang utama kertas kerja. "Ini belum pernah dilakukan sebelumnya."
SeKVM disahkan menggunakan MicroV, kerangka baru untuk mengesahkan sifat keselamatan sistem besar. Ini berdasarkan hipotesis bahawa perubahan kecil pada sistem dapat menjadikannya lebih mudah untuk disahkan, teknik baru yang disebut oleh penyelidik sebagai pengesahan MICR. Teknik pelapisan novel ini memperbaik sistem yang ada dan mengekstrak komponen yang menegakkan keamanan menjadi inti kecil yang disahkan dan menjamin keselamatan seluruh sistem.
Perubahan yang diperlukan untuk memperbaiki sistem yang besar cukup sederhana - para penyelidik menunjukkan bahawa jika inti kecil dari sistem yang lebih besar itu utuh, maka sistemnya aman dan tidak ada data pribadi yang akan dibocorkan. Ini adalah bagaimana mereka dapat mengesahkan sistem besar seperti KVM, yang sebelumnya dianggap mustahil.
"Fikirkan rumah - keretakan di drywall tidak bermaksud integriti rumah itu berisiko," jelas Nieh. "Ini masih kukuh dan sistem struktur utamanya bagus."
Shih-Wei Li, Ph.D. Nieh pelajar dan pengarang utama kajian ini, menambah, "SeKVM akan berfungsi sebagai perlindungan dalam pelbagai domain, dari sistem perbankan dan peranti Internet of Things hingga kenderaan autonomi dan cryptocurrency."
Sebagai penyelia komoditi pertama yang disahkan, SeKVM dapat mengubah bagaimana perkhidmatan awan harus dirancang, dikembangkan, digunakan, dan dipercayai. Di dunia di mana keselamatan siber semakin membimbangkan, ketahanan ini sangat diminati. Syarikat awan utama sudah meneroka bagaimana mereka dapat memanfaatkan SeKVM untuk memenuhi permintaan ini.