Kursus MIT "Keamanan Sistem Komputer". Kuliah 10: Eksekusi Simbolik, Bagian 1

Institut Teknologi Massachusetts. Kursus Kuliah # 6.858. "Keamanan sistem komputer." Nikolai Zeldovich, James Mickens. Tahun 2014

Keamanan Sistem Komputer adalah kursus tentang pengembangan dan implementasi sistem komputer yang aman. Ceramah mencakup model ancaman, serangan yang membahayakan keamanan, dan teknik keamanan berdasarkan pada karya ilmiah baru-baru ini. Topik meliputi keamanan sistem operasi (OS), fitur, manajemen aliran informasi, keamanan bahasa, protokol jaringan, keamanan perangkat keras, dan keamanan aplikasi web.

Kuliah 1: “Pendahuluan: model ancaman” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 2: "Kontrol serangan hacker" Bagian 1 / Bagian 2 / Bagian 3
Kuliah 3: “Buffer Overflows: Exploits and Protection” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 4: “Pemisahan Hak Istimewa” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 5: "Dari mana sistem keamanan berasal?" Bagian 1 / Bagian 2
Kuliah 6: “Peluang” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 7: “Kotak Pasir Klien Asli” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 8: “Model Keamanan Jaringan” Bagian 1 / Bagian 2 / Bagian 3
Kuliah 9: "Keamanan Aplikasi Web" Bagian 1 / Bagian 2 / Bagian 3
Kuliah 10: “Eksekusi simbolik” Bagian 1 / Bagian 2 / Bagian 3

Selamat pagi semuanya, saya Armando Solar-Lesam dan hari ini saya akan memberikan ceramah tentang kinerja simbolik. Siapa di antara mereka yang hadir di sini yang akrab dengan istilah ini atau pernah mendengar tentang ini sebelumnya? Saya hanya ingin mendapatkan ide dari audiens kami. Jadi mari kita mulai. Saya menjatuhkan laptop saya beberapa kali, jadi butuh waktu lama untuk memuat.



Eksekusi simbolik adalah pekerja keras dari analisis program modern. Ini adalah salah satu metode yang tumbuh dari penelitian dan kemudian mulai digunakan dalam banyak aplikasi. Misalnya, hari ini di Microsoft ada sistem yang disebut SAGE, yang bekerja dengan banyak perangkat lunak Microsoft yang penting, mulai dari Power Point dan diakhiri dengan Windows sendiri, untuk benar-benar menemukan masalah keamanan dan kerentanan.

Ada banyak proyek akademik yang memiliki dampak besar pada dunia nyata, seperti mendeteksi bug penting dalam perangkat lunak sumber terbuka menggunakan eksekusi simbolik. Dan keindahan dari eksekusi simbolik sebagai teknik adalah dibandingkan dengan pengujian, ini memberi Anda kesempatan untuk membayangkan bagaimana program Anda akan berperilaku dengan set data input yang berpotensi tak terbatas. Ini memungkinkan kami untuk menyelidiki array data input, yang akan sepenuhnya tidak praktis dan tidak praktis untuk menyelidiki, katakanlah, dengan pengujian acak, bahkan jika ada sejumlah besar penguji. Di sisi lain, dibandingkan dengan metode analisis statis yang lebih tradisional, ia memiliki keuntungan sebagai berikut. Saat menyelidiki masalah, eksekusi simbolik dapat membuat input dan jejak, jalur eksekusi yang dapat dijalankan dalam program nyata dan menjalankan program ini berdasarkan input ini. Dan setelah itu, kita dapat mengidentifikasi bug nyata dan mulai memperbaikinya menggunakan mekanisme debugging tradisional. Dan ini sangat berharga ketika Anda berada di lingkungan pengembangan industri di mana Anda mungkin tidak punya waktu untuk mengurus setiap masalah kecil dalam kode Anda.

Misalnya, Anda benar-benar ingin dapat membedakan antara masalah nyata dan positif palsu. Bagaimana cara kerjanya?

Untuk benar-benar memahami cara kerjanya, sebaiknya mulai dengan eksekusi normal. Jika kita menganggap eksekusi simbolik sebagai generalisasi dari eksekusi tradisional dan sederhana, masuk akal untuk mengetahui tampilannya. Karena itu, saya akan menggunakan program yang sangat sederhana ini sebagai ilustrasi untuk banyak hal yang akan kita bicarakan hari ini.



