Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее Читать полностью »
Как проверить идеи, архитектуру и алгоритмы без написания кода? Как сформулировать и проверить их свойства? Что такое model-checkers и model-finders? Что делать, когда возможностей тестов недостаточно?
Привет. Меня зовут Васил Дядов, сейчас я работаю программистом в Яндекс.Почте, до этого работал в Intel, ещё раньше разрабатывал RTL-код (register transfer level) на Verilog/VHDL для ASIC/FPGA. Давно увлекаюсь темой надёжности софта и аппаратуры, математикой, инструментами и методами, применяемыми для разработки ПО и логики с гарантированными, заранее определёнными свойствами.
Это вторая статья из цикла (первая статья тут), призванного привлечь внимание разработчиков и менеджеров к инженерному подходу к разработке ПО. В последнее время он незаслуженно обойдён вниманием, несмотря на революционные изменения в подходе и инструментах поддержки.
Many programmers struggle when using formal methods to solve problems within their programs, as those methods, while effective, can be unreasonably complex. To understand why this happens, let’s use the model checking method to solve a relatively easy puzzle:
You’re in a hallway with seven doors on one side leading to seven rooms. A cat is hiding in one of these rooms. Your task is to catch the cat. Opening a door takes one step. If you guess the correct door, you catch the cat. If you do not guess the correct door, the cat runs to the next room.
Читать полностью »
Формальные методы считаются эффективным, но неоправданно сложным способом обеспечения надежности программного обеспечения. Используемые при этом инструменты существенно отличаются от привычных программисту. Эта статья написана с целью снизить порог вхождения в этот инструментарий. Я применю систему model checking не для решения сложно формулируемых задач спецификации ПО, а для решения понятной даже школьникам головоломки.
Вы находитесь в прямом коридоре с семью комнатами по одну сторону. В одной из них находится кот. За один шаг можно заглянуть в одну из комнат, если там есть кот, он пойман. Как только дверь закроется, кот перейдет в одну из соседних комнат к той, в которой находился. Задача — поймать кота.
Читать полностью »
На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.
Прежде чем начать, нужно сформулировать некоторые условия. На самом деле существует не так много формальных методов: всего несколько крошечных групп. Это означает, что разные группы по-разному применяют термины. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Сюда входят и код, и абстрактные системы. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Читать полностью »
В этой статье мы смоделируем и исследуем протокол двухфазного коммита с помощью TLA+.
Протокол двухфазного коммита практичный и сегодня используется во многих распределённых системах. Тем не менее, он достаточно краткий. Поэтому мы можем быстро смоделировать его и многому научиться. На самом деле этим примером мы проиллюстрируем, какой результат в распределённых системах фундаментально невозможен.
Транзакция проходит через диспетчеры ресурсов (RM). Все RM должны договориться, будет транзакция завершена или прервана.
Менеджер транзакций (TM) принимает окончательное решение: коммит или отмена. Условием для коммита является готовность к коммиту всех RM. В противном случае транзакцию следует отменить.
Читать полностью »
