タイトル（掲載誌）Research report (School of Information Science, Japan Advanced Institute of Science and Technology)
一般注記Model checking software consists of two steps: model generation and model checking. A model is often generated statically by abstraction, and sometimes refined iteratively. However, model generation is not easy for malware, since malware is often distributed without source codes, but as binary executables. Worse, sophisticated malware tries to obfuscate its behavior, like self-modification, which dynamically modifies itself and destination of indirect jumps. This paper proposes a pushdown model generation of x86 binaries in an on-the-fly manner with concolic testing to decide the precise destinations of indirect jumps. A tool BE-PUM (Binary Emulation for Pushdown Model generation) is built on JakStab, and currently it covers 52 popular x86 instructions. Experiments are performed on 1700 malwares taken from malware database. Compared to JakStab and IDA Pro, two state-of-the-art tools in this field, BE-PUM shows better tracing ability, which sometimes shows significant differences.
リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/12136
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