Di sini kita memiliki kutipan kode yang sangat sederhana dari beberapa cabang dan pernyataan bahwa jika, dalam kondisi tertentu, nilai t <x, maka ini adalah pernyataan yang salah. Kami ingin mengetahui apakah pernyataan ini dapat diajukan. Apakah mungkin? Apakah ada input yang akan membuat pernyataan ini gagal?

Salah satu hal yang dapat saya lakukan adalah memeriksa pelaksanaan program ini menggunakan nilai input data tertentu sebagai contoh. Misalkan kita menggunakan input yang X = 4 dan Y = 4. Nilai T adalah nol, seperti yang diumumkan di awal program.

Jadi, sebelum kita sampai pada eksekusi normal, mari kita cari tahu apa yang penting di sini. Kita perlu memiliki beberapa gagasan tentang keadaan program, kan? Apakah kita melakukan eksekusi normal atau apakah kita melakukan eksekusi simbolik, kita perlu memiliki beberapa cara untuk mengkarakterisasi keadaan program. Dalam hal ini, ini adalah program sederhana yang tidak menggunakan heap, tidak menggunakan stack, dan tidak ada panggilan fungsi di sini.

Dengan demikian, negara dapat sepenuhnya ditandai oleh tiga variabel ini, bersama dengan mengetahui keberadaan saya dalam program ini. Oleh karena itu, jika saya memulai eksekusi dari 4, 4 dan 0 dan sampai ke ujung cabang, maka saya akan memeriksa ekspresi: 4 lebih besar dari 4? Jelas tidak.
Sekarang saya akan menjalankan program di T = Y, yaitu, T tidak lagi 0, tetapi memiliki nilai 4. Ini adalah keadaan saat ini dari program saya, dan sekarang saya dapat mengevaluasi cabang ini.



Benarkah T <X? Tidak. Kami menghindari peluru, pernyataan salah tidak bekerja. Tidak ada masalah dalam eksekusi pribadi ini.

Tapi ini tidak memberi tahu kita tentang eksekusi lainnya. Kita tahu bahwa dengan nilai X = 4 dan Y = 4, program tidak akan gagal. Tetapi ini tidak memberi tahu kami apa pun yang akan terjadi jika nilai inputnya adalah 2 dan 1.



Dengan nilai input ini, eksekusi akan berjalan dengan cara yang berbeda. Kali ini kita melihat bahwa T = X, dan setelah mengeksekusi baris ini T akan mengambil nilai sama dengan 2. Apakah ada masalah dalam eksekusi ini? Apakah akan ada kesalahan pernyataan dengan input seperti itu?

Baiklah, mari kita lihat. Jadi, jika T adalah 2 dan X adalah 2, maka T tidak kurang dari X. Tampaknya kita kembali menghindari peluru. Benar? Jadi, di sini kita memiliki dua nilai input spesifik tempat program bekerja tanpa kesalahan. Tapi sebenarnya, itu tidak memberi tahu kami apa pun tentang nilai input lainnya.

Jadi, ide eksekusi simbolik adalah bahwa kita ingin melampaui eksekusi program dengan satu set data input. Kami ingin dapat benar-benar berbicara tentang perilaku program ketika menggunakan kumpulan data yang sangat besar, dalam beberapa kasus, jumlah tak terbatas dari nilai input yang mungkin. Gagasan utama ini adalah sebagai berikut.



Untuk program seperti ini, keadaannya ditentukan oleh nilai dari tiga variabel yang berbeda: X, Y, dan T, dan mengetahui di mana saya saat ini dalam program. Tapi sekarang alih-alih nilai spesifik untuk X dan Y, saya akan memiliki nilai simbolik, hanya sebuah variabel. Variabel yang memungkinkan saya untuk menyebutkan nilai ini, yang digunakan pengguna sebagai input. Ini berarti bahwa keadaan program saya tidak lagi ditandai dengan mencocokkan nama variabel dengan nilai tertentu. Sekarang ini adalah pemetaan nama variabel ke nilai simbolik ini.

Nilai simbolik dapat dianggap sebagai formula. Dalam hal ini, rumus untuk X sama dengan X dan rumus untuk Y hanyalah Y, dan untuk T sebenarnya sama dengan 0. Kita tahu bahwa untuk setiap nilai input tidak masalah apa yang Anda lakukan. Nilai T setelah pernyataan pertama adalah 0.

