#формальная_верификация — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #формальная_верификация, aggregated by home.social.
-
Формальная верификация «для богатых»: используем Jasper C2RTL App из Cadence JasperGold
Приве! Меня зовут Андрей, я занимаюсь в YADRO верификацией аппаратного обеспечения. В разработке цифровых устройств (GPU, CPU, AI-ускорители) большое внимание уделяют трактам обработки данных (datapath). Архитекторы создают эталонные модели блоков на языках высокого уровня (C/C++), чтобы быстрее проводить архитектурные исследования и отладку алгоритмов — например, операции с плавающей точкой, полиномы, матричные умножения. Однако конечная реализация выполняется на RTL (Verilog/SystemVerilog). После реализации в виде RTL-кода всегда хочется проверить соответствие итогового дизайна оригинальной модели. В этот момент в мире ASIC-разработки часто начинают думать сразу о UVM, корнер-кейсах и прочих долгих прелюдиях перед оформлением багов. В качестве альтернативы здесь выступает формальная верификация. Если вы работаете в небольшом стартапе, то, скорее всего, вам нужен маршрут формальной верификации, описанный моим коллегой в статье «Формальная верификация „для бедных“: выбираем open-source решение» . Но если вам повезло работать в крупной полупроводниковой компании с доступом к коммерческим инструментам формальной верификации, то можно подумать о проверке логической эквивалентности между C и RTL-кодом. Один из популярных инструментов для такой проверки — это Jasper C2RTL App в составе платформы Cadence JasperGold. По механике он очень похож на известные многим инструменты LEC и SEC, но в качестве эталонной реализации здесь выступает код на C. В этой статье мы рассмотрим, как работает C2RTL, из каких этапов состоит процесс верификации с ним, как формируются проверки (ассерты) и с какими ограничениями здесь сталкиваются инженеры.
-
Применяем TLA+ на практике
Привет, Хабр! Меня зовут Сергей, я работают в компании InfoWatch разработчиком на продукте ARMA Стена (NGFW). Подробнее о том, что такое ARMA Стена, можно прочитать тут . В этой статье я хочу поделиться опытом применения метода формальной верификации в решении практической бизнес-задачи. Сразу оговорюсь, что в статье используется TLA+, без введения в инструмент, чтобы не увеличивать объём статьи. Подробнее про инструмент вы можете почитать на сайте создателя , тут и тут . Необходимые объяснения даются по ходу изложения. Статья состоит из двух частей: 1) Что такое формальная верификация и где она применятся 2) Решение бизнес-задачи в NGFW Верифицировать статью
-
Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.
https://habr.com/ru/companies/pt/articles/864754/
#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft
-
Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.
https://habr.com/ru/companies/pt/articles/864754/
#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft
-
Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.
https://habr.com/ru/companies/pt/articles/864754/
#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft
-
Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.
https://habr.com/ru/companies/pt/articles/864754/
#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft
-
Формальная верификация смарт-контрактов во фреймворке ConCert
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье мы продолжим обсуждать методы и инструменты формальной верификации смарт-контрактов и их практическое применение для предотвращения уязвимостей. Мы подробно поговорим о методе дедуктивной верификации, а точнее, о фреймворке для тестирования и верификации смарт-контрактов — ConCert. Под кат
https://habr.com/ru/companies/pt/articles/804861/
#формальная_верификация #формальная_верификация_криптовалют #formal_verification #formal_methods #тестирование #смартконтракты #блокчейн #solidity #coq #Concert
-
Путь к совершенному ПО: Искусственный интеллект в автоматической формальной верификации
При написании высококачественного программного обеспечения не обойтись без этапа формальной верификации . Несмотря на то, что наша жизнь уже была в некоторой степени упрощена, благодаря таким помощникам доказательства как Coq и Isabelle/HOL, обучающим модель предсказывать один шаг доказательства за раз, оптимизация формальной верификации еще не была достигнута. Новый метод автоматической генерации доказательств – модель Baldur . Данный метод основывается на использовании больших языковых моделей, возможности восстановления доказательства и исправления благодаря указанию ошибки и добавлению контекста. Baldur превосходит все существующие подходы, он может самостоятельно полностью за раз доказывать 47.9% теорем, и даже этот результат – не предел. В данной статье я познакомлю Вас со всей теоретической и практической подноготной данной модели, этапами реализации и оценки метода, чтобы стать чуточку ближе к созданию идеального ПО! Приятного прочтения :)
https://habr.com/ru/companies/bothub/articles/792196/
#ии #ии_и_машинное_обучение #программное_обеспечение #формальная_верификация #проверка_кода #доказательство_теорем #isabelle #thor #компиляторы #baldur
-
Формальные методы проверки смарт-контрактов
Друзья, приветствую! Меня зовут Сергей Соболев, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье начну рассказывать про методы и инструменты формальной верификации, их практическое применение в аудите смарт-контрактов, а также про подводные камни. Сегодня поговорим про общие теоретические аспекты формальной верификации, проблемы SAT и SMT и закрепим все это на простом примере с использованием хайпового инструмента для анализа смарт-контрактов Certora Prover со своим языком спецификаций. Под кат
https://habr.com/ru/companies/pt/articles/786078/
#формальная_верификация #solidity #смартконтракты #ethereum #формальная_верификация_криптовалют #formal_specification #formal_methods #sat #certora_prover #smt