Model Checking awalnya digunakan untuk melakukan verifikasi keutuhan sebuah sistem terhadap spesifikasinya. Pada metode ini behavior malware diekstrak secara manual, behavior group kemudian dikodekan menggunakan LTL (linear temporal logic) untuk menampilkan feature tertendu. Behavior program didapatkan dengan melihat alur hubungan dari satu atau beberapa system calls. Behavior didefinisikan dengan property seperti hiding, spreading dan injecting. Dengan membandingkan behavior2 tersebut, dapat diklasifikasikan apakah sampel tersebut malware atau benign. Metode ini dapat mendeteksi beberapa jenis malware baru.
Penelitian yang menggunakan model checking based:
- Kinder et.al menggunakan bahasa CTPL (computation tree predicate logic) yang merupakan pengembangan CTL (Computation tree logic). Teknik ini dapat mendeteksi berbagai varian worm dengan sebuah spesifikasi.
- Holzer et.al membuat teknik verifikasi untuk mendeteksi malware. Pada teknik ini malicious behaviour di formulasikan dengan bahasa expressive speficiation CTPL, dan mengekstrak sebuah model fintie state dari disassembled executable. Teknik ini dapat menangkap semantik malware lebih akurat dan mencapai DR yang lebih tinggi.
- Kinder et.al mengajukan sistem model checking yang dapat mendeteksi variant worm tanpa perlu update signature. Sistem mengekstrak annotated control flow graph dari binary dan secara otomatis melakukan verifikasi terhadap spesifikasi formal malware. Teknik ini mengenalkan bahasa CTPL baru, yang menyeimbangkan high expressive power untuk signatur malware dengan algoritma model checking. Sistem ini memiliki beberapa keterbaasan: 1) ekstraksi proses adalah syntactic dan tidak memasukan analisa data flow; 2) behavior malicios dibagi menjadi beberapa prosedur dan tidak dapat diidentifikasi kecuali prosedurnya inlined yang menurunkan performa; 3) macro tidak melingkupi semua set instruksi pada arsitektur x86
- Beaucamps et.al engajukan teknik rewriting dan model checking dengan menangkap high-level malware behavior. Teknik ini menggunakan mekanisme rewriting-based abstraction yang menghasilkan abstracted forms of program traces yang independen dari implementasi program.
- Song and Touili mengajukan metode pushdown model-checking. Tahapannya adalah: 1) kode binary diterjemahkan menjadi pushdown systems (PDS); 2) representasi malicious behavior menggunakan stack computation tree predicate logic (SCTPL); 3) menyediakan algoritma untuk melakukan pengujian model check pushdown system terhadap spesifikasi SCTPL. Teknik ini mengurangi permasalahan model-checking untuk menguji apakah sistem symbolic alternating Buchi pushdown kosong.
- Battista et.al mengajukan sistem identifikasi family malware android dengan model checking. Algoritma ini dapat menganalisa dan verifikasi bytecode java yang dihasilkan ketika source code dikompile. Pengujian dilakukan pada family malware DroidKungFu dan Opfake
Secara umum teknik model checking-based ini digunakan untuk melakukan verifikasi program. Dari beberapa penelitian teknik ini dapat mendeteksi beberapa varian baru malware, namun tidak dapat mendeteksi semua malware. Kekurangan lainnya adalah teknik ini kompleks dan membutuhkan resource besar
Sampai disini dulu pada tulisan berikutnya akan saya lanjutkan sharing tentang teknik deteksi malware deep-learning based
Reference:
Aslan, Ö. A., & Samet, R. (2020). A comprehensive review on malware detection approaches. IEEE Access, 8, 6249-6271.