Ilmuwan komputer dapat membuktikan bahwa tidak ada kesalahan dalam program dengan kepastian yang sama seperti ahli matematika dapat membuktikan teorema. Kemajuan ini digunakan untuk meningkatkan keamanan di berbagai bidang, dari drone ke Internet.

Pada musim semi 2015, tim peretas mencoba membobol helikopter militer tak berawak bernama Little Bird ("Bird"). Helikopter, mirip dengan versi berawak dari pesawat favorit pasukan khusus AS, terletak di Boeing di Arizona. Para peretas memiliki awal yang baik: pada awal pekerjaan mereka, mereka memiliki akses ke salah satu subsistem dari komputer kontrol. Mereka hanya bisa meretas komputer penerbangan utama dan mendapatkan kendali atas UAV.

Di awal proyek, tim peretas Tim Merah dapat memecahkan sistem helikopter semudah WiFi di rumah Anda. Pada bulan-bulan berikutnya, para insinyur DARPA menerapkan mekanisme keamanan baru, sistem perangkat lunak yang tidak tunduk pada pengambil-alihan paksa. Parameter kunci dari sistem Little Bird tidak dapat dipecahkan menggunakan teknologi yang ada, dan kodenya dapat dipercaya sebagai bukti matematika. Dan meskipun tim diberi enam minggu akses ke UAV, dan akses ke sistem komputer melebihi kemampuan akses tim peretas yang sebenarnya, mereka tidak dapat memecahkan pertahanan Bird.

"Mereka tidak bisa memecahkan atau mengganggu operasi," kata Kathleen Fisher, profesor ilmu komputer di Tufts University dan manajer proyek untuk Sistem Militer Cyber Berkualitas Tinggi (HACMS). "Akibatnya, perwakilan DARPA bangkit dan berkata, ya ampun, Anda benar-benar dapat menggunakan teknologi ini dalam sistem yang penting."

Peretas yang menentang teknologi adalah gaya pemrograman yang disebut konfirmasi formal . Tidak seperti kode biasa yang ditulis secara informal dan biasanya dievaluasi hanya dengan kinerjanya, perangkat lunak yang diverifikasi secara formal terlihat seperti bukti matematis: setiap pernyataan secara logis mengikuti dari yang sebelumnya. Seluruh program dapat diverifikasi dengan kepastian yang sama dengan teorema matematika.

“Anda menulis rumus matematika yang menggambarkan perilaku suatu program, dan menggunakan alat bukti konsep yang menguji validitas pernyataan ini,” kata Brian Parno , seorang peneliti di konfirmasi formal dan keamanan di Microsoft Research.

Keinginan untuk membuat program yang dikonfirmasi secara formal ada hampir sepanjang bidang ilmu komputer itu sendiri. Dan untuk waktu yang sangat lama ini tetap mustahil, tetapi pencapaian sepuluh tahun terakhir di bidang "metode formal" telah membawa pendekatan ini lebih dekat ke praktik konvensional. Hari ini, konfirmasi resmi perangkat lunak sedang dipelajari dalam kelompok akademik yang didanai, dalam proyek militer AS, dan di perusahaan teknologi seperti Microsoft dan Amazon.

Minat meningkat seiring dengan peningkatan jumlah tugas vital yang dilakukan secara online. Ketika komputer ada dalam isolasi di rumah dan kantor, kesalahan pemrograman hanyalah gangguan. Sekarang, mereka membuka lubang keamanan pada mesin di jaringan, yang memungkinkan setiap orang yang berpengetahuan untuk menembus sistem komputer.

"Pada abad kedua puluh, ketika sebuah program memiliki kesalahan, itu buruk, itu bisa jatuh, ya Tuhan memberkati dia," kata Andrew Appel , seorang profesor ilmu komputer di Princeton University dan seorang pemimpin dalam validasi program. Namun di abad ke-21, kesalahan dapat membuka jalan bagi peretas untuk mendapatkan kendali atas program dan mencuri data Anda. Dari kesalahan yang bisa ditoleransi, itu telah menjadi kerentanan, yang jauh lebih buruk, ”katanya.

Kathleen Fisher

Mimpi program yang sempurna

Pada Oktober 1973, Edsger Dijkstra muncul dengan ide membuat kode tanpa kesalahan. Pada malam hari, ketika berada di sebuah hotel di sebuah konferensi, dia tiba-tiba berpikir tentang bagaimana membuat pemrograman lebih matematis. Menjelaskan gagasan itu kemudian, dia berkata, "Dengan pikiran yang bersemangat, saya bangun dari tempat tidur pada jam 2:30 pagi, dan menulis lebih dari satu jam." Bahan ini adalah awal dari bukunya yang berbuah 1976, The Discipline of Programming, yang, bersama dengan karya Charles Hoare (seperti Dijkstra, yang menerima Hadiah Turing ), mendefinisikan pandangan tentang penggunaan bukti kebenaran dalam program penulisan.

