Семинары
Семинары
Семинар "Системное программирование"
Семинар ведёт член корреспондент РАН Аветисян Арутюн Ишханович, д.ф.-м.н., руководитель научной школы по теме «Методы и средства обеспечения информационной безопасности» (НШ-2739.2018.9).
Семинар отдела "Технологии программирования"
Внутренний семинар отдела проходит по средам в 15:15 в здании ИСП РАН.
На семинаре рассматриваются различные вопросы, связанные с анализом и преобразованием последовательных и параллельных программ.
Управление данными и информационные системы
Семинар посвящен различным аспектам информационных систем и управления данными.
Доклады приглашенных участников
KernelThreadSanitizer: инструмент для поиска состояния гонки в ядре ОС Linux
Операционные системы, построенные на основе ядра Linux, становятся популярнее с каждым днем. Поиск и исправление ошибок в ее ядре, особенно ошибок безопасности, является важной задачей. В докладе представлен детектор KernelThreadSanitizer, позволяющий находить состояния гонки в ядре Linux. Состоянием гонки называется ситуация, когда два или более потока исполнения программы могут одновременно осуществить доступ к одной области памяти (например, переменной) и как минимум один из этих доступов является записью.
Мотивация и дизайн концептов с ограничениями подтипирования для языка программирования C#.
Концепты С++, предложенные в качестве замены шаблонов, представляют собой механизм обобщённого программирования на основе явных ограничений. Механизм явных ограничений на параметры обобщённого кода широко применяется в обобщённом программировании, примером являются интерфейсы Java и C#. Однако, было показано, что возможности интерфейсов уступают концептам C++.
Формальные модели и верификация свойств программ с использованием предметно-ориентированных языков
В рамках работы, результаты которой представлены в докладе, предлагается подход к верификации сложных, наукоемких программных комплексов. Его суть в том, чтобы описывать их покомпонентно с помощью языков, адекватно отражающих специфику предметной области (предметно-ориентированных языков), которые при этом имеют заданную формальную семантику. Для построения таких языков и их формальной семантики разработано промежуточное представление на основе λ-исчисления с зависимыми типами.
Методы и программные средства макромодульной разработки программ
В рамках работы, результаты которой представлены в докладе, предлагается подход к верификации сложных, наукоемких программных комплексов. Его суть в том, чтобы описывать их покомпонентно с помощью языков, адекватно отражающих специфику предметной области (предметно-ориентированных языков), которые при этом имеют заданную формальную семантику.
Разработка и исследование методов и алгоритмов организации мультиклиентских кластеров баз данных
Построение, моделирование и верификация ПЛК-программ по LTL-спецификации.
Статико-динамическая верификация драйверов файловых систем ядра Linux
На семинаре будет рассмотрен метод concolic тестирования и его применение для верификации модулей ядра ОС GNU/Linux. Будет рассказано об использовании особенностей реализации драйверов файловых систем для осуществления данного вида тестирования. А также рассмотрен вопрос автоматического создания тестовых образцов файловых систем. Concolic (от англ конкретный и символический) тестирование представляет собой гибридный метод верификации программного обеспечения, который чередует конкретное исполнение (исполнение с определёнными входными данными) с символическим исполнением. Последнее рассматривает переменные программы как символические переменные. Символическое исполнение используется в сочетании со средством автоматизированного доказательства теорем для создания новых конкретных входных данных с целью максимального покрытия кода.
Методы модульной верификации ядра ОС Linux
Система верификации LDV нацелена на проверку правил корректности использования интерфейсов ядра Linux динамически загружаемыми модулями при помощи инструментов статической верификации. Одновременно анализировать исходный код модуля вместе с кодом остального ядра затруднительно для существующих инструментов верификации из-за большого объема и сложности кода такой системы. Поэтому в системе LDV для целевого модуля генерируется модель окружения, вместе с которой исходный код проверяется инструментами верификации.
Верификация изменений в коде модулей ядра ОС Linux
Ядро Linux разрабатывается чрезвычайно быстрыми темпами. По оценкам, опубликованным в отчете Linux Kernel Development 2013, каждый час появляется 5-9 коммитов, содержащих изменения ядра, которые могут добавлять новую функциональность, исправлять или удалять существующую, исправлять ошибки. Каждое изменение может привносить новые ошибки.
Cистема для выявления состояний гонки в модулях ядра Linux
Одним из важных классов ошибок в программах являются состояния гонки, особенно распространенные и опасные в таких программных продуктах, как ядро операционной системы. В докладе будут рассмотрены некоторые подходы к поиску таких ошибок. Будет представлена система Racehound для выявления состояний гонки в ядре ОС Linux, а также описаны некоторые особенности ее реализации.
Нахождение всех ошибок в модулях ядра Linux за один запуск верификатора
Современные статические верификаторы используются только для поиска первой встретившейся ошибки для лишь одного выбранного правила корректности. В результате процесс нахождения всех ошибок в ядре Linux оказывается очень долгим. В настоящей работе предлагается идея мульти-аспектной верификации, а также представлены первые эксперименты в области нахождения всех нарушений выбранного правила с помощью инструментов LDV Tools и статического верификатора CPAchecker.
Генерация тестовых данных для покрытия путей в формальных спецификациях системы команд
Основным методом функциональной верификации микропроцессоров по-прежнему остаётся выполнение тестовых программ. Одним из способов автоматизации построения тестов является использование моделей аппаратуры. Генерация тестовых программ включает в себя построение тестовых последовательностей и генерацию тестовых данных. Одной из метрик качества тестовых данных является покрытие путей в формальных спецификациях системы команд. В докладе рассматривается подход к генерации тестовых данных на основе модели микропроцессора, полученной из формальной спецификации системы команд.
Генерация и выполнение тестовых программ - основной метод функциональной верификации микропроцессоров. Несмотря на доступные на рынке мощные автоматические генераторы, создание тестов требует значительных усилий и временных затрат и существенно удлиняет цикл разработки дизайна микропроцессора. Главная проблема состоит в том, что большинство средств разрабатывается под конкретную архитектуру и для их адаптации к новой архитектуре приходится реализовывать заново значительную часть их логики.
Построение EFSM -моделей на основе статического анализа HDL -описаний
Сложность цифровой микроэлектронной аппаратуры неуклонно возрастает, что существенно затрудняет ее верификацию — проверку функциональной корректности. Многие автоматизированные методы верификации аппаратуры основаны на использовании моделей, удобных для генерации тестов и формальной проверки свойств. В докладе описывается новый подход к извлечению моделей в форме расширенных конечных автоматов ( Extended Finite State Machine , EFSM ) из исходного кода HDL-описаний, а также обсуждаются возможности использования таких моделей в процессе верификации.
Работа с указателями и динамической памятью до сих пор остается одной из плохо поддерживаемых возможностей во многих инструментах автоматической статической верификации, реализующих метод CEGAR с предикатной абстракцией. В соревнованиях автоматических статических верификаторов SV-COMP'14 из 5 участников, использующих CEGAR с предикатной абстракцией, только 2 участвовало в категории HeapManipulation, состоящей из заданий, проверяющих поддержку динамической памяти. При этом один из этих инструментов занял в данной категории последнее место. В то же время инструменты, основанные на CEGAR с предикатной абстракцией, используются для верификации драйверов операционных систем (например, драйверов Linux в проекте LDV), в которых указатели, в том числе на динамическую память, используются очень активно.
Поиск состояний гонки методами статического анализа
Ошибки, связанные с многопоточным выполнением, остаются одними из самых сложно выявляемых. Наиболее распространенными причинами таких ошибок являются состояния гонок. Одним из способов поиска состояний гонок является использование методов статического анализа, в частности метода адаптивного статического анализа. В докладе будет рассказано о методе статического анализа, реализованного в инструменте CPAchecker, для поиска состояний гонок и об одном из направлений развития данного подхода - применении метода CEGAR (Counter Example Guided Abstraction Refinement) для этого.
Reusing Precisions for Efficient Regression Verification (and beyond)
Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions.
Distributing Verification Tasks with VerifierCloud
Software verification of real-world programs is still a time- and resource-consuming process, dependent on sophisticated tools that often require expert knowledge. We present VerifierCloud, a job distribution tool that allows optimal hardware utilization. It is integrated with the CPAchecker framework and can be used to run competitive benchmarks. A web front-end for registration-based software verification is under development to make verification technology more accessible for non-experts.
Динамический анализ расширенных AADL-моделей
AADL -- расширяемый язык описания архитектуры программно-аппаратных систем, используемый при моделировании систем авионики, а также других ответственных и встраиваемых систем. Для проверки тех или иных свойств этих моделей могут использоваться различные подходы, которым могут требоваться различные расширения AADL. Рассмотрено расширение AADL-моделей описаниями поведения компонентов модели исполнимым кодом на Java с определёнными ограничениями. Такой подход позволяет описывать поведения сложных подсистем на стадии проектирования одновременно с детальным описанием уже разработанных компонент. Тем самым появляется возможность симуляции модели и анализа её свойств с ранних этапов проектирования.
MMU, Memory Management Unit (подсистема управления памятью) - ключевой компонент микропроцессора, отвечающий за обработку обращений к памяти, соответственно, к его функционированию предъявляются высокие требования. Многоуровневая иерархия памяти (как правило, кэши нескольких (L1/L2, иногда и L3) уровней) создает огромное число ситуаций в работе модуля, проверить которые вручную не представляется возможным. Требуются средства генерации тестовых программ для верификации функциональности подсистемы управления памятью микропроцессоров. Архитектура целевого микропроцессора в генераторе тестовых программ MicroTESK описывается на ADL языке Sim-nML. Однако семантики и синтаксиса Sim-nML не хватает для описания работы модулей памяти. Появляется необходимость в разработке языка высокого уровня для формальной спецификации MMU.
Генератор тестовых программ MicroTESK: средства моделирования системы команд микропроцессорах
Основной метод функциональной верификации микропроцессоров - генерация и выполнение тестовых программ. Несмотря на доступные на рынке мощные автоматические генераторы, создание тестов требует серьёзных усилий и временных затрат и значительно удлиняет цикл разработки дизайна микропроцессора. Главная проблема состоит в том, что большинство существующих средств разработано под конкретную архитектуру и для их адаптации к новой архитектуре или к изменениям в текущей приходится переписывать значительную часть их кода.
Динамическое обнаружение гонок в Java-программах
Состояния гонки (data races) – это несинхронизированные обращения к одному и тому же участку памяти разных потоков параллельной программы. Состояния гонки являются одними из самых труднообнаружимых ошибок многопоточного программирования. Автоматический поиск гонок является предметом активных исследований в последние двадцать лет, однако, для Java-приложений на настоящий момент не существует полноценного программного средства (динамического детектора гонок), применимого для промышленных приложений (сотни и тысячи классов). Основная причина - высокие накладные расходы на анализ программ.
Поиск состояний гонки методами статического анализа
Ошибки, связанные с многопоточным выполнением, остаются одними из самых сложно выявляемых. Наиболее распространенными причинами таких ошибок являются состояния гонок. В докладе будет рассказано о методе статической верификации для обнаружения состояний гонок в исходном коде ОС. Особенности задачи состоят в том, что должна учитываться специфика исходного кода ядер ОС, должна масштабироваться для применения к поиску состояний гонок в современных ОС. Метод основан на использовании адаптивного статического анализа, позволяющего совмещать различные техники анализа, в том числе использовать имеющийся в мире задел в области статической верификации.
Статико-динамическая верификация драйверов файловых систем ядра Linux
В докладе рассказано о методе concolic тестирования и возможностях его применения для верификации модулей ядра ОС GNU/Linux, об использовании особенностей реализации драйверов файловых систем для осуществления этого тестирования. Concolic (от англ конкретный и символический) тестирование представляет собой гибридный метод верификации программного обеспечения, который чередует конкретное исполнение (исполнение с определёнными входными данными) с символическим исполнением. Последнее рассматривает переменные программы как символические переменные. Символическое исполнение используется в сочетании со средством автоматизированного доказательства теорем для создания новых конкретных входных данных с целью максимального покрытия кода.
Диагностика ошибочного поведения аппаратуры при динамической верификации на основе моделей
При верификации различных аппаратных средств значительное количество усилий тратится на интерпретацию полученных в ходе верификации ошибочных результатов и поиск причин, породивших их. Сложность ситуации обуславливается значительным параллелизмом аппаратуры, большим количеством входных и выходных интерфейсов. На семинаре будет рассказано о подходе к автоматическому анализу и интерпретации результатов тестирования, полученных в рамках динамической модульной верификации на основе моделей с использованием инструмента C++TESK.
Генерация тестовых программ для микропроцессоров на основе моделей их архитектуры
Генерация тестовых программ играет важную роль в функциональной верификации микропроцессоров. Нарастающая сложность современного аппаратного обеспечения и сжатые сроки разработки делают создание тестов непростой задачей. Сложность состоит в том, что не смотря на доступные на рынке мощные средства генерации тестов, написание тестовых программ требует существенных временных затрат и значительно удлиняет цикл разработки архитектуры микропроцессора.
Комбинаторная генерация программных конфигураций ОС
Было рассказано об автоматической генерации тестов для конфигурационного тестирования ядра ОС. В основе предлагаемого метода лежит использование покрывающих наборов и учет условий использования различных параметров конфигурации. Сгенерированные таким образом тесты использовались на практике для тестирования ОС2000.
Инструменты для динамического анализа модулей и драйверов ядра Linux
Самым распространенным способом проверки качества драйверов Linux является тестирование. Однако за счет работы только в пользовательском пространстве могут быть проверены не все свойства драйвера. Не вмешиваясь в работу драйвера на уровне ядра невозможно проверить, например, освобождает ли драйвер все используемые им ресурсы, и правильно ли драйвер работает в случае системных сбоев.
Моделирование памяти при верификации программ методом CEGAR
Об инструментировании и генерировании окружения для драйверов, верифицируемых в системе Linux Driver Verification (LDV) было рассказано на предыдущих семинарах. Проверка же подготовленного кода драйвера, вместе со сгенерированным окруженем, в среде LDV в настоящее время осуществляется инструментами статического анализа кода, такими как CPAchecker и BLAST. В основе работы этих инструментов лежит подход CEGAR -- уточнение абстракции по контрпримерам.
Моделирование окружения драйверов операционной системы Linux для их статической верификации
Ядро операционной системы Linux является одним из самых динамично развивающихся проектов в мире. Драйверы занимают большую часть ядра Linux и в большинстве случаев именно ошибки в драйверах приводят к падению системы. Осуществлять проверку драйверов ОС Linux вручную достаточно трудоемко.
Система для выявления состояний гонки в ядре Linux
Важным классом ошибок в программах являются состояния гонки: ситуации, когда несколько потоков одновременно пытаются получить доступ к одним и тем же данным, причем хотя бы один из них выполняет запись. Ошибки этого класса становятся более распространенными и более опасными с развитием многопроцессорных и многоядерных систем, особенно в таких принципиально работающих параллельно программных средах, как ядро операционной системы.
Тестирование автоматизированных процессов
Для крупных компаний, где количество клиентов исчисляется миллионами, а сотрудников тысячами, автоматизация повседневных задач не просто важна, она определяет способность компании развиваться. Проблема автоматизации процессов в которые вовлекаются различные системы, зачастую принадлежащие разным компаниям, относительно нова. Один из важных аспектов этой проблемы - тестирование. Тестирование таких процессов должно масштабироваться от уровня отдельных модулей до уровня программных систем. При таком масштабировании возникают "бытовые" проблемы с обеспечением целостности процесса тестирования - теряются сведения о покрытии, невозможно проследить требования, процесс в целом становится неуправляем. На семинаре, на примере опыта работы с Вымпелком, будет представлен обзор актуальных проблем тестирования процессов и ряда перспективных методов их решения.
Методы инструментирования Си-программ для поиска ошибок с помощью статического анализа кода
Для того, чтобы программы работали корректно, при разработке программисты должны придерживаться определенных правил. Как показал анализ изменений в драйверах ядра операционной системы Linux, одним из основных источников ошибок в драйверах является нарушение драйверами правил использования интерфейса ядра. На сегодняшний день перспективным подходом к автоматизированному обнаружению ошибок является статический анализ кода. Для его применения требуется некоторым образом задавать проверяемые свойства программы.
Стандарт DO-178B содержит требования к процессам разработки бортового ПО воздушных судов гражданской авиации. Бортовое ПО подлежит обязательной сертификации, в ходе которой проверяется соответствие процессов разработки ПО требованиям стандарта. Помимо прочего стандарт определяет MC/DC - структурный критерий тестового покрытия на основе потока управления. Стандарт требует, чтобы исходный код наиболее критичных с точки зрения надежности модулей бортового ПО был покрыт функциональными тестами по MC/DC. В связи со сложностью обеспечения покрытия по MC/DC в реальной практике разработки бортового ПО для измерения покрытия используют специализированные программные инструменты. Целью настоящей работы является выявление ограничений и слабых мест данных инструментов.
Автоматизация тестирования моделей аппаратуры на основе статического анализа HDL-описаний
В настоящее время активно развиваются различные методы и инструментальные средства верификации аппаратуры. При этом сохраняет свою актуальность задача автоматизации тестирования. В докладе будут кратко рассмотрены существующие подходы к решению данной задачи, а также предложена идея метода построения прототипов тестовых систем, основанного на статическом анализе HDL-описаний.
Разработка, реализация и анализ производительности модифицированного транспортного протокола
В докладе представлен протокол транспортного уровня TCP TIPS, разработанный для эффективного использования доступной пропускной способности проводной, беспроводной и гетерогенной сети, обеспечивающий передачу данных, не вызывающую рост задержек. Протокол TCP TIPS использует отправку данных через определенные интервалы времени (TCP pacing), задающие скорость передачи данных. Он не использует такие механизмы как окно перегрузки и пороговое значение медленного старта, вместо этого контролируя значения межсегментных интервалов, применяемых отправителем, с помощью алгоритмов оценки доступной пропускной способности сети и управления потоком данных, основанных на анализе значений межсегментных интервалов, наблюдаемых получателем.
Методы синтеза установочных и различающих экспериментов с недетерминированными автоматами
Методы синтеза умозрительных экспериментов развиваются с 1956 г., когда Э. Мур определил понятие эксперимента с конечным автоматом в одноименной статье. Тем не менее, большая часть известных результатов по синтезу различающих (диагностических) и установочных экспериментов получена для детерминированных автоматов. Исследования, посвященные синтезу таких экспериментов для недетерминированных (неинициальных) автоматов, только начинают развиваться, и известные результаты по синтезу условных и безусловных различающих экспериментов покрывают только класс автоматов с двумя начальными состояниями.
Верификация драйверов операционной системы Linux при помощи предикатных абстракций
В работе ставится задача верификации драйверов операционной системы (ОС) Linux. Верификация драйверов ОС Linux является критически важной задачей, так как драйверы - это большой, стремительно растущий класс программных систем, а поскольку драйверы работают с тем же уровнем привилегий, что и остальное ядро, то корректность драйверов является необходимым условием обеспечения надежности и безопасности систем.
Динамическая верификация цифровой аппаратуры на основе формальных спецификаций
Сложные системы, к которым относится цифровая аппаратура, проектируются от общего к частному: сначала создается обобщенное представление системы, может быть создана ее модель, затем происходит декомпозиция системы на составные части, определяется порядок их взаимодействия. Подобным же образом может проводиться и верификация, причем определенная технология построения тестовых систем может помочь достичь большого уровня повторного использования их обобщенных частей, что существенно экономит ресурсы на их разработку. Также следует отметить, что для аппаратуры характерен высокий уровень параллелизма, что приводит к конкурентному доступу к общим ресурсам и «комбинаторному взрыву» числа состояний.
Исследование и разработка методов и средств обеспечения интероперабельности в облачных вычислениях