Di situlah mulai menarik sekarang. Kita sampai pada cabang ini, yang mengatakan bahwa jika X lebih besar dari Y, kita akan menuju satu arah. Jika X kurang dari atau sama dengan Y, kita akan pergi ke arah lain.

Apakah kita tahu sesuatu tentang X dan Y? Apa yang kita ketahui tentang mereka? Setidaknya kita tahu tipenya, kita tahu bahwa mereka akan bervariasi dari min int ke max int, tapi hanya itu yang kita ketahui tentang mereka. Ternyata informasi yang kita ketahui tentang mereka tidak cukup untuk mengatakan ke arah mana cabang ini bisa pergi. Dia bisa pergi ke segala arah
Ada banyak hal yang bisa kita lakukan, tetapi apa yang bisa kita lakukan saat ini? Cobalah untuk membuat tebakan yang paling liar.



Pemirsa: kami dapat melacak pelaksanaan program di kedua cabang.

Profesor: ya, kita bisa melacak kemajuan di kedua cabang. Balik koin, dan tergantung bagaimana jatuh, pilih satu atau cabang lainnya.

Jadi, jika kita ingin mengikuti kedua cabang, pertama kita harus mengikuti satu dan kemudian yang lain, kan? Misalkan kita mulai dengan cabang ini - T = X. Kita tahu bahwa jika kita sampai ke tempat ini, T akan memiliki arti yang sama dengan X. Kita tidak tahu apa nilai ini, tetapi kita memiliki nama untuk itu - ini adalah skrip X.



Jika kita mengambil cabang yang berlawanan, lalu apa yang akan terjadi? Nilai T akan sama dengan sesuatu yang lain, bukan? Di cabang ini, nilai T akan menjadi nilai simbolis dari Y.



Jadi apa artinya nilai T ini ketika kita sampai pada titik ini dalam program? Mungkin itu X, mungkin Y. Kami tidak tahu persis apa nilai ini, tetapi mengapa kita tidak memberi nama? Sebut saja t ₀ . Dan apa yang kita ketahui tentang t ₀ ? Dalam kasus apa t ₀ akan sama dengan X?

Pada dasarnya, kita tahu bahwa jika X lebih besar dari Y, maka variabelnya sama dengan X, dan jika X kurang dari atau sama dengan Y, maka variabelnya sama dengan Y. Oleh karena itu, kita memiliki nilai yang kita definisikan, sebut saja t ₀ , dan ia memiliki ini sifat logis.



Jadi, pada titik ini dalam program, kami memiliki nama untuk nilai T, ini t ₀ . Apa yang sudah kita lakukan di sini? Kami mengambil kedua cabang dari pernyataan if, dan kemudian menghitung nilai simbolik, melihat dalam kondisi apa satu cabang dari program akan dieksekusi, dan di bawah yang lainnya.
Sekarang sampai pada titik bahwa kita harus bertanya apakah T bisa kurang dari X. Sekarang nilai T adalah t ₀ , dan kami ingin tahu apakah mungkin untuk t ₀ menjadi kurang dari X? Ingat cabang pertama yang kami periksa - kami mengajukan pertanyaan tentang X dan Y dan tidak tahu apa-apa tentang mereka, kecuali bahwa mereka bertipe int.

Tetapi dengan t ₀ , kami benar-benar tahu banyak tentang itu. Kita tahu bahwa dalam beberapa kasus itu akan sama dengan X, dan dalam beberapa kasus itu akan sama dengan Y. Jadi sekarang memberi kita satu set persamaan yang bisa kita pecahkan. Jadi, kita dapat mengatakan apakah mungkin ₀ t kurang dari X, mengetahui bahwa t ₀ memenuhi semua kondisi ini? Jadi, kita dapat menyatakan ini sebagai batasan, menunjukkan apakah t ₀ mungkin lebih kecil dari X. Dan jika X lebih besar dari Y, maka t ₀ adalah X, dan jika X kurang dari atau sama dengan Y, ini berarti bahwa t ₀ = Y.



Jadi kita punya persamaan. Jika memiliki solusi, jika mungkin untuk menemukan nilai t ₀ , nilai X dan nilai Y yang memenuhi persamaan ini, maka kita mengenali nilai-nilai ini, dan ketika kita memasukkannya ke dalam program, maka ketika dieksekusi akan berjalan di sepanjang cabang ini jika t <x dan " akan meledak ”ketika dinyatakan salah.

