Static verification of worm and virus behavior in binary executables using model checking

被引：13

作者：

Singh, PK ^{[1
]}

Lakhotia, A ^{[1
]}

机构：

[1] Univ SW Louisiana, Ctr Adv Comp Studies, Lafayette, LA 70504 USA

来源：

IEEE SYSTEMS, MAN AND CYBERNETICS SOCIETY INFORMATION ASSURANCE WORKSHOP | 2003年

关键词：

virus behavior; decompilation; verification; model checking; modeling language; flow graphs;

D O I：

10.1109/SMCSIA.2003.1232440

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Use of formal methods in any application scenario requires a precise characterization and representation of the properties that need to be verified The target, which is desired to be verified for these properties, needs to be abstracted in a suitable form that can be fed to a mechanical theorem prover. The most challenging question that arises in the case of malicious code is "What are the properties that need to be proved?" We provide a decomposition of virus and worm programs based on their core functional components and a method of formally encoding and verifying functional behavior to detect malicious behavior in binary executables.

引用

页码：298 / 300

页数：3

共 39 条

[31] Formal Verification of Radio Communication Management in Railway Systems Using Model Checking Technique
Borrelli, Antonio
Di Lucca, Giuseppe Antonio
Nardone, Vittoria
Santone, Antonella
2019 IEEE 28TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2019, : 249 - 254
[32] Formal Verification for Interaction Protocol in Agent-Based E-Learning System Using Model Checking Toolkit - MCMAS
Latif, Norizal Abd
Hassan, Mohd Fadzil
Hasan, Mohd Hilmi
SOFTWARE ENGINEERING AND COMPUTER SYSTEMS, PT 2, 2011, 180 : 412 - 426
[33] Verification of out-of-order processor designs using model checking and a light-weight completion function
Berezin, S
Clarke, E
Biere, A
Zhu, YS
FORMAL METHODS IN SYSTEM DESIGN, 2002, 20 (02) : 159 - 186
[34] Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function
Sergey Berezin
Edmund Clarke
Armin Biere
Yunshan Zhu
Formal Methods in System Design, 2002, 20 : 159 - 186
[35] Modeling and Verification of Service Allocation Policies for Multi-Access Edge Computing Using Probabilistic Model Checking
Ray, Kaustabha
Banerjee, Ansuman
IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT, 2021, 18 (03): : 3400 - 3414
[36] Optimization of State Clustering and Safety Verification in Deep Reinforcement Learning Using KMeans plus plus and Probabilistic Model Checking
Kwon, Ryeonggu
Kwon, Gihwon
IEEE ACCESS, 2025, 13 : 28085 - 28097
[37] Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking
Bolton, Matthew L.
Bass, Ellen J.
Siminiceanu, Radu I.
INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES, 2012, 70 (11) : 888 - 906
[38] Increasing Usability of Spin-Based C Code Verification using a Harness Definition Language: Leveraging Model-Driven Code Checking to Practitioners
Ratiu, Daniel
Ulrich, Andreas
SPIN'17: PROCEEDINGS OF THE 24TH ACM SIGSOFT INTERNATIONAL SPIN SYMPOSIUM ON MODEL CHECKING OF SOFTWARE, 2017, : 60 - 69
[39] Evaluating Human-automation Interaction Using Task Analytic Behavior Models, Strategic Knowledge-based Erroneous Human Behavior Generation, and Model Checking
Bolton, Matthew L.
Bass, Ellen J.
2011 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS (SMC), 2011, : 1788 - 1794

← 1 2 3 4 →