Статьи журнала - Труды Института системного программирования РАН

Все статьи: 115

Stealth debugging of programs in QEMU emulator with WinDbg debugger

Stealth debugging of programs in QEMU emulator with WinDbg debugger

Abakumov M.A., Dovgalyuk P.M.

Статья научная

When programs are analyzed for the presence of vulnerabilities and malicious code, there is a need for a quality isolation of the analysis tools. There are two reasons for this. At first, the program can influence the tool environment. This problem is solved by using the emulator. At second, the tool environment can influence behavior of the analyzed program. So, the programmer will think that the program is harmless, but in fact it is not. This problem is solved by the mechanism of stealth debugging. The WinDbg debugger has the possibility of connecting to a remote debug service (Kdsrv.exe) in the Windows kernel. Therefore, it is possible to connect to the guest system running in the QEMU emulator. Interaction between WinDbg client and server occurs through packets by protocol KDCOM. However, kernel debugging is possible only with the enabled debugging mode in boot settings. And it reveals the debugging process. We developed special module of WinDbg debugger for Qemu emulator. It is an alternative of the remote debugging service in the kernel. Thus, the debugger client tries to connect to the WinDbg server, but module intercepts all packets, generates all the necessary information from the Qemu emulator and sends response to the client. Module completely simulates the behavior of the server, so the client does not notice the spoofing and perfectly interacts with it. At the same time for debugging there is no need to enable debugging mode in the kernel. This leads to stealth debugging. Our module supports all features of WinDbg regarding remote debugging, besides interception of events and exceptions.

Бесплатно

Technology for application family creation based on domain analysis

Technology for application family creation based on domain analysis

Gudoshnikova A.A., Litvinov Y.V.

Статья научная

The theme of code reuse in software development is still important. Sometimes it is hard to find out what exactly we need to reuse in isolation of context. However, there is an opportunity to narrow the context problem, if applications in one given domain are considered. Same features in different applications in one domain have the same context respectively so the common part must be reused. Hence, the problem of domain analysis arises. On the other hand, there is metaCASE-techonology that allows to generate code of an application using diagrams, which describe this application. The main objective of this article is to present the technology for application family creation which connects the metaCASE-techonology and results of domain analysis activity. We propose to use some ideas of FODA (feature-oriented domain analysis) approach for domain analysis and use feature diagrams for describing of variability in a domain. Then we suggest to generate metamodel of the domain-specific visual language, based on feature diagram. After that based on generated metamodel domain-specific visual language editor is generated with the aid of metaCASE-tool. With this language user can connect and configure existing feature implementations thus producing an application. This technology supposed to be especially useful for software product lines.

Бесплатно

The study into "Cross-Site Request Forgery" attacks within the framework of analysis of software vulnerabilities

The study into "Cross-Site Request Forgery" attacks within the framework of analysis of software vulnerabilities

Barabanov A.V., Lavrov A.I., Markov A.S., Polotnyanschikov I.A., Tsirlov V.L.

Статья научная

Nowadays, web applications are one of the most popular types of target of evaluation within the framework of the information security certification. The relevance of the study of web applications vulnerabilities during information security certification is due to the fact that web technologies are actively used while producing modern information systems, including information systems critical from the information security point of view, and on the other hand carrying out basic attacks on such information systems do not require violators of high technical competence, since data on typical vulnerabilities and attacks, including the attacking tools are heavily represented in publicly available sources of information, and the information systems themselves are usually available from public communication networks. The paper presents the results of a study of the security of web applications that are target of evaluation within the framework of certification for information security requirements against cross-site requests forgery attacks. The results of systematization and generalization of information about the cross-site requests forgery attacks and security controls used by web application developers are presented. The results of experimental studies of 10 web applications that have passed certification tests against information security requirements are presented. The results of experimental studies have shown that most developers do not pay enough attention to protection from cross-site request forgery attack - 7 out of 10 web applications tested have been vulnerable to this type of attack. Based on the results of processing the results of experimental studies, the distribution of security controls used in web applications and identified vulnerabilities by programming languages were obtained. Recommendations regarding the protection of web applications against cross-site request forgery attack for developers planning to certify their software are formulated.

