Cтатистичний аналіз вихідного коду змодельований для java-програм, які містять додатки з безпекою Android
DOI:
https://doi.org/10.18372/2306-1472.63.8859Ключові слова:
Android-безпека, Java-програма, програмний код, статичний аналіз, статична теорія моделюванняАнотація
Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішеньтеорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду,
автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект.
Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів API в наближенні першого порядку. Аналізатор, використовуючи ці наближення як моделі та їх формули першого порядку, залучає поведінку специфікації (його негативність) описаної програми. Рішення SMT-LIB формул розглядається як комбінована формула для того, щоб їх «обмежувати» та «розв’язувати». Форма «розв’язку» може використовуватися для ідентифікації логічних помилок (безпеки) Java-програм на базі Android. Властивості
безпеки Android представлено як обмежувальні аналітичні цілі, щоб показати важливість цих обмежень.
Посилання
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.
Downloads
Опубліковано
Як цитувати
Номер
Розділ
Ліцензія
Автори, які публікуються у цьому журналі, погоджуються з такими умовами:- Автори залишають за собою право на авторство своєї роботи та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons Attribution License, котра дозволяє іншим особам вільно розповсюджувати опубліковану роботу з обов'язковим посиланням на авторів оригінальної роботи та першу публікацію роботи у цьому журналі.
- Автори мають право укладати самостійні додаткові угоди щодо неексклюзивного розповсюдження роботи у тому вигляді, в якому вона була опублікована цим журналом (наприклад, розміщувати роботу в електронному сховищі установи або публікувати у складі монографії), за умови збереження посилання на першу публікацію роботи у цьому журналі.
- Політика журналу дозволяє і заохочує розміщення авторами в мережі Інтернет (наприклад, у сховищах установ або на особистих веб-сайтах) рукопису роботи, як до подання цього рукопису до редакції, так і під час його редакційного опрацювання, оскільки це сприяє виникненню продуктивної наукової дискусії та позитивно позначається на оперативності та динаміці цитування опублікованої роботи (див. The Effect of Open Access).