Luận án TS Nguyễn Thiên Bình: Phát hiện, Phân loại Mã độc với Kiểm tra Mô hình & Phân tích Khái niệm

ĐẠI HỌC QUỐC GIA TP. HCM TRƯỜNG ĐẠI HỌC BÁCH KHOA NGUYỄN THIÊN BÌNH ÁP DỤNG KIỂM TRA MÔ HÌNH VÀ PHÂN TÍCH KHÁI NIỆM HÌNH THỨC ĐỂ PHÂN LOẠI VÀ PHÁT HIỆN MÃ ĐỘC LUẬN ÁN TIẾN SĨ KỸ THUẬT TP. HỒ CHÍ MINH NĂM 2019 ĐẠI HỌC QUỐC GIA TP. HCM TRƯỜNG ĐẠI HỌC BÁCH KHOA NGUYỄN THIÊN BÌNH ÁP DỤNG KIỂM TRA MÔ HÌNH VÀ PHÂN TÍCH KHÁI NIỆM HÌNH THỨC ĐỂ PHÂN LOẠI VÀ PHÁT HIỆN MÃ ĐỘC Chuyên ngành: Khoa học máy tính Mã số chuyên ngành: 62.01 Phản biện độc lập 1: PGS.

Võ Trung Hùng Phản biện độc lập 2: PGS. Trương Ninh Thuận Phản biện 1: PGS. Đỗ Văn Nhơn Phản biện 2: PGS. Trần Minh Triết Phản biện 3: PGS.

Bùi Hoài Thắng NGƯỜI HƯỚNG DẪN KHOA HỌC PGS. Quản Thành Thơ TP. HỒ CHÍ MINH NĂM 2019 LÕI CAM OAN Tác gi£ xin cam oan ây là công trình nghiên c˘u cıa b£n thân tác gi£. Các k∏t qu£ nghiên c˘u và các k∏t lu™n trong lu™n án này là trung th¸c và không sao chép t¯ bßt k˝ mÎt nguÁn nào và d˜Ói bßt k˝ hình th˘c nào.

Viªc tham kh£o các nguÁn tài liªu (n∏u có) ã ˜Òc th¸c hiªn trích d®n và ghi nguÁn tài liªu tham kh£o úng quy ‡nh. Tác gi£ lu™n án Ch˙ k˛ Nguyπn Thiên Bình i TÓM TçT LUäN ÁN ∫ kh≠c phˆc nh˜Òc i∫m cıa ph˜Ïng pháp phát hiªn mã Îc b¨ng cách so trùng ch˙ k˛ trong công nghiªp, hiªn nay có các nghiên c˘u theo h˜Óng ti∏p c™n áp dˆng ki∫m tra mô hình ∫ phát hiªn mã Îc nhÌ vào viªc cho phép bi∫u diπn hành vi nguy h§i mÎt cách lu™n l˛. Tuy nhiên, tr ng§i cÏ b£n cıa ph˜Ïng pháp ki∫m tra mô hình là vßn ∑ bùng nÍ không gian tr§ng thái. Dù ã có nhi∑u nghiên c˘u ∫ gi£i quy∏t vßn ∑ này, nh˜ng hiªn v®n ch˜a có nghiên c˘u nào t™p trung vào bài toán phát hiªn mã Îc.

