Sebuah artikel ilmiah diterbitkan dalam Communications of the ACM , Oktober 2018, Volume 61, Number 10, hal. 68−77, doi: 10.1145 / 3230627

Pada bulan Februari 2017, sebuah helikopter lepas landas dari lapangan terbang Boeing di Arizona dengan misi biasa: terbang di sekitar bukit terdekat. Dia terbang sepenuhnya secara mandiri. Menurut persyaratan keselamatan dari Administrasi Penerbangan Federal AS, pilot tidak menyentuh kontrol. Ini bukan penerbangan otonom pertama AH-6, yang disebut perusahaan sebagai Burung Kecil Tak Berawak (ULB). Dia telah terbang seperti ini selama bertahun-tahun. Namun, kali ini di tengah penerbangan helikopter mengalami serangan cyber. Komputer on-board menyerang perangkat lunak berbahaya camcorder, serta virus yang dikirimkan melalui flash drive yang terinfeksi, yang dimasukkan selama pemeliharaan. Serangan itu mengancam beberapa subsistem, tetapi tidak dapat mempengaruhi operasi yang aman dari pesawat.

Ide-ide kunci

• Bukti formal dari arsitektur perangkat lunak dari sebuah kernel mikro yang terverifikasi dapat diskalakan dengan biaya murah ke sistem yang sebenarnya.
• Berbagai tingkat keamanan dan keandalan dalam sistem yang sama dimungkinkan dan diinginkan. Tidak perlu memastikan keandalan maksimum seluruh kode.
• Redesign dan refactoring moderat sudah cukup untuk meningkatkan sistem yang ada ke tingkat kode yang sangat andal.

Anda mungkin berpikir bahwa penerbangan militer dapat dengan mudah mengusir serangan dunia maya semacam itu. Pada kenyataannya, tim pentester profesional yang ditugaskan oleh agen DARPA, sebagai bagian dari program Cyber ​​Military Systems (HACMS) Jaminan Tinggi untuk mengembangkan sistem komputer militer yang sangat andal, berhasil meretas versi pertama perangkat lunak ULB pada tahun 2013, yang pada awalnya dikembangkan untuk memastikan keamanan penerbangan daripada perlindungan. dari serangan siber. Peretas mendapat kesempatan untuk menabrak helikopter atau mendaratkannya di mana saja sesuai keinginan. Oleh karena itu, risiko serangan seperti itu dengan penumpang di atas kapal hampir tidak dapat ditaksir terlalu tinggi, dan upaya peretasan yang gagal pada Februari 2017 menunjukkan beberapa perubahan mendasar pada perangkat lunak.

Artikel ini menjelaskan perubahan ini dan teknologi yang memungkinkannya. Ini adalah teknologi yang dikembangkan sebagai bagian dari program HACMS yang bertujuan untuk memastikan operasi yang aman dari sistem kritis dalam lingkungan cyber yang bermusuhan - dalam hal ini, beberapa kendaraan otonom. Teknologi ini didasarkan pada verifikasi perangkat lunak formal - ini adalah program dengan bukti matematis terverifikasi otomatis yang bekerja sesuai dengan spesifikasinya. Meskipun artikel itu tidak dikhususkan untuk metode formal itu sendiri, artikel ini menjelaskan cara menggunakan verifikasi artefak untuk melindungi sistem nyata dalam praktiknya.

Mungkin hasil yang paling mengesankan dari HACMS adalah bahwa teknologi dapat diperluas ke sistem nyata yang ada, sangat meningkatkan perlindungan mereka terhadap serangan cyber. Proses ini disebut "retrofit keamanan seismik", mirip dengan peningkatan bangunan seismik. Selain itu, sebagian besar rekayasa ulang dilakukan oleh insinyur Boeing, daripada spesialis verifikasi formal.


"Bird" selama penerbangan uji coba tanpa awak

