Bài viết đề xuất việc sử dụng phương pháp hình thức nhằm nhận dạng packer bằng cách kết hợp giữa hai công cụ BE-PUM và công cụ NuSMV. Mời các bạn cùng tham khảo bài viết để nắm chi tiết hơn nội dung nghiên cứu. | Kỷ yếu Hội nghị Khoa học Quốc gia lần thứ IX Nghiên cứu cơ bản và ứng dụng Công nghệ thông tin FAIR 9 Cần Thơ ngày 4-5 8 2016 DOI SỬ DỤNG PHƯƠNG PHÁP HÌNH THỨC ĐỂ NHẬN DẠNG PACKER Nguyễn Minh Hải 1 Đỗ Duy Phong1 Quản Thành Thơ1 1 Khoa Khoa học và Kỹ thuật máy tính Trƣờng Đại học Bách Khoa Thành phố Hồ Chí Minh hainmmt@ doduyphongbktphcm@ qttho@ TÓM TẮT Hiện nay an toàn thông tin là một vấn đề vô cùng quan trọng và thu hút sự quan tâm rất lớn. Những phần mềm độc hại malware đã và đang dần trở thành mối đe doạ thực sự đối với mỗi quốc gia. Năm 2006 theo một thống kê bởi Computer Economics 2007 Malware Report khoảng tỉ đô la đã được tiêu tốn để khắc phục những hậu quả của malware và con số này vẫn tiếp tục gia tăng do mức độ độc hai và tinh vi của malware ngày càng lớn. Để phân tích và phát hiện malware đa phần những phần mềm trong công nghiệp sử dụng kỹ thuật nhận dạng chữ ký. Trong kỹ thuật này mỗi malware sẽ được biểu diễn dưới dạng một chuỗi bit nhị phân duy nhất đặc trưng cho malware. Tuy nhiên với việc những malware ngày này sử dụng các phần mềm đóng gói packer để tạo ra nhiều biến thể mới đã khiến kỹ thuật nhận dạng chữ ký trở nên không hiệu quả. Hơn thế nữa khi phân tích malware đã được đóng gói kỹ thuật dịch ngược vốn được xem là kỹ thuật hiệu quả để phát hiện malware cũng trở nên rất khó khăn và nhiều thách thức bởi packer đã sử dụng rất nhiều kỹ thuật rắc rối hóa cũng như kỹ thuật chống dịch ngược và chống gỡ lỗi. Xuất phát từ những khó khăn thực tế đó bài báo đề xuất việc sử dụng phương pháp hình thức nhằm nhận dạng packer bằng cách kết hợp giữa hai công cụ BE-PUM và công cụ NuSMV. Chúng tôi đã phát triển công cụ BE-PUM Binary Emulator for PU shdown Model generation với mục tiêu xây dựng mô hình chính xác của một chương trình mã nhị phân và xử lý được những kỹ thuật obfuscation đặc trưng của packer như lệnh nhảy không trực tiếp code tự thay đổi. Hiện tại BE-PUM đã xử lý được các kỹ .