Бесплатно

Usability of AutoProof: a case study of software verification

Usability of AutoProof: a case study of software verification

Khazeev Mansur, Rivera Victor, Mazzara Manuel, Tchitchigin Alexander

Статья научная

Verification tools are often the result of several years of research effort. The development happens as a distributed effort inside academic institutes relying on the ability of senior investigators to ensure continuity. Quality attributes such as usability are unlikely to be targeted with the same accuracy required for commercial software where those factors make a financial difference. In order for such tools to become of widespread use, it is therefore necessary to spend an extra effort and attention on users' experience, and allow software engineers to benefit out of them without the necessity of understanding the mathematical machinery in full detail. In order to put the spotlight on usability of verification tools we chose an automated verifier for the Eiffel programming language, AutoProof, and a well-known benchmark, the Tokeneer problem. The tool is used to verify parts of the implementation of the Tokeneer so to identify AutoProof's strengths and weaknesses, and finally propose the necessary updates. The results show the efficacy of the tool in verifying a real piece of software and automatically discharging nearly two thirds of verification conditions. At the same time, the case study shows the demand for improved documentation and emphasizes the need for improvement in the tool itself and in the Eiffel IDE.

Бесплатно

Variants of Chinese postman problems and a way of solving through transformation into vehicle routing problems

Variants of Chinese postman problems and a way of solving through transformation into vehicle routing problems

Gordenko M.K., Avdoshin S.M.

Статья научная

In this article, the routing problems are described. It is shown, that almost all routing problem can be transformed into each other. An example of the Mixed Chinese Postman problem is discussed. The article gives an overview of various variants of Chinese Postman Problem. For all problems the mathematical formulation is given. Moreover, the useful real-life application is presented, too. Then, the article provides a table of possible Chinese Postman problems and identifies parameters that can be varied for obtaining new problems. Five parameters have been identified, such as: presence of set of edges; presence of set of arcs; presence of edges with cost, depending on traversing; the presence of set of required edges; the presence of set of required arcs. It was shown that by varying these parameters one can obtain tasks that were not described earlier but can be used in real life. Four new tasks were identified. Then it is shown that the Chinese Postman problem can be solved as another routing tasks through graph transformations. The method for transforming Chinese Postman problem into the Generalized Travelling Salesman problem is given. Then the results of solving the above problem are presented by simple algorithms, and their effectiveness is shown. The research is not over yet. The testing of other algorithms is planned.

Бесплатно

Verification of system on chip integrated communication controllers

Verification of system on chip integrated communication controllers

Petrochenkov M.V., Mushtakov R.E., Shpagilev D.I.

Статья научная

This article presents an approach used to verify communication controllers developed for Systems on Chip (SOC) at MCST. We provide a list of communication controllers developed in MCST and present their characteristics. We describe principles of communication controller’s operation on transaction, data link and physical layers and highlight their similarities. Then we describe a common method of device verification: principles of test system design, constrained random test stimuli generation and checking of device behavior. Based on common features of the controllers, we provide the general design of their test system. It includes components to work with transaction level interface (system agent of system on chip communication protocol) and physical interface (physical agent of protocol for SOC communication on a single board), configuration agent that determines device mode of operation and a scoreboard. Because controllers only execute transformation of transactions between different representation, scoreboard checks accordance of in and outgoing transactions. In addition, we describe specific features of devices that require the adjustments to the common approach. We describe how verification of those features affected the design of different test systems. We explain how a replacement of a physical agent with a second communication controller allows to speed up the development of test systems. We explain challenges of link training and status state machine (LTSSM) verification. We provide a way to work with devices with direct memory access (DMA) in a system agent. In conclusion, we present a list of found errors and directions of further research.

Бесплатно

Visual dataflow language for educational robots programming

Visual dataflow language for educational robots programming

Zimin G.A., Mordvinov D.A.

Статья научная

Visual domain-specific languages usually have low entry barrier. Sometimes even children can program on such languages by working with visual representations. This is widely used in educational robotics domain, where most commonly used programming environments are visual. The paper describes a novel dataflow visual programming environment for embedded robotic platforms. Obviously, complex dataflow languages are not simple for understanding. The purpose of our tool is to "bridge" between lightweight educational robotic programming tools (commonly these tools provide languages which are based on control flow model) and complex industrial tools (which provide languages based on more complex dataflow execution model). We compare programming environments mostly used by robotics community with our tool. After brief review of behavioural robotic architectures, some thoughts on expressing them in terms of our dataflow language are given. Visual language, which is described here, provides opportunity to mix dataflow and control flow models for robotics programming. We believe that it is important for educational purposes. Program on our language consists of different blocks (visual representation of data transformation processes) and "links" which presents data flow between them. Domain-specific modelling approach was used to develop our language. Also, this paper provides the examples of solving two typical robot control tasks in our language.

Бесплатно

Автоматизированная генерация декодеров машинных команд

Автоматизированная генерация декодеров машинных команд

Фокина Н.Ю., Соловьев М.А.

Статья научная

В работе предложен метод автоматизированной генерации декодеров машинных команд широкого класса процессорных архитектур с использованием транслятора языка ассемблера целевой архитектуры. Реализована программная система, использующая предложенный метод для генерации декодеров машинных команд различных архитектур. Система была протестирована на нескольких микроконтроллерах: PIC16F877A, AVR, Tricore, H8/300H.

Бесплатно

Активное обучение и краудсорсинг: обзор методов оптимизации разметки данных

Активное обучение и краудсорсинг: обзор методов оптимизации разметки данных

Гилязев Р.А., Турдаков Д.Ю.

Статья научная

Качественные аннотированные коллекции являются ключевым элементом при построении систем, использующих машинное обучение. В большинстве случаев создание таких коллекций предполагает привлечение к разметке данных людей, а сам процесс является дорогостоящим и утомительным для аннотаторов. Для оптимизации этого процесса был предложен ряд методов, использующих активное обучение и краудсорсинг. В статье приводится обзор существующих подходов, обсуждается их комбинированное применения, а также описываются существующие программные системы, предназначенные для упрощения процесса разметки данных.

Бесплатно

Алгоритм удаления невидимых поверхностей на основе программных проверок видимости

Алгоритм удаления невидимых поверхностей на основе программных проверок видимости

Гонахчян В.И.

Статья научная

Визуализация больших трехмерных сцен занимает существенное время. Для сокращения количества обрабатываемых объектов используются методы удаления невидимых поверхностей. В статье рассматривается семейство интерактивных методов удаления невидимых поверхностей, обладающих пространственной и временной когерентностью. Наиболее распространенным является метод с использованием аппаратных запросов видимости. Однако посылка и получение результатов запросов видимости занимают значительное время при большом количестве объектов. Предлагается алгоритм удаления невидимых поверхностей на основе программных проверок видимости относительно составленного на графическом процессоре буфера глубины. Предлагается эвристика для определения высоты иерархии, соответствующей наибольшей эффективности проверок видимости. Предложенный алгоритм позволяет сократить количество команд визуализации, что улучшает производительность визуализации трехмерных сцен с большим количеством объектов по сравнению с алгоритмом, основанным на аппаратных запросах видимости.

Бесплатно

Анализ баллистокардиограммы на граничных вычислительных узлах

Анализ баллистокардиограммы на граничных вычислительных узлах

Нужный А.С., Прозоров А.А., Бугаев В.И., Шувалов Н.Д., Подымов В.В.

Статья научная

В работе рассматривается бесконтактный метод анализа сердечной активности человека, основанный на регистрации и обработке баллистокардиографичекого сигнала. В измерительной установке для фиксации микроскопических движений тела используется пьезоэлектрический датчик высокой чувствительности. Появляющийся вследствие высокой чувствительности шум, существенно превышающий полезный сигнал, в дальнейшем фильтруется математическими методами. Для выделения кардио компоненты используется полосный фильтр Баттерворта. Этот подход к фильтрации полезного сигнала является более экономичным с точки зрения необходимых вычислительных ресурсов, чем сравнимые по точности методы, основанные на машинном обучении, и может быть реализован на граничном (промежуточном) вычислительном узле, к которому подключены несколько датчиков. Качество полученной после фильтрации кардио компоненты позволяет с высокой точностью выделить на ней циклы сердечной активности (сердцебиения). Предлагаемый в работе алгоритм выделения сердцебиений также обладает достаточно низкой вычислительной стоимостью, чтобы быть использованным на граничном вычислительном узле. После фильтрации данные передаются выше - в центр обработки данных (облако)

Бесплатно

Анализ методов оценки надежности оборудования и систем. Практика применения методов

Анализ методов оценки надежности оборудования и систем. Практика применения методов

Пакулин Н.В., Лаврищева Е.М., Рыжов А.Г., Зеленов С.В.

Статья научная

Проводится анализ моделей и методов оценки надежности технических и программных средств. Определяются основные понятия методов надежности и безопасности таких систем и ситуаций, приводящих к ошибкам, дефектам и отказам. Дано определение надежности и безопасности технических систем и программного обеспечения (ПО) систем. Приведена классификация моделей надежности: прогнозирующего, измерительного и оценочного типов. Описаны оценочные модели, которые применяются на практике. Определен стандарт жизненного цикла ПО (ISO 15288:2002), ориентированный на разработку и контроль компонентов систем на ошибки, начиная с требований к системе. Представлены результаты применения моделей надежности (Мусы, Гоэла-Окомото и др.) к малым, средним и большим проектам и дана сравнительная их оценка. Описан технологический модуль (ТМ) оценки надежности сложных комплексов программ ВПК (1989). Показана модель качества стандарта ISO 9126 (1-4):2002-2004 с показателями функциональность, надежность, эффективность и др., которые используются при определении зрелости и сертификата качества продукта.

Бесплатно

Анализ программ на языке Java в инструменте Svace

Анализ программ на языке Java в инструменте Svace

Меркулов А.П., Поляков С.А., Белеванцев А.А.

Статья научная

В статье описываются работы, выполненные для поддержки анализа программ на языке Java в статическом анализаторе Svace, разрабатываемом в ИСП РАН. Приводятся методы построения внутреннего представления для анализа Java, включая изменения в компоненте контролируемой сборки, доработки компилятора OpenJDK, трансляцию байткода Java в окончательное представление для анализа. Описываются особенности анализа Java-программ - алгоритм девиртуализации, спецификации методов стандартной библиотеки Java, некоторые специфичные детекторы. Представлены результаты выполнения анализа для исходного кода операционной системы Android 5.

Бесплатно

Вопросы индустриального применения синхронизационных контрактов при динамическом поиске гонок в Java-программах

Вопросы индустриального применения синхронизационных контрактов при динамическом поиске гонок в Java-программах

Трифанов В.Ю.

Статья научная

Состояния гонки (data race) возникает в многопоточной программе при одновременном обращении нескольких потоков к разделяемым данным. Существует два основных подхода к обнаружению гонок - статический анализ программы (без её запуска) и динамическое обнаружение гонок в процессе работы программы. Ранее авторами был предложен точный высокопроизводительный динамический подход к обнаружению гонок на основании специальным образом составленных синхронизационных контрактов - частичных спецификаций поведения классов и наборов методов целевого приложения в многопоточной среде. Данная статья рассматривает вопрос индустриального применения концепции синхронизационных контрактов на крупных нагруженных многопоточных приложениях. Предложены метод обработки контрактов и архитектура соответствующего модуля динамического детектора jDRD, выявлены основные проблемные места и потенциальные точки падения производительности, разработано техническое решение, лишённое подобных проблем.

Бесплатно

Высокопроизводительное численное моделирование стратифицированных течений около клина в OpenFOAM

Высокопроизводительное численное моделирование стратифицированных течений около клина в OpenFOAM

Димитриева Н.Ф., Чашечкин Ю.Д.

Статья научная

Представлены результаты численного моделирования течений непрерывно стратифицированной жидкости, которые характеризуются широким диапазоном значений внутренних масштабов, отсутствующих в однородной жидкости. Поставленная задача решалась с использованием метода конечных объемов в открытом пакете OpenFOAM. Тестирование разработанной модели проводилось для течений непрерывно стратифицированных жидкостей около неподвижного и движущегося клиновидного тела с прямыми и искривленными гранями. Расчеты, проведенные с использованием вычислительных ресурсов web-лаборатории UniHUB, показали сложную структуру течений, включающую высокоградиентные прослойки около неподвижного препятствия и присоединенные внутренние волны вблизи острых кромок движущегося препятствия.

Бесплатно

Динамическая компиляция выражений в SQL-запросах для СУБД PostgreSQL

Динамическая компиляция выражений в SQL-запросах для СУБД PostgreSQL

Шарыгин Е.Ю., Бучацкий Р.А., Скворцов Л.В., Жуйков Р.А., Мельник Д.М.

Статья научная

В последние годы по мере увеличения производительности и роста объема оперативной и внешней памяти производительность СУБД для некоторых классов запросов определяется непосредственно скоростью обработки запросов процессором. В СУБД PostgreSQL для исполнения SQL-запросов традиционно используется механизм интерпретации, который приводит к накладным расходам, например, связанным с множественным ветвлением, неявными вызовами функций-обработчиков и выполнением лишних проверок, которых можно избежать, используя информацию, доступную только во время выполнения запроса. В данной работе рассматривается метод динамической компиляции запросов, в частности, компиляция выражений оператора WHERE и метода последовательного сканирования таблиц SeqScan для СУБД PostgreSQL с помощью компиляторной инфраструктуры LLVM. Рассматривается оптимизация доступа к атрибутам, заключающаяся в вычислении смещений атрибутов кортежа во время компиляции запроса, а также метод автоматической трансляции встроенных функций PostgreSQL во внутреннее представление LLVM IR, что позволяет использовать один и тот же исходный код как для JIT-компилятора, так и для имеющегося интерпретатора. Генерация машинного кода во время выполнения запроса дает возможность избежать накладных расходов традиционной системы интерпретации. Метод реализован в виде расширения к СУБД PostgreSQL и не требует изменения исходного кода СУБД. Результаты проведенного тестирования показывают, что динамическая компиляция запросов с помощью JIT-компилятора LLVM позволяет получить ускорение в несколько раз на синтетических тестах.

Бесплатно

Инструментальная поддержка создания и трансформации функционально-потоковых параллельных программ

Инструментальная поддержка создания и трансформации функционально-потоковых параллельных программ

Легалов А.И., Васильев В.С., Матковский И.В., Ушакова М.С.

Статья научная

В работе рассмотрен нетрадиционный подход к созданию параллельных программ, их анализу и трансформации с использованием языка функционально-потокового параллельного программирования, обеспечивающего написание программ без учёта ресурсных ограничений, что позволяет изначально ориентироваться на алгоритмы с максимальным параллелизмом. Разработанные инструментальные средства обеспечивают трансляцию, выполнение, отладку, оптимизацию и верификацию функционально-потоковых параллельных программ. Выполнение разработанных программ осуществляется путём «сжатия» параллелизма с учётом ограниченных ресурсов реальных вычислительных систем. Вычислительный процесс рассматривается как наложение управляющего графа, определяющего организацию вычислений, на информационный граф, описывающий функциональные особенности реализуемого алгоритма. Возможно использование различных стратегий управления путём модификации управляющих графов. Предложенные инструменты обеспечивают формирование промежуточных представлений, на основе которых возможны дальнейшие преобразования исходных программ в программы для реальных архитектур параллельных вычислительных систем.

Бесплатно

Инфраструктура статического анализа программ на языке C#

Инфраструктура статического анализа программ на языке C#

Кошелев В.К., Игнатьев В.Н., Борзилов А.И.

Статья научная

В работе рассмотрены различные аспекты статического анализа программ на языке C# с целью обнаружения максимального количества ошибок за минимально приемлемое время. Описан полный цикл статического анализа программного обеспечения, при этом основное внимание уделяется особенностям, возникающим при анализе языка C#. Рассмотрены методы, позволяющие учитывать популярные возможности языка на всех уровнях анализа: построение графа вызовов и графа потока управления, проведение анализа потоков данных и чувствительного к контексту и путям межпроцедурного анализа. Предлагается метод символьного исполнения, основанный на таких работах, как Bounded Model Checking и Saturn Software Analysis Project. В статье описана организация модели памяти, позволяющая как проводить точный внутрипроцедурный анализ, так и создавать компактные представления для привязанных к функциям условий, используемые при межпроцедурном анализе. Особое внимание уделяется теме оптимизации возникающих на этапе чувствительного к путям анализа условий. Условия необходимо оптимизировать как по размеру, поскольку при межпроцедурном чувствительном к путям анализе необходимо сохранять большое количество условий для каждой проанализированной функции, так и по сложности, поскольку время анализа ограничено. Решение условий производится при помощи современных SMT-решателей, таких как Microsoft Z3 Prover. В статье также рассмотрены различные подходы к моделированию поведения библиотечных функций: при помощи резюме в виде набора признаком или в виде упрощенных реализаций на языке C#. Все приведённые решения реализованы в инструменте статического анализа SharpChecker и протестированы на наборе проектов различного объема (от 1.5 тыс. до 1.35 млн. строк кода) с открытым исходным кодом.

Бесплатно

К построению модульной модели распределенного интеллекта

К построению модульной модели распределенного интеллекта

Словохотов Ю.Л., Неретин И.С.

Статья научная

Описание и моделирование динамики мультиагентных социальных систем методами, заимствованными из статистической физики «неживых» многочастичных систем, не отражает принципиальную особенность совокупности взаимодействующих автономных агентов: способность воспринимать, обрабатывать и использовать внешнюю информацию. Распределенный интеллект социальных систем следует непосредственно учитывать в их экспериментальных и теоретических исследованиях. В работе предложена «модульная» модель интеллектуальной деятельности, включающая производство новой информации и пригодная для описания как индивидуального, так и распределенного интеллекта, перечислены возможные области ее использования. «Количественную оценку» эффективности распределенного интеллекта иллюстрирует компьютерная модель искусственной социальной системы; обсуждаются полученные результаты.

Бесплатно

Комбинация методов статической верификации композиции требований

Комбинация методов статической верификации композиции требований

Мордань В.О.

Статья научная

Статическая верификация программного обеспечения доказывает выполнение требований в программах, однако для этого необходимо большое количество вычислительных ресурсов, кроме того, соответствующая задача не всегда может быть решена. На данный момент не существует универсальный метод статической верификации, который мог бы эффективно проверять произвольные программы, поэтому на практике необходимо выбирать более подходящий метод и настраивать его под конкретную задачу. В данной статье предлагается комбинировать различные методы для повышения производительности и улучшения результата верификации, что можно рассматривать как первый шаг в создании универсального метода статической верификации. Предложенные методы были реализованы для комбинации активно развивающихся в настоящее время методов верификации композиции требований. Апробация реализованных методов на модулях ядра операционной системы Linux продемонстрировала их преимущества относительно отдельного применения методов верификации композиции требований.

Бесплатно

Журнал