K-Smali: an Executable Semantics for Program Verification of Reversed Android Applications

EasyChair Preprint 10387

Abstract

One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal verification of application actions, thus early detection of any malicious behavior, before irreversible damage is done. In this regard, formal methods appear to be the most natural and secure way for rigorous and unambiguous specification as well as for the verification of such applications. In previous work, we proposed a formal approach to build the operational semantics of a given Android application by reverse engineering its assembly code, which we called Smali+. In this paper, we rely on the same idea and we enhance it by using a language definitional framework. We choose K framework to define Smali semantics. We briefly introduce the K framework. Then, we present a formal K semantics of Smali code, called K-Smali. Semantics includes multi-threading, threads scheduling and synchronization. The proposed semantics supports linear temporal logic model-checking that provides a suitable and comprehensive formal environment for checking a wide range of Android security-related properties.

Keyphrases: Android applications, K framework, formal semantics, formal verification, smali

@booklet{EasyChair:10387,
  author    = {Marwa Ziadia and Mohamed Mejri and Jaouhar Fattahi},
  title     = {K-Smali: an Executable Semantics for Program Verification of Reversed Android Applications},
  howpublished = {EasyChair Preprint 10387},
  year      = {EasyChair, 2023}}