STATIC ANALYSIS OF SOURCE CODE MODELED FOR JAVA-PROGRAMS CONTAINING APPLICATIONS WITH ANDROID SECURITY - Melnyk, Vasyl; Melnyk, Katerina; Zhyharevych, Oksana (Proceedings of National Aviation University, 2015)
A static analysis techniques were combined with model-based deductive verification using solvers of the static model theory (SMT) to create a framework that, given an aspect of analysis of the source code, automatically generated with an analyzer outputting a conclusion information about this aspect. The analyzer is generated by translating of a program collecting semantic to outlined formula in first order over a few multiple submitted theories. The underscore can be looked as some set of holes or contexts corresponding to the uninterpreted APIs invoked in the program. As the program makes an import of the packages and uses classes’ methods of these packages, it is importing the semantics of API invocations in first order assertion. The analyzer is using these assertions as models and their first logic order formula incorporates the specification behavior (its negation) of the described programs. A solver of SMTLIB formula is treated as the combined formula for “constrain” and “solve” it. The “solved” form can be used for logic errors (security) identification Android-based Java-programs. The properties of Android security are represented as constraint and analysis aims to show the respecting for these constraints.