Математические модели вычислений

Вводное занятие

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

Я — Максим Александрович Кривчиков, к.ф.-м.н., с.н.с. МГУ имени М. В. Ломоносова

maxim.krivchikov@gmail.com

Материалы курса: https://maxxk.github.io/formal-models/

Обзор курса

В этом семестре — более теоретические вопросы:

• каким образом в принципе можно что-то доказывать про программы
• какие математические модели используются для описания вычислений
• теоретические положения программирования с зависимыми типами этот подход тесно связан с активно развивающимся направлением современной математики — теорией типов

В следующем семестре («Математические модели программ и языков программирования», на английском языке) — практические вопросы:

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

Общая информация

Основные материалы для подготовки — по презентациям; по основным темам будут ссылки на литературу для расширенного изучения (в том числе — список литературы к билетам).

Любые возникающие вопросы лучше задавать прямо по ходу занятия.

Зачёт/экзамен

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

В рамках курса будут даваться задания для самостоятельного выполнения «со звёздочками». По итогам курса: 10* — «автомат» (попрошу ответить на один вопрос, но ответ не будет влиять на оценку), 6* — нужно ответить на один вопрос, 3* — на два вопроса, менее 3* — на три вопроса из билета.

Принимаются предложения по семестровым проектам и инициативным заданиям, не включённым в список, но позволяющим лучше иллюстрировать темы курса.

Похожие курсы в других университетах мира

Первый семестр:

• CMU (US) 15-819 Homotopy Type Theory
• Университет Стокгольма (Швеция) MM8036 ht15 Type Theory
• Университет Неймегена (Нидерланды) IMC010: Type Theory and Coq
• Университет Ноттингема (Великобритания) G52IFR Introduction to Formal Reasoning

Второй семестр:

• Cornell University (US) CS4110–CS6110
• University of Edinburgh INFR11114 Types and Semantics for Programming Languages
• University of Texas in Dallas CS 6371: Advanced Programming Languages

Программы пишут на разных языках программирования

С JavaScript:

• 5.9% (74) без языков программирования (ЯП),
• 40.5% (509) используют один ЯП,
• 26.8% (337) используют два ЯП,
• 26.8% (336) используют три и более ЯП.

Без JavaScript и репозиториев без языков

• 51.6% (239) используют один ЯП,
• 25.5% (118) используют два ЯП,
• 22.8% (106) используют три и более ЯП.

Данные получены по 1256 репозиториям GitHub, наиболее популярных по количеству голосов пользователей и по количеству производных репозиториев в 2013 году.

Программы модифицируются и усложняются

GNU gzip (утилита для сжатия данных)

версии 1.2.4 – 1.6 (1993–2013) × 6 файлов, × 7 строк (34 ⟶ 216 файлов, 5.8 ⟶ 42 тыс. строк кода)

Ядро ОС FreeBSD для архитектуры i386

версии 2.0.5 – 8.4 (1995–2013)

× 8 файлов, × 12 строк (1066 ⟶ 8860 файлов, 280 ⟶ 3380 тыс. строк кода)

Данные получены утилитой CLOC 1.60 для следующих типов файлов: C, C++, C/C++ Header

Программы содержат ошибки

Coverity Scan Open Source Report 2013:

Статический анализ кода 741 Open Source проекта от  ≈10 тыс. строк до ≈8 млн строк, в среднем ≈340 тыс. строк на проект.

Плотность обнаруженных ошибок: 0.59 на 1 тыс. строк кода. Для небольших проектов масштаба gzip (42 тыс. строк) — в среднем 24 ошибки обнаружено.

В.В. Липаев отмечал [1]:

• высококачественное ПО имеет плотность порядка 0.20 ошибок на 1 тыс. строк кода
• существующими средствами достижима минимальная плотность порядка 0.05 ошибок на 1 тыс. строк кода

[1] Липаев В.В. Программная инженерия. Методологические основы: Учебник

Ошибки в программах могут приводить к серьёзным последствиям

Уязвимости в ПО