Tetapi ilmu komputer tidak mengikuti ide ini, terutama karena selama bertahun-tahun tampaknya tidak praktis, atau bahkan tidak mungkin, untuk menentukan fungsi suatu program menggunakan aturan logika formal.

Definisi formal adalah cara untuk menentukan apa yang dilakukan suatu program secara spesifik. Konfirmasi formal adalah cara untuk membuktikan tanpa keraguan bahwa kode program sangat cocok dengan definisi ini. Bayangkan Anda sedang menulis sebuah program untuk robomobile yang membawa Anda ke toko kelontong. Pada tingkat operasi, Anda menentukan gerakan yang harus dicapai oleh robomobile untuk mencapai tujuan - ia dapat berputar, melambat atau mempercepat, menghidupkan atau mematikan di awal dan akhir jalan. Program Anda akan terdiri dari operasi dasar ini, diatur dalam urutan yang benar sehingga pada akhirnya Anda datang ke toko, dan bukan ke bandara.

Cara tradisional untuk menguji kesehatan suatu program adalah melalui pengujian. Programmer memberikan program banyak input data (unit test) untuk memastikan bahwa ia berperilaku sebagaimana mestinya. Jika program Anda mendefinisikan algoritma untuk pergerakan robomobile, Anda dapat menguji perjalanannya di antara berbagai titik. Pengujian semacam itu memastikan operasi program yang benar dalam banyak kasus, yang cukup untuk sebagian besar aplikasi. Tetapi tes unit tidak menjamin bahwa perangkat lunak akan selalu bekerja dengan benar - Anda tidak dapat memeriksa program terhadap semua data input yang mungkin. Bahkan jika algoritma bekerja untuk semua tujuan, selalu ada kemungkinan bahwa ia akan berperilaku berbeda dalam kondisi langka - atau, seperti yang mereka katakan, dalam "kondisi batas" - dan membuka lubang keamanan. Dalam program nyata, kesalahan seperti itu bisa sederhana, misalnya, buffer overflows,di mana program menyalin sedikit data lebih dari yang diperlukan, dan menimpa bagian dari memori komputer. Kesalahan yang tampaknya tidak berbahaya ini sulit dihilangkan, dan memberikan lubang untuk serangan hacker - engsel pintu yang lemah yang membuka jalan ke kastil.

“Satu lubang di suatu tempat dalam perangkat lunak, dan ini adalah kerentanan. Sangat sulit untuk memeriksa semua jalur untuk semua kemungkinan input, "kata Parno.

Spesifikasi ini lebih rumit daripada perjalanan ke toko. Programmer, misalnya, mungkin memerlukan program notaris dan membubuhkan tanggal penerimaan dokumen dalam urutan mereka diterima. Dalam hal ini, spesifikasi harus menunjukkan bahwa penghitung selalu meningkat, dan bahwa program tidak boleh membiarkan kunci yang digunakan untuk masuk bocor.

Dalam bahasa manusia, ini mudah digambarkan. Mengubah spesifikasi menjadi bahasa formal yang dipahami komputer jauh lebih sulit - yang menjelaskan masalah utama penulisan program.

"Membangun spesifikasi formal yang dapat dimengerti untuk komputer pada dasarnya sulit," kata Parno. "Sangat mudah di level atas untuk mengatakan" jangan biarkan kata sandi bocor ", tetapi Anda perlu memikirkan cara mengubahnya menjadi definisi matematika."

Contoh lain adalah program yang mengurutkan daftar angka. Seorang programmer dalam mencoba memformalkan spesifikasi untuknya dapat muncul dengan ini:

Untuk setiap item j dalam daftar, pastikan j ≤ j + 1

Tetapi bahkan dalam spesifikasi formal ini - untuk memastikan bahwa setiap elemen dalam daftar kurang dari atau sama dengan yang berikutnya - ada kesalahan. Programer mengasumsikan bahwa output akan mengandung input yang dimodifikasi. Jika daftarnya [7, 3, 5], ia mengharapkan program untuk kembali [3, 5, 7]. Tetapi output dari program [1, 2] akan memenuhi spesifikasi - karena “ini juga merupakan daftar yang diurutkan, tetapi bukan daftar yang mungkin Anda harapkan,” kata Parno.

