Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішеньтеорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду,автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект.Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів 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 holesor 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.