• OpenSSL Heartbleed (CVE-2014-0160) — значительная часть TLS-серверов в Интернет (популярные дистрибутивы Linux — Debian-based, RedHat-based; OpenBSD, FreeBSD, NetBSD, роутеры Cisco, Juniper, …) имели уязвимость в течение более 1 года
• (подставьте уязвимость, о которой вы читали за последние полгода, за исключением различных тайминг-атак)

Недокументированные возможности

• Volkswagen (2015) — занижались данные по выбросам вредных веществ дизельными двигателями, компанию ожидает штраф до 18 млрд. долл.

...и даже к катастрофическим

Уязвимости в ПО

• Stuxnet, Иранская ядерная программа (2009) — предположительно, повреждены центрифуги, используемые при обогащении урана

Некорректная работа ПО

• «Фобос-Грунт» (2011) — утрачена автоматическая межпланетная станция, ущерб ≈5 млрд руб.
• Панама, установки лучевой терапии (2000-2001) — пострадало 28 человек, погибло не менее 5
• Therac-25, установки лучевой терапии (1985-1987) — 6 пострадавших, 3 погибших
• FADEC (Chinook HC.2), отказ ПО управления двигателем вертолёта — одна из вероятных причин крушения в 1994 г. — 29 погибших

Airbus (ArsTechnica, BBC)

As Ars reported on May 19, Airbus had issued a warning to its military customers about a potential software problem in the engine control software for the A400M. The release of the exact cause of the crash, however, had been delayed because a Spanish magistrate placed the flight data recorders from the aircraft under seal. Airbus has since been able to obtain the flight data, which Lahoud said confirms that the engine control software had been improperly configured during the installation of the engines on the ill-fated aircraft.

"The black boxes attest to that," Lahoud told Handelsblatt. "There are no structural defects, but we have a serious quality problem in the final assembly." The error was not in the code itself, but in configuration settings programmed into the electronic control unit (ECU) of the engines.

It said the focus of the inquiry was a theory that files known as "torque calibration parameters" had been accidentally deleted during a software installation process ahead of the plane's first flight. A source later confirmed this to the BBC. The control systems of the A400M aircraft are heavily automated. Each engine is run by a separate computer called an Electronic Control Unit. The ECUs take the pilot's inputs and make the engines they control respond in the optimum way. The parameter files are used by the ECUs to interpret sensor readings about the turning force generated by each engine - the torque - which is used to make the attached propellers spin. Without the files, the ECUs cannot make sense of this data.

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

верификация

процесс, целью которого является показать соответствие продукта, сервиса или системы требованиям, спецификациям и другим условиям, которые накладываются на продукт

валидация

процесс, целью которого является определить адекватность продукта, сервиса или системы потребностям заказчика

Рецензирование (code review)

— экспертный контроль качества кода.

1. Формализованный процесс (например, Fagan inspection)
   • отдельная стадия разработки
   • большое количество участников и ролей
   • несколько этапов
   • критерии
2. Неформализованный процесс
   • рецензирование «из-за спины»
   • наборы изменений по email
   • парное программирование
   • средства рецензирования (например, Reviewable или встроенные в GitHub, GitLab)
   • pull-requests

Рецензирование в Mozilla

Проект Servo (перспективный параллельный движок Web-браузера)

• разработка ведётся на GitHub
• все изменения в код вносятся в отдельных ветках, которые вливаются в основную после рецензирования

Пример запроса на внесение изменений (pull request) с рецензией: Prefetch img, scripts and stylesheets during parsing

Рецензирование в Chromium

Пример набора изменений с рецензией: https://codereview.chromium.org/1234223005/#ps260001

Рецензирование в ядре ОС Linux

Для ядра ОС Linux (десятки тысяч разработчиков) используется распределённая система на основе email. По словам ведущих разработчиков, никакие другие существующие средства не работают на таком масштабе.

Пример набора изменений с рецензией: https://lkml.org/lkml/2015/10/1/521

Средства рецензирования в GitHub

https://github.com/servo/webrender/pull/397

https://github.com/rust-lang/rust/pull/36592

(Динамическое) тестирование

