Задачу анализа программного обеспечения (ПО) будем рассматривать как задачу получения некоторых свойств исследуемого ПО. Это могут быть и описания реализуемых алгоритмов, и информация о структурах файлов, данных в памяти или пакетов сетевых протоколов, и информация об имеющихся ошибках. В данной статье будет рассмотрен подход к анализу программного обеспечения, представленного в виде исполняемого кода при отсутствии исходных текстов, с целью выявления некоторых видов программных закладок. Согласно ГОСТ Р 51275-2006 программная закладка - это преднамеренно внесенный в ПО функциональный объект, который при определенных условиях инициирует реализацию недекларированных возможностей ПО. Программная закладка может быть реализована в виде вредоносной программы или программного кода. Предлагаемый подход к анализу описывается в пятом разделе статьи. Первые четыре раздела кратко описывают принципы работы системы анализа программного обеспечения по трассе исполнения программы TREX, в рамках которой ведется практическая реализация данного подхода

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

Двоичная трансляция - это процесс получения по заданной программе P программы Q, удовлетворяющей заданным требованиям, если обе программы записаны в виде машинных кодов. Если двоичная трансляция производится во время выполнения программы, то она называется динамической двоичной трансляцией. В данной статье рассматриваются возможности применения различных оптимизаций во время динамической двоичной трансляции, а именно: мы улучшили алгоритм поиска блоков трансляции в кэше трансляций в QEMU, проанализировали влияние алгоритма распределения регистров на быстродействие кода в QEMU, реализовали простые машинно-независимые оптимизации в QEMU и планировщик инструкций в Valgrind. Изменения алгоритма поиска блоков трансляций в кэше дали наибольший эффект, планировщик инструкций также является многообещающей оптимизацией

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

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

Рассмотрены особенности и проблемы эффективного создания в 70-е годы сложных комплексов программ оборонного применения, базирующихся на специализированных ЭВМ. Представлены методы, требования и реализация адаптируемых кросс-систем автоматизации программирования и тестирования для различных типов сложных комплексов программ объектных ЭВМ. Изложены результаты многолетнего применения в ряде предприятий кросс-системы автоматизации программирования и отладки ЯУЗА-6 с использованием БЭСМ-6

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

В статье рассматриваются вопросы тестирования почтовых протоколов с использованием формальных моделей протоколов: предложен метод моделирования почтовых протоколов, рассмотрены особенности почтовых протоколов в контексте тестирования, представлены результаты тестирования популярных почтовых серверов с открытым кодом. В качестве примера представлена разработка тестовых наборов для протоколов SMTP и POP3 на языке JavaTESK - расширении языка Java, реализующем тестирование с формальными методами. Тестовые наборы состоят из двух частей: независимого тестирования соответствия протоколов спецификациям и совместного теста, имитирующего работу почтовых протоколов в сети

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

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

Возможность построения неограниченно масштабируемых кластерных систем привела к резкой активизации исследований и разработок архитектур систем управления данными без совместного использования ресурсов. Образовались два основных фронта: "NoSQL", где отрицаются основные принципы, свойственные СУБД, и "один размер непригоден для всех", где упор делается на специализацию систем при сохранении важнейших свойств СУБД. Особенно интересным является противостояние этих фронтов в области "транзакционных" систем управления данными. Опираясь на "теорему" CAP Эрика Брювера (Eric Bruwer), представители лагеря NoSQL отказываются от обеспечения в своих системах традиционных свойств ACID в транзакциях баз данных. В этой статье обсуждается суть "теоремы" Брювера и обосновывается, что она не имеет отношения к свойствам ACID. Рассматриваются наиболее интересные современные исследовательские работы, обеспечивающие классические ACID-транзакции в параллельных средах без общих ресурсов, а также наиболее здравые подходы, в которых из чисто прагматических соображений свойства ACID частично ослабляются (но совсем не в связи с "теоремой" CAP).

Приложения, обрабатывающие большие массивы данных, являются широко распространенным типом программного обеспечения. В частности, такие приложения решают задачи интеграции данных в области интеграции корпоративных приложений. При решении таких задач используются специальные инструментальные среды, поддерживающие разработку, выполнение и мониторинг приложений, реализующих шаблон извлечения, трансформации и загрузки данных (Extract, Transform and Load - ETL). Специфика функционального тестирования таких приложений заключается в большом количестве возможных комбинаций входных данных. Подходы, реализованные в инструментах генерации данных для функциональной проверки приложений над базами данных, в лучших случаях основываются на схемах баз данных и запросах на SQL, используемых в тестируемых приложениях. Гарантированное покрытие функциональности тестируемого приложения при таких подходах может быть достигнуто только полным перебором возможных комбинаций исходных данных. При помощи предложенного в статье подхода к генерации данных возможно достижение покрытия функциональности приложения с близким к оптимальному объему данных (один набор данных для одной функциональной ветви приложения)

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

Поиск среди больших объёмов текстовых данных, хотя и изучается в computer science давно, не теряет своей актуальности. В работе представлена структура данных для поиска и эффективного хранения во внешней памяти массивов текстовых строк, реализованная для поддержки индексов в XML СУБД Sedna. Описываются алгоритмы для вставки, удаления и поиска строк переменной длинны в префиксных деревьях, хранимых на дисках. Мы также сравниваем нашу реализацию с существующей реализацией B-дерева. В работе показано, что в некоторых случаях предложенная структура данных занимает в несколько раз меньше места во внешней памяти при той же скорости поиска.