Tidak semua perangkat lunak helikopter dibangun berdasarkan model matematika dan bukti. Bidang verifikasi formal belum siap untuk skala seperti itu. Namun, program HACMS telah menunjukkan bahwa aplikasi strategis metode formal ke bagian terpenting dari keseluruhan sistem sangat meningkatkan perlindungan. Pendekatan HACMS bekerja untuk sistem di mana fitur keamanan yang diinginkan dapat dicapai dengan murni penegakan pada tingkat arsitektur. Ini didasarkan pada microkernel terverifikasi sel4 kami, yang akan kami bicarakan di bawah ini. Ini menjamin isolasi antara subsistem, dengan pengecualian saluran komunikasi yang jelas yang tunduk pada kebijakan keamanan sistem. Isolasi ini dijamin pada tingkat arsitektur dengan kerangka kerja CAmkES terverifikasi untuk komponen sistem. Menggunakan bahasa khusus domain dari Galois Inc. CAmkES terintegrasi dengan alat analisis arsitektur dari Rockwell Collins dan University of Minnesota, serta komponen perangkat lunak yang sangat andal.

Prestasi HACMS didasarkan pada teman setia lama dari seorang insinyur perangkat lunak - modularisasi. Inovasi adalah bahwa metode formal membuktikan kemampuan mengamati antarmuka dan enkapsulasi internal modul. Kepatuhan terhadap modularitas yang dijamin ini memungkinkan para insinyur yang tidak ahli dalam metode formal (seperti pada Boeing) untuk membuat baru atau bahkan meningkatkan sistem yang ada dan mencapai stabilitas tinggi. Meskipun alat belum memberikan bukti lengkap tentang keamanan sistem.

Verifikasi formal

Bukti kebenaran matematis dari program berawal pada setidaknya tahun 1960-an , tetapi untuk waktu yang lama manfaat nyata mereka untuk pengembangan perangkat lunak terbatas dalam cakupan dan kedalamannya. Namun, dalam beberapa tahun terakhir telah ada sejumlah terobosan mengesankan dalam verifikasi formal di tingkat kode sistem nyata, dari kompiler C CompCert yang terverifikasi hingga mikrokernel seL4 terverifikasi (lihat artikel ilmiah tentang itu), sistem konferensi terverifikasi CoCon , kompiler CakeML ML terverifikasi, program terverifikasi, program terverifikasi untuk membuktikan teorema Milawa dan Candle , sistem file gagal FSCQ yang diverifikasi, sistem distribusi IronFleet yang terverifikasi, dan kerangka kerja kernel paralel CertiKOS yang terverifikasi, serta hal-hal penting teorema matematika, termasuk masalah empat warna , bukti otomatis hipotesis Kepler dan teorema Iman - Thompson pada urutan aneh . Semua ini adalah sistem nyata. Sebagai contoh, CompCert adalah produk komersial, mikrokernel seL4 digunakan dalam aerospace dan pesawat tak berawak, sebagai platform Internet, dan sistem CoCon telah digunakan di berbagai konferensi ilmiah besar.

Proyek verifikasi ini membutuhkan upaya yang cukup besar. Untuk membuat metode formal tersedia untuk umum, upaya ini perlu dikurangi. Di sini kami menunjukkan bagaimana kombinasi strategis dari metode formal dan informal, otomatisasi parsial dari metode formal dan pengembangan perangkat lunak yang cermat untuk memaksimalkan manfaat komponen terisolasi telah memungkinkan kami untuk secara signifikan meningkatkan keandalan sistem yang ukuran keseluruhan dan kompleksitasnya adalah urutan besarnya lebih besar daripada yang disebutkan di atas.

Harap perhatikan bahwa kami menerapkan verifikasi formal terutama untuk kode yang menjadi sandaran keamanan sistem. Namun ada manfaat lain. Sebagai contoh, bukti bahwa kode itu benar membuat asumsi tentang konteks di mana ia dieksekusi (misalnya, perilaku perangkat keras dan konfigurasi perangkat lunak). Verifikasi formal membuat asumsi ini eksplisit, yang membantu pengembang fokus pada alat verifikasi lain, seperti pengujian. Selain itu, dalam banyak kasus, sistem menyertakan kode yang diverifikasi dan tidak diverifikasi. Selama ulasan kode, pengujian, dan debugging, verifikasi formal bertindak seperti lensa, dengan fokus pada kode sistem kritis dan tidak diverifikasi.

