We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
STATIC ANALYSIS OF SOURCE CODE MODELED FOR JAVA-PROGRAMS CONTAINING APPLICATIONS WITH ANDROID SECURITY.
- Authors
Melnyk, Vasyl; Melnyk, Katerina; Zhyharevych, Oksana
- Abstract
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.
- Subjects
SOURCE code; JAVA programming language; ANDROID (Operating system); SECURITY systems
- Publication
Proceedings of National Aviation University, 2015, Vol 63, Issue 2, p46
- ISSN
1813-1166
- Publication type
Article
- DOI
10.18372/2306-1472.63.8859