Jadi apa yang sudah kita lakukan di sini? Kami mengeksekusi program, tetapi alih-alih memetakan nama variabel ke nilai tertentu, kami memberikan nama variabel ini nilai simbolik. Bahkan, mereka memberi mereka nama variabel lain. Dan dalam hal ini, nama variabel kami yang lain adalah skrip X, skrip Y, t ₀ , dan di samping itu, kami memiliki seperangkat persamaan yang menunjukkan bagaimana nilai-nilai ini terkait. Kami memiliki persamaan yang memberi tahu kami bagaimana t ₀ terkait dengan X dan Y dalam kasus ini.

Solusi dari persamaan ini memungkinkan kita untuk menjawab pertanyaan apakah cabang ini dapat dieksekusi atau tidak. Lihatlah persamaannya - apakah mungkin untuk mengambil cabang ini atau tidak? Tampaknya tidak, karena kami mencari kasus di mana t ₀ lebih kecil dari X, tetapi jika dalam kondisi pertama t ₀ = X, maka ekspresi t ₀ <X tidak akan benar.

Jadi, ini berarti bahwa ketika X> Y, ini tidak dapat terjadi, karena t ₀ = X dan tidak dapat sama dengan atau kurang dari X pada saat yang sama.

Tetapi apa yang terjadi jika t ₀ = Y? Bisakah t ₀ kurang dari X dalam hal ini?

Tidak, itu pasti tidak bisa, karena kita tahu bahwa X <Y. Jadi jika t ₀ kurang dari X, maka itu juga akan kurang dari Y. Tetapi kita tahu bahwa dalam hal ini t ₀ = Y. Dan karena itu, lagi , kondisi ini tidak dapat dipenuhi. Jadi, di sini kami memiliki persamaan yang tidak memiliki solusi, dan tidak masalah apa nilai yang Anda sertakan dalam persamaan ini.

Anda tidak dapat menyelesaikannya, dan ini memberi tahu kami bahwa apa pun input X dan Y yang kami berikan ke program, ia tidak akan turun ke cabang jika t <x.

Sekarang perhatikan bahwa dalam membuat argumen ini di sini, pada dasarnya saya mengisyaratkan intuisi Anda tentang bilangan bulat, tentang bilangan bulat matematika. Dalam praktiknya, kita tahu bahwa int mesin tidak berperilaku persis seperti int matematika. Ada kasus di mana hukum yang diterapkan pada tipe data integer matematis tidak berlaku untuk int terprogram.

Oleh karena itu, kita harus sangat berhati-hati ketika menyelesaikan persamaan ini, karena kita harus ingat bahwa ini bukan bilangan bulat yang kita diberitahu di sekolah dasar. Ini adalah bilangan bulat 32-bit yang digunakan oleh mesin. Dan ada banyak kasus kesalahan yang terjadi karena programmer memikirkan kode mereka dalam hal bilangan bulat matematika, tidak menyadari bahwa ada hal-hal seperti luapan yang dapat menyebabkan perilaku program yang berbeda untuk input matematika.

Hal lain yang saya jelaskan di sini adalah argumen yang murni intuitif. Saya akan memandu Anda melalui proses, menunjukkan cara melakukannya secara manual, tetapi ini tidak berarti suatu algoritma. Namun, keindahan dari eksekusi simbolik ini adalah bahwa ia dapat dikodekan ke dalam suatu algoritma. Dan Anda dapat menyelesaikannya secara mekanis, yang memungkinkan Anda melakukan ini tidak hanya untuk program 10-line, tetapi untuk jutaan program. Ini memungkinkan kami untuk menggunakan alasan intuitif yang sama yang kami gunakan dalam kasus ini dan berbicara tentang apa yang terjadi ketika kami menjalankan program ini dengan nilai input yang berbeda. Dan pertimbangan ini dapat ditingkatkan dan diperluas ke program yang sangat besar.



Audiens: bagaimana jika program tidak mendukung input dari jenis variabel tertentu?

Profesor: ini pertanyaan yang sangat bagus! Misalkan kita memiliki program yang sama, tetapi alih-alih t = x kita akan memiliki t = (x-1). Lalu, secara intuitif, kita bisa membayangkan bahwa sekarang program ini bisa "meledak", kan?



