LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Melnyk, Vasyl; Lutsk National Technical University; Melnyk, Katerina; Lutsk National Technical University; Zhyharevych, Oksana; Lutsk National Technical University (2015)
Publisher: National Aviation University
Languages: Ukrainian
Types: Unknown
Subjects: Android-безпека; Java-програма; програмний код; статичний аналіз; статична теорія моделювання, 004.056.52/004.432(045), Android-безопасность; Java-программа; программный код; статический анализ; статическая теория моделирования, Android security; Java-program; static analysis; static model theory; program code
Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішеньтеорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду,автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект.Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів 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.