Рубрика «формальная верификация»

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

Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.

Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «Proof инженер» или «Специалист по формальной верификации». А люди, работающие по этой специальности — есть.

Читать полностью »

Наконец-то в России вышел учебник по SystemVerilog уровнем выше чем для начинающих. Учебник описывает технологии и приемы, которые спрашивают на интервью в NVidia, Intel, AMD, Apple и другие электронные компании: использование concurrent assertions и functional coverage, что сейчас требуют не только от инженеров по верификации, но и от дизайнеров микросхем; алгоритм работы симулятора с дельта-циклами; вменяемое объяснение static timing analysis; схемы коммуникации аппаратных блоков через аппаратные очереди; реализацию этих коммуникаций с помощью конечных автоматов с трактами данных и т.д.

В главе про последнее российского читателя может озадачить упоминание «политкорректной системы». Что бы это значило? Это вероятно намек на казус, который произошел в округе Лос-Анжелес в 2003 году. Чиновники Лос-Анджелеса попросили производителей, поставщиков и подрядчиков прекратить использование терминов «master/slave» («хозяин» и «раб») в отношении компьютерного оборудования, так как одному из работников округа эти термины напомнили про рабовладельческое прошлое.

Сейчас авторы технической литературы избегают терминов master/slave. В современной Америке работают и афро-американские инженеры (например София Мвокани из Камеруна — на фото слева), и использование старых терминов выглядит архаично, как выглядели бы например термины «пан/холоп» в украинской технической литературе вместо принятых «провідний/ведений» (рус. «ведущий/ведомый»).

Это не первый раз, когда в российском электронном образовании появляется тема борьбы афро-американцев за гражданские права. Например Татьяна Волкова, известный специалист по образованию в электронике, носит маечку с эмблемой «Черных Пантер», калифорнийского движения, которое в свое время сочло мирный протест недостаточным, и занялось вооруженным протестом.

Политкорректность проникает в Россию через книги про проектирование чипов на SystemVerilog для не-начинающих - 1

Полное изображение эмблемы под кожанкой Татьяны Александровны — под катом, но в основном я буду рассказывать про дельта-циклы и конечные автоматы:
Читать полностью »

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

Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.

Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.

Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.

Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.

Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.

Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.

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

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

Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.

Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.

А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.

Задача о 8 ферзях (Взята из англоязычного мануала).

Формальная верификация на примере задачи о волке, козе и капусте - 1
Читать полностью »

Научная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627

Микроядро seL4. Формальная верификация программ в реальном мире - 1В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
Читать полностью »

Думаю никто не станет спорить с тем, что качество сколь-либо сложных систем создаваемых землянами далеко от идеала.
Конечно, можно сказать, что всё работает — самолёты летают, космические корабли бороздят просторы орбиты Земли т.д.
Но при этом все привыкли к тому, что ПО на их устройствах работает непредсказуемо, через раз, что даже установка самых последних обновлений не гарантирует отсутствия проблем с безопасностью, что часто в открытом, массово используемом коде находят ошибки существующие там много лет, что даже у крупных и «технологических» компаний бывают сбои и утечки данных, что космические аппараты разбиваются или теряют часть функциональности вовсе не из-за козней инопланетян (марсиане клянутся что не сбивали ExoMars).
Хотелось бы рассмотреть причины и возможные пути решения этой планетарной проблемы.
Читать полностью »

Agda is too mainstream!

«Предвидение»

Материалов о языке Idris на русском практически нет, попробую это исправить кратким обзором. Также постараюсь сделать текст понятным для начинающих, не-функциональных и незнакомых с зависимыми типами программистов, и потому тем, кто знаком с подобными языками, может быть проще отмотать в конец или сразу прочесть официальную документацию. Писать серьёзное введение в язык и теорию не берусь, но надеюсь показать, о чём это вообще.

Итак, Idris — чистый функциональный язык программирования общего назначения с зависимыми типами.
Читать полностью »

Пары и списки

В предыдущих частях мы научились задавать новые типы данных, определять функции над ними и доказывать их корректность с помощью распространенных тактик. Настало время определить некоторые структуры данных и функции высших порядков (далее ФВП) над ними.
Читать полностью »

Доказательство упрощением

Итак, в предыдущих частях мы определили новые типы данных и функции над ними. Настало время обратиться к вопросу о том, как сформулировать и доказать их свойства и поведение. В некотором смысле мы уже начали делать это – в первой части мы написали своего рода юнит-тест, используя ключевое слово Example, который содержал некоторые утверждения о поведении некоторой функции, применяемой к определенному набору аргументов. Используя определение функции, Coq упрощает выражение и проверяет на равенство его левую и правую часть.Читать полностью »

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

Ранее я сказал, что в Coq нет батареек. На самом деле я слукавил — в Coq есть стандартная библиотека, которая содержит множество полезных определений. Помимо стандартной библиотеки существуют и более специфические вещи, на которых мы пока не будем останавливаться.
Читать полностью »

Предисловие

Ни для кого не секрет, что ошибки в программах могут привести печальным последствиям. История знает множество случаев, когда переполнение счетчика или необработанное исключение приводило к большим материальным затратам и человеческим жертвам. Так, например, 4 июня 1996 года европейская ракета-носитель «Ariane 5» буквально развалилась на части на 39-й секунде полета. Анализ инцидента показал, что авария произошла из-за ошибки в программном обеспечении. Ущерб составил около $7 млрд. В феврале 1991 года ракета «Patriot» промахнулась мимо цели из-за ошибки округления, успела пролететь лишние 500 метров. Ущерб: 28 убитых и более сотни раненых. Подобного рода ошибки встречаются и в аппаратном обеспечении. Недавний баг в процессорах Pentium, связанный с неправильным делением чисел с плавающей точкой, вынудил Intel пойти на замену бракованных чипов. Эта ошибка стоила компании $475 млн.
Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js