seL4

Mari kita mulai dengan fondasi untuk membangun sistem yang terbukti andal - kernel sistem operasi (OS). Ini adalah bagian terpenting yang menjamin keandalan seluruh sistem dengan biaya yang efektif.

Mikrokernel seL4 menyediakan serangkaian mekanisme minimum yang diverifikasi secara formal untuk menerapkan sistem yang aman. Tidak seperti kernel standar , ini sengaja universal dan karenanya cocok untuk menerapkan sejumlah kebijakan keamanan dan persyaratan sistem.

Salah satu tujuan utama pengembangan seL4 adalah untuk menyediakan isolasi yang kuat antara komponen yang saling tidak percaya yang berjalan di atas kernel. Ini mendukung pekerjaannya sebagai hypervisor, misalnya, untuk seluruh sistem operasi Linux, sambil menjaga mereka terisolasi dari komponen penting keamanan yang dapat bekerja bersama, seperti yang ditunjukkan pada Gambar 1. Secara khusus, fungsi ini memungkinkan pengembang sistem untuk menggunakan komponen warisan dengan menyembunyikan kerentanan di sebelah komponen yang sangat andal.


Fig. 1. Isolasi dan komunikasi terkontrol di seL4

Inti seL4 menempati posisi khusus di antara mikronuklei tujuan umum. Tidak hanya memberikan kinerja yang lebih baik di kelasnya , 10.000 baris kode C-nya telah menjalani verifikasi formal yang lebih ketat daripada perangkat lunak lain yang tersedia secara publik dalam sejarah manusia dalam hal tidak hanya jalur bukti, tetapi juga kekuatan properti yang terbukti. Ini didasarkan pada bukti "kebenaran fungsional" dari implementasi inti dalam C. Ini memastikan bahwa setiap perilaku kernel diprediksi oleh spesifikasi abstrak formalnya: lihat aplikasi online untuk ide bagaimana bukti ini terlihat. Mengikuti jaminan ini, kami telah menambahkan bukti tambahan yang akan kami jelaskan setelah pengenalan mekanisme dasar nukleus.

API seL4

Kernel seL4 menyediakan sekumpulan mekanisme minimal untuk mengimplementasikan sistem yang aman: stream, manajemen kemampuan, ruang alamat virtual, komunikasi antarproses (IPC), pensinyalan dan pengiriman interupsi.

Kernel mempertahankan statusnya dalam "objek kernel". Misalnya, untuk setiap utas dalam sistem, ada "aliran objek" yang menyimpan informasi tentang penyembunyian, pelaksanaan, dan kontrol akses. Program ruang-pengguna dapat merujuk ke objek kernel hanya secara tidak langsung melalui apa yang disebut "kemampuan" atau "kemampuan", yang menggabungkan tautan ke objek dengan serangkaian hak akses ke objek tersebut. Misalnya, utas tidak dapat memulai atau menghentikan utas lain jika tidak memiliki "kemampuan" untuk objek utas yang terkait.

Utas berinteraksi dan menyinkronkan dengan mengirim pesan melalui "titik akhir" komunikasi antarproses. Satu utas dengan kemampuan untuk mengirim ke titik akhir yang sesuai dapat mengirim pesan ke utas lain yang memiliki kemampuan untuk menerima ke titik akhir ini. Objek notifikasi menyediakan sinkronisasi antar set semaphore biner. Terjemahan alamat virtual dikendalikan oleh objek kernel yang mewakili direktori halaman, tabel halaman, dan objek frame atau abstraksi halus atas objek arsitektur prosesor yang sesuai. Setiap aliran memiliki kemampuan "VSpace" tertentu, yang menunjuk ke akar pohon objek terjemahan alamat aliran. Kemampuan itu sendiri dikelola oleh kernel dan disimpan dalam objek kernel "CNodes" yang terletak di struktur grafik, yang memetakan tautan ke objek dengan hak akses, mirip dengan membandingkan tabel halaman virtual dengan alamat fisik dalam memori. Setiap utas memiliki kemampuannya sendiri untuk mengidentifikasi root CNode. Seperangkat kemampuan yang tersedia dari root ini, kami sebut "CSpace Stream." Kemampuan dapat ditransfer melalui titik akhir dengan transfer pekerjaan, dan mereka juga dapat dinyatakan dibagikan menggunakan CSpace umum. Gambar 2 menunjukkan objek kernel ini.


