STATIC ANALYSIS OF SOURCE CODE MODELED FOR JAVA-PROGRAMS CONTAINING APPLICATIONS WITH ANDROID SECURITY
DOI:
https://doi.org/10.18372/2306-1472.63.8859Keywords:
Android security, Java-program, static analysis, static model theory, program codeAbstract
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 forlogic 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.
References
Yu W. D. A software fault prevention approach in coding and root cause analysis. Bell Labs Technical Journal. 1998. Vol. 3, no. 2, pp. 3–21 [Online]. Available: http://dx.doi.org/10.1002/bltj.2101
Software horror stories: http://www.cs.tau.ac.il/∼nachumd/verify/horror.html.
Forum on risks to the public in computers and related systems: http://catless.ncl.ac.uk/Risks/19.88.html.
Beizer B. Software testing techniques (2-nd ed.). New York, NY, USA: Van Nostrand Reinhold Co., 1990.
Woldman K. I. A dual programming approach to software testing. Master’s thesis, Santa Clara University, 1992.
Collard J.-F. Burnstein I Practical Software Testing. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2002.
Nielson F., Nielson H.R., C. Hankin Principles of Program Analysis. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999.
Cousot P., Cousot R. “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.” in Proceedings of the 4th ACM SIGACTSIGPLAN symposium on Principles of programming languages. ser. POPL ’77. New York, NY, USA: ACM, 1977. – P. 238–252. [Online]. Available: http://doi.acm.org/10.1145/512950.512973
Holzmann G. J. “Software analysis and model checking,” in CAV, 2002. – P. 1–16.
Evans D., Guttag J., Horning J., and Tan Y., “Lclint: A tool for using specifications to check code.” in ACM SIGSOFT Software Engineering Notes. vol. 19, no. 5. ACM, 1994. – P. 87–96.
Anderson P., Reps T.W., Teitelbaum T., Zarins M. «Tool support for fine-grained software inspection.» IEEE Software, vol. 20, no. 4. 2003. – P. 42–50.
Evans D., Guttag J., Horning J., and Y. Tan, “Lclint: A tool for using specifications to check code.” in ACM SIGSOFT Software Engineering Notes. vol. 19, no. 5. ACM, 1994. – P. 87–96.
Das M., Lerner S., Seigle M. “Esp: Pathsensitive program verification in polynomial time.” in PLDI, 2002. – P. 57–68.
Martin F. “PAG – an efficient program analyzer generator.” International Journal on Software Tools for Technology Transfer. vol. 2, no. 1, 1998. – P. 46–67.
Hallem S., Chelf B., Xie Y., Engler D. «A system and language for building systemspecific, static analyses.» In Proceedings of the ACM SIGPLAN 2002 Conference on Programming
Language Design and Implementation. ACM Press, 2002. – P. 69–82.
Halbwachs N., Proy Y.-E., Roumanoff P. “Verification of real-time systems using linear relation analysis.” in FORMAL METHODS IN
SYSTEM DESIGN. 1997. – P. 157–185.
Halbwachs N., Merchat D., Parentvigouroux C. “Cartesian factoring of polyhedra in linear relation analysis.” In Static Analysis Symposium. SAS03. Springer Verlag, 2003. – P. 355–365.
Alur R., Dang T., Ivancic F. “Counterexample-guided predicate abstraction of hybrid systems.” Theor. Comput. Sci., vol. 354,
no. 2, 2006. – P. 250-271.
Dutertre B., Moura L. D. “The yices smt solver.” Tech. Rep., 2006.
Burns J. “Developing Secure Mobile Applications for Android: An Introduction to Making Secure Android Applications.” iSec
Partners, Tech. Rep., Oct. [Online]. Available: http://www.isecpartners.com/files/iSECSecuringAndroidApps.pdf
Shin W., Kiyomoto S., Fukushima K., and Tanaka T. “Towards formal analysis of the permission-based security model for android.” in Proceedings of the 2009 Fifth International
Conference on Wireless and Mobile Communications. ser. ICWMC ’09. Washington, DC, USA: IEEE Computer Society, 2009. – P. 87–92. [Online]. Available: http://dx.doi.org/10.1109/ICWMC.2009.21
S.H.D.S. Adrienne Porter Felt, Erika Chin, D. Wagner “Android permissions demystified.” in ACM Conference on Computer and Communication Security. 2011.
Frhwirth T., Abdennadher S. “Principles of constraint systems and constraint solvers.” 2005.
Barrett C., Stump A., Tinelli C. “The Satisfiability Modulo Theories Library (SMT-LIB).” www.SMT-LIB.org, 2010.
Cytron R., Ferrante J., Rosen B.K., Wegman M.N., Zadeck F.K. “Efficiently computing static single assignment form and the control dependence graph.” ACM transactions on programming languages and systems. Vol. 13, 1991. – P. 451–490.
