Cтатистичний аналіз вихідного коду змодельований для java-програм, які містять додатки з безпекою Android
Наукові журнали НАУ
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
Cтатистичний аналіз вихідного коду змодельований для java-програм, які містять додатки з безпекою Android
Cтатистический анализ исходного кодо смоделированный для java-программ содержащих приложения с безопасностью android STATIC ANALYSIS OF SOURCE CODE MODELED FOR JAVA-PROGRAMS CONTAINING APPLICATIONS WITH ANDROID SECURITY |
|
| Creator |
Melnyk, Vasyl; Lutsk National Technical University
Melnyk, Katerina; Lutsk National Technical University Zhyharevych, Oksana; Lutsk National Technical University |
|
| Subject |
—
Android-безпека; Java-програма; програмний код; статичний аналіз; статична теорія моделювання 004.056.52/004.432(045) — Android-безопасность; Java-программа; программный код; статический анализ; статическая теория моделирования 004.056.52/004.432(045) — Android security; Java-program; static analysis; static model theory; program code 004.056.52/004.432(045) |
|
| Description |
Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішеньтеорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду,автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект.Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів API в наближенні першого порядку. Аналізатор, використовуючи ці наближення як моделі та їх формули першого порядку, залучає поведінку специфікації (його негативність) описаної програми. Рішення SMT-LIB формул розглядається як комбінована формула для того, щоб їх «обмежувати» та «розв’язувати». Форма «розв’язку» може використовуватися для ідентифікації логічних помилок (безпеки) Java-програм на базі Android. Властивостібезпеки Android представлено як обмежувальні аналітичні цілі, щоб показати важливість цих обмежень.
Проведено сопоставление методов статического анализа с моделью дедуктивной проверки и использования решений теории статической модели (ТСМ) для создания основания, которая, учитывая аспект анализа исходного кода, автоматически создается с помощью анализатора, выводящего конечную информацию об этом аспекте. Анализатор генерируется путем перевода программы для сбора семантики с целью изложения формул в первом приближении на основании нескольких представленных теорий. Так как программа делает импорт пакетов и использует классовые методы этих пакетов, она импортирует семантику вызовов API в приближении первого порядка. Анализатор, используя эти приближения как модели та их формулы первого порядка, включает поведение спецификации (его отрицательность) описанной программы. Решения SMT-LIB формул рассматривается как скомбинирована формула для того, чтобы их «ограничивать» и «решать». Форма «решения» может использоваться для идентификации логических ошибок (безопасности) Java-программ на базе Android. Свойства безопасности Android представлены как ограничивающие аналитические цели, чтобы показать важность этих ограничений. 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. |
|
| Publisher |
National Aviation University
|
|
| Contributor |
—
— — |
|
| Date |
2015-09-24
|
|
| Type |
—
— — |
|
| Format |
application/pdf
application/pdf application/pdf |
|
| Identifier |
http://jrnl.nau.edu.ua/index.php/visnik/article/view/8859
|
|
| Source |
Proceedings of National Aviation University; Том 63, № 2 (2015); 46-53
Вестник Национального авиационного университета; Том 63, № 2 (2015); 46-53 Вісник Національного Авіаційного Університету; Том 63, № 2 (2015); 46-53 |
|
| Language |
uk
|
|
| Rights |
Автори, які публікуються у цьому журналі, погоджуються з наступними умовами:Автори залишають за собою право на авторство своєї роботи та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons Attribution License, котра дозволяє іншим особам вільно розповсюджувати опубліковану роботу з обов'язковим посиланням на авторів оригінальної роботи та першу публікацію роботи у цьому журналі.Автори мають право укладати самостійні додаткові угоди щодо неексклюзивного розповсюдження роботи у тому вигляді, в якому вона була опублікована цим журналом (наприклад, розміщувати роботу в електронному сховищі установи або публікувати у складі монографії), за умови збереження посилання на першу публікацію роботи у цьому журналі.Політика журналу дозволяє і заохочує розміщення авторами в мережі Інтернет (наприклад, у сховищах установ або на особистих веб-сайтах) рукопису роботи, як до подання цього рукопису до редакції, так і під час його редакційного опрацювання, оскільки це сприяє виникненню продуктивної наукової дискусії та позитивно позначається на оперативності та динаміці цитування опублікованої роботи (див. The Effect of Open Access).
|
|