Fig. 2. Objek kernel dalam sistem seL4 dengan dua utas berinteraksi melalui titik akhir

Bukti keamanan

Karena sifatnya yang fleksibel, API kernel seL4 adalah level rendah dan mendukung arsitektur sistem yang sangat dinamis. Oleh karena itu, bukti langsung untuk API ini sulit diperoleh.

Konsep kebijakan kontrol akses tingkat tinggi mengabstraksi dari objek individual dan kapabilitas kernel, sebagai gantinya menangkap konfigurasi kontrol akses sistem menggunakan seperangkat "subjek" (komponen) abstrak dan kekuatan yang dimiliki masing-masing atas yang lain (misalnya, untuk membaca data dan mengirim pesan) . Dalam contoh dalam gambar. 2, komponen A dan B memperoleh otoritas atas titik akhir.

Sewell dan rekannya telah membuktikan bahwa kebijakan kontrol akses seL4 memastikan bahwa dua fitur keamanan dasar dihormati: pembatasan hak istimewa dan integritas.

Pembatasan wewenang berarti bahwa kebijakan kontrol akses adalah perkiraan statis (tidak berubah) aman untuk kemampuan khusus dan objek kernel dalam sistem untuk keadaan di masa depan. Properti ini menyiratkan bahwa tidak peduli bagaimana sistem berevolusi, tidak ada komponen yang akan menerima otoritas lebih dari yang diprediksi kebijakan kontrol akses. Pada Gambar 2, kebijakan untuk komponen B tidak memiliki akses tulis ke komponen A. Dengan demikian, komponen B tidak akan pernah bisa mendapatkan akses ini di masa depan. Properti ini menyiratkan bahwa penalaran pada tingkat kebijakan adalah perkiraan yang aman untuk penalaran tentang keadaan spesifik dari kontrol akses dalam sistem.

Integritas berarti bahwa apa pun komponennya, ia tidak akan pernah dapat mengubah data dalam sistem (termasuk panggilan sistem apa pun yang dapat dibuatnya) yang jelas tidak diizinkan mengubah kebijakan kontrol akses. Sebagai contoh, dalam gbr. 2, satu-satunya komponen otoritas A atas komponen lain adalah hak untuk mengirim data ke titik akhir dari mana komponen B. menerima informasi. Ini berarti komponen A hanya dapat mengubah statusnya, status utas B, dan status buffer pesan. Itu tidak dapat mengubah bagian lain dari sistem.

Efek samping dari integritas adalah kerahasiaan, ketika komponen tidak dapat membaca informasi dari komponen lain tanpa izin : itu adalah properti yang kuat terbukti seL4 non-transitif non-interferensi. Yaitu, dalam sistem yang dikonfigurasikan dengan benar (dengan batasan yang lebih ketat daripada hanya untuk integritas), tidak ada komponen yang dapat, tanpa izin, mencari tahu informasi tentang komponen lain atau pelaksanaannya. Bukti menyatakan properti ini dalam hal kebijakan arus informasi, yang dapat diekstraksi dari kebijakan kontrol akses yang digunakan dalam bukti integritas. Informasi hanya akan dikirim ketika secara eksplisit diizinkan oleh kebijakan. Buktinya mencakup arus informasi eksplisit serta saluran penyimpanan potensial yang tersembunyi di dalam kernel. Tetapi saluran sinkronisasi berada di luar wilayahnya dan harus diproses dengan cara lain .