Thông qua viªc phân tích các hành vi nguy h§i cıa mã Îc trong th¸c t∏, chúng tôi nh™n thßy hành vi nguy h§i cıa mã Îc chø xußt hiªn trong mÎt o§n mã nguÁn ˜Òc gÂi là !-region. ∞c tính này là cÏ s ∫ lu™n án ∑ xußt ph˜Ïng pháp ki∫m tra gia t´ng t¯ng ph¶n giúp thu gi£m Î ph˘c t§p cıa mô hình ch˜Ïng trình, t¯ ó giúp gi£i quy∏t vßn ∑ bùng nÍ không gian tr§ng thái. Bên c§nh vßn ∑ bùng nÍ không gian tr§ng thái, ph˜Ïng pháp ki∫m tra mô hình ∫ phát hiªn mã Îc còn g∞p mÎt tr ng§i lÓn, ó là mã Îc th˜Ìng áp dˆng các kˇ thu™t làm rËi mã (obfuscation) ∫ che dßu hành vi nguy h§i cıa chúng. Tuy ã có mÎt sË ∑ xußt theo h˜Óng ti∏p c™n c£i ti∏n lu™n l˛ thÌi gian ∫ gi£i quy∏t vßn ∑ nói trên nh˜ng mÈi ∑ xußt theo h˜Óng này chø có th∫ gi£i quy∏t ˜Òc mÎt kˇ thu™t làm rËi mã, Áng thÌi ph£i c™p nh™t công cˆ ki∫m tra mô hình, d®n ∏n chi phí ∫ x˚ l˛ mÎt kˇ thu™t làm rËi mã là rßt lÓn.

Do ó, lu™n án ã nghiên c˘u áp dˆng suy diπn tr¯u t˜Òng ∫ tr¯u t˜Òng hoá ch˜Ïng trình c¶n ˜Òc ki∫m tra thành mÎt bi∫u diπn trung gian tËi gi£n, giúp lo§i b‰ h¶u h∏t các kˇ thu™t làm rËi mã. Ngoài ra, lu™n án ∑ xußt khung th˘c HOPE, vÓi viªc phân tách b˜Óc gi£i rËi mã (deobfuscation) và b˜Óc ki∫m tra mô hình. NhÌ v™y, khi x˚ l˛ mÎt kˇ thu™t làm rËi mã mÓi, công cˆ ki∫m tra mô hình không c¶n ˜Òc c™p nh™t, t¯ ó tËi ˜u ˜Òc chi phí. Vßn ∑ còn l§i cıa ph˜Ïng pháp ki∫m tra mô hình ∫ phát hiªn mã Îc là các hành vi nguy h§i ˜Òc bi∫u diπn b¨ng các công th˘c lu™n l˛, vì v™y các h˜Óng ti∏p c™n khai phá d˙ liªu d¸a trên viªc trích xußt ∞c tính g∞p rßt nhi∑u khó kh´n.

Lu™n án gi£i quy∏t vßn ∑ này b¨ng mÎt khung th˘c ˜Òc gÂi là MarCHGen (Malware Conceptual Hierarchy Generation). Trong khung th˘c này, b¨ng cách m rÎng phân tích khái niªm hình th˘c, ph˜Ïng pháp phân tích khái niªm lu™n l˛ mã Îc (Viral Logical Concept Analysis - V-LCA) ˜Òc lu™n án ∑ xußt ∫ xây d¸ng giàn khái niªm mã Îc. Sau ó, lu™n án ∑ xußt kˇ thu™t gom cˆm khái niªm liên tˆc giúp xây d¸ng cây phân cßp khái niªm mã Îc. CuËi cùng, cây phân cßp khái niªm mã Îc ˜Òc giám sát bi mÎt kˇ thu™t ˜Òc gÂi là qu£n l˛ t™p c™n phÍ bi∏n (pre-large dataset management), giúp tránh viªc tái gom cˆm nhi∑u l¶n không c¶n thi∏t.

T¯ khoá: Phân tích mã th¸c thi, suy diπn tr¯u t˜Òng, ki∫m tra mô hình, bùng nÍ không gian tr§ng thái, !-region, phân tích khái niªm hình th˘c, phân tích khái niªm lu™n l˛ mã Îc, gom cˆm khái niªm liên tˆc. ii ABSTRACT To overcome the drawbacks of signature matching malware detection methods that widely used in industry, there is much research approaching the application of model checking to detect malware since this technique can logically represent malicious behaviors. However, model checking usually suffers from the infamous state explosion problem. Many studies have been conducted to address this, but none of them is dedicated for malware detection.