Dengan kata lain, sulit untuk mengubah ide tentang apa yang harus dilakukan program menjadi spesifikasi formal yang mengecualikan interpretasi yang salah dari apa yang Anda inginkan dari program. Dan contoh yang diberikan menjelaskan program penyortiran yang paling sederhana. Sekarang bayangkan deskripsi dari sesuatu yang jauh lebih abstrak, seperti perlindungan kata sandi. “Apa artinya ini secara matematis? Untuk definisi seperti itu, mungkin perlu untuk menulis deskripsi matematis tentang apa artinya "menjaga rahasia", atau apa artinya algoritma enkripsi menjadi aman, "kata Parno. "Kami mempertimbangkan semua masalah ini, dan maju dalam studi mereka, tetapi mereka bisa sangat sulit untuk diterapkan."

Blokir aman

Bahkan, perlu untuk menulis spesifikasi dan komentar tambahan yang diperlukan untuk perangkat lunak untuk menarik kesimpulan tentang kode. Suatu program, termasuk konfirmasi formalnya, dapat lima kali lebih besar dari program reguler yang ditulis untuk tujuan yang sama.

Beban ini dapat dikurangi sedikit dengan alat yang sesuai - bahasa pemrograman dan program tambahan yang membantu programmer membuat program anti peluru. Tetapi pada 1970-an mereka tidak ada. "Banyak aspek ilmu pengetahuan dan teknologi tidak tumbuh cukup, sehingga pada 1980-an banyak bidang ilmu komputer telah kehilangan minat dalam hal ini," kata Appel, seorang peneliti utama di DeepSpec, sekelompok pengembang sistem komputer yang divalidasi secara formal.

Terlepas dari perbaikan alat-alat, penghalang lain muncul dalam cara mengkonfirmasi program: tidak ada kepastian bahwa itu diperlukan sama sekali. Meskipun penggemar metode ini mengatakan bahwa kesalahan kecil dapat menyebabkan masalah besar, sisanya menarik perhatian pada kenyataan bahwa pada dasarnya program komputer bekerja dengan baik. Kadang-kadang mereka crash, ya - tetapi kehilangan sedikit data yang belum disimpan, atau kadang-kadang restart sistem sepertinya harga kecil yang harus dibayar karena tidak harus susah payah menerjemahkan setiap bagian dari program ke dalam bahasa logika formal. Seiring waktu, bahkan mereka yang berada di tempat asal konfirmasi program mulai meragukan manfaatnya. Pada 1990-an, bahkan Hoar mengakui bahwa spesifikasi bisa menjadi solusi yang menghabiskan waktu untuk masalah yang tidak ada. Pada 1995, ia menulis:

( ) , … , , .

Kemudian muncul Internet, yang melakukan hal yang sama untuk kesalahan dalam kode yang dilakukan perjalanan udara untuk infeksi: ketika semua komputer terhubung satu sama lain, kesalahan yang tidak nyaman tetapi toleran dapat menyebabkan masalah keamanan yang semakin besar.

"Kami tidak sepenuhnya mengerti," kata Appel. "Ada program yang terbuka untuk semua peretas Internet, dan jika ada kesalahan dalam program seperti itu, itu bisa menjadi kerentanan."

Pada saat para peneliti mulai memahami keseriusan ancaman keamanan yang ditimbulkan oleh Internet, konfirmasi program akan kembali. Untuk memulainya, para peneliti telah membuat kemajuan di bagian mendasar dari metode formal. Ini merupakan peningkatan dalam program pendukung seperti Coq dan Isabelle; pengembangan sistem logis ( teori tipe dependen) menyediakan platform pengembangan yang membantu komputer mengevaluasi kode; "Operasional semantik" adalah bahasa yang memiliki kata-kata yang tepat untuk mengekspresikan apa yang diperlukan dari program.

"Dimulai dengan spesifikasi dalam bahasa manusia, Anda telah menemukan ambiguitas," kata Janette Wing , wakil presiden Microsoft Research. - Setiap bahasa alami mengandung ambiguitas. Dalam spesifikasi formal, Anda menuliskan deskripsi yang tepat berdasarkan matematika untuk menjelaskan apa yang Anda inginkan dari program. "

Janette Wing dari Microsoft Research

Selain itu, peneliti metode formal telah mendefinisikan kembali tujuan mereka. Pada 1970-an dan 1980-an, mereka ingin membuat sistem komputer yang sepenuhnya teruji, dari sirkuit elektronik hingga program. Saat ini, sebagian besar peneliti bekerja pada bagian sistem yang kecil, tetapi paling kritis atau rentan - misalnya, sistem operasi atau protokol kriptografi.

"Kami tidak mengatakan bahwa kami akan membuktikan seluruh sistem 100% benar, sampai ke sirkuit elektronik," kata Wing. - Pernyataan seperti itu konyol. Kami akurat dalam apa yang bisa atau tidak bisa kami lakukan. ”