Bukti lebih lanjut dalam seL4 mencakup perluasan kebenaran fungsional dan, oleh karena itu, teorema keamanan ke tingkat biner untuk arsitektur ARMv7 dan profil runtime kasus terburuk untuk kernel ( 1 , 2 ), yang diperlukan untuk sistem waktu nyata. Inti seL4 tersedia untuk berbagai arsitektur: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 dan Intel x64. Saat ini, telah lulus pengujian mesin pada arsitektur ARMv7 untuk seluruh tumpukan verifikasi, serta pada ARMv7a dengan ekstensi hypervisor untuk kebenaran fungsional.

Keamanan Arsitektur

Bagian sebelumnya menjelaskan metode pemrograman dengan mana seL4 kernel menciptakan fondasi yang kokoh untuk sistem yang terbukti andal. Kernel membentuk basis komputasi yang andal (TCB) - komponen penting dari perangkat lunak yang harus bekerja dengan benar untuk keamanan sistem yang terjamin. Dalam sistem nyata, basis ini jauh lebih luas dari sekadar mikrokernel. Penting untuk memverifikasi tumpukan perangkat lunak tambahan untuk mendapatkan tingkat kepercayaan yang sama seperti untuk kernel. Namun, ada kelas-kelas sistem yang tidak perlu untuk verifikasi seperti itu: mereka memerlukan teorema isolasi pada level kernel untuk mendapatkan properti keamanan tertentu pada level sistem. Bagian ini memberikan contoh sistem semacam itu.

Ini adalah sistem di mana arsitektur komponen telah menerapkan properti kritis, mungkin bersama dengan beberapa komponen kecil yang tepercaya. Contoh kami adalah perangkat lunak kontrol penerbangan quadcopter, perangkat demo dalam program HACMS yang disebutkan sebelumnya.

Gambar 3 menunjukkan komponen perangkat keras utama quadrocopter. Arsitektur sengaja lebih kompleks daripada yang dibutuhkan oleh quadcopter, karena itu seharusnya mewakili ULB dan pada tingkat abstraksi ini mirip dengan arsitektur ULB.


Fig. 3. Arsitektur pesawat terbang otonom

Gambar tersebut menunjukkan dua komputer utama: komputer di kapal yang berinteraksi dengan stasiun bumi dan mengendalikan perangkat lunak di kapal (misalnya, kamera), dan komputer navigasi untuk mengendalikan penerbangan kendaraan, membaca data sensor, dan mengendalikan mesin. Komputer terhubung melalui jaringan internal atau CAN bus pada quadrocopter, Ethernet pada ULB. Quadrocopter juga memiliki titik WiFi yang tidak terlindungi, yang memungkinkan untuk menunjukkan metode perlindungan tambahan.

Dalam contoh ini, pertimbangkan komputer terpasang. Empat sifat dasar harus dipenuhi untuk itu:

• otentikasi perintah yang tepat dari stasiun bumi;
  
• ;
  
• ;
  
• .

, , , , . , , .

4 , , . (VM) Linux , WiFi. , CAN, Linux . — () CAN- . , ( ) .


.4.

, . , , . Linux . 4 . CAN , — . WiFi, Linux, .

, . MILS , — , . .

seL4 , : - , . «», , . , , .

, . Camkes seL4 , , . 5. , seL4 , , (RPC), .


. 5. CAmkES

CAmkES seL4. ( ) , CSpace VSpace. RPC , CAmkES IPC. , — , — . , seL4.

CAmkES capDL . seL4, seL4 .

, . , . , .

, . CAmkES .

«» CAmkES Isabelle/HOL, , «» , capDL CAmkES . , seL4 . .

, -. , , . CAmkES API , API . . RPC . 6 $$$f$$$$g$. , $$$f$$$$g$. , $$$f$RPC $$$g$.


. 6. C RPC

() , , $$$g$, , $$$g$dan $$$f$. , . , , , .

CAmkES RPC ( 1 , 2 ). ( ) , RPC, , .