• процесс исследования, выполняемый с целью предоставления «заказчикам» информации о качестве продукта или сервиса.
• (отдельная большая тема)
• классификации:
  • ручное или автоматизированное
  • методы чёрного/белого/серого ящика
  • модульное (юнит-) тестирование, интеграционное, интерфейсное, системное, приёмочное
  • регрессионное тестирование
  • smoke-тестирование, sanity-тестирование
  • функциональное или нефункциональное тестирование (производительность, безопасность, живучесть, удобство использования)

Автоматизированные модульные тесты

describe("simple parsers", function() {
  it("regex", () => {
    const p = pr.regex(/h(i)?/);
    (() => p.run("no")).should.throw(/h\(i\)\?/);
    const rv = p.execute("hit");
    rv.state.pos.should.equal(2);
    rv.value[0].should.eql("hi");
    rv.value[1].should.eql("i");
  });
})

TDD / BDD

Test Driven Development / Behaviour Driven Development

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

Пример: https://github.com/orfjackal/tdd-tetris-tutorial — пишем Tetris на Java с использованием TDD (есть скринкасты)

1. FallingBlocksTest
2. RotatingPiecesOfBlocksTest
3. RotatingTetrominoesTest
4. FallingPiecesTest
5. MovingAFallingPieceTest
6. RotatingAFallingPieceTest
7. And beyond…

Регрессионные тесты

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

Применимы в том числе и к нефункциональным требованиям (например, производительность: https://arewefastyet.com/):

Приблизительная схема работы:

1. Получаем сообщение об ошибке.
2. Воспроизводим ошибку.
3. Пишем тест, который автоматически воспроизводит ошибку.
4. ???
5. Всё работает.

Пример:

• сообщение об ошибке: https://github.com/meteor/meteor/issues/2691
• тест: https://github.com/meteor/meteor/pull/5038

Формальные методы в тестировании

model-based testing или specification-based testing: тесты генерируются автоматически на основе спецификации программы

• библиотека QuickCheck языка программирования Haskell (и производные для большого количества других языков программирования) автоматически генерирует тестовые данные для опровержения гипотез о поведении функции и пытается свести такие контрпримеры к минимальному размеру;
• теория конформности (И.Б. Бурдонов, ИСП РАН)

Fuzzing

— автоматическое или полуавтоматическое тестирование на большом наборе корректно (или некорректно) сгенерированных входных данных.

тестирование на основе спецификации входных данных:

• Csmith, генератор случайных корректных C-программ для тестирования компиляторов
• http://www.cs.utah.edu/~regehr/papers/pldi13.pdf
• American Fuzzy Lop, использует генетические алгоритмы для автоматического подбора наборов входных данных, обеспечивающих максимальное покрытие целевого кода. Пример использования — Pulling JPEGs out of thin air

Дополнительно: https://fuzzing-project.org/

Статический анализ

• автоматизированная проверка исходного кода (статический = без запуска программы) алгоритмом, который предназначен для поиска того или иного класса дефектов.
• фундаментальное ограничение: автоматическое доказательство свойств произвольных программ неразрешимо.

Одно из основных свойств — достоверность (soundness) или недостоверность.

Достоверные методы статического анализа не дают ложных отрицательных результатов (но дают ложные положительные).

Примеры «недостоверных» средств

Коммерческие средства:

• Coverity — использовалось для статистики на слайде 9

• PVS-Studio (российская разработка)

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

  static int crypt_iv_tcw_whitening(....) {
    ....
    u8 buf[TCW_WHITENING_SIZE];
    ....
    out:
    memset(buf, 0, sizeof(buf));
    return r;

Средства с открытым исходным кодом:

• Clang-analyzer

Статический анализ — достоверные средства

• Frama-C, OpenSource, пример

int max_array(int* a, int length) {
  int m = a[0];
  /*@
  loop invariant 0<=i<=length; loop invariant
  \forall integer j; 0<=j<i ==> m >= a[j]; loop invariant
  \exists integer j; 0<=j<i && m == a[j]; loop assigns i,m;
  */
  for (int i = 1; i<length; i++) {
    if (a[i] > m) m = a[i]; }
  return m;

• Polyspace, коммерческое средство от разработчиков MATLAB, на сайте есть примеры

Динамический анализ

• автоматизированная проверка кода и состояния программы в процессе исполнения алгоритмом, который предназначен для поиска того или иного класса дефектов.
• вносит изменения в процесс исполнения программы.
• в целом, имеет те же фундаментальные ограничения, что и статический анализ.
• пример: valgrind позволяет обнаруживать какая строка кода вызывает ошибку работы с памятью (использование после освобождения и выход за границы массива), кроме того содержит средства для профилирования и оценки использования кеша процессора.
• пример: в комплект с современными компиляторами GCC и Clang входят так называемые «санитайзеры» — библиотеки, которые обнаруживают выходы за границы массива, утечки памяти и т.д.

Распространённые подходы не гарантируют отсутствия ошибок

• Рецензирование
  • зависит от экспертного мнения;
  • не автоматизировано;
  • на больших объёмах кода сложно в применении.
• (динамическое автоматизированное) тестирование
  • большой объём кода тестов по сравнению с кодом продукта (SQLite: 80 тыс. строк кода / 90 млн. строк тестов);
  • тесты необходимо поддерживать в актуальном состоянии;
  • тесты не гарантируют отсутствия дефектов/ошибок.
• Статический и динамический анализ
  • нетривиальные свойства неразрешимы согласно теореме Райса;
  • большое количество ложных срабатываний;
  • на практике встречаются дефекты, необнаружимые средствами статического анализа (OpenSSL Heartbleed bug: информация раскрыта 7 апреля 2014 г., адаптированные средства статического анализа появились 18 апреля 2014 г.).

Формальная верификация

• процесс, результатом которого является получение строгого математического доказательства соответствия программы требуемой спецификации, наличия у программы требуемых свойств.

Недостатки:

• является трудоёмким и наукоёмким процессом
• не имеет широкого распространения (в отличие от формальной верификации аппаратного обеспечения)

Область применимости формальной верификации:

• риски, превышающие затраты на верификацию
• сложность системы

Разработку программы необходимо вести с учётом требований по её формальной верификации.

SeL4 — 3 тыс. строк формальных спецификаций, 10 тыс. строк кода на C, 100 тыс. строк формальных доказательств.

Проблематика формальной верификации

• программа — это нестрого определённый объект реального мира (исполнимый код? исходный код? алгоритмы?)
• требования — это нестрого определённые представления заказчика о том, как должна выглядеть программа
• если достаточно детализировать спецификацию, не станет ли она сложнее, чем программа?
• не определено, чему можно доверять — и ОС, и стандартная библиотека, и компиляторы, и даже аппаратная реализация системы команд процессора содержат ошибки и могут вносить ошибки в процесс работы программы (пример — ошибка в реализации расширения TSX транзакционной памяти в процессорах семейства Haswell)

Системы типов и верификация

• в языке программирования со статической типизацией компилятор на этапе проверки типов выполняет работу статического анализатора — если компилятор принимает программу, значит она удовлетворяет спецификации с позиций безопасности типов
• «выразительные способности» систем типов разных языков программирования существенно различаются:
  • в динамических языках есть только один тип
  • на языке Go не получится создать пользовательский тип обобщённых списков, сохраняя строгую типизацию, тогда как в C, например, получится [1, 2]
  • на языках Java, C#, C++ можно задавать сложные пользовательские обобщённые типы (std::map, Dictionary<TKey, TValue>)
  • система типов языка Rust позволяет выразить понятие времени жизни объекта, владельца области памяти, а также передачу прав на чтение и запись по ссылкам;
  • язык Haskell поддерживает полноценный полиморфизм с широкими возможностями по выводу типов

  instance (Eq a, Ord a)  => Eq (Set a) where
    (Set xs) == (Set ys) = (sort xs) == (sort ys)

План на следующее занятие

Общая проблематика курса: каким образом мы можем описывать спецификации программ в понятном для машины виде.

Проблема разрешения. Машина Тьюринга. Конечные автоматы и формальные языки.

• как вышло, что модели вычислений предшествовали появлению программируемых вычислительных устройств?
• алгоритмически неразрешимые задачи