Smali+: An Operational Semantics for Low-Level Code Generated from Reverse Engineering Android Applications

被引：4

作者：

Ziadia, Marwa ^{[1
]}

Fattahi, Jaouhar ^{[1
]}

Mejri, Mohamed ^{[1
]}

Pricop, Emil ^{[2
]}

机构：

[1] Laval Univ, Dept Comp Sci & Software Engn, Pavillon Adrien Pouliot 1065,Ave Med, Quebec City, PQ G1V 0A6, Canada

[2] Petr Gas Univ Ploiesti, Automat Control Comp & Elect Dept, Ploiesti 100680, Romania

来源：

INFORMATION | 2020年 / 11卷 / 03期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Android applications; multi-threading; operational semantics; reverse engineering; Smali(+);

D O I：

10.3390/info11030130

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Today, Android accounts for more than 80% of the global market share. Such a high rate makes Android applications an important topic that raises serious questions about its security, privacy, misbehavior and correctness. Application code analysis is obviously the most appropriate and natural means to address these issues. However, no analysis could be led with confidence in the absence of a solid formal foundation. In this paper, we propose a full-fledged formal approach to build the operational semantics of a given Android application by reverse-engineering its assembler-type code, called Smali. We call the new formal language Smali+. Its semantics consist of two parts. The first one models a single-threaded program, in which a set of main instructions is presented. The second one presents the semantics of a multi-threaded program which is an important feature in Android that has been glossed over in the-state-of-the-art works. All multi-threading essentials such as scheduling, threads communication and synchronization are considered in these semantics. The resulting semantics, forming Smali+, are intended to provide a formal basis for developing security enforcement, analysis and misbehaving detection techniques for Android applications.

引用

页数：23