CAmkES . , — capDL CAmkES — , CAmkES capDL. , capDL. . , CAmkES. , capDL, , , , CAmkES . , , CAmkES , capDL, , , , , .

, CAmkES , . seL4 ( ) , «» capDL, . , , . , . , , (EAL7) .

, . seL4 , « », . , , . ULB, .

, . 3. : , ( ). Linux. «» , , HACMS.

1.

(. . 7). . seL4 CAmkES, (VMM) , Linux. , VMM . seL4 , VMM, VMM . VMM , .


. 7.

, , . MMU IOMMU . , . 1 2.

2.

Langkah kedua modernisasi seismik memperkuat tembok yang ada. Dalam perangkat lunak, pengembang dapat meningkatkan keamanan dan keandalan dengan membagi sistem sumber menjadi beberapa subsistem, yang masing-masing terdiri dari mesin virtual yang hanya menjalankan bagian dari kode sistem sumber. Setiap kombinasi VM / VMM dilakukan dalam komponen CAmkES yang terpisah, yang memperkenalkan isolasi antara berbagai subsistem, tidak memungkinkan mereka untuk saling memengaruhi, dan kemudian memungkinkan koeksistensi berbagai tingkat keamanan.

Secara umum, bagian mengikuti arsitektur perangkat lunak yang ada, meskipun jika arsitektur tidak cukup untuk isolasi yang efektif, desain ulang mungkin diperlukan.

Sebagai aturan, bagian harus saling berinteraksi, jadi pada titik ini kami juga akan menambahkan saluran komunikasi. Untuk memastikan keamanan, sangat penting bahwa antarmuka ini sempit, membatasi koneksi antara partisi hanya apa yang benar-benar diperlukan. Selain itu, protokol antarmuka harus efisien, dengan jumlah pesan atau volume data minimum. Sangat penting bahwa seL4 memungkinkan Anda untuk mengontrol dan membatasi pertukaran memori antara partisi untuk meminimalkan jumlah data.

Selain mesin virtual yang mewakili subsistem dari sistem sumber, kami juga mengekstrak dan mengimplementasikan komponen untuk sumber daya bersama (seperti antarmuka jaringan).

Anda dapat mengulangi langkah 2 hingga kami mencapai detail bagian yang diinginkan. Perincian yang benar adalah kompromi antara kekuatan isolasi, di satu sisi, dan peningkatan biaya komunikasi dan rekonstruksi, di sisi lain.

Dalam contoh kami, kami mendapat tiga bagian: mesin virtual yang mengimplementasikan fungsi komunikasi stasiun bumi yang menjalankan Linux; mesin virtual lain yang mengimplementasikan fungsi navigasi berbasis kamera (juga menjalankan Linux); dan komponen berbagi jaringan asli, seperti yang ditunjukkan pada gambar. 8.


Gbr. 8. Fungsionalitas dibagi menjadi beberapa mesin virtual

Langkah 3. Komponen asli

Ketika suatu sistem didekomposisi menjadi bagian-bagian terpisah dari mesin virtual, beberapa atau semua bagian individu dapat diimplementasikan kembali sebagai komponen asli, daripada mesin virtual. Ini secara signifikan akan mengurangi permukaan serangan untuk fungsi yang sama. Keuntungan tambahan mengubah komponen menjadi kode mesin adalah mengurangi beban dan meningkatkan produktivitas, menghapus OS tamu dan overhead dari eksekusi kode dan komunikasi VMM.

Komponen asli juga meningkatkan potensi untuk menerapkan verifikasi formal dan metode lain untuk meningkatkan keandalan suatu komponen. Pilihannya berbeda: mulai dari verifikasi fungsional penuh kode asli hingga pembuatan kode bersama bersama dan bukti, verifikasi model, penggunaan bahasa pemrograman yang aman, analisis statis, atau pengujian ketat tradisional terhadap basis kode yang lebih kecil.

