• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Software Verification

2018/2019
Academic Year
RUS
Instruction in Russian
4
ECTS credits
Course type:
Elective course
When:
1 year, 3, 4 module

Программа дисциплины

Аннотация

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

Цель освоения дисциплины

  • подготовка студентов к теоретическому и практическому применению методов анализа программного обеспечения (ПО)
  • получение знаний в области статического анализа ПО, моделей кода, систем типов и их применения в анализе ПО
  • освоение инструментов анализа ПО
Планируемые результаты обучения

Планируемые результаты обучения

  • Знает понятия анализа и верификации ПО, основные подходы к статистическому анализу ПО, понятие абстрактного синтаксического дерева
  • Знает связь классических систем типов и анализа ПО, понятие анализа на основе ограничений, способы решения задачи присвоения типов, алгоритмы решения задачи унификации
  • Знает понятие графа потока управления и моделей на его основе, понятие частично упорядоченного множества, теорему о наименьшей неподвижной точке
  • Умеет применять на практике потокочувствительный анализ
  • Умеет решать проблемы реализации анализов на основе бесконечных решеток, применяет методы объединения widening и narrowing
  • Знает понятие чувствительности к пути исполнения, умеет применять интервальный анализ и знает проблемы, связанные с ним, знает метод уточнения абстракции на основе контрпримеров
  • Демонстрирует знание метода ограниченной проверки моделей, интерпретирует контрпримеры SMT-решателя
  • Знает понятие межпроцедурности в анализе ПО, применяет метод контекстной чувствительности на основе входных данных, знает понятие аппроксимации функции в программе
  • Умеет анализировать указатели, динамическое выделение памяти и нулевые указатели
  • Демонстрирует понимание направленного и ненаправленного анализа указателей
Содержание учебной дисциплины

Содержание учебной дисциплины

  • Основы статического анализа программ
    Введение в предмет курса. Понятия анализа и верификации ПО. Классификация методов анализа ПО. Непротиворечивость, полнота и точность анализа. Проблемы анализа ПО: теорема Тьюринга, теорема Райса. Основные подходы к статическому анализу ПО. Сигнатурный поиск. Язык TIP и его особенности. Понятие абстрактного синтаксического дерева, другие модели ПО. Анализ ПО на основе типов. Связь классических систем типов и анализа ПО. Системы типов как простейший вид анализа ПО. Полнота и точность анализа на основе систем типов. Понятие анализа на основе ограничений, типичная структура такого анализа. Применение к языку TIP. Способы решения задачи присвоения типов. Задача унификации. Алгоритмы решения задачи унификации. Рекурсивные типы и регулярная унификация. Унификационный солвер для языка TIP. Монотонный фреймворк. Понятие графа потока управления и моделей на его основе. Понятие чувствительности к потоку управления в анализе ПО. Виды потокочувствительных анализов. Абстрактный домен и абстрактное состояние. Потокочувствительный анализ знаков. Введение в теорию решёток. Понятие частично упорядоченного множества. Верхние и нижние грани. Примеры решёток, применимых в анализе ПО. Анализ знака для TIP на основе теории решёток. Теорема о наименьшей неподвижной точке. Понятие монотонного фреймворка. Алгоритмы поиска неподвижной точки. May- и must- анализ. Практическое применение потокочувствительных анализов. Анализ живости. Анализ готовых выражений. Анализ занятости. Анализ достижимых значений. Распространение констант. Примеры задач и их решений для языка TIP. Интервальный анализ. Тривиальная интервальная решётка. Проблемы реализации анализов на основе бесконечных решёток. Widening в применении к решёткам и ограничения, связанные с его применением. Narrowing в применении к решёткам и ограничения, связанные с его применением. Методы объединения widening и narrowing. Модификации алгоритма решения задачи поиска неподвижной точки с применением widening и narrowing.
  • Расширенные вопросы статического анализа программ
    Анализ ПО, чувствительный к путям исполнения. Понятие чувствительности к пути исполнения. Зависимости по данным и по управлению. Предикаты путей. Интервальный анализ, чувствительный к путям исполнения, проблемы, связанные с ним. Выбор множества предикатов путей в общем случае. Метод уточнения абстракции на основе контрпримеров (CEGAR). Метод ограниченной проверки моделей. Метод проверки моделей: применение и проблемы. Метод ограниченной проверки моделей как вид статического анализа ПО. Анализ метода ограниченной проверки моделей в сравнении с монотонным фреймворком и CEGAR. Проблема анализа циклов и раскрутка циклов как способ её решения. Задача выполнимости логических формул как способ решения задачи ограниченной проверки моделей. SAT/SMT-решатели, их ограничения и применение. Теории в основе задачи SMT и их влияние на анализ. Статическое однократное присваивание как модель кода, её преимущества в применении к рассмотренным методам анализа. Сложность и разрешимость задачи ограниченной проверки моделей ПО. Интерпретация контрпримеров SMT-решателя, проблемы и решения. Межпроцедурный анализ ПО. Понятие межпроцедурности в анализе ПО. Пессимистичный межпроцедурный анализ и проблемы, связанные с ним. Полная подстановка тела функции и проблемы, связанные с ней. Понятие полного графа потока управления для программы и анализ на его основе. Понятие контекстной чувствительности. Метод ограниченного клонирования процедур, его ограничения и параметризация. Методы улучшения контекстной чувствительности. Метод контекстной чувствительности на основе входных данных, его анализ в сравнении с методом ограниченного клонирования процедур. Понятие аппроксимации функции в программе. Проблема внешних функций и варианты её решения. Анализ памяти Проблема анализа кода с использованием памяти и указателей. Анализ указателей: анализ формы, анализ псевдонимов. Анализ динамического выделения памяти, проблемы контекстной чувствительности. Анализ нулевых указателей. Анализ указателей Расширенное определение понятия анализа указателей. Анализ псевдонимов. Анализ цели. Анализ формы. Направленный и ненаправленный анализ указателей. Алгоритм Стенсгаарда, его реализация на основе унификации. Кубический фреймворк, постановка задачи и алгоритм её решения. Алгоритм Андерсена, его реализация на основе кубического фреймворка. Контекстно-чувствительный анализ указателей. Чувствительный к потоку управления анализ указателей. Анализ указателей на основе типов. Использование анализа указателей.
Элементы контроля

Элементы контроля

  • неблокирующий Домашнее задание 1
  • неблокирующий Домашнее задание 2
  • неблокирующий Домашнее задание 3
  • неблокирующий Экзамен
Промежуточная аттестация

Промежуточная аттестация

  • Промежуточная аттестация (4 модуль)
    0.167 * Домашнее задание 1 + 0.166 * Домашнее задание 2 + 0.167 * Домашнее задание 3 + 0.5 * Экзамен
Список литературы

Список литературы

Рекомендуемая основная литература

  • Mukherjee, S., & Blasband, D. (2016). Source Code Analytics With Roslyn and JavaScript Data Visualization. [Berkeley, CA]: Apress. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=1450659

Рекомендуемая дополнительная литература

  • Forest, E. (2016). From Tracking Code to Analysis : Generalised Courant-Snyder Theory for Any Accelerator Model. Japan: Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=1178523
  • Hyde, R. (2004). Write Great Code, Volume 1 : Understanding the Machine. San Francisco, CA: No Starch Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=440094
  • van der Linden, M. A. (2007). Testing Code Security. Boca Raton, FL: Auerbach Publications. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=928213