Proyek HACMS menunjukkan bagaimana Anda dapat mencapai jaminan keamanan yang hebat dengan menggambarkan satu bagian kecil dari sistem komputer. Tujuan pertama dari proyek ini adalah untuk menciptakan quadrocopter untuk hiburan. Perangkat lunak yang datang dengan quadric adalah monolitik - yaitu, dengan mendapatkan akses ke satu bagian dari itu, peretas memperoleh akses ke yang lain. Selama dua tahun, tim HACMS telah membagi kode di komputer kontrol menjadi beberapa bagian.

Tim menulis ulang arsitektur perangkat lunak menggunakan apa yang oleh Fisher disebut "blok bangunan kepercayaan tinggi" - alat yang memungkinkan seorang programmer untuk membuktikan kemurnian kode. Salah satunya memberikan bukti bahwa, setelah mendapatkan akses ke salah satu unit, tidak mungkin untuk meningkatkan hak istimewa untuk mencapai yang lain.

Kemudian, programmer menginstal perangkat lunak seperti itu di "Bird". Dalam pengujian dengan Tim Merah, dia diberi akses ke salah satu bagian sistem yang mengendalikan beberapa bagian helikopter, misalnya, kamera - tetapi bukan fungsi utama. Kegagalan para peretas dijamin secara matematis. "Mereka membuktikan dengan cara yang dapat diverifikasi mesin bahwa peretas tidak akan dapat melampaui partisi sistem, jadi ini tidak mengejutkan," kata Fisher. "Ini konsisten dengan teorema, tetapi selalu berguna untuk melakukan tes."

Pada tahun setelah audit, DARPA menerapkan alat dan teknologi proyek ke bidang teknologi militer lainnya, misalnya satelit dan truk otomatis. Inisiatif baru bertepatan dengan bagaimana konfirmasi formal telah menyebar selama sepuluh tahun terakhir: setiap proyek yang berhasil mendorong yang berikutnya. "Alasan tentang kompleksitas prinsip ini tidak lagi berhasil," kata Fisher.

Periksa internet

Keselamatan dan keandalan adalah dua tujuan utama yang menginspirasi metode formal. Setiap hari, kebutuhan untuk perbaikan menjadi semakin jelas. Pada tahun 2014, kesalahan perangkat lunak kecil, yang akan ditangkap oleh deskripsi formal, membuka jalan bagi kesalahan Heartbleed yang mengancam akan merusak Internet. Setahun kemudian, beberapa peretas "legal" mengkonfirmasi ketakutan terburuk tentang mobil yang terhubung ke Internet, mendapatkan kendali jarak jauh atas Jeep Cherokee .

Dengan angka yang lebih tinggi, peneliti metode formal menetapkan tujuan yang semakin ambisius. Tim DeepSpec, yang dipimpin oleh Appel (juga bekerja pada HACMS), sedang mencoba membangun sistem yang sedemikian kompleks dan telah teruji sepenuhnya sebagai server web. Jika berhasil, proyek, yang menerima hibah dari State Science Foundation sebesar $ 10 juta, akan menyatukan banyak proyek sukses yang lebih kecil pada dekade terakhir. Para peneliti telah membuat beberapa komponen yang terbukti aman seperti kernel sistem operasi. "Apa yang belum dilakukan sejauh ini adalah integrasi komponen-komponen ini ke dalam antarmuka spesifik spesifikasi," kata Appel.

Di Microsoft Research, programmer memiliki dua proyek ambisius. Yang pertama, Everest, bertujuan untuk membuat versi HTTPS yang divalidasi, sebuah protokol untuk mengamankan browser web yang oleh Wing disebut “tumit Achilles dari Internet.”

Yang kedua adalah penciptaan spesifikasi yang dikonfirmasi untuk sistem fisik-cyber yang kompleks, seperti UAV. Proyek ini memiliki kesulitan yang signifikan. Sementara program konvensional bekerja dengan langkah-langkah terpisah, tidak ambigu, program kendali drone menggunakan pembelajaran mesin untuk membuat keputusan probabilistik berdasarkan aliran data lingkungan yang berkelanjutan. Jauh dari jelas bagaimana keputusan logis dapat dibuat dengan tingkat ketidaktepatan sedemikian, atau digambarkan sebagai spesifikasi formal. Tetapi hanya dalam sepuluh tahun terakhir, metode formal telah maju cukup jauh, dan Wing, yang mengelola proyek, optimis percaya bahwa para peneliti akan dapat menyelesaikan semua masalah ini.

Ada kode yang tidak terputus

Mimpi program yang sempurna

Blokir aman

Periksa internet

More articles: