TMPA-2015: программа
12.11.2015
Открытие конференции
Статический и динамический анализ программ
Динамический анализ исполняемого кода в формате ELF на основе статической бинарной инструментации
Михаил Ермаков, Институт системного программирования РАН, Москва
Статья посвящена возможностям применения статической инструментации исполняемых файлов и файлов динамических библиотек в формате ELF для проведения динамического анализа программ. В статье приводится обзор существующих решений в данной и смежных областях и предлагается подход к обработке бинарных файлов ARM ELF. Описываются основные особенности предлагаемого подхода: разметка целевых файлов и генерация инструментационного кода на основе пользовательских спецификаций, использование промежуточного языка описания инструкций ассемблера ARM, компоновка итоговых инструментированных файлов исполняемого кода. Приводятся результаты применения реализации данного подхода для создания модулей трассировки помеченных данных, используемых в рамках инструмента автоматического поиска дефектов Avalanche.
Применение статического анализа для оптимизации динамического поиска гонок
Яков Роскошный, Дмитрий Цителов, Виталий Трифанов, Роман Елизаров, Университет ИТМО, OOO "Эксперт-Система", Санкт-Петербург
Обнаружение гонок – актуальная задача верификации многопоточных программ. Существующие методы подразделяются на динамические, статические и смешанные. Одной из основных проблем динамических методов являются высокие накладные расходы, в частности, необходимость контролировать все обращения к разделяемым переменным, по которым возможна гонка. Для обеспечения корректной синхронизации при обращении к потенциально разделяемых переменным часто применяются устойчивые шаблонные решения. В статье рассматриваются некоторые наиболее типичные шаблоны обеспечения синхронизации доступа к разделяемым переменным и перспективы доказательства их корректности средствами статического анализа. Предложен алгоритм определения переменных защищённых во всех возможных ветвях исполнения и реализован соответствующий инструмент для языка Java. Инструмент апробирован на различных синтетических тестах и реальных программах, интегрирован с ранее разработанным авторами динамическим детектором гонок jDRD, который был представлен на TMPA-2013
Лексический анализ динамически формируемых строковых выражений
Марина Полубелова, Семён Григорьев, Санкт-Петербургский государственный университет, Санкт-Петербург
Строковые выражения могут использоваться для формирования и последующего исполнения кода во время выполнения основной программы. Такой подход обладает высокой выразительностью, однако затрудняет разработку, отладку и сопровождение, а также является источником таких уязвимостей, как внедрение SQL и межсайтовый скриптинг. Статический анализ строковых выражений предназначен для борьбы с недостатками подхода посредством проверки, что все формируемые выражения удовлетворяют некоторым свойствам, без запуска программы. Лексический анализ или токенизация формируемого кода является важным шагом такого статического анализа. В данной статье описан автоматизированный подход к созданию лексических анализаторов динамически формируемого кода, который позволит упростить создание инструментов, предназначенных для статического анализа такого кода.
Применение технологии иерархических параметризируемых шаблонов для автоматизированного исправления ошибок в программном коде
Артем Алексюк, Владимир Ицыксон, Санкт-Петербургский государственный политехнический университет Петра Великого, Санкт-Петербург
Статья посвящена автоматизированному исправлению ошибок в программном коде с использованием результатов статического анализа. Рассмотрены существующие подходы, применяемые в данной области, основные задачи и сложности, стоящие при создании инструментов автоматического исправления ошибок. Предложенный в статье способ описания исправлений на основе иерархических параметризируемых шаблонов позволяет находить и заменять участки кода, учитывая в процессе поиска то, что некоторые элементы программы, такие как идентификаторы, могут иметь произвольное значение в рамках заданных условий. Разработана архитектура системы, в которой применён описанный способ описания исправлений. Архитектура воплощена в прототипе программной системы, и подготовлен набор шаблонов, исправляющих сигнатурные ошибки, найденные статическим анализатором. Проведенное тестирование разработанного инструмента показало работоспособность подхода.
Автоматическое тестирование линеаризуемости реализаций многопоточных структур данных
Антон Евдокимов, Дмитрий Цителов, Роман Елизаров, Виталий Трифанов, Университет ИТМО, OOO "Эксперт-Система", Санкт-Петербург
В разработке алгоритма помимо теоретической корректности важна правильная реализация. Для однопоточного случая задача проверки реализации решается, например, модульным и нагрузочным тестированием. Однако, в многопоточных системах применение этих средств затруднено, поскольку выполнение программы зависит от чередования операций в потоках. Существует потребность в инструментах, которые проверяют корректность реализации многопоточного алгоритма. Аналогом понятия «корректности» для многопоточных программ служит понятие линеаризуемости — свойство алгоритма, при котором результат любого параллельного выполнения эквивалентен некоторому последовательному. В статье предлагается инструмент, проверяющий структуру данных на линеаризуемость при определенных допущениях (структура данных должна быть неблокирующейся и не зависящей от внешней среды). Инструмент работает «по определению» — ищет набор операций над структурой данных, параллельное исполнение которых не может быть объяснено последовательным. С помощью инструмента было показано, что несколько структур данных из общедоступных библиотек ведут себя некорректно на определенных наборах операций.
Язык Котлин: от разадресации нуля до умных преобразований типов
Михаил Глухих, JetBrains, Санкт-Петербург
Котлин - новый open-source язык программирования, разрабатываемый компанией JetBrains. Главная цель разработки -- создать полностью Java-совместимый язык, не уступающий Java по скорости компиляции, но при этом более безопасный и более лаконичный по сравнению с Java. В данной презентации рассматриваются два аспекта языка, реализация которых использует статический анализ кода. Это механизм проверок для защиты от разадресации нуля при выполнении программы, повышающий безопасность, и механизм умных преобразований типов на основе их вывода, повышающий лаконичность.
Михаил Глухих родился 3 июня 1978 года в Ленинграде. В 1995 году закончил лицей «Физико-техническая школа», в 2001 году – с отличием – Санкт-Петербургский государственный политехнический университет. В 2007 году защитил кандидатскую диссертацию. С 2002 по 2012 год – сотрудник лаборатории программно-аппаратных разработок кафедры компьютерных систем и программных технологий. С 2007 года – доцент кафедры. В 2013 году работал в технологическом университете Клаусталя, Германия в качестве приглашенного исследователя. В 2014 года работал в петербургском офисе корпорации Intel, с марта 2015 является одним из разработчиков языка Котлин в компании JetBrains.
Трейдинговые системы
Спонсорский доступ с малой задержкой посредством FPGA
Валерий Флоров, Павел Гарин, Павел Смирнов, Максим Метелков, Exactpro, Кострома
В статье рассматривается реализация спонсорского доступа к бирже с помощью FPGA платы с несколькими сетевыми разъемами. Рассмотрен способ снижения задержки прохождения пакетов через такое устройство за счет ранней передачи пакетов, еще не прошедших полную обработку (прием). Описываются использованные инструменты для тестирования разработанной системы, процедура проверки корректности ее функционирования и механизм измерения задержек.
Reference test harness for algorithmic trading platforms
Виктория Леончик, Алексей Сухов, Евгений Ушаков, Иосиф Иткин, Анна-Мария Лукина, Exactpro, Кострома, Москва, Саратов
Dynamic verification of input and output data streams for market data aggregation and quote dissemination systems (Ticker Plant)
Алёна Булда, Мария Орлова, Exactpro Systems, Кострома
Инструмент для автоматизированного тестирования систем проведения расчетов и клиринга ClearTH
Анна Торопова, Екатерина Димова, Иосиф Иткин, Exactpro, Кострома, Москва
Системы, обеспечивающие проведение расчетов и клиринга, называемые также post trade, составляют существенную часть инфраструктуры финансовых рынков. Эти системы ответственны за большую часть доходов и расходов участников электронной торговли. Подобно торговым платформам, отвечающим за сведение транзакций в реальном режиме времени, большинство платформ для проведения расчетов и клиринга представляют собой распределенный диверсифицированный высоконагруженный набор взаимодействующих подсистем. Однако, системы для проведения расчетов и клиринга также характеризуются дополнительным набором свойств. Структура данных в таких системах часто приводит к невозможности проверки корректности их функционирования с помощью индивидуальных независимых сценариев тестирования. В статье рассматриваются особенности систем для проведения расчетов и клиринга и анализируется применимость существующих инструментов по автоматизации тестирования для их динамической верификации. Авторы описывают разработанный ими инструмент ClearTH, позволяющий структурировать библиотеку тестов в соответствии с расписанием операционного дня/цикла систем для проведения расчетов и клиринга. Описанный подход может быть применен и к другим типам систем, обладающим аналогичными свойствами.
Автоматизированное создание сценариев тестирования финансовых протоколов и подключений
Анна Торопова, Сергей Павлов, Андрей Соловьев, Александр Бормотин, Иосиф Иткин, Exactpro Systems, Кострома, Москва
Современные брокерские, биржевые и клиринговые платформы неотделимы от финансовых протоколов, обеспечивающих интеграцию подсистем и подсоединение пользовательских систем. Верификация корректной работы протоколов и подключений является неотъемлемой частью тестирования любой реализации программного обеспечения для таких платформ. В данной статье рассмотрен комплексный подход к автоматизированной генерации тест-кейсов для тестирования различных финансовых протоколов. Выявлены требования к документации, необходимые для реализации данного подхода, а именно к способам описания словарей сообщений и способам описания состояний и переходов между ними. Рассмотрена реализация стандартного протокола распространения данных о котировках - ITCH. Предложены способы автоматизированной генерации тест-кейсов для его динамической верификации.
13.11.2015
A Theory of Programs (EN)
Бертран Мейер, создатель языка программирования Эйфель, Франция
Верификация
Implementing the MetaVCG approach in the C-light system
Алексей Промский, Дмитрий Кондратьев, Институт систем информатики им. А.П. Ершова СО РАН, Новосибирск
Расширение метагенерации условий корректности концепцией семантической разметки
Дмитрий Кондратьев, Институт систем информатики им. А.П. Ершова СО РАН, Новосибирск
Верификация программ традиционно основана на генерации условий корректности (УК). В проекте C-light по созданию системы дедуктивной верификации Си-программ возникла задача разработки расширенных или специализированных версий генераторов УК. Для решения данной задачи было решено использовать концепцию метагенерации УК. Получая на вход логику Хоара, метагенератор автоматически порождает рекурсивный алгоритм генерации УК. Идея метагенерации позволила органично дополнить систему C-light и концепцией семантической разметки, ориентированной на такую важную задачу, как анализ, трассировку и объяснение самих УК. Основываясь на предложенным Денни и Фишере методе, опишем такое расширение правил Хоара семантическими метками, что само по себе исчисление может использоваться для построения объяснений УК. Объяснения могут быть построены для различных аспектов УК, в этой статье рассмотрим построение объяснений для их структуры и целей. Также опишем отличие нашего метода от метода Денни и Фишера, заключающееся во введении иерархии на метках.
A Need To Specify and Verify Standard Functions
Николай Шилов, Институт систем информатики им. А.П. Ершова СО РАН, Новосибирск
Формальные методы в робототехнике
Дмитрий Мордвинов, Юрий Литвинов, Санкт-Петербургский государственный университет, Санкт-Петербург
В статье дается обзор применения формальных методов в контексте робототехники. Рассматриваются недавние работы, посвященные спецификациям поведения роботов в терминах темпоральных логик, применению идей подхода model checking к таким системам. Также рассматриваются применения формальных методов анализа сетей Петри и моделирования поведения робототехнических систем с их помощью. Отдельное внимание уделяется верификации гибридных систем, применению хоаровского исчисления процессов для спецификации поведения параллельных систем, а также использованию других подходов для верификации программ поведения роботов.
Верификация функциональных программ методом построения диаграмм состояний
Андрей Миронов, Институт проблем информатики РАН, Москва
В настоящей статье рассматривается проблема верификации функциональных программ (ФП) над символьными строками, где спецификации свойств ФП определяются другими ФП и ФП Σ1 удовлетворяет спецификации, определяемой ФП Σ2, если композиция функций, определяемых ФП Σ1 и Σ2, принимает значение 1 на всех аргументах. Мы вводим понятие диаграммы состояний ФП и сводим проблему верификации ФП к проблеме анализа диаграмм состояний ФП. Предложенный подход иллюстрируется примером верификации ФП сортировки.
Towards a usable defect prediction tool: crossbreeding machine learning and heuristics
Владимир Коваленко, Галина Алперович, JetBrains, Санкт-Петербург
Стандарты и стандартизация в программной инженерии. Какое отношение это имеет к вам?
Николай Пакулин, Институт системного программирования РАН, Москва
Кандидат физико-математических наук, старший научный сотрудник отдела технологий программирования, Института системного программирования РАН. Опубликовал 40 статей и докладов, в том числе на международных и зарубежных конференциях. Участвовал в совместных проектах с крупными отечественными и зарубежными компаниями. В 2005-2011 годах принимал участие в проектах Шестой и Седьмой Рамочных программ Евросоюза, консультировал российские компании и научные организации по вопросам участия в проектах Рамочных программ ЕС.
14.11.2015
Автоматизированное тестирование вчера, сегодня, завтра – векторы развития (EN)
Антон Семенченко, DPI Solutions, Минск
Инструменты тестирования и отладки
Мультиплатформенный метод обратной отладки виртуальных машин
Павел Довгалюк, Мария Климушенкова, Денис Дмитриев, Владимир Макаров, Новгородский государственный университет им. Ярослава Мудрого, Новгород
Отладка и прототипирование новых аппаратных платформ, переферийных устройств и операционных систем осложняется недетерминированностью их поведения, воздействием отладчика на систему, длительностью процесса воспроизведения ошибок, отказами всей системы и другими подобными факторами. В работе представлен метод детерминированного воспроизведения работы виртуальных машин, и показано, как он позволяет бороться со сложностями, возникающими при отладке. На основе разработанного подхода авторами создан мультиплатформенный полносистемный обратный отладчик. С помощью этого отладчика становится возможным изучение сбоев без воздействия на их проявление. Можно воспроизводить и многократно изучать состояние всей виртуальной машины и всех ее переферийных устройств. В работе представлен обратный отладчик, поддерживающий целевые платформы i386, x86-64, MIPS, PowerPC и ARM. Он протестирован для гостевых ОС Windows и GNU/Linux. Отладчик можно использовать для моделирования периферийных устройств и отладке пользовательского и системного кода. Влияние на процесс отладки ограничено лишь вносимым при записи работы системы замедлением. Это замедление незначительно влияет на работу гостевой системы и позволяет отлаживать критичные ко времени приложения.
Трассировка многомодульного приложения в среде операционной системы z/OS
Ростислав Ефремов, Санкт-Петербургский государственный университет, Санкт-Петербург
Динамический анализ бинарного кода методика, позволяющая с помощью информации о ходе выполнения программы на различных данных, получать данные о том, как она работает. Задача динамического анализа особенно актуальна для операционной системы z/OS, так как для нее существует множество программ, написанных десятки лет назад, которые до сих пор поддерживаются и развиваются. Mainframe - специфичная бизнес платформа, и публикации, освещающие в ее контексте некоторые проблемы достаточно редки. В частности, это относится к исследованиям в области динамического анализа в среде операционной системы z/OS. В данном исследовании рассмотрена эта проблема, а также определены основные методики получения графа динамических вызовов по результатам исполнения исследуемой программы. Кроме того, произведено сравнение их производительности, уровня воздействия на окружение исследуемой программы. Дополнительно в статье описан реализованный автором прототип трассировщика, который строит таблицу переходов для исследуемой программы. В ходе исследования оказалось, что решение центральной задачи динамического анализа: трассировки, сопряжено с рядом трудностей, связанных со специфичностью платформы. Тем не менее, выявлено два наиболее предпочтительных метода, которые используются в таких популярных коммерческих отладчиках как TDF и z/XDC. Эти подходы позволяют сохранить реентерабельность приложения, имеют слабые ограничения на окружение, являются достаточно производительными. Результаты исследования открывают возможности для разработки своих продуктов, осуществляющих динамический анализ, создания отладчиков. Кроме того, в работе рассматриваются некоторые слабо освещенные вопросы относительно архитектуры операционной системы z/OS.
Тестирование среды программирования роботов
Дмитрий Мордвинов, Юрий Литвинов, Санкт-Петербургский государственный университет, Санкт-Петербург
В статье представлен опыт тестирования достаточно сложной визуальной среды программирования роботов, написанной на C++ с использованием библиотеки Qt. Рассматриваются три аспекта тестирования среды — модульное тестирование, тестирование пользовательского интерфейса и функциональное тестирование посредством интерпретации программ, написанных в среде, на имитационной модели с заданными ограничениями на состояние модели. Приводится описание языка задания ограничений. Описываются другие задачи, помимо тестирования, где представленные в статье решения оказались полезны — код для тестирования пользовательского интерфейса переиспользован для реализации режима обучения, код для функционального тестирования переиспользован для проверки заданий учащихся онлайн-курса. Статья может быть полезна специалистом, занимающимся разработкой приложений на C++ с Qt и людям, занимающимся тестированием с использованием имитационных моделей физических объектов, которыми управляет программа.
Generation of Test Scenarios for Non Deterministic and Concurrent Telecommunication Applications
Павел Дробинцев,Всеволод Котляров, Никита Воинов, Санкт-Петербургский государственный политехнический университет Петра Великого, Санкт-Петербург
Система информационной поддержки разработки макропрограмм автономного управления космическим аппаратом
Андрей Тюгашев, Антон Насекин , Университет ИТМО, Санкт-Петербург
В докладе описывается ход работ по созданию инструментальных программных средств информационной поддержки процессов жизненного цикла разновидности бортового программного обеспечения космических аппаратов – «макропрограмм интегрального управления». Работы выполняются для конкретного предприятия-заказчика российской космической отрасли.
Закрытие конференции
TMPA-2015: Tools and Methods of Program Analysis Conference
About TMPA-2015. POLITECH