By studying large amount of malware, we found that malicious behavior should not occupy in more than one code segment so-called !-region. This provides a solid fundamental for the thesis to propose incremental verification method, which allows reducing program model complexity, thus helping to solve the state explosion problem. In addition to the state explosion problem, model checking approach for malware detection encounters a major drawback that malware often employs obfuscation techniques to mask their harmful behavior. Despite some suggestions into the direction of improving temporal logic to solve this problem, each proposal following this direction can only handle one obfuscation technique with the requirement to update the model checker, resulting in enormous costs to handle one code obfuscation technique.

Thus, the thesis studied the utilization of abstract interpretation in order to abstract the program into a minimal intermediate representation, eliminating most of the obfuscation techniques. Moreover, the thesis proposes HOPE framework, with the separation of the deobfuscation step and the model checking step. As a result, when processing a new obfuscation technique, model checking tool does not need to be updated, thus optimizing the costs. The remaining problem of model checking for malicious code detection is that malicious behaviors are represented by logical formulae.

Therefore, the typical data mining approaches based on feature extraction are not easily applied. The thesis solves this problem with a framework called MarCHGen (Malware Conceptual Hierarchy Generation). In this framework, by extending Formal Concept Analysis (FCA), Viral Logical Concept Analysis (V-LCA) is proposed in the thesis to generate viral concept lattice. Then, the thesis proposes an On-the-fly Conceptual Clustering (OCC) technique to generate malware concept hierarchy.

Finally, the malware concept hierarchy will be monitored by the pre-large dataset management technique to avoid re-clustering several times unnecessarily. Keywords: Binary code analysis, abstract interpretation, model checking, state explosion, !-region, formal concept analysis, viral logical concept analysis, on-the-fly conceptual clustering technique. iii LÕI CÁM ÃN Cho phép tôi ˜Òc g˚i ∏n PGS. Qu£n Thành ThÏ lÌi c£m Ïn sâu s≠c và s¸ tri ân chân thành nhßt cıa tôi vì nh˙ng s¸ hÈ trÒ, quan tâm, d§y b£o, ‡nh h˜Óng và Îng viên mà th¶y ã dành cho tôi trong suËt thÌi gian nghiên c˘u, th¸c hiªn và b£o vª lu™n án.

Bên c§nh ó, tôi xin phép c£m Ïn Ban giám hiªu, Phòng Sau §i hÂc, Khoa Khoa hÂc và Kˇ thu™t máy tính, BÎ môn Công nghª ph¶n m∑m; và các Th¶y Cô, các b§n nghiên c˘u sinh  Tr˜Ìng §i hÂc Bách Khoa TP. HÁ Chí Minh ã hÈ trÒ tôi trong quá trình nghiên c˘u, hÂc t™p t§i Tr˜Ìng. CuËi cùng, tôi cÙng muËn chia s¥ s¸ trân trÂng Ëi vÓi nh˙ng ıng hÎ cıa gia ình tôi và nhßt là vÒ tôi, cho quá trình nghiên c˘u và hÂc t™p cıa tôi trong thÌi gian qua. HCM, tháng 1, n´m 2019 Nguyπn Thiên Bình iv M÷C L÷C Danh sách hình v≥ vii Danh sách b£ng viii 1 GiÓi thiªu 1 1.2 Các kˇ thu™t phân tích mã Îc trong công nghiªp .3 Áp dˆng ki∫m tra mô hình ∫ phân tích mã Îc .4 S¸ c¶n thi∏t th¸c hiªn ∑ tài .8 T¶m quan trÂng cıa lu™n án.