Berkat isolasi yang disediakan oleh seL4 dan arsitektur komponen, dimungkinkan untuk bekerja bersama dalam sistem komponen dengan tingkat keandalan yang berbeda. Dalam hal ini, komponen dengan keandalan rendah tidak mengurangi keandalan sistem secara keseluruhan, dan pengembang mendapat manfaat dari kenyataan bahwa Anda tidak perlu mengeluarkan biaya untuk memverifikasi kode ini.

Dalam contoh kami, kami akan menganalisis mesin virtual untuk saluran komunikasi antara komputer yang terpasang dan stasiun bumi ke modul-modul asli. Dalam komponen asli, komunikasi, kriptografi, dan fungsi kontrol (misi-manajer) diimplementasikan. Kami akan meninggalkan kamera dan WiFi di mesin virtual sebagai komponen usang yang tidak dapat diandalkan (lihat Gambar 9). Pemisahan ini telah menjadi kompromi antara upaya untuk membuat kembali subsistem dan manfaat menggunakan komponen asli dalam hal kinerja dan keandalan.


Fig. 9. Fungsi diimplementasikan dalam komponen asli

Langkah 4. Keandalan sistem secara keseluruhan

Setelah menerima semua modul yang diperlukan, kami akan mengambil langkah terakhir: analisis seluruh sistem secara keseluruhan berdasarkan keandalan arsitektur dan komponen individu.

Dalam kerangka kerja HACMS, komunikasi, kriptografi, dan modul kontrol diimplementasikan dalam bahasa berorientasi objek yang terbukti aman , Gading , dengan alokasi jumlah memori yang tetap pada heap. Tanpa verifikasi tambahan, Gading tidak memberi kami jaminan kebenaran fungsional, tetapi memberikan kepercayaan pada toleransi kesalahan dan keandalan darurat. Mengingat isolasi komponen, kami percaya bahwa jaminan ini tetap di hadapan komponen yang tidak dapat diandalkan (seperti mesin virtual kamera).

Komponen jaringan diimplementasikan pada kode C standar, yang terdiri dari kode pengguna untuk platform dan kode perpustakaan yang ada. Tingkat keandalannya sesuai dengan tingkat yang diperoleh melalui penerapan kode yang terkenal dengan cermat. Keandalan dapat ditingkatkan tanpa banyak biaya dengan menggunakan metode seperti sintesis driver , serta menggunakan bahasa tipe-aman seperti Ivory. Dalam analisis umum keamanan sistem, segala kompromi komponen jaringan hanya akan memengaruhi paket jaringan. Karena lalu lintas dienkripsi, serangan semacam itu tidak akan membahayakan kondisi spesifikasi yang hanya dapat diperintahkan perintah ke komputer on-board.

Mesin virtual camcorder adalah bagian terlemah dari sistem, karena ini berjalan pada sistem Linux dan seharusnya mengandung kerentanan. Tetapi VM terisolasi, jadi jika penyerang membobolnya, mereka tidak akan dapat pindah ke komponen lain. Hal terburuk yang bisa dilakukan penyerang adalah mengirim data yang salah ke komponen kontrol. Seperti pada quadrocopter, komponen ini memeriksa data yang diterima dari kamera. Dan dia berhasil menahan serangan cyber yang disebutkan di awal artikel. Itu adalah serangan "kotak putih", di mana tim Pentester diberi akses ke semua kode dan dokumentasi, serta ke semua saluran komunikasi eksternal. Dia sengaja diberikan akses root ke mesin virtual kamera, mensimulasikan serangan yang berhasil pada perangkat lunak yang ketinggalan zaman. Penahanan serangan dan kemampuan untuk bertahan terhadap skenario yang sangat kuat ini telah menjadi ujian yang layak untuk persyaratan keamanan kami dan identifikasi asumsi yang terlewat, masalah antarmuka, atau masalah keamanan lainnya yang mungkin tidak dikenali oleh tim peneliti.

Keterbatasan dan Pekerjaan Masa Depan

