Testing a Formally Verified Compiler, David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
https://hal.science/hal-04096390
https://hal.science/hal-04096390
hal.science
Testing a Formally Verified Compiler
We report on how we combine tests and formal proofs while developing extensions to the CompCert formally verified compiler.
(продолжение отзыва на книгу "Эффективное тестирование ПО")
Давно не читал что-то на тему тестирования ПО, написанное живым языком. Напомню, что автор - преподаватель Делфтского университета, то есть человек из академии. Но несмотря на это он сумел объединить в книге и теорию и практику - каждая глава изобилует и примерами с кодом и отсылками к научным публикациям. Книга не покрывает некоторые из тем, которые полезно было бы осветить (например генерация тестовых данных), автор это понимает и честно об этом предупреждает читателя в предисловии. Книга написана на основе курса, преподававшегося в Делфтском техническом университете в течение многих лет. Сами авторы признаются, что им "было трудно найти книгу, соответствующую их представлению о том, что эффективный инженер-программист должен быть эффективным тестировщиком программного обеспечения". Потому что "многие академические учебники соредоточены на результатах исследований, а книги, ориентированные на разработчиков, посвящены конкретным инструментам или процессам."
Понравилось, что автор описывает тестирование и с точки зрения спецификации (забавно было увидеть "Вам передан набор требований для разработки", звучит немного идеалистично) и с точки зрения кода. В главе о критериях охвата он разбирает полярные мнения об отношении к покрытию кода: почему некоторые испытывают неприязнь к оценке охвата кода и почему вам не стоит всегда использовать максимальный критерий охвата, рассуждает о том, чем руководствоваться в выборе критерия охвата тестирования. Мне нравится автор своей объективностью и непредвзятостью. При возможности иллюстрирует случаями из реальной жизни (например рассказ Ричарда Хиппа о том, что ему пришлось работать целый год по 60 часов в неделю, чтобы увеличить охват кода SQLite до 100% по критерию MC/DC.).
Тема тестирования с помощью свойств представлена небольшой главой. Для введения в тему этого достаточно, остальное, как рекомендует автор прийдется узнать на практике: "Тестирование на основе свойств в большей степени требует наличия практического опыта , чем традиционное тестирование на основе примеров, поэтому экспериментируйте как можно больше.".
Глава "Качество тестового кода" рассказывает о том, как писать поддерживаемые тесты, какими чертами должен такой код обладать, как выявлять "дурно пахнущие" тесты.
Вообщем эта книга выглядит свежо на фоне всей другой литературы по тестированию ПО за последнее время и я рекомендую её всем, кто хочет узнать о современном тестировании. Есть только один момент - почему-то русскоязычный перевод был издан маленьким тиражом - всего 200 экземпляров. Даже для такой узкоспециализированной книги это очень мало. Возможно издательство будет ориентироваться на спрос и это не последний тираж.
P.S. Мои коллеги могут взять книгу в корп. библиотеке.
Давно не читал что-то на тему тестирования ПО, написанное живым языком. Напомню, что автор - преподаватель Делфтского университета, то есть человек из академии. Но несмотря на это он сумел объединить в книге и теорию и практику - каждая глава изобилует и примерами с кодом и отсылками к научным публикациям. Книга не покрывает некоторые из тем, которые полезно было бы осветить (например генерация тестовых данных), автор это понимает и честно об этом предупреждает читателя в предисловии. Книга написана на основе курса, преподававшегося в Делфтском техническом университете в течение многих лет. Сами авторы признаются, что им "было трудно найти книгу, соответствующую их представлению о том, что эффективный инженер-программист должен быть эффективным тестировщиком программного обеспечения". Потому что "многие академические учебники соредоточены на результатах исследований, а книги, ориентированные на разработчиков, посвящены конкретным инструментам или процессам."
Понравилось, что автор описывает тестирование и с точки зрения спецификации (забавно было увидеть "Вам передан набор требований для разработки", звучит немного идеалистично) и с точки зрения кода. В главе о критериях охвата он разбирает полярные мнения об отношении к покрытию кода: почему некоторые испытывают неприязнь к оценке охвата кода и почему вам не стоит всегда использовать максимальный критерий охвата, рассуждает о том, чем руководствоваться в выборе критерия охвата тестирования. Мне нравится автор своей объективностью и непредвзятостью. При возможности иллюстрирует случаями из реальной жизни (например рассказ Ричарда Хиппа о том, что ему пришлось работать целый год по 60 часов в неделю, чтобы увеличить охват кода SQLite до 100% по критерию MC/DC.).
Тема тестирования с помощью свойств представлена небольшой главой. Для введения в тему этого достаточно, остальное, как рекомендует автор прийдется узнать на практике: "Тестирование на основе свойств в большей степени требует наличия практического опыта , чем традиционное тестирование на основе примеров, поэтому экспериментируйте как можно больше.".
Глава "Качество тестового кода" рассказывает о том, как писать поддерживаемые тесты, какими чертами должен такой код обладать, как выявлять "дурно пахнущие" тесты.
Вообщем эта книга выглядит свежо на фоне всей другой литературы по тестированию ПО за последнее время и я рекомендую её всем, кто хочет узнать о современном тестировании. Есть только один момент - почему-то русскоязычный перевод был издан маленьким тиражом - всего 200 экземпляров. Даже для такой узкоспециализированной книги это очень мало. Возможно издательство будет ориентироваться на спрос и это не последний тираж.
P.S. Мои коллеги могут взять книгу в корп. библиотеке.
Detecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction
https://jzuming.github.io/paper/osdi23-jiang.pdf
https://jzuming.github.io/paper/osdi23-jiang.pdf
В Perl есть модуль Mail-Sendmail и в этом модуле тест отправляет письмо на почту автору:
https://github.com/neilb/Mail-Sendmail/blob/1ba769c9c80ce35131bad412d897c55563a4c788/t/original.t#L23-L35
print <<EOT
Test Mail::Sendmail $Mail::Sendmail::VERSION
Trying to send a message to the author (and/or whoever if you edited test.pl)
(The test is designed so it can be run by Test::Harness from CPAN.pm.
Edit it to send the mail to yourself for more concrete feedback. If you
do this, you also need to specify a different mail server, and possibly
a different From: address.)
Current recipient(s): '$mail{To}'
EOT
;
https://github.com/neilb/Mail-Sendmail/blob/1ba769c9c80ce35131bad412d897c55563a4c788/t/original.t#L23-L35
GitHub
Mail-Sendmail/t/original.t at 1ba769c9c80ce35131bad412d897c55563a4c788 · neilb/Mail-Sendmail
Perl 5 module Mail::Sendmail. Contribute to neilb/Mail-Sendmail development by creating an account on GitHub.
Расшифровка доклада: О чём я говорю, когда говорю о тестировании корректности работы компиляторов
https://habr.com/ru/companies/oleg-bunin/articles/742122/
https://habr.com/ru/companies/oleg-bunin/articles/742122/
Хабр
Расшифровка доклада: О чём я говорю, когда говорю о тестировании корректности работы компиляторов
Привет, Хабр! Эта статья о том, как тестируют компиляторы. Она будет интересна разработчикам и тестировщикам компиляторов, а также всем, кто тестирует сложные технологии. Разберём проблемы...
Tavis Ormandy, исследователь из Google Project Zero, сегодня в своем блоге раскрыл новую уязвимость в процессорах AMD Zen 2. Уязвимость Zenbleed затрагивает весь стек продуктов Zen 2, от процессоров AMD EPYC для центров обработки данных до процессоров Ryzen 3000, и может использоваться для кражи конфиденциальных данных, хранящихся в процессоре, включая ключи шифрования и учетные данные для входа. Атака может быть осуществлена даже удаленно через JavaScript на веб-сайте, а это означает, что злоумышленнику не нужно иметь физический доступ к компьютеру или серверу. Если у вас процессор AMD, то обязательно обновите микрокод в процессоре.
Все, дальше не буду отбирать хлеб у ресурсов на тему информационной безопасности и лучше напишу как именно уязвимость была обнаружена.
Производители регулярно используют фаззинг для тестирования своих процессоров, для такого тестирования есть даже отдельный термин — Post-Silicon Validation. Успех этой уязвимости был обусловлен использованием нетипичного источника обратной связи для фаззера и нетипичным тестовым оракулом.
Современные фаззеры используют источник обратной связи, чтобы генерировать данные, которые будут увеличивать покрытие. Проблема в том, что ничего похожего на покрытие кода в процессорах нет. Вместо счётчиков о покрытии использовали счетчики производительности, которые изначально предназначались для профилирования производительности программ. Некоторые из этих счетчиков срабатывают когда происходят всевозможные интересные архитектурные события. Это позволило находить интересные последовательности инструкций CPU.
Самый простой тестовый оракул в генеративном тестировании это "упадет"/"не упадет": передавать в программу сгенерированные данные и проверять, что нет необработанных исключений, нет аварийных завершений программы и т.д. При нормальном поведении программа не должна давать сбоев, этот постулат и используется в тестовом оракуле. С использованием такого тестового оракула для тестирования ПО всё понятно, но как узнать, что CPU правильно выполняет случайно сгенерированную программу? Один из подходов называется реверси. Общая идея состоит в том, что для каждой случайной инструкции, которую вы генерируете, вы также генерируете обратную ей (например,
В случае с Zenbleed использовался другой тестовый оракул, который назвали "сериализованный оракул". Во время фаззинга отслеживается макроархитектурное состояние, как например значения регистров. Существует также микроархитектурное состояние, которое в основном невидимо для нас, например, предсказатель ветвлений, состояние спекулятивного выполнения инструкций и конвейер инструкций. Сериализация позволяет иметь некоторый контроль над этим, указывая CPU отключить параллельное выполнение инструкций. Основная идея сериализованного оракуласостоит в том, чтобы сгенерировать случайную программу, а затем автоматически преобразовывать её в сериализованную форму. Случайно сгенерированная последовательность инструкций и та же последовательность, но с добавлением рандомизированного выравнивания (см. пример инструкций), сериализации и спекулятивных ограждений. Эти две программы могут иметь разные характеристики производительности, но они должны выдавать одинаковый результат. Если конечные состояния не совпадают, то, должно быть, была какая-то ошибка в том, как они были выполнены на уровне микроархитектуры, что может указывать на ошибку. Так Zenbleed и обнаружили - вывод сериализованного оракула не совпал.
via
Все, дальше не буду отбирать хлеб у ресурсов на тему информационной безопасности и лучше напишу как именно уязвимость была обнаружена.
Производители регулярно используют фаззинг для тестирования своих процессоров, для такого тестирования есть даже отдельный термин — Post-Silicon Validation. Успех этой уязвимости был обусловлен использованием нетипичного источника обратной связи для фаззера и нетипичным тестовым оракулом.
Современные фаззеры используют источник обратной связи, чтобы генерировать данные, которые будут увеличивать покрытие. Проблема в том, что ничего похожего на покрытие кода в процессорах нет. Вместо счётчиков о покрытии использовали счетчики производительности, которые изначально предназначались для профилирования производительности программ. Некоторые из этих счетчиков срабатывают когда происходят всевозможные интересные архитектурные события. Это позволило находить интересные последовательности инструкций CPU.
Самый простой тестовый оракул в генеративном тестировании это "упадет"/"не упадет": передавать в программу сгенерированные данные и проверять, что нет необработанных исключений, нет аварийных завершений программы и т.д. При нормальном поведении программа не должна давать сбоев, этот постулат и используется в тестовом оракуле. С использованием такого тестового оракула для тестирования ПО всё понятно, но как узнать, что CPU правильно выполняет случайно сгенерированную программу? Один из подходов называется реверси. Общая идея состоит в том, что для каждой случайной инструкции, которую вы генерируете, вы также генерируете обратную ей (например,
ADD r1, r2 → SUB r1, r2). Любое отклонение от начального состояния в конце выполнения должно быть ошибкой. Реверсивный подход хорош, но он усложняет создание тестовых сценариев для архитектуры CISC, такой как x86.В случае с Zenbleed использовался другой тестовый оракул, который назвали "сериализованный оракул". Во время фаззинга отслеживается макроархитектурное состояние, как например значения регистров. Существует также микроархитектурное состояние, которое в основном невидимо для нас, например, предсказатель ветвлений, состояние спекулятивного выполнения инструкций и конвейер инструкций. Сериализация позволяет иметь некоторый контроль над этим, указывая CPU отключить параллельное выполнение инструкций. Основная идея сериализованного оракуласостоит в том, чтобы сгенерировать случайную программу, а затем автоматически преобразовывать её в сериализованную форму. Случайно сгенерированная последовательность инструкций и та же последовательность, но с добавлением рандомизированного выравнивания (см. пример инструкций), сериализации и спекулятивных ограждений. Эти две программы могут иметь разные характеристики производительности, но они должны выдавать одинаковый результат. Если конечные состояния не совпадают, то, должно быть, была какая-то ошибка в том, как они были выполнены на уровне микроархитектуры, что может указывать на ошибку. Так Zenbleed и обнаружили - вывод сериализованного оракула не совпал.
via
Wikipedia
Hardware performance counter
In computers, hardware performance counters (HPCs), or hardware counters are a set of special-purpose registers built into modern microprocessors to store the counts of hardware-related activities. Advanced users often rely on those counters to conduct low…
Мини-рецензия на книгу "Introduction to Software Testing" автора Panagiotis Leloudas.
Содержание книги оправдывает название - книга пытается охватить множество тем и уместить все это в 200 страниц текста. Ни в одной главе тема не освящается достаточно глубоко, везде изложение ведется в формате буллетов и тезисов. Возможно книга будет полезна тем, кто хочет быстро освоить тему тестирования ПО и за глубокими знаниями обращаться уже к книгам, которые более полно освещают представленные в этой книге темы. Тем более что для любой главы из книги можно найти соответствующую книгу, которая более основательно раскрывает тему. Плюсы книги: сжатое введение в тему, освещены вопросы, с которыми тестировщик может встретиться на практике. Минусы: читать может быть скучновато из-за формата конспекта.
Содержание книги оправдывает название - книга пытается охватить множество тем и уместить все это в 200 страниц текста. Ни в одной главе тема не освящается достаточно глубоко, везде изложение ведется в формате буллетов и тезисов. Возможно книга будет полезна тем, кто хочет быстро освоить тему тестирования ПО и за глубокими знаниями обращаться уже к книгам, которые более полно освещают представленные в этой книге темы. Тем более что для любой главы из книги можно найти соответствующую книгу, которая более основательно раскрывает тему. Плюсы книги: сжатое введение в тему, освещены вопросы, с которыми тестировщик может встретиться на практике. Минусы: читать может быть скучновато из-за формата конспекта.
Доступен код Mallory [1], расширения для Jepsen, которое помогает быстрее находить баги в распределенных системах.
> It hooks into an existing Jepsen test and takes the role of the nemesis, deciding in real-time which actions to inject and when, based on the runtime behaviour of the system under test.
По словам авторов [2] с Mallory баги можно искать быстрее:
> Compared to the start-of-the-art black-box fuzzer Jepsen, Mallory explores 54.27% more distinct states within 24 hours while achieving a speed-up of 2.24×. At the same time, Mallory finds bugs 1.87× faster, thereby finding more bugs within the given time budget. Mallory discovered 22 zeroday bugs (of which 18 were confirmed by developers), including 10 new vulnerabilities, in rigorously-tested distributed systems such as Braft, Dqlite and Redis. 6 new CVEs have been assigned
1. https://github.com/dsfuzz/mallory
2. https://pirlea.net/papers/mallory-ccs23.pdf
> It hooks into an existing Jepsen test and takes the role of the nemesis, deciding in real-time which actions to inject and when, based on the runtime behaviour of the system under test.
По словам авторов [2] с Mallory баги можно искать быстрее:
> Compared to the start-of-the-art black-box fuzzer Jepsen, Mallory explores 54.27% more distinct states within 24 hours while achieving a speed-up of 2.24×. At the same time, Mallory finds bugs 1.87× faster, thereby finding more bugs within the given time budget. Mallory discovered 22 zeroday bugs (of which 18 were confirmed by developers), including 10 new vulnerabilities, in rigorously-tested distributed systems such as Braft, Dqlite and Redis. 6 new CVEs have been assigned
1. https://github.com/dsfuzz/mallory
2. https://pirlea.net/papers/mallory-ccs23.pdf
GitHub
GitHub - dsfuzz/mallory: Greybox Fuzzing of Distributed Systems (CCS'23)
Greybox Fuzzing of Distributed Systems (CCS'23). Contribute to dsfuzz/mallory development by creating an account on GitHub.
Model Checking Guided Testing for Distributed Systems
https://muratbuffalo.blogspot.com/2023/08/model-checking-guided-testing-for.html
https://muratbuffalo.blogspot.com/2023/08/model-checking-guided-testing-for.html
Blogspot
Model Checking Guided Testing for Distributed Systems
This paper appeared in Eurosys 2023. It shows how to generate test-cases from a TLA+ model of a distributed protocol and apply it to the Ja...
"Universal Fuzzing via Large Language Models"
https://arxiv.org/pdf/2308.04748.pdf
LLM обязательно найдут себе применение в фаззинге, потому что это именно та область, где создание большого количества чуши является плюсом.
https://arxiv.org/pdf/2308.04748.pdf
LLM обязательно найдут себе применение в фаззинге, потому что это именно та область, где создание большого количества чуши является плюсом.
В этом году на конференции Strange Loop был необычный доклад.
Через год, в октябре 2024 планируется запуск на орбиту распределенного космического телескопа, т.н. миссия VISORS. Такой телескоп будет состоять из двух спутников 6U CubeSats (популярный форм-фактор для спутников) на низкой орбите. Основная цель запуска телескопа - получение высококачественных фотографий солнечной короны. Тоби поделился техниками тестирования ПО для полетов миссии, симуляционного тестирования ПО и тем, как это можно переиспользовать для тестирования других систем. В выводах в докладе нет никаких срывов покровов. Ещё автор ссылается на два других доклада про тестирование: "Testing Distributed Systems w/ Deterministic Simulation" от Will Wilson и "Simulation Testing" от Michael Nygard, оба тоже рекомендуемые к просмотру доклады.
https://www.youtube.com/watch?v=prM-0i58XBM
Через год, в октябре 2024 планируется запуск на орбиту распределенного космического телескопа, т.н. миссия VISORS. Такой телескоп будет состоять из двух спутников 6U CubeSats (популярный форм-фактор для спутников) на низкой орбите. Основная цель запуска телескопа - получение высококачественных фотографий солнечной короны. Тоби поделился техниками тестирования ПО для полетов миссии, симуляционного тестирования ПО и тем, как это можно переиспользовать для тестирования других систем. В выводах в докладе нет никаких срывов покровов. Ещё автор ссылается на два других доклада про тестирование: "Testing Distributed Systems w/ Deterministic Simulation" от Will Wilson и "Simulation Testing" от Michael Nygard, оба тоже рекомендуемые к просмотру доклады.
https://www.youtube.com/watch?v=prM-0i58XBM
YouTube
"Designing Dope Distributed Systems for Outer Space with High-Fidelity Simulation" by Toby Bell
This talk will recount the use of deterministic, high-fidelity simulation to develop the guidance, navigation, and control software for VISORS, a state of the art solar science mission, launching 2024, that will demand tight coordination between multiple…
Часто цитируют фразу Кнута: "Beware of bugs in the above code; I have only proved it correct, not tried it.".
В 98-м году он пишет:
> More than a hundred webpages ascribe that quote to me, and it sounds like something I might well have said. But lately people have been asking me for the authentic source, and I've totally forgotten where I wrote it. Probably not in a published paper, since I've written few papers in the first person that include untried code.
> My best guess is that it was in a letter I sent to somebody. So if you were that somebody, or if you have any other clues about the source of that line, please let me know.
Потом адресат того письма всё-таки нашёлся:
> On March 22, 1977, as I was drafting Section 7.1 of The Art of Computer Programming, I read four papers by Peter van Emde Boas that turned out to be more appropriate for Chapter 8 than Chapter 7. I wrote a five-page memo entitled ``Notes on the van Emde Boas construction of priority deques: An instructive use of recursion,'' and sent it to Peter on March 29 (with copies also to Bob Tarjan and John Hopcroft). The final sentence was this: ``. Beware of bugs in the above code; I have only proved it correct, not tried it.''.
В 98-м году он пишет:
> More than a hundred webpages ascribe that quote to me, and it sounds like something I might well have said. But lately people have been asking me for the authentic source, and I've totally forgotten where I wrote it. Probably not in a published paper, since I've written few papers in the first person that include untried code.
> My best guess is that it was in a letter I sent to somebody. So if you were that somebody, or if you have any other clues about the source of that line, please let me know.
Потом адресат того письма всё-таки нашёлся:
> On March 22, 1977, as I was drafting Section 7.1 of The Art of Computer Programming, I read four papers by Peter van Emde Boas that turned out to be more appropriate for Chapter 8 than Chapter 7. I wrote a five-page memo entitled ``Notes on the van Emde Boas construction of priority deques: An instructive use of recursion,'' and sent it to Peter on March 29 (with copies also to Bob Tarjan and John Hopcroft). The final sentence was this: ``. Beware of bugs in the above code; I have only proved it correct, not tried it.''.