11 2 N∑n t£ng và các nghiên c˘u liên quan 13 2.1 Phân lo§i mã Îc .2 Kˇ thu™t phân tích Îng mã Îc .3 Kˇ thu™t phân tích tænh mã Îc .2 Ki∫m tra mô hình .1 Mô hình hoá. 23 Linear Temporal Logic (LTL). 24 Computational Temporal Logic (CTL) .3 Vßn ∑ bùng nÍ không gian tr§ng thái .1 Các kˇ thu™t làm rËi mã .2 Các kˇ thu™t làm rËi mã ˜Òc mã Îc s˚ dˆng .3 Các kˇ thu™t gi£i rËi mã .1 Ph˜Ïng pháp gom cˆm phân ho§ch .2 Ph˜Ïng pháp gom cˆm phân cßp. 36 3 Ph˜Ïng pháp ki∫m tra gia t´ng t¯ng ph¶n 38 3.1 Các nghiên c˘u liên quan .1 Xây d¸ng CFG .2 Ph˜Ïng pháp ki∫m tra thành ph¶n .2 Các ‡nh nghæa ban ¶u .3 Ki∫m tra gia t´ng t¯ng ph¶n trên !-region .4 Xây d¸ng t™p !-region .5 Tr¯u t˜Òng hoá !-region .6 Xây d¸ng t™p !-instruction .1 H˜Óng ti∏p c™n ki∫m tra mô hình thông th˜Ìng .2 Ph˜Ïng pháp ki∫m tra gia t´ng t¯ng ph¶n .1 Môi tr˜Ìng .4 Các ph˜Ïng pháp ki∫m tra .5 K∏t qu£ thí nghiªm.

71 4 Áp dˆng suy diπn tr¯u t˜Òng ∫ lo§i b‰ các kˇ thu™t làm rËi mã 73 4.1 Các nghiên c˘u liên quan .2 HOPE - khung th˘c x˚ l˛ các kˇ thu™t làm rËi mã .3 Tr¯u t˜Òng hoá hành vi ∫ gi£i rËi mã .4 Ch˘ng minh kh£ n´ng gi£i rËi mã. 83 5 Hª thËng hoá mã Îc 84 5.1 Các nghiên c˘u liên quan .1 Phân tích khái niªm hình th˘c và các m rÎng .2 Phân tích khái niªm hình th˘c h˜Óng ∞c tính .3 TÍng quát hoá lu™n l˛ cho phân tích khái niªm hình th˘c .4 ∞c t£ và phân lo§i mã Îc .2 Các ‡nh nghæa ban ¶u .1 Phân tích khái niªm hình th˘c .2 Phân tích khái niªm lu™n l˛ mã Îc .3 Hª thËng hoá mã Îc d¸a vào V-LCA .4 Gom cˆm khái niªm liên tˆc .5 Qu£n l˛ t™p c™n phÍ bi∏n .1 Khái niªm phÍ bi∏n .2 Qu£n l˛ c™p nh™t khái niªm phÍ bi∏n .1 Hiªu sußt cıa kˇ thu™t gom cˆm d¸a trên FCA .2 S˚ dˆng Î o AUP ∫ so sánh chßt l˜Òng gom cˆm .3 ánh giá hiªu sußt theo chßt l˜Òng cˆm. 106 6 K∏t lu™n và h˜Óng m rÎng 107 6. 108 vi DANH SÁCH HÌNH Vì 1.1 Ch˙ k˛ virus Chernobyl.2 Cßu trúc nÎi dung lu™n án.1 Bi∫u diπn ch˜Ïng trình.2 Áp dˆng ki∫m tra mô hình ∫ phát hiªn mã Îc.5 Ph˜Ïng pháp gom cˆm phân cßp.1 Ph˜Ïng pháp ki∫m tra thành ph¶n.2 Các b˜Óc th¸c hiªn ki∫m tra thành ph¶n.3 ASM, CFG và không gian tr§ng thái cıa ch˜Ïng trình.4 Quy t≠c th¸c thi.5 Nh˙ng lªnh không ch˘a trong m®u nh™n diªn mã Îc.6 Ph˜Ïng pháp ki∫m tra gia t´ng t¯ng ph¶n.8 Không gian tr§ng thái ki∫m tra mô hình.9 Ch˜Ïng trình r≥ nhánh Ïn gi£n và ph˘c t§p.10 So sánh tÍng thÌi gian ch§y.11 So sánh bÎ nhÓ s˚ dˆng.12 So sánh sË tr§ng thái duyªt.