Artikel ini memberikan tinjauan umum metode untuk mencapai tingkat keamanan yang sangat tinggi untuk sistem di mana fitur keamanan berlaku melalui arsitektur komponen. Kami telah membuktikan teorema untuk tingkat kernel dan konfigurasi yang benar, serta teorema yang menjamin bahwa platform komponen dengan benar menetapkan batas keamanan sesuai dengan deskripsi arsitekturnya, dan bahwa ia menghasilkan kode yang benar untuk panggilan prosedur jarak jauh. Koneksi dengan analisis keamanan tingkat tinggi dari sistem tetap informal, dan teorema kode komunikasi tidak mencakup semua komunikasi primitif yang disediakan oleh platform. Untuk secara otomatis mendapatkan teorema yang mencakup seluruh sistem dari awal hingga akhir, pekerjaan tambahan diperlukan. Namun, pada tahap ini jelas bahwa ini adalah tugas yang layak.

Tujuan utama dari karya yang disajikan adalah untuk secara drastis mengurangi upaya verifikasi untuk kelas sistem tertentu. Pendekatan arsitektur murni yang dijelaskan di sini dapat diperluas ke sistem selain ULB, tetapi jelas dibatasi oleh fakta bahwa itu hanya dapat mengekspresikan properti yang ditentukan oleh arsitektur komponen sistem. Pengembalian akan berkurang jika arsitektur ini berubah selama eksekusi program, dan jika properti sangat bergantung pada perilaku komponen yang terlalu banyak tepercaya atau komponen yang ukurannya terlalu besar.

Langkah pertama untuk mengurangi batasan-batasan ini adalah membuat perpustakaan komponen pra-uji tingkat keandalan yang tinggi untuk digunakan sebagai blok bangunan yang andal dalam arsitektur tersebut. Perpustakaan ini dapat mencakup pola keamanan (seperti desinfeksi data input, filter keluaran, privasi dan monitor runtime) yang berpotensi dihasilkan dari spesifikasi tingkat yang lebih tinggi, serta komponen infrastruktur seperti modul kripto yang dapat digunakan kembali, penyimpanan kunci, sistem file, Tumpukan dan driver jaringan yang sangat andal. Jika keamanan tergantung pada lebih dari satu komponen seperti itu, maka ada kebutuhan untuk membenarkan keandalan interaksi dan berbagi mereka. Masalah teknis utama di sini adalah diskusi tentang konkurensi dan protokol, serta aliran informasi di hadapan komponen tepercaya. Terlepas dari keterbatasan ini, pekerjaan ini menunjukkan perkembangan pesat dari sistem nyata yang sangat andal berdasarkan seL4. Saat ini, pembuatan sistem semacam itu dimungkinkan dengan biaya lebih rendah daripada pengujian tradisional.

Aplikasi: biaya tenaga kerja

Pengembangan desain dan kode untuk seL4 memakan waktu dua tahun manusia. Jika kita menambahkan semua bukti serotipe-spesifik, total 18 orang-tahun akan diperoleh untuk 8700 baris kode untuk C. Sebagai perbandingan, pengembangan microkernel berukuran sebanding L4Ka :: Pistachio dari keluarga seL4 membutuhkan waktu enam orang-tahun dan tidak memberikan tingkat keandalan yang signifikan. Ini berarti perbedaan dalam kecepatan pengembangan hanya 3,3 kali antara perangkat lunak yang diverifikasi dan tradisional. Menurut metode penilaian Colbert dan Bohm , sertifikasi menurut kriteria EAL7 tradisional untuk 8700 baris kode C akan memakan waktu lebih dari 45,9 orang-tahun. Ini berarti bahwa verifikasi formal implementasi di tingkat biner sudah 2,3 kali lebih murah daripada tingkat sertifikasi tertinggi sesuai dengan kriteria umum, sambil memberikan keandalan yang jauh lebih tinggi.

Sebagai perbandingan, pendekatan HACMS yang dijelaskan di sini hanya menggunakan bukti yang ada untuk setiap sistem baru, termasuk bukti yang dihasilkan oleh alat. Dengan demikian, upaya pembuktian umum untuk suatu sistem yang cocok dengan pendekatan ini turun ke man-minggu, bukan tahun, dan pengujian turun hanya untuk memvalidasi asumsi.