Setiap kali Anda membeli sesuatu di Amazon, data pelanggan Anda secara otomatis diperbarui dan disimpan di ribuan mesin virtual di cloud. Untuk bisnis seperti Amazon, memastikan keselamatan dan keamanan data jutaan pelanggannya sangatlah penting. Ini berlaku untuk organisasi besar dan kecil. Namun hingga saat ini, belum ada cara untuk menjamin bahwa suatu sistem perangkat lunak aman dari bug, peretas, dan kerentanan.
Peneliti Columbia Engineering mungkin telah memecahkan masalah keamanan ini. Mereka telah mengembangkan SeKVM, sistem pertama yang menjamin — melalui bukti matematis — keamanan mesin virtual di cloud. Dalam makalah baru yang akan dipresentasikan pada 26 Mei 2021, pada Simposium IEEE ke-42 tentang Keamanan & Privasi, para peneliti berharap dapat meletakkan dasar untuk inovasi masa depan dalam verifikasi perangkat lunak sistem, yang mengarah pada generasi baru perangkat lunak sistem yang tahan siber.
SeKVM adalah sistem terverifikasi resmi pertama untuk komputasi awan. Verifikasi formal adalah langkah penting karena merupakan proses untuk membuktikan bahwa perangkat lunak benar secara matematis, bahwa kode program berfungsi sebagaimana mestinya, dan tidak ada bug keamanan tersembunyi yang perlu dikhawatirkan.
“Ini adalah pertama kalinya sistem perangkat lunak multiprosesor dunia nyata terbukti secara matematis benar dan aman,” kata Jason Nieh, profesor ilmu komputer dan wakil direktur Laboratorium Sistem Perangkat Lunak. “Artinya, data pengguna dikelola dengan benar oleh perangkat lunak yang berjalan di cloud dan aman dari bug dan peretas keamanan.”
Pembangunan perangkat lunak sistem yang benar dan aman telah menjadi salah satu tantangan besar komputasi. | Nieh telah mengerjakan berbagai aspek sistem perangkat lunak sejak bergabung dengan Columbia Engineering pada 1999. Ketika Ronghui Gu, Asisten Profesor Ilmu Komputer Keluarga Tang dan pakar verifikasi formal, bergabung dengan departemen ilmu komputer pada 2018, dia dan Nieh memutuskan untuk berkolaborasi dalam mengeksplorasi verifikasi formal sistem perangkat lunak.
Penelitian mereka mendapatkan minat besar: kedua peneliti tersebut memenangkan Amazon Research Award, berbagai hibah dari National Science Foundation, serta kontrak Badan Proyek Penelitian Lanjutan Pertahanan (DARPA) bernilai jutaan dolar untuk mengembangkan proyek SeKVM lebih lanjut. Selain itu, Nieh dianugerahi Guggenheim Fellowship untuk pekerjaan ini.
Selama belasan tahun terakhir, terdapat banyak perhatian yang diberikan pada verifikasi formal, termasuk pekerjaan untuk memverifikasi sistem operasi multiprosesor. "Tapi semua penelitian itu telah dilakukan pada sistem seperti mainan kecil yang tidak digunakan siapa pun dalam kehidupan nyata," kata Gu. “Memverifikasi sistem komoditas multiprosesor, sistem yang digunakan secara luas seperti Linux, dianggap kurang lebih mustahil.”
Pertumbuhan komputasi awan yang eksponensial telah memungkinkan perusahaan dan pengguna untuk memindahkan data dan komputasi mereka ke luar situs ke mesin virtual yang berjalan pada host di awan. Penyedia komputasi awan, seperti Amazon, menerapkan hypervisor untuk mendukung mesin virtual ini
Hypervisor adalah bagian kunci dari perangkat lunak yang memungkinkan komputasi awan. Keamanan data mesin virtual bergantung pada kebenaran dan kepercayaan hypervisor. Meskipun penting, hypervisor itu rumit — hypervisor dapat menyertakan seluruh sistem operasi Linux. Hanya satu tautan lemah dalam kode — yang hampir tidak mungkin dideteksi melalui pengujian tradisional — dapat membuat sistem rentan terhadap peretas. Bahkan jika hypervisor ditulis 99% dengan benar, seorang hacker masih bisa menyelinap ke dalam set-up 1% tersebut dan mengambil kendali sistem.
Pekerjaan Nieh dan Gu adalah yang pertama memverifikasi sistem komoditas, khususnya hypervisor KVM yang banyak digunakan, yang digunakan untuk menjalankan mesin virtual oleh penyedia cloud seperti Amazon. Mereka membuktikan bahwa SeKVM, yang merupakan KVM dengan beberapa perubahan kecil, aman dan menjamin bahwa komputer virtual diisolasi satu sama lain.
"Kami telah menunjukkan bahwa sistem kami dapat melindungi dan mengamankan data pribadi dan komputasi yang diunggah ke cloud dengan jaminan matematis," kata Xupeng Li, Ph.D. mahasiswa dan penulis pendamping makalah. Ini belum pernah dilakukan sebelumnya.
SeKVM diverifikasi menggunakan MicroV, kerangka kerja baru untuk memverifikasi properti keamanan sistem besar. Hal ini didasarkan pada hipotesis bahwa perubahan kecil pada sistem dapat mempermudah verifikasi secara signifikan, sebuah teknik baru yang oleh para peneliti disebut verifikasi MICR. Teknik pelapisan baru ini memperbaiki sistem yang ada dan mengekstrak komponen yang menegakkan keamanan menjadi inti kecil yang diverifikasi dan menjamin keamanan seluruh sistem.
Perubahan yang diperlukan untuk retrofit sistem besar cukup sederhana — para peneliti menunjukkan bahwa jika inti kecil dari sistem yang lebih besar utuh, maka sistem tersebut aman dan tidak ada data pribadi yang akan bocor. Ini adalah bagaimana mereka dapat memverifikasi sistem besar seperti KVM, yang sebelumnya dianggap tidak mungkin.
"Pikirkan sebuah rumah — celah di drywall tidak berarti integritas rumah terancam," jelas Nieh. "Secara struktural masih bagus dan sistem struktur utamanya bagus."
Shih-Wei Li, Ph.D. Mahasiswa dan penulis bersama studi tersebut, menambahkan, "SeKVM akan berfungsi sebagai pengaman di berbagai domain, dari sistem perbankan dan perangkat Internet of Things hingga kendaraan otonom dan mata uang kripto."
Sebagai hypervisor komoditas terverifikasi pertama, SeKVM dapat mengubah bagaimana layanan cloud harus dirancang, dikembangkan, disebarkan, dan dipercaya. Di dunia dimana keamanan cyber adalah kekhawatiran yang berkembang, ketahanan ini sangat dibutuhkan. Perusahaan cloud besar sudah menjajaki bagaimana mereka dapat memanfaatkan SeKVM untuk memenuhi permintaan ini.