Karena ketika program berjalan seperti ini, t benar-benar akan kurang dari x. Apa yang akan terjadi pada program semacam itu? Akan seperti apakah keadaan simbolis kita? Apa yang akan menjadi ₀ ketika x lebih besar dari y? Kami mengoreksi garis dalam persamaan kami sesuai dengan nilai lain ketika t = (x-1). Sekarang program mungkin gagal, dan Anda pergi ke pengembang dan katakan padanya: "hei, fungsi ini bisa meledak ketika x lebih besar dari y"!

Pengembang melihat ini dan berkata: "Oh, saya lupa memberi tahu Anda - sebenarnya, fungsi ini tidak akan pernah dipanggil dengan parameter, di mana x lebih besar dari y. "Saya hanya menulisnya untuk beberapa alasan historis, jadi jangan khawatir, saya tidak akan mengingatnya jika Anda tidak memberi tahu saya."

Misalkan kita memiliki asumsi bahwa x akan kurang dari atau sama dengan y.



Ini adalah prasyarat atau kesepakatan untuk fungsi kita. Fungsi berjanji untuk melakukan sesuatu, tetapi hanya jika nilainya memuaskan asumsi ini. Tetapi jika tidak puas, fungsi mengatakan: "Saya tidak peduli apa yang terjadi. Saya berjanji bahwa tidak akan ada kesalahan hanya jika asumsi ini dipenuhi. "

Jadi, bagaimana kita memberi kode batasan ini ketika kita memecahkan persamaan? Pada dasarnya, kami memiliki serangkaian kendala yang memberi tahu kami apakah cabang ini layak atau tidak. Dan di samping keterbatasan, kita juga harus memastikan bahwa prasyarat, atau asumsi, dipenuhi.

Pertanyaannya adalah, dapatkah saya menemukan x dan y yang memenuhi semua batasan ini dan pada saat yang sama memiliki properti yang diperlukan? Anda dapat melihat bahwa batasan X ≤ Y ini merepresentasikan perbedaan antara case ketika batasan ini dipenuhi dan case ketika tidak dipenuhi.

Ini adalah masalah yang sangat penting ketika bekerja dengan analisis, terutama ketika Anda ingin melakukan ini secara bersamaan di tingkat fungsi individu. Dianjurkan untuk mengetahui apa yang ada dalam pikiran programmer ketika menulis fungsi ini. Karena jika Anda tidak tahu tentang asumsi-asumsi ini, Anda mungkin berpikir bahwa ada beberapa masukan bahwa program akan gagal.

Bagaimana melakukan ini dengan cara mekanis? Ada dua aspek untuk masalah ini. Aspek nomor satu - bagaimana Anda benar-benar menghasilkan formula ini?

Dalam hal ini, secara intuitif jelas bagaimana kami sampai pada formula ini, kami hanya membuatnya secara manual. Tetapi bagaimana cara membuat formula ini secara mekanis?

Dan aspek kedua - bagaimana Anda memecahkan formula ini setelah Anda memilikinya? Apakah mungkin untuk benar-benar menyelesaikan formula ini yang menjelaskan apakah program Anda macet atau tidak?
Mari kita mulai dengan pertanyaan kedua. Kita bisa mengurangi masalah kita dengan rumus-rumus ini, yang mencakup penalaran bilangan bulat dan vektor bit. Saat membuat program, Anda mengurus array, fungsi, dan sebagai hasilnya, Anda mendapatkan formula raksasa. Apakah mungkin untuk menyelesaikannya secara mekanis?



Banyak teknologi yang kita bicarakan hari ini adalah alat praktis yang terkait dengan kemajuan luar biasa dalam mengembangkan pemecah untuk pertanyaan logis. Secara khusus, ada kelas pemecah yang sangat penting, yang disebut SMT, atau "pemecah solvabilitas teori modular." SMT solver adalah solvabilitas formula logis dengan mempertimbangkan teori yang mendasari mereka.

Banyak orang mengklaim bahwa nama ini tidak terlalu baik, tetapi telah diperbaiki sebagai yang paling umum digunakan.

SMT-solver adalah suatu algoritma karena rumus logis ini pada output akan memberikan Anda satu dari dua opsi: apakah memenuhi tujuannya atau tidak memuaskan. , , .

. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


Versi lengkap dari kursus ini tersedia di sini .

, . ? ? , 30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB DDR4).

VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps hingga Desember secara gratis ketika membayar untuk jangka waktu enam bulan, Anda dapat memesan di sini .

Dell R730xd 2 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?