Интересная история, где неправильное поведение в quick-lint-js было следствием бага в GNU Binutils.

https://quick-lint-js.com/blog/bug-journey/

David R. MacIver, создатель Hypothesis, анонсировал shrinkray - модуль на Питоне для минимизации тестовых данных. С одной стороны он утверждает, что результаты и скорость работы должны быть лучше чем у подобных инструментов (creduce, cvise, halfempty, dd etc), а с другой стороны "он не удивится, если это будет не так" :-)

> It should produce better results than all of the ones that are basically delta-debugging variants, because delta debugging isn't actually very good. I would also expect it to produce better results than HDD-based ones but am less confident. It's likely also often faster, but I'm less confident of this too.

У Давида получилась удобная библиотека для PBT-тестирования, думаю что shrinkray тоже со временем станет стоящим инструментом.

https://github.com/DRMacIver/shrinkray

TLA+ 2023 survey

https://docs.google.com/forms/d/e/1FAIpQLScmEprc8WcXzNoRqYO8qeO8TS83FRlTrN2qYOCu8ORfoea6Gg/viewform

В начале ноября в рамках Семинара по семантике, спецификации и верификации программ PSSV-2023 проходили соревнования по верификации моделей и дедуктивной верификации aka контест VeHa. В контесте было два трека: задачи по дедуктивной верификации (проверка правильности программы относительно ее формальной спецификации с помощью системы логических правил вывода) и задачи по модел-чекингу (превращение программы на формальном языке в систему переходов и проверка ее свойств с использованием темпоральных формул). Организаторами выступили преподаватели и сотрудники Института Систем Информатики, Института Автоматики и Электрометрии СО РАН, СПбПУ и НГУ, а основной целью мероприятия организаторы ставили ознакомление участников с автоматизированными средствами формальной верификации и заданием формальных требований.

Здорово, что у нас проводят мероприятия призванные ознакомить и популяризовать методы формальной верификации и спецификации среди студентов. Особенно хочется отметить прикладной характер задач, предложенных в контесте (см. ниже). Пусть предлагалось использовать не самые популярные инструменты для этих целей (SPIN/Promela и C-lightVer), но ведь не это главное.

В первой задаче начального уровня по модел-чекингу предлагалось смоделировать проблему станции "Луна-25". Легенда всем известа из новостей: "19 августа 2023 года при выдаче корректирующего импульса для перевода космического аппарата с круговой окололунной орбиты на эллиптическую предпосадочную орбиту двигательная установка «Луны-25» проработала 127 секунд вместо запланированных 84 секунд. В итоге станция перешла на нерасчетную незамкнутую орбиту и столкнулась с лунной поверхностью. Установлено, что наиболее вероятной причиной аварии «Луны-25» стало нештатное функционирование бортового комплекса управления, связанное с невключением блока акселерометров в приборе БИУС-Л (блок измерения угловых скоростей) из-за возможного попадания в один массив данных команд с различными приоритетами их исполнения прибором. В связи с этим в бортовой комплекс управления приходили нулевые сигналы с блока акселерометров прибора БИУС-Л. Это не позволило при выдаче корректирующего импульса зафиксировать момент набора требуемой скорости и произвести своевременное выключение двигательной установки космического аппарата, в результате чего ее отключение произошло по временной отсечке.". Далее необходимо было на языке Promela формализовать взаимодействие модулей станции и найти сценарий, приводящий к ошибке, описанной в СМИ. Полное описание задачи.

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

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

В задаче по дедуктивной верификации предлагалось задать формальные спецификации программы, предназначенной для решения такой проблемы миссии "Луна-25", как проверка равенства всех приоритетов в массиве команд, и провести автоматическую дедуктивную верификацию данной программы в системе C-lightVer. Полное описание задачи.

Рубрика: видео на выходные.

Доклад "Gain confidence in system correctness & resilience with formal methods" с "AWS re:Invent 2023".

https://www.youtube.com/watch?v=FdXZXnkMDxs

Если до этого читали статьи об использовании формальных методов в Амазоне (CBMC: "Model checking boot code from AWS data centers", TLA+: "Use of Formal Methods at Amazon Web Services"), то в доклад в основном про использование языка P (What is P?) для моделирования распределённых сервисов.

Рабочая группа по разработке C++ одобрила новый синтаксис описания контрактов, в новой версии отсутствуют квадратные скобки.

Пример кода с контрактами:

int f(int x)
pre (x > 0)
post (r: r > x)
{
contract_assert(i > 0);
return x + i;
}

https://wg21.link/p2961r2

Контракты можно было использовать и раньше, но для этого надо было использовать внешние библиотеки. Документ предлагает нативную поддержку контрактов в языке. Интересна секция 5.3.2, где описывается использование существующих библиотек для контрактов в проектах с открытым кодом и их популярность.

Экспериментальная поддержка контрактов реализована в GCC, включить можно опциями -fcontracts -fcontracts-nonattr.

Как-то давно сам хотел добавить поддержку контрактов в Go, не очень успешно впрочем.

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

https://lyra.horse/misc/chromium_vrp_tree.html

20 советов по тестированию от Russ Cox:

1. Make it easy to add new test cases.
2. Use test coverage to find untested code.
3. Coverage is no substitute for thought.
4. Write exhaustive tests.
5. Separate test cases from test logic.
6. Look for special cases.
7. If you didn’t add a test, you didn’t fix the bug.
8. Not everything fits in a table.
9. Test cases can be in testdata files.
10. Compare against other implementations.
11. Make test failures readable.
12. If the answer can change, write code to update them.
13. Use txtar for multi-file test cases.
14. Annotate existing formats to create testing mini-languages.
15. Write parsers and printers to simplify tests.
16. Code quality is limited by test quality.
17. Scripts make good tests.
18. Try rsc.io/script for your own script-based test cases.
19. Improve your tests over time.
20. Aim for continuous deployment.

То же самое, но голосом - https://research.swtch.com/testing

4-5 декабря прошла конференция ISP RAS Open, которую из года в год организует ИСП РАН. Я в основном был на секции, посвященной SDL, но в других залах тоже было интересно. Например в Синем зале было много докладов, по теме фаззинга и модел-чекинга:

Доклады секции «Технологии анализа, моделирования и трансформации программ» (Синий зал):

1-й день, видеозапись https://www.youtube.com/watch?v=_PMywI4MTL0 (таймкоды в описании видео)

- Разработка прототипа безопасного компилятора на основе Clang
- Программный комплекс для измерения производительности базовых блоков на современных ЦПУ
- Разработка инструмента автоматического обнаружения гонок при параллельной сборке с использованием утилиты Маке
- Автоматизированная генерация модульных тестов для Java-программ при помощи фаззинга
- Проверка программ на соответствие стандарту MISRA С с использованием инфраструктуры Clang
- Обнаружение возможной перезаписи переменных вследствие использования функций нелокальных переходов
- Статический анализ языка со: контролируемая сборка
- Повышение точности моделирования библиотечных функций в статическом анализаторе
- Статический анализ на основе обобщенного абстрактного синтаксического дерева
- Повышение масштабируемости межмодульного статического анализа помеченных данных

2-й день, видеозапись https://www.youtube.com/watch?v=oMpSgMFFiXc (таймкоды в описании видео)

- Метод надежной пространственной изоляции для ARINC 653 OCPB
- Извлечение опорных тестовых наборов из спецификаций криптопротоколов на предметно-ориентированном языке
- Эффективное дополнение авто-активной верификации программ дедуктивными доказательствами
- Инструмент для поиска гонок по данным RaceHunter
- Моделирование операционных, программных и и технических систем в проектах РФФИ 2016-2022
- Награждение победителей контеста Veha
- Результаты переработки уровней ролевого управления доступом и мандатного контроля целостности формальной модели управления доступом ОС Astra Linux
- К моделированию системы обработки прерываний Linux для SMP систем
- Автоматический поиск фазз-блокеров
- Метод мутации сложноструктурированных входных данных при фаззинг тестировании JavaScript интерпретаторов
- Предикат безопасности для ошибки целочисленного усечения
- Фаззинг полиморфных систем в структурах микросервисов
- Язык программирования для обучения технологиям компиляции и трансформации
- Исследование возможности идентификации веб-сайтов, посещаемых пользователем, на основе НТТР/2 трафика

Test of Time Award

Есть такая премия Test of Time, учрежденная в 2017 году. Присуждается за выдающиеся статьи, опубликованные за последние 10 лет на одной из конференций ETAPS. Сейчас открылось голосование за статьи, опубликованные с 2014 по 2024. На сайте можно посмотреть статьи, взявшие премию в предыдущие года, и интересно, что три раза за последние семь лет побеждали статьи про модел чекинг.

https://etaps.org/awards/test-of-www.tg-me.com/

Лампорт опубликовал черновик своей новой книги с предварительным названием "A Science of Concurrent Programs". Если "Specifying Systems" больше про использование TLA+, то эта книга рассказывает про научные принципы, лежащие в основе языка TLA+ и почему TLA+ такой, какой он есть. Лампорт предупреждает, что книга содержит много математики. Вообще Лампорт классно объясняет и если например выбирать книгу про TLA+ между Specifying Systems и Practical TLA+, то мой выбор будет за первой. Из новой книги я успел прочитать только первую главу и стиль написания Лампорт не поменял.

https://lamport.azurewebsites.net/tla/science.pdf

Слайд Bryan Cantrill из доклада "Things I Learned the Hard Way". Он рассказывает чему и где он учился в течение своей карьеры и какие знания достались ему легко, а какие с трудом.

Источник: https://speakerdeck.com/bcantrill/things-i-learned-the-hard-way?slide=6

На прошлой неделе закончилась POPL (Principles of Programming Languages). Трансляцию я не смотрел, но после завершения прошелся по программной сетке и посмотрел что было интересного на этой конференции. Сейчас есть только запись трансляции по залам, обычно потом нарезают на отдельные видео. Если внизу есть ссылка на запись, значит это прямая ссылка на доклад в видео.

How Hard is Weak-Memory Testing?

Страница доклада, препринт публикации.

Weak Memory Demands Model-based Compiler Testing

Есть такой редкий класс ошибок компилятора, когда поведение параллельной программы соответствует модели памяти целевой архитектуры, но нарушает поведение, разрешенное исходной программой в ее исходной модели. Несмотря на то, что популярные компиляторы C/C++ существуют довольно давно, такие ошибки всё еще встречаются. Авторы демонстрируют, что реализации новых процессоров все чаще используют поведение моделей расслабленной архитектуры. Таким образом, скомпилированные программы могут содержать ошибки, не встречавшиеся на старом оборудовании. Чтобы учесть ослабленное оборудование, нам необходимо тестирование компилятора на основе модели.
В результате исследования был найден баг в LLVM - [AArch64]: Atomic Exchange Allows Reordering past Acquire Fence, https://github.com/llvm/llvm-project/issues/68428

Страница доклада

Randomised Testing of the Dafny Compiler

Доклад о результатах рандомизированного тестирования компилятора Dafny https://dafny.org/. Суть исследования в разработке двух инструментов: fuzz-d для сравнительного тестирования и DafnyFuzz (где исходники?) для метаморфического тестирования. Оба инструмента в свою очередь дополняют XDsmith, который до этого успешно использовали для тестирования Dafny. С помощью всех трёх инструментов получилось найти около 30 багов в компиляторе Dafny. Дополнительно все три инструмента сравнили по трем критериям: количество найденных багов, покрытие кода по строкам и ветвлениям и покрытие кода с помощью мутационного тестирования. Спойлер: fuzz-d по всем трём критериям оказался лучше. Во время доклада также рассказали о нескольких найденных багах.

Запись трансляции, cтраница доклада.

Dafny Test Generation

Если правильно понял, то доклад про DTest, инструмент для тестирования компилятора Dafny, представленного в статье "A Toolkit for Automated Testing of Dafny".

Страница доклада, запись трансляции.

Testing Specifications In Dafny

Страница доклада, запись трансляции.

Verified Software at Scale

Название интригующе, но на странице доклада нет описания и записи трансляции я не нашел. Дайте знать, если запись где-то все-таки есть.

Страница доклада

Verifying a concurrent file system with sequential reasoning

Доклад устаойчивую к сбоям реализацию файловой системы NFS - DaisyNFS. Если правильно понял устойчивость к сбоям достигается за счет формальной верификации кода на Go с помощью Perennial.

Страница доклада, запись доклада, код проекта

String Solving for Verification

Страница доклада

UTC time, formally verified

Доклад про библиотеку FVTime, написанную с помощью Coq/MathComp, которая формализует арифметику с временными типами (Unix timestamp, UTC и високосные секунды). Если я правильно понял, то одна из основных проблем была связана с представлением Coq-типов Uint63 и Sint63 в типах MathComp nat и int и, как следствие, поддержкой тактик для этого. Вторая основная проблема была связана с объемом кода в OCaml, который получился после экстракции из Coq, - около 40 Mb.

Страница доклада, запись трансляции, публикация, код библиотеки

VCFloat2: Floating-point error analysis in Coq

Профессор Эндрю Аппель рассказывает про разработку библиотеки VCFloat2 (VCFloat с улучшениями) на Coq.

Страница доклада, запись трансляции

ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC

Страница доклада

Ownership Types for Verification of Programs with Pointer Arithmetic

Страница доклада

Memory simulations, security and optimization in a verified compiler

Доклад о реализации двух функций безопасности (стековые канарейки и аутентификация указателей) и оптимизации "хвостовая рекурсия" в компиляторе CompCert.

Страница доклада, запись трансляции

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Запись трансляции

A Fully Verified Persistency Library

Запись трансляции

An Iris Instance for Verifying CompCert C Programs

Страница доклада

CertiCoq-Wasm: Verified compilation from Coq to WebAssembly

Страница доклада, код проекта.

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Страница доклада, запись трансляции

Mechanizing Abstract Interpretation

Страница доклада, запись трансляции

Trust but Verify: Scaling Deductive Verification with Abstract Interpretation

Страница доклада, запись трансляции

Under-approximation for Scalable Bug-Detection

Запись трансляции, cтраница доклада, есть статья на эту же тему "Incorrectness Logic by Example".

Scaling Static Analyses at Facebook

Почему-то этот доклад отсутствует в программе конференции, нашел его случайно в записи трансляции одного из залов.
Сначала про Infer, статический анализатор, разаработанный командой из Facebook. Немного цифр из доклада: в FB >100k коммитов в неделю. Infer запускается на самой ранее стадии, одновременно с ревью кода, так что ревьюер видит все сообщения об ошибках, которые нашел Infer.
Потом про другой стат. анализатора Zoncolan ориентированного на поиск уязвимостей в коде. С 2017 по 2019 Zoncolan нашел 43% серьезных проблем в безопасности. Zoncolan быстрый: 100MLOC проверяет за полчаса, данные на 2019 год. Дальше докладчик сравнивает Infer и Zoncolan.

Запись трансляции

API-driven Program Synthesis for Testing Static Typing Implementations

В докладе рассказывают про новый подход к тестированию статической типизации, основанный на концепции синтеза программ на основе API. Идея состоит в том, чтобы синтезировать ресурсоемкие, но небольшие и хорошо типизированные программы, используя и комбинируя интерфейсы прикладного программирования (API), полученные из существующих программных библиотек. Наше основное предположение подкреплено реальными фактами: значительное количество ошибок типизации компилятора вызвано небольшими тестовыми примерами, в которых используются API из стандартной библиотеки тестируемого языка. Это объясняется внутренней сложностью большинства этих API, которые часто реализуют широкий спектр сложных функций, связанных с типами. Основным вкладом нашего подхода является возможность создавать небольшие клиентские программы с расширенным набором функций, не неся при этом бремя создания соответствующих правильно сформированных определений API с нуля. Для проверки различных аспектов процедур статической типизации (например, правильности и точности вывода типов) мы также обогащаем наш подход, основанный на API, режимами внедрения ошибок и сохранения семантики, а также соответствующими тестовыми оракулами. С помощью Thalia тестировали компиляторы для трех языков программирования (Scala, Kotlin и Groovy) и получилось найти 82 ошибки (76 подтвержденных и 20 исправленных), большинство из которых вызваны тестовыми примерами с использованием API, основанных на параметрическом полиморфизме, перегрузке и функциях высшего порядка.

Страница доклада, запись трансляции, код проекта

> Overall, this framework manages to successfully leverage LLMs to generate valid fuzz targets (which generate non-zero coverage increase) for 160 C/C++ projects. The maximum line coverage increase is 29% from the existing human-written targets.

https://github.com/google/oss-fuzz-gen

Я писал, что вместе со студентами в Летней школе мы сделали фаззинг тест для нашего форка LuaJIT. Тест тогда интегрировали в Tarantool CI, а непосредственно запуск теста организовали в инфраструктуре OSS Fuzz. Тогда с помощью этого теста нашли несколько багов в нашем форке и несколько багов в ванильной версии LuaJIT, которые мы конечно же отрепортили в апстрим. Значит вся работа была проделана не зря!

Первая версия теста технически была относительно простой: грамматика Lua 5.1 описана в формате Protobuf и с помощью библиотеки libprotobuf-mutator генерировались случайные структуры в формате Protobuf, которые сериализовались в программы на Lua и исполнялись в LuaJIT. Такой тест позволил нам тестировать LuaJIT с помощью синтаксически (почти, об этом ниже) корректных программ. Однако у этой версии теста была проблема: программы часто содержали зацикливания из-за рекурсивных функций и бесконечных циклов. Из-за этого тест часто зависал и тестирование завершалось по таймауту. Нужно было придумать как избегать таких проблем. Тут важно сказать, что так как мы тестируем JIT-компилятор, то функции и циклы в сгенерированных программах нам нужны чтобы включать компиляцию горячих участков кода, мы не можем убрать их из грамматики. То есть задача была такой: использовать функции с ограничением по количеству запусков и циклы с ограничением по количеству итераций. Решение заимствовали из статьи "Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs" - в каждый цикл и функцию добавили счетчик и выполнение тела функции и цикла прекращается по достижении некоторого значения.

-- Было:
while (true) do
   foo = 'bar'
   ...
end

-- Стало:
counter_0 = 0
while (true) do
    if counter_0 > 5 then
        break
    end
    ...
end

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

Стадии исполнения Lua программы в LuaJIT: лексический разбор, синтаксический разбор, интерпретация, компиляция "горячих" участков кода в трассы, частичное исполнение кода на трассах. Так как наш тест основан на грамматике, то наши программы лексически и синтаксически корректные, они выполняются в виртуальной машине и, возможно, часть Lua-кода компилируется. Вопрос: а как часто работает JIT-компилятор? Мы добавили в тест сбор метрик, которые предоставляет LuaJIT, чтобы понять сколько программ интерпретируется, сколько программ включают компиляцию, как часто происходит выход с трасс и как часто включаются снапшоты (выход в интерпретатор). Такие метрики дали больше контроля над тестированием.

Теперь стало понятно, что не все программы интерпретируются успешно. В чем может быть причина? Изначально мы для исполнения кода сгенерированных программ испоьзовали т.н. protected call (lua_pcall), чтобы возможные ошибки исполнения не прерывали тестирование. Мы проанализировали ошибки исполнения и выяснили, что ошибок выполнения очень много. И часть (sic!) ошибок были синтаксическими. Как так, если мы грамматику используем? Дело в том, что в Lua некоторые операторы могут использоваться не в любом месте программы. Например после return не может быть других выражений, break может использоваться не в любом месте программы, оператор variable arguments (...) может использоваться только в основном теле программы или в функциях, в которых один из аргументов это variable argument. Такие ошибки исправили за счет добавления контекста в сериализаторе. Только решение проблем из-за неверного использования return и break позволило избавиться от 42% ошибок.

В своем докладе я рассказывал про семантические ошибки в сгенерированных программах. Львиная доля ошибок в сгенерированных программах были из-за нарушения семантики: использование операций над типами, которые эти операции не поддерживают: сложения таблиц, возведение строк в степень и т.д., некорректные значения для оператора for и другие менее редкие проблемы. Решение проблемы с использованием неподдерживаемых операций получилось интересным. В Lua для каждого объекта или типа можно определить метаметод, который позволит применять стандартную Lua операцию для этого объекта или типа. То есть для сложения надо определить метаметод __add, для вычитания __sub и т.д. Если мы реализуем недостающие метаметоды, то выполнение программы не будет прерываться из-за ошибки. Да, такие метаметоды в большинстве своем бесмыссленны, зато какие бенефиты: большая часть программ начинает выполняться и доходит до компиляции, сгенерированные программы чаще используют метаметоды и метатаблицы, это повышает покрытие кода. Ещё один плюс заключается в том, что мы минимально меняем сериализацию, программы остаются такими же, мы только меняем их поведение. Решение нам понравилось и мы его реализовали в тесте.

Полученный результат я считаю хороший: до проделанных изменений 61% программ были с ошибками, после всех изменений их количество снизилось до нуля. Если быть совсем точным, то одна ошибка все-таки осталась - main function has more than 200 local variables, но встречается она редко. Покрытие кода для LuaJIT выросло, вырос процент программ с трассами (+44%), процент программ со снапшотами (+40%) и количество программ с прерванными трассами (+31), значит JIT-компилятор работает гораздо чаще и количество переключений между виртуальной машиной и выполнением трасс выросло.

Какие выводы из этой работы можно сделать? Работать над генератором программ для тестирования языковых рантаймов можно и нужно, работа нетривиальная, но оно того стоит. Какие-то ошибки исполнения можно исправить статически, а какие-то только в динамике, во время выполнения программы.

Нашел мем про Alloy Analyzer.

Все любят понятные и стабильные репродьюсеры, но не все хотят и любят их делать.

В GLibc и Musl отличается работа с разделяемыми библиотеками. Мне понравился репродьюсер, который демонстирует эту разницу в поведении. Если собрать тестовую библиотеку и исполняемый файл, код которых приведен ниже, с GLibc и c Musl и потом запустить исполняемые файлы, то разница в поведении становится наглядной:

$ make 
Build with GLibc
=^-^=
=^-^=
=^-^=
Build with Musl
=^-_-^=

#include "stdio.h"

const char* s = "-_-";
int i = 0;

__attribute__((constructor))
static void before() {
    printf("=^");
}

void f() {
    printf("%c", s[i++]);
}

__attribute__((destructor))
static void after() {
    printf("^=\n");
}

#include "dlfcn.h"

int main()
{
    for (int i = 0; i < 3; i++) {
        void* a = dlopen("./liba.so", RTLD_LAZY);
        void(*f)() = dlsym(a, "f");
        f();
        dlclose(a);
    }
}