Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.
Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.
Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.
Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.
В случае невозможности нахождения ответа, зачастую можно переработать неясные места программы, уменьшив их алгоритмическую сложность, для того чтобы получить конкретный ответ да либо нет.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.
А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.
Задача о 8 ферзях (Взята из англоязычного мануала).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
Запустив Z3, мы получаем решение:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Задача о ферзях сравнима с программой, которая принимает на вход координаты 8 ферзей и выводит ответ, бьют ли ферзи друг друга.
Если бы мы решали такую программу с помощью формальной верификации, то по сравнению с задачей, нам бы просто понадобилось сделать ещё один шаг в виде преобразования кода программы в уравнение: оно бы получилось по своей сути идентичным нашему (разумеется, если программа написана безошибочно).
Практически то же самое будет происходить в случае поиска уязвимостей: мы лишь задаем нужные нам выходные условия, например пароль админа, преобразуем исходный или декомпилированный код в совместимые с верификацией уравнения, и затем получаем ответ, какие данные нужно подать на вход для достижения цели.
На мой взгляд, задача о волке, козе и капусте ещё интересней, так как для её решения нужно уже много (7) шагов.
Если задача о ферзях сравнима со вариантом, когда можно проникнуть на сервер с помощью одного GET или POST запроса, то волк, коза и капуста демонстрирует пример из гораздо более сложной и распространённой категории, в которой цели можно достичь только несколькими запросам.
Это сравнимо, например, со сценарием, где нужно найти SQL иньекцию, записать через неё файл, после повысить свои права и только затем получить пароль.
Разгадка в том, что на 4 шаге фермеру нужно будет отвезти козу обратно.
Теперь приступим к решению программным способом.
Обозначим фермера, волка, козу и капусту как 4 переменные, которые принимают значение только 0 или 1. Ноль означает что они на левом берегу, а единица- что на правом.
import json
from z3 import *
s = Solver()
Num= 8
Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
Num — это число шагов необходимых для решения. Каждый шаг представляет собой состояние речки, лодки и всех сущностей.
Пока что выберем его наугад и с запасом, возьмём 10.
Каждая сущность представлена в 10 экземплярах — это её значение на каждом из 10 шагов.
Теперь зададим условия для старта и финиша.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Затем зададим условия, где волк съедает козу, или коза капуста, как ограничения в уравнении.
(В присутствии фермера агрессия невозможна)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
И наконец, зададим все возможные действия фермера при переправе туда или обратно.
Он может как взять с собой волка, козу или капусту, или же никого не брать, или же вообще никуда не плыть.
Разумеется, без фермера никто переправиться не может.
Это будет выражено тем, что каждое следующее состояние речки, лодки и сущностей может отличаться от предыдущего только строго ограниченным образом.
Не более чем на 2 бита, и со множеством других лимитов, так как фермер может перевезти за раз лишь одну сущность и не всех можно оставить вместе.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Запустим решение.
solve(Side + Start + Finish + Safe + Travel)
И мы получаем ответ!
Z3 нашёл непротиворечивую, и удовлетворяющую всем условиям совокупность состояний.
Эдакий четырёхмерный слепок пространства-времени.
Давайте разберёмся, что же произошло.
Мы видим, что в итоге все переправились, вот только вначале наш фермер решил отдохнуть, и никуда на первых 2 шагах не плывёт.
Human_2 = 0
Human_3 = 0
Это говорит о том, что число состояний мы выбрали избыточное, и 8 будет вполне достаточно.
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Но в итоге задача решена.
#Старт.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#Фермер отдыхает.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#Фермер отдыхает.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#Фермер отвозит козу на нужный берег.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#Фермер возвращается.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#Фермер отвозит капусту на нужный берег.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#Ключевая часть операции: фермер возвращает козу обратно.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#Фермер возвращается за козой.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#Фермер повторно доставляет козу на нужный берег и завершают переправу.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
Теперь попробуем поменять условия и доказать, что решений нет.
Для этого мы наделим нашего волка травоядностью, и он захочет съесть капусту.
Это можно сравнить со случаем, в котором наша цель — защита приложения и мы должны удостовериться что лазеек нет.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 Выдал нам следующий ответ:
no solution
Он означает, что решений действительно нет.
Таким образом мы программным способом доказали невозможность переправы со всеядным волком, без потерь для фермера.
Если аудитория сочтёт эту тематику интересной, то в дальнейших статьях я расскажу, как превратить обычную программу или функцию в совместимое с формальными методами уравнение, и решить его, обнаружив тем самым как все легитимные сценарии, так и уязвимости. Сначала на этой же задаче, но представленной уже в виде программы, а затем постепенно усложняя и переходя к актуальным примерам из мира разработки ПО.
Комментарии (48)
mafia8
22.04.2019 16:24> Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
> Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
>… все… доказать, что их нет.
Круто.
worldmind
22.04.2019 19:46Жаль только неверно, баги-то могут быть, но только такие, которые есть и в самой спецификации, это конечно реже, чем просто ошибки в реализации, но тоже бывает.
smart77
22.04.2019 20:11Это одна из самых серьезных проблем в формальной верификации, которая приводит к тому что создание программ с доказанной эффективностью обходится в 10 раз дороже: это сложнее и требует больше времени.
Но если правила игры или условия программы, системы или контракта написаны естественным языком, но предельно чётким и без двухсмысленностей, как юридический, но ещё строже, так чтобы и человек, и компьютер понимал, то становится вполне возможным включить саму спецификацию в формальную систему вместе с программой и доказать её корректность.
Тем не менее, в спецификации всё равно может быть ошибка в том плане, что авторы спецификации задумали одно, а описали другое, но это уже выходит за рамки таких методов.
Задача формальной верификации — доказать, что во-первых, программа полностью соответствует спецификации, и во-вторых, что она не допускает никаких других сценариев (в том числе уязвимостей), которые в спецификации не описаны.
И она с этим справляется.worldmind
23.04.2019 09:52создание программ с доказанной эффективностью обходится в 10 раз дороже
дороже чего?
The researchers state that the cost of formal software verification is lower than the cost of engineering traditional «high-assurance» software despite providing much more reliable results.[21] Specifically, the cost of one line of code during the development of seL4 was estimated at around US$400, compared to US$1,000 for traditional high-assurance systems.[22]
но это уже выходит за рамки таких методов
и это нужно оговаривать чтобы не ввести в заблуждение тех кто ещё не в темеsmart77
23.04.2019 10:53Согласен, разница в цене и времени может сильно отличаться при разработке софта разного типа.
Если стоит задача разработать самое безопасное в мире микроядро операционной системы, как в случае seL4, то формальная верификация действительно будет дешевле других методов.
Что в принципе неудивительно, если разработка одной строчки кода даже до применения формальной верификации обходилась им в 1000$.
А стоимость создания верифицированного приложения по сравнению с обычным, в среднестатистических случаях программирования, как например, разработка веб-сайтов или создание мобильных приложений, будет уже от 10 раз дороже.
Это главная причина, по которой формальная верификация применяется довольно узко, и только там, где требуется максимальная надёжность и цена ошибки очень высока.
Akela_wolf
23.04.2019 08:35Интересно будет почитать применение формальной верификации к реальным фрагментам кода
amarao
23.04.2019 12:11Просто желтизна так и прёт.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Разумеется, нет. Формальная верификация проверяет соответствие программы формальной спецификации и только. Сама спецификация — специальный вид тестов с 100% покрытием (всех веток).
Баг в тесте (спецификации) — и у вас ровно такие же CVE'шки, как и без неё, только теперь у CVE есть тест, который проверяет, чтобы она была на месте.
Серебрянных пуль не бывает и писать софт без багов ещё никто не научился.smart77
23.04.2019 12:44Я не согласен с тем что это желтизна.
На мой взгляд формальная верификация действительно является самым мощным средством поиска и устранения уязвимостей, и это подтверждается её применением в ядре Windows, беспилотниках Darpa и самом безопасном микроядре seL4.
Формальная верификация на самом деле позволяет найти все проблемы в программе, и доказать её соответствие спецификации.
А то, что она гарантированно способна находить баги в самой спецификации, я и не утверждал.
Да и вообще склонен думать, что полное решения проблемы багов связанных с неверной спецификацией либо невозможно, или очень далеко.
Не вижу способов, как справиться с той ситуацией, когда программист или заказчик задумал одно, а в ТЗ написал другое. И на практике такое встречается сплошь и рядом.
Поэтому с тем, что формальная верификация серебряной пулей не является, я согласен.amarao
23.04.2019 14:06Я не понимаю, почему ядро Windows приводится в качестве примера системы без багов. www.cvedetails.com/cve/CVE-2019-0797 win32k — вполне себе ядро. www.cvedetails.com/cve/CVE-2019-0796 — тоже ядро.
Если формальная верификация находит эти баги, то почему они CVE? Насчёт «самое мощное» — мне сложно сказать, потому что сложность написания спецификации делает этот процесс не менее сложным, чем написание кода. А вот чем тестировать спецификацию — это вопрос открытый. end2end? Интеграционное тестирование? И дальше поехало обычное.
… Когда я говорю про баги в спецификации я говорю не про проблемы коммуникации между заказчиком и разработчиком, я говорю про обычные баги в коде. Спецификация пишется на формальном языке, мало отличающемся от какого-нибудь ML'я. И в нём делают натуральные баги. Букву перепутали, цифру не ту написали и т.д.
То есть если мы заменим «доказательство кода» на «тесты с 100% покрытием всех ветвлений», то картинка станет понятнее. В тестах тоже бывают баги. Хуже, если код пишется под тесты и тест заставляет реализующего реализовать ошибочное поведение, чтобы тест зелёным стал.smart77
23.04.2019 14:27Насколько мне известно, ядро Windows имеет элементы, прошедшие формальную верификацию, но полного покрытия нет.
Оно приведено лишь в качестве примера, где используется формальная верификация, и не более того.
То что Microsoft признает такой подход и применяет его, свидетельствует о наличии в нём определённых преимуществ.
Более наглядным примером будет микроядро seL4, которое состоит из доказанного кода на 100%, и является одним из самых безопасным в мире.
Именно его использует Darpa в своих беспилотниках.
Ядро дополнительно проходило их серьезный аудит, и уязвимостей найти не удалось, что подтверждает мощность формальной верификации.
securityaffairs.co/wordpress/27087/hacking/sel4-hack-proof-darpa-derived-micro-kernel-goes-open-source-tomorrow.html
Если написать спецификацию в формате, понятном как человеку, так и компьютеру (например, в виде более строгой и ограниченной версии юридического языка исключающую двоякое трактование), а затем включить её внутрь формальной модели, то соответствие программы формальной спецификации вполне будет доказано.
Затем конечный пользователь программы может прочесть его описание, и сделать вывод, устраивает оно его или нет.
Если устраивает, то можно пользоваться. Если заметит опечатки или подозрительные цифры, можно отказаться от использования такой программы.
Я описывал не проблему коммуникации между заказчиком и разработчиком, а более конкретный и узкий случай переноса задуманной спецификации из мозга на бумагу.
Можно сформулировать это так, что спецификация считается корректной если выполняется 2 условия:
1) Спецификация полностью соответствует тому что делает программа, созданная на её основе.
2) Спецификация полностью отражает то, что задумал её создатель.
Формальная верификация позволяет на 100% обеспечить выполнение первого пункта, но полностью решить второй ей не под силу.amarao
23.04.2019 14:41То есть мы возвращаемся к модели «тесты с 100% покрытием».
С точки зрения надёжности программы это примерно эквивалентно «программа реализована два раза на разных языках программирования», с той поправкой, что точно известно, что покрыты все ветвления.
smart77
23.04.2019 14:58Думаю можно сказать и так.
Двойная реализация обладает синергетическим эффектом и снижает число багов гораздо существеннее, чем в 2 раза.
Для того, чтобы баг выжил, необходимо наличие ошибок сразу в 2 местах: как в коде программе, так и в коде самого формального верификатора.
Если вероятность бага в верификаторе 1%, а в программе 10%, то мы получаем общую надёжность программы в 99.9%
На практике же верификаторы многократно проверяются, в том числе и другими верификаторами, поэтому надёжность формальной верификации рекурсивно стремится вообще к 100%
Известность того, что покрыты все ветвления как раз и является ключевым преимуществом формальной верификации перед тестами.
Тестами можно покрыть только те сценарии, о которых знает тот кто их пишет, а критерий полноты покрытия определяется человеком либо эвристически.
В то время как верификация проверяет вообще абсолютно все, в её случае 100% покрытие будет уже доказанным.amarao
23.04.2019 15:01+1Во, мне нравится формулировка: «У формальной верификации доказанное 100% покрытие тестами всех случаев для всех видов данных». Оно не утверждает, что программа без багов, оно не содержит схоластическое «соответствует спецификации» (потому что в голове в этот момент «спецификация» человеком, а на самом деле это код). Оно реально говорит о существенном преимуществе — гарантированном покрытии всех случаев тестами.
Сами тесты могут быть с багами. Но хотя бы они есть.smart77
23.04.2019 15:08Вполне согласен.
На мой взгляд концептуально формальная верификация и покрытие кода тестами похожи и относятся к одной категории.
Если попробовать их сравнить, то я вижу 2 отличия:
1) Это как раз то, что формальная верификация дает доказанное 100% покрытие тестами.
2) Тесты пишет не человек, а формальный верификатор, который хоть и может ошибаться, но надёжность его стремится к 100% и многократно превосходит человеческую.amarao
23.04.2019 15:16Тесты пишет человек. На том самом «языке спецификаций» который с точки зрения написания ничем от мунспика bdd, например, не отличается. Что там из него генерируют машины уже не важно. Исходный код тестов — это спеицификация.
smart77
23.04.2019 15:23Я сторонник такого подхода, в котором тесты должны автоматически генерироваться из публичного описания программы на естественном, или, по крайней мере, понятном для обычного и не обладающего навыками программирования человека языке.
Это позволит исключить человеческий фактор из процесса написания тестов.
В идеале, формальная верификация должна доказывать что программа соответствует её публичному, человеческому описанию.amarao
23.04.2019 15:25вы всего лишь один машиночитаемый язык заменяете на другой. Все языки программирования исходят из того, что «естественный» и «понятный для человека». С этим лозунгом писали фортран, си и т.д., сути проблемы это не меняет — это язык программирования (как бы он не маскировался под естественный) и цена ошибки или неоднозначности в нём — баг в программе.
Уже много раз была шутка про «купи в магазине бутылку молока, а если будут яйца, то возьми шесть».smart77
23.04.2019 15:35Я не спорю с тем, что существующие «естественные и понятные для человека» языки программирования оставляют желать лучшего.
Надеюсь, мы увидим прогресс в направлении создания действительно понятных языков программирования, и формализации человеческой речи вообще.
На мой взгляд, вполне возможно (или будет возможно) генерировать человеко-понятные приказы или спецификации исходя из лишь из конечных целей.
Допустим, компьютеризированный холодильник обнаружил, что ему не хватает 1 бутылки молока и 6 яиц.
На примере этого он должен сгенерировать однозначное и понятное приказание для человека вида «Необходимо купить бутылку молока и 6 яиц, а если яиц не будет, то только молоко.».
И ответственность здесь лежит именно на холодильнике, это он должен генерировать адекватные описания, а не человек разбираться в непонятных.amarao
23.04.2019 15:38Я вам привёл пример спецификации, написанной на ествественном, понятном человеку языке, которая вызывает неоднозначности и баги.
С лёгкостью можно накрутить достаточно, чтобы баг остался в любом уровне фашизма при валидации, просто потому, что ествественный язык всегда оставляет пространство для неоднозначности, а как только вы его исключаете, язык перестаёт быть естественным.
Надо перестать пытаться натянуть сову на пень и признать, что любая спецификация — машиночитаемый язык программирования. К которому применимы все те же проблемы и решения, как и к любому другому языку.smart77
23.04.2019 15:44Вы привели пример, когда один человек даёт задачу, или создаёт спецификацию, для другого.
На мой взгляд это выходит за рамки информационных технологий, а помогать людям взаимодействовать между собой будет лучше социологам и психологам.
Но я считаю, что проблема создания человеком понятной для компьютера спецификации, или же наоборот, создание компьютером понятной для человека в принципе решаема.
На настоящий момент я признаю то, что любые спецификации ещё очень далеки от естественных.
Но я искренне верю, что в будущем обязательно появятся спецификации, которые будут читаемы как людьми, и машинами.
Я сам увлекаюсь созданием таких спецификаций в том числе.
Кроме того, я считаю что нужно идти к решению этой проблемы с 2 концов: как повышать естественность языков, так и образованность людей, обучая их основам логики и программирования.amarao
23.04.2019 15:46Дело не в том, кому они будут понятны. Дело в том, можно ли в таких спецификациях написать код с багами. Очевидно, что можно. Особенно, если баг ведёт не к внутренней неконсистентности (это можно отследить), а к внешней (вне модели). Шутка про молоко — отличный пример.
smart77
23.04.2019 15:56Не спорю с тем, что пример отличный, но он относится только к взаимодействию 2 людей, что совершенно меняет всю картину и больше относится к социологии, чем IT.
Если и спецификацию, и код пишет машина, с применением формальных методов, то на данный момент вполне достижимо добиться практически 100% отсутствия багов.
И я верю, что в будущем, в дополнении к этому, удастся добиться и 100% естественности/понятности таких спецификаций как для людей, так и машин.
Надеюсь, что и мне удастся внести свой вклад в объединение этих двух миров.amarao
23.04.2019 17:40Если и код и спецификацию пишет машина, то откуда она знает что писать? Вот это «что-то» и есть исходный код.
smart77
23.04.2019 18:07Машина может сгенерировать исходный код только имея входные и выходные данные.
Для этого обычно применяют нейросети или генетические алгоритмы, но SMT/SAT решатели тоже применяются для этой цели и в некоторых случаях превосходят все другие подходы.
И даже более того, машина в принципе может сгенерировать описание, спецификацию, входные данные и исходный код только лишь имея выходные данные в достаточном количестве.
Но это уже к синтезу программ и алгоритмов относится.amarao
23.04.2019 18:25А вот тут Остапа начало нести.
Удачи ездить на лифте, чей код и спецификация сгенерированы нейронной сетью.smart77
23.04.2019 18:33Благодарю, удача в этом нелёгком деле мне пригодится!
Остапом, однако, я себя не считаю, а все свои доводы и суждения буду подкреплять работающим кодом.
Нейронные сети уже достаточно хорошо изучены, и в эту сферу сложно привнести что-то новое.
Меня больше интересуют методы синтеза программ только лишь по входным и выходным данным конкретно с помощью SMT/SAT.
Это не моё изобретение, такой подход уже имеет место быть, хоть и не слишком известен.
В одной из следующей статей я намерен осветить и эту тематику, тоже на конкретных примерах.amarao
23.04.2019 18:38А, я понял о чём вы. Дайте мне ввод и вывод и я сгенерирую вам код.
… Это работает только в мире розовых пони и функций без сайд-эффектов. Как вы сайд-эффект в выводе опишите-то? Трепыхать светодиодом 3 милисекунды.
Что такое 3 милисекунды? Какой тип данных позволяет запретить выполнение кода дольше трёх милисекунд?smart77
24.04.2019 13:04Как ни странно, но в программировании немало и таких миров.
Кроме розовых пони, там порой обитают и единороги: стартапы или компании которые вышли на капитализацию свыше миллиарда долларов.
Приведу цитату из официального сайта той, самой безопасной в мире OS seL4:
seL4 is the world’s only hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming. (If someone else tells you they can make such guarantees, ask them to make them in public so Gernot can call out their bullshit.)
docs.sel4.systems/FrequentlyAskedQuestions.html#can-i-run-a-real-time-os-in-a-virtual-machine-on-sel4
Они решили вашу проблему, и смогли предсказать (и доказать!) время исполнения кода в самом худшем случае.
В итоге беспилотники Darpa летают не взирая на сайд-эффекты.amarao
24.04.2019 13:09Простите, а каким образом worst case execution time может быть вычислен алгоритмически?
Вот, скажите, у меня есть два i16. Мне нужна их сумма с битом переполнения в i16. Какая дисциплина в CS мне ответит, сколько времени эта операция будет выполняться?
mentin
23.04.2019 12:33+1Я эту же задачу делал на Майкрософтовском (MSR) пруфере TLA.
Там похоже, но чуть проще на мой взгляд и выглядит математичнее.
Опишу кратко здесь, полный код можно найти на
https://github.com/mentin/tla/blob/master/river2/mega_crossing.tla
В TLA /\ обозначает "или", а \/ — "и", они для красоты пишутся и вначале тоже.
(* описываем кто у нас есть *) Things == { "Man", "Goat", "Wolf", "Cabbage" } (* вначале никто не пересек реку *) Init == locs = [x \in Things |-> FALSE] (* условие безопасности: козел с человеком либо не там где волк или капуста *) IsSafe == \/ locs'["Goat"] = locs'["Man"] \/ (/\ locs'["Goat"] /= locs'["Wolf"] /\ locs'["Goat"] /= locs'["Cabbage"]) (* следующее состояние после пересечения реки с "х" - "х" и человек меняют сторону реки *) CrossWith(x) == /\ locs["Man"] = locs[x] /\ locs' = [locs EXCEPT !["Man"] = ~locs[x], ![x] = ~locs[x]] (* шаг это пересечение реки, можно с кем угодно из Things *) Next == /\ (\E x \in Things : CrossWith(x)) /\ IsSafe (* хотим чтобы все пересекли реку *) IsDone == locs = [x \in Things |-> TRUE]smart77
23.04.2019 12:53Простые и наглядные альтернативы очень радуют!
Я не претендую на академичность своей статьи, и сосредоточился на том чтобы сделать её понятной для максимального числа читателей.
Tla относится к той же категории языков, что и Coq либо Isabelle.
Они позволяют создавать формально доказанные программы.
А мой выбор Z3Prover обусловлен тем, что я больше смотрю на практический поиск уязвимостей, и в следующих статьях приступлю к трансляции программ с типичных языков в формальную логику.
Z3 подходит для этого лучше всего.
johnklymenko
23.04.2019 13:24+2А никого не смущает, что решение, которое описано в тексте — неправильное?
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Момент с вторичной переправой капусты (которой уже нет на берегу) — это как?
smart77
23.04.2019 13:27+1Вы правы, и оказились наблюдательней меня!
Решение, которое выдала формальная верификация полностью корректно, в чём можно убедиться проверив запись в виде 0 и 1.
А вот моя текстовая интерпретация — нет.
Я всё-таки человек, и в отличии от формального верификатора иногда допускаю ошибки…
Вместо
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Должно быть
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Я исправлю статью, но оставлю хронику ошибки в этом комментарии.
Это наглядная демонстрация того, почему формальная верификация не является серебряной пулей.
Если сравнить с поиском уязвимостей, то это такой случай, где верификатор выдал мне конкретный и верный рецепт, но в итоге проникнуть в систему я не смог так как перепутал шаги.
sergey-b
24.04.2019 07:25We know each queen must be in a different row. So, we represent each queen by a single integer: the column position
Мы уже знаем правильный ответ, поэтому используем такую форму представления, где всего 40 тыс. возможных комбинаций, чтобы программа справилась с задачей.
Давайте «упростим» задачу. Сделаем не 8, а 9 ферзей. Любой ребенок, знакомый с шахматами, за секунду скажет, что задача не имеет решения. Правда, теперь мы не будем использовать то, что мы «знаем», что каждый ферзь находится в своем ряду, а представим каждого ферзя двумя координатами, как и положено в шахматах. С каждым ферзем свяжем не одно целое число, а набор координатных пар, соответствующих тем клеткам, которые ферзь бьет. И единственным ограничением будет то, что множество битых ферзями клеток не пересекается с множеством занятых ферзями клеток. Сможет ли замечательный верификатор за разумное время решить задачу?smart77
24.04.2019 13:34У меня раньше был разряд по шахматам, и я пробовал писать свои шахматные программы.
Такая форма представления в виде 8 строчек и колонок сразу приходит в голову. Она позволяет проще проверять, какие поля бьёт слон, ладья или ферзь, да и по сути является способом представления геометрии доски в программе.
И в задаче с ферзями это будет банально самая лаконичная запись.
Если взять 64 клетки, то придётся гораздо дольше описывать сами понятия горизонталей и вертикалей.
Это я к тому, что никакой подгонки под задачу нет, а попросту было выбрано самое удобное и быстрое в написании представление.
Но ваша идея мне нравится, если будет свободная минутка, то постараюсь её опробовать и рассказать, справился ли верификатор или нет.
С точки зрения вычисления такая задача будет действительно сложней.
А пока проведём более простой эксперимент:
В такой задаче 40 320 (если не брать в учёт перестановки).
Это факториал от 8.
Если увеличить число ферзей до 20, это даст уже порядка 10^18 вариантов.
Z3Prover при этом всё так же справляется мгновенно.
Добавим нагрузки и увеличим их число до 30, что даст около 10^32 способов расстановки ферзей на доске.
# We know each queen must be in a different row. # So, we represent each queen by a single integer: the column position import json from z3 import * Q = [ Int('Q_%i' % (i + 1)) for i in range(30) ] # Each queen is in a column {1, ... 30 } val_c = [ And(1 <= Q[i], Q[i] <= 30) for i in range(30) ] # At most one queen per column col_c = [ Distinct(Q) ] # Diagonal constraint diag_c = [ If(i == j, True, And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) for i in range(30) for j in range(i) ] solve(val_c + col_c + diag_c)
Z3Prover задумался секунд на 5, но решение выдал.
Вот оно:
[Q_13 = 4, Q_5 = 7, Q_16 = 3, Q_17 = 25, Q_3 = 30, Q_4 = 9, Q_7 = 18, Q_1 = 13, Q_18 = 10, Q_19 = 2, Q_24 = 20, Q_27 = 21, Q_14 = 15, Q_23 = 12, Q_29 = 17, Q_8 = 8, Q_12 = 22, Q_22 = 29, Q_2 = 28, Q_15 = 24, Q_28 = 26, Q_26 = 19, Q_10 = 14, Q_25 = 11, Q_20 = 23, Q_30 = 1, Q_6 = 5, Q_11 = 27, Q_9 = 6, Q_21 = 16]
Наш замечательный верификатор справляется неплохо, поскольку он использует гораздо более мощные алгоритмы нежели обычный перебор.
Но у Z3Prover, конечно, тоже есть свои пределы, связанные главным образом с тем что в итоге он упирается в проблему P=NP.
При 40 ферзях дать быстрый ответ он уже не смог.
xi-tauw
Что-то я не понял как происходит переход от
к
В какой момент ядро Windows перешло во вполне детерминированную задачу о 8 ферзях, а ОС беспилотников Darpa в задачу о козе, волке и капусте.
Какие уязвимости могут быть в задаче о 8 ферзях?
Я бы попробовал высказать лемму, что если в алгоритме нет условных циклов, безусловных переходов и рекурсии (фактические есть только несколько циклов for с фиксированным счетчиком), то такая программа всегда остановит свою работу, ибо у нее просто нет способов зациклиться.
Что вы в итоге верифицировали?
smart77
Вначале статьи я обозначил, что расскажу несколько слов о том что такое формальная верификация, а затем приведу наглядные примеры, так, немного скомкано, переход и происходит…
Ядро Windows и задача о 8 ферзях связаны тем, что Z3Prover применяется в обоих случаях.
К тому же Z3Prover является разработкой от Microsoft Research, которым они же и ищут уязвимости в ядре.
Но вы правы, целостность повествования не столь хороша как хотелось бы.
В задаче о 8 ферзях уязвимостей нет, а сам пример был приведён главным образом для наглядной демонстрации механизмов и принципов работы Z3Prover, начиная с самых простых случаев.
Я показал принцип нахождения необходимой комбинации входных данных, в том случае, когда выходные данные и алгоритм известны.
Я согласен с вашей леммой о программе без условных циклов, переходов, которая всегда остановит свою работу.
Могу добавить, что некоторые языки программирования специально устанавливают такие ограничения, и таким образом все программы будут иметь конечную и предсказуемую сложность.
В следующей статье я как раз собираюсь написать о применении формальной верификации для нахождения уязвимостей в программах на таком языке, поскольку они прекрасно совместимы.
А итоге я верифицировал, что задача о волке, козе и капусты имеет решение за 8 шагов, а также то, что версия этой задачи со всеядным волком решения не имеет.
xi-tauw
Тут дело не столько в целостности повествования, сколько в том, что переход о котором я говорю, так сказать, важнее, чем все что есть в статье. Точнее мне это так видится, сейчас объясню почему.
Из статьи видно как солвер находит и не находит решения некоторой задачи описанной на формальном языке. Так вот тот переход, который опущен — это объяснение как переносить готовый код (с обвязкой в виде ОС, системных вызов и еще кучи чего) на формальную логику.
Возьмем условно банальный хартблид. Расскажите как можно через формальную верификацию найти его в коде. Поскольку на входе комбинаторный взрыв, то вангую ответ — никак. Вот если взять один файл, с 3 функциями, то наверное найдет. Ну как бы: знал бы где упал — соломки постелил бы.
Ладно это все то, о чем в статье нет. И вполне вероятно можно отмахнуться фразами типа в следующих статьях раскроете, хотя все же я почти уверен, что все сведется к «берем код без внешних вызовов, без работы с файловой системой, без сети и доказываем, что 2+2 никогда не вызовет переполнения стека».
Спасибо, что рассказываете об формальной верификации, это все реально интересно. Но попробуйте быть ближе к настоящему применению и если пишете о чем-то, то раскрывайте.
smart77
Вы абсолютно правы!
Этот переход от перехода от кода к системе уравнений действительно является ключевым во всей концепции формальной верификации.
Именно этому моменту будет посвящена следующая статья, которая уже не за горами.
Я не хотел, чтобы первая статья показалась чрезмерно сложной для понимания.
Поэтому начал с упрощенного варианта, где вместо программы, на формальную логику переносится задача.
Хочу заверить, что принципы остаются теми же самыми, и следующая статья будет только дополнять эту новыми шагами.
В ней я расскажу о том как распарсить программу, превратить её в логическое выражение, сначала на языке самой программы.
А затем покажу, как сконвертировать это выражение в формальную логику.
Файлы, хранение данных и внешние вызовы я намерен затронуть в том числе.
Надеюсь, что моя статья несёт хоть какую-то полезность и в таком виде, так как статей по формальной верификации с примерами и кодом я на хабре не нашёл. (буду рад ошибиться)
Очень важно в формальной верификации то, что она ищет входные варианты гораздо более совершенным способом чем перебор, и находит нужные комбинации, даже если их 10^100.
Поэтому комбинаторного взрыва на входе она боится куда меньше чем брутфорс, и обнаружить даже Heartblead в принципе реально.
Благодарю вас за интересные и важные вопросы, которые помогают раскрыть статью.
0xd34df00d
А зачем так делать, когда можно сразу писать proof-carrying code? А z3 и подобные использовать в стиле тактик Coq.
smart77
Так и есть, Coq или Isabelle гораздо лучше подойдут для создания верифицированного кода.
В то время как Z3Prover удобней использовать для проверки уже написанного кода на любых других языках программирования.
Существует много фреймворков для автоматического аудита на базе Z3, которые заточены под поиск уязвимостей и не ставят перед собой задачи 100% формального доказательства.
Tsvetik
А можно поподробнее про Coq или Isabelle? Как этим вообще пользоваться?
smart77
Я больше увлекаюсь практическим поиском уязвимостей, нежели формальным доказательством программ, поэтому интересуюсь в первую очередь Z3Prover и SMT/SAT решателями.
Но возможно я расскажу об этих языках в будущих статьях.
0xd34df00d
Я больше по Idris, чем по Coq, а у них и метатеория разная, и подход (Coq экстрагируется в другие языки, Idris сам является целевым компилируемым языком).
Общая идея в том, что если у вас достаточно мощная и разумная система типов, то типу соответствует некоторое высказывание, а терму этого типа — доказательство этого высказывания. При этом в типах вы можете делать высказывания вроде «xs — сортированный список» или «r — остаток от деления m на n». Так что в итоге вы просто пишете в типах спецификацию, а в термах — ее реализацию.
Tsvetik
По-видимому, программу, которая делает переход от кода к системе уравнений надо тоже верифицировать.
smart77
Не помешает.
Кроме того качество формальных верификаторов можно обеспечить проверкой того, что он находит в том числе все баги и уязвимости найденные как людьми, так и другими формальными верификаторами, в итоге надёжность стремится к 100%.
0xd34df00d
Языки программирования с тоталити чекерами позволяют делать такие вещи и для алгоритмов с рекурсией (ограниченной ее формой, Walther recursion, которой, впрочем, для многих приложений хватает), и для потенциально бесконечно работающих алгоритмов типа веб-серверов (за счёт коданных).
sergey-b
Да и в задаче о ферзях самую интересную работу за программу человек выполнил.