Comments 50
Что-то я не понял как происходит переход от
к
В какой момент ядро Windows перешло во вполне детерминированную задачу о 8 ферзях, а ОС беспилотников Darpa в задачу о козе, волке и капусте.
Какие уязвимости могут быть в задаче о 8 ферзях?
Я бы попробовал высказать лемму, что если в алгоритме нет условных циклов, безусловных переходов и рекурсии (фактические есть только несколько циклов for с фиксированным счетчиком), то такая программа всегда остановит свою работу, ибо у нее просто нет способов зациклиться.
Что вы в итоге верифицировали?
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
к
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
В какой момент ядро Windows перешло во вполне детерминированную задачу о 8 ферзях, а ОС беспилотников Darpa в задачу о козе, волке и капусте.
Какие уязвимости могут быть в задаче о 8 ферзях?
Я бы попробовал высказать лемму, что если в алгоритме нет условных циклов, безусловных переходов и рекурсии (фактические есть только несколько циклов for с фиксированным счетчиком), то такая программа всегда остановит свою работу, ибо у нее просто нет способов зациклиться.
Что вы в итоге верифицировали?
Вначале статьи я обозначил, что расскажу несколько слов о том что такое формальная верификация, а затем приведу наглядные примеры, так, немного скомкано, переход и происходит…
Ядро Windows и задача о 8 ферзях связаны тем, что Z3Prover применяется в обоих случаях.
К тому же Z3Prover является разработкой от Microsoft Research, которым они же и ищут уязвимости в ядре.
Но вы правы, целостность повествования не столь хороша как хотелось бы.
В задаче о 8 ферзях уязвимостей нет, а сам пример был приведён главным образом для наглядной демонстрации механизмов и принципов работы Z3Prover, начиная с самых простых случаев.
Я показал принцип нахождения необходимой комбинации входных данных, в том случае, когда выходные данные и алгоритм известны.
Я согласен с вашей леммой о программе без условных циклов, переходов, которая всегда остановит свою работу.
Могу добавить, что некоторые языки программирования специально устанавливают такие ограничения, и таким образом все программы будут иметь конечную и предсказуемую сложность.
В следующей статье я как раз собираюсь написать о применении формальной верификации для нахождения уязвимостей в программах на таком языке, поскольку они прекрасно совместимы.
А итоге я верифицировал, что задача о волке, козе и капусты имеет решение за 8 шагов, а также то, что версия этой задачи со всеядным волком решения не имеет.
Ядро Windows и задача о 8 ферзях связаны тем, что Z3Prover применяется в обоих случаях.
К тому же Z3Prover является разработкой от Microsoft Research, которым они же и ищут уязвимости в ядре.
Но вы правы, целостность повествования не столь хороша как хотелось бы.
В задаче о 8 ферзях уязвимостей нет, а сам пример был приведён главным образом для наглядной демонстрации механизмов и принципов работы Z3Prover, начиная с самых простых случаев.
Я показал принцип нахождения необходимой комбинации входных данных, в том случае, когда выходные данные и алгоритм известны.
Я согласен с вашей леммой о программе без условных циклов, переходов, которая всегда остановит свою работу.
Могу добавить, что некоторые языки программирования специально устанавливают такие ограничения, и таким образом все программы будут иметь конечную и предсказуемую сложность.
В следующей статье я как раз собираюсь написать о применении формальной верификации для нахождения уязвимостей в программах на таком языке, поскольку они прекрасно совместимы.
А итоге я верифицировал, что задача о волке, козе и капусты имеет решение за 8 шагов, а также то, что версия этой задачи со всеядным волком решения не имеет.
Тут дело не столько в целостности повествования, сколько в том, что переход о котором я говорю, так сказать, важнее, чем все что есть в статье. Точнее мне это так видится, сейчас объясню почему.
Из статьи видно как солвер находит и не находит решения некоторой задачи описанной на формальном языке. Так вот тот переход, который опущен — это объяснение как переносить готовый код (с обвязкой в виде ОС, системных вызов и еще кучи чего) на формальную логику.
Возьмем условно банальный хартблид. Расскажите как можно через формальную верификацию найти его в коде. Поскольку на входе комбинаторный взрыв, то вангую ответ — никак. Вот если взять один файл, с 3 функциями, то наверное найдет. Ну как бы: знал бы где упал — соломки постелил бы.
Ладно это все то, о чем в статье нет. И вполне вероятно можно отмахнуться фразами типа в следующих статьях раскроете, хотя все же я почти уверен, что все сведется к «берем код без внешних вызовов, без работы с файловой системой, без сети и доказываем, что 2+2 никогда не вызовет переполнения стека».
Спасибо, что рассказываете об формальной верификации, это все реально интересно. Но попробуйте быть ближе к настоящему применению и если пишете о чем-то, то раскрывайте.
Из статьи видно как солвер находит и не находит решения некоторой задачи описанной на формальном языке. Так вот тот переход, который опущен — это объяснение как переносить готовый код (с обвязкой в виде ОС, системных вызов и еще кучи чего) на формальную логику.
Возьмем условно банальный хартблид. Расскажите как можно через формальную верификацию найти его в коде. Поскольку на входе комбинаторный взрыв, то вангую ответ — никак. Вот если взять один файл, с 3 функциями, то наверное найдет. Ну как бы: знал бы где упал — соломки постелил бы.
Ладно это все то, о чем в статье нет. И вполне вероятно можно отмахнуться фразами типа в следующих статьях раскроете, хотя все же я почти уверен, что все сведется к «берем код без внешних вызовов, без работы с файловой системой, без сети и доказываем, что 2+2 никогда не вызовет переполнения стека».
Спасибо, что рассказываете об формальной верификации, это все реально интересно. Но попробуйте быть ближе к настоящему применению и если пишете о чем-то, то раскрывайте.
Вы абсолютно правы!
Этот переход от перехода от кода к системе уравнений действительно является ключевым во всей концепции формальной верификации.
Именно этому моменту будет посвящена следующая статья, которая уже не за горами.
Я не хотел, чтобы первая статья показалась чрезмерно сложной для понимания.
Поэтому начал с упрощенного варианта, где вместо программы, на формальную логику переносится задача.
Хочу заверить, что принципы остаются теми же самыми, и следующая статья будет только дополнять эту новыми шагами.
В ней я расскажу о том как распарсить программу, превратить её в логическое выражение, сначала на языке самой программы.
А затем покажу, как сконвертировать это выражение в формальную логику.
Файлы, хранение данных и внешние вызовы я намерен затронуть в том числе.
Надеюсь, что моя статья несёт хоть какую-то полезность и в таком виде, так как статей по формальной верификации с примерами и кодом я на хабре не нашёл. (буду рад ошибиться)
Очень важно в формальной верификации то, что она ищет входные варианты гораздо более совершенным способом чем перебор, и находит нужные комбинации, даже если их 10^100.
Поэтому комбинаторного взрыва на входе она боится куда меньше чем брутфорс, и обнаружить даже Heartblead в принципе реально.
Благодарю вас за интересные и важные вопросы, которые помогают раскрыть статью.
Этот переход от перехода от кода к системе уравнений действительно является ключевым во всей концепции формальной верификации.
Именно этому моменту будет посвящена следующая статья, которая уже не за горами.
Я не хотел, чтобы первая статья показалась чрезмерно сложной для понимания.
Поэтому начал с упрощенного варианта, где вместо программы, на формальную логику переносится задача.
Хочу заверить, что принципы остаются теми же самыми, и следующая статья будет только дополнять эту новыми шагами.
В ней я расскажу о том как распарсить программу, превратить её в логическое выражение, сначала на языке самой программы.
А затем покажу, как сконвертировать это выражение в формальную логику.
Файлы, хранение данных и внешние вызовы я намерен затронуть в том числе.
Надеюсь, что моя статья несёт хоть какую-то полезность и в таком виде, так как статей по формальной верификации с примерами и кодом я на хабре не нашёл. (буду рад ошибиться)
Очень важно в формальной верификации то, что она ищет входные варианты гораздо более совершенным способом чем перебор, и находит нужные комбинации, даже если их 10^100.
Поэтому комбинаторного взрыва на входе она боится куда меньше чем брутфорс, и обнаружить даже Heartblead в принципе реально.
Благодарю вас за интересные и важные вопросы, которые помогают раскрыть статью.
UFO just landed and posted this here
Так и есть, Coq или Isabelle гораздо лучше подойдут для создания верифицированного кода.
В то время как Z3Prover удобней использовать для проверки уже написанного кода на любых других языках программирования.
Существует много фреймворков для автоматического аудита на базе Z3, которые заточены под поиск уязвимостей и не ставят перед собой задачи 100% формального доказательства.
В то время как Z3Prover удобней использовать для проверки уже написанного кода на любых других языках программирования.
Существует много фреймворков для автоматического аудита на базе Z3, которые заточены под поиск уязвимостей и не ставят перед собой задачи 100% формального доказательства.
По-видимому, программу, которая делает переход от кода к системе уравнений надо тоже верифицировать.
UFO just landed and posted this here
Да и в задаче о ферзях самую интересную работу за программу человек выполнил.
> Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
> Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
>… все… доказать, что их нет.
Круто.
> Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
>… все… доказать, что их нет.
Круто.
Жаль только неверно, баги-то могут быть, но только такие, которые есть и в самой спецификации, это конечно реже, чем просто ошибки в реализации, но тоже бывает.
Это одна из самых серьезных проблем в формальной верификации, которая приводит к тому что создание программ с доказанной эффективностью обходится в 10 раз дороже: это сложнее и требует больше времени.
Но если правила игры или условия программы, системы или контракта написаны естественным языком, но предельно чётким и без двухсмысленностей, как юридический, но ещё строже, так чтобы и человек, и компьютер понимал, то становится вполне возможным включить саму спецификацию в формальную систему вместе с программой и доказать её корректность.
Тем не менее, в спецификации всё равно может быть ошибка в том плане, что авторы спецификации задумали одно, а описали другое, но это уже выходит за рамки таких методов.
Задача формальной верификации — доказать, что во-первых, программа полностью соответствует спецификации, и во-вторых, что она не допускает никаких других сценариев (в том числе уязвимостей), которые в спецификации не описаны.
И она с этим справляется.
Но если правила игры или условия программы, системы или контракта написаны естественным языком, но предельно чётким и без двухсмысленностей, как юридический, но ещё строже, так чтобы и человек, и компьютер понимал, то становится вполне возможным включить саму спецификацию в формальную систему вместе с программой и доказать её корректность.
Тем не менее, в спецификации всё равно может быть ошибка в том плане, что авторы спецификации задумали одно, а описали другое, но это уже выходит за рамки таких методов.
Задача формальной верификации — доказать, что во-первых, программа полностью соответствует спецификации, и во-вторых, что она не допускает никаких других сценариев (в том числе уязвимостей), которые в спецификации не описаны.
И она с этим справляется.
создание программ с доказанной эффективностью обходится в 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]
но это уже выходит за рамки таких методов
и это нужно оговаривать чтобы не ввести в заблуждение тех кто ещё не в теме
Согласен, разница в цене и времени может сильно отличаться при разработке софта разного типа.
Если стоит задача разработать самое безопасное в мире микроядро операционной системы, как в случае seL4, то формальная верификация действительно будет дешевле других методов.
Что в принципе неудивительно, если разработка одной строчки кода даже до применения формальной верификации обходилась им в 1000$.
А стоимость создания верифицированного приложения по сравнению с обычным, в среднестатистических случаях программирования, как например, разработка веб-сайтов или создание мобильных приложений, будет уже от 10 раз дороже.
Это главная причина, по которой формальная верификация применяется довольно узко, и только там, где требуется максимальная надёжность и цена ошибки очень высока.
Если стоит задача разработать самое безопасное в мире микроядро операционной системы, как в случае seL4, то формальная верификация действительно будет дешевле других методов.
Что в принципе неудивительно, если разработка одной строчки кода даже до применения формальной верификации обходилась им в 1000$.
А стоимость создания верифицированного приложения по сравнению с обычным, в среднестатистических случаях программирования, как например, разработка веб-сайтов или создание мобильных приложений, будет уже от 10 раз дороже.
Это главная причина, по которой формальная верификация применяется довольно узко, и только там, где требуется максимальная надёжность и цена ошибки очень высока.
Интересно будет почитать применение формальной верификации к реальным фрагментам кода
Просто желтизна так и прёт.
Разумеется, нет. Формальная верификация проверяет соответствие программы формальной спецификации и только. Сама спецификация — специальный вид тестов с 100% покрытием (всех веток).
Баг в тесте (спецификации) — и у вас ровно такие же CVE'шки, как и без неё, только теперь у CVE есть тест, который проверяет, чтобы она была на месте.
Серебрянных пуль не бывает и писать софт без багов ещё никто не научился.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Разумеется, нет. Формальная верификация проверяет соответствие программы формальной спецификации и только. Сама спецификация — специальный вид тестов с 100% покрытием (всех веток).
Баг в тесте (спецификации) — и у вас ровно такие же CVE'шки, как и без неё, только теперь у CVE есть тест, который проверяет, чтобы она была на месте.
Серебрянных пуль не бывает и писать софт без багов ещё никто не научился.
Я не согласен с тем что это желтизна.
На мой взгляд формальная верификация действительно является самым мощным средством поиска и устранения уязвимостей, и это подтверждается её применением в ядре Windows, беспилотниках Darpa и самом безопасном микроядре seL4.
Формальная верификация на самом деле позволяет найти все проблемы в программе, и доказать её соответствие спецификации.
А то, что она гарантированно способна находить баги в самой спецификации, я и не утверждал.
Да и вообще склонен думать, что полное решения проблемы багов связанных с неверной спецификацией либо невозможно, или очень далеко.
Не вижу способов, как полностью справиться с той ситуацией, в которой программист или заказчик задумал одно, а в ТЗ написал другое, потеряв или неточно передав часть своих мыслей в процессе переноса на бумагу. И на практике такое встречается сплошь и рядом.
Поэтому с тем, что формальная верификация серебряной пулей не является, я согласен.
На мой взгляд формальная верификация действительно является самым мощным средством поиска и устранения уязвимостей, и это подтверждается её применением в ядре Windows, беспилотниках Darpa и самом безопасном микроядре seL4.
Формальная верификация на самом деле позволяет найти все проблемы в программе, и доказать её соответствие спецификации.
А то, что она гарантированно способна находить баги в самой спецификации, я и не утверждал.
Да и вообще склонен думать, что полное решения проблемы багов связанных с неверной спецификацией либо невозможно, или очень далеко.
Не вижу способов, как полностью справиться с той ситуацией, в которой программист или заказчик задумал одно, а в ТЗ написал другое, потеряв или неточно передав часть своих мыслей в процессе переноса на бумагу. И на практике такое встречается сплошь и рядом.
Поэтому с тем, что формальная верификация серебряной пулей не является, я согласен.
Я не понимаю, почему ядро Windows приводится в качестве примера системы без багов. www.cvedetails.com/cve/CVE-2019-0797 win32k — вполне себе ядро. www.cvedetails.com/cve/CVE-2019-0796 — тоже ядро.
Если формальная верификация находит эти баги, то почему они CVE? Насчёт «самое мощное» — мне сложно сказать, потому что сложность написания спецификации делает этот процесс не менее сложным, чем написание кода. А вот чем тестировать спецификацию — это вопрос открытый. end2end? Интеграционное тестирование? И дальше поехало обычное.
… Когда я говорю про баги в спецификации я говорю не про проблемы коммуникации между заказчиком и разработчиком, я говорю про обычные баги в коде. Спецификация пишется на формальном языке, мало отличающемся от какого-нибудь ML'я. И в нём делают натуральные баги. Букву перепутали, цифру не ту написали и т.д.
То есть если мы заменим «доказательство кода» на «тесты с 100% покрытием всех ветвлений», то картинка станет понятнее. В тестах тоже бывают баги. Хуже, если код пишется под тесты и тест заставляет реализующего реализовать ошибочное поведение, чтобы тест зелёным стал.
Если формальная верификация находит эти баги, то почему они CVE? Насчёт «самое мощное» — мне сложно сказать, потому что сложность написания спецификации делает этот процесс не менее сложным, чем написание кода. А вот чем тестировать спецификацию — это вопрос открытый. end2end? Интеграционное тестирование? И дальше поехало обычное.
… Когда я говорю про баги в спецификации я говорю не про проблемы коммуникации между заказчиком и разработчиком, я говорю про обычные баги в коде. Спецификация пишется на формальном языке, мало отличающемся от какого-нибудь ML'я. И в нём делают натуральные баги. Букву перепутали, цифру не ту написали и т.д.
То есть если мы заменим «доказательство кода» на «тесты с 100% покрытием всех ветвлений», то картинка станет понятнее. В тестах тоже бывают баги. Хуже, если код пишется под тесты и тест заставляет реализующего реализовать ошибочное поведение, чтобы тест зелёным стал.
Насколько мне известно, ядро 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% обеспечить выполнение первого пункта, но полностью решить второй ей не под силу.
Я также считаю проблему создания верной спецификации гораздо более сложной, чем её проверка на соответствие того что делает программа, и готов признать, что инструменты позволяющие эти проблемы решить можно рассматривать даже как более мощные, чем формальная верификация, средства.
Кроме того, я увлекаюсь генетическим программированием и прочими технологиями для синтеза программ, и зачастую сталкиваюсь с проблемой как создания спецификации вручную, так и её автоматической генерации.
Я на своём опыте убедился, что эти задачи гораздо сложнее формальной верификации.
Оно приведено лишь в качестве примера, где используется формальная верификация, и не более того.
То что 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% обеспечить выполнение первого пункта, но полностью решить второй ей не под силу.
Я также считаю проблему создания верной спецификации гораздо более сложной, чем её проверка на соответствие того что делает программа, и готов признать, что инструменты позволяющие эти проблемы решить можно рассматривать даже как более мощные, чем формальная верификация, средства.
Кроме того, я увлекаюсь генетическим программированием и прочими технологиями для синтеза программ, и зачастую сталкиваюсь с проблемой как создания спецификации вручную, так и её автоматической генерации.
Я на своём опыте убедился, что эти задачи гораздо сложнее формальной верификации.
То есть мы возвращаемся к модели «тесты с 100% покрытием».
С точки зрения надёжности программы это примерно эквивалентно «программа реализована два раза на разных языках программирования», с той поправкой, что точно известно, что покрыты все ветвления.
С точки зрения надёжности программы это примерно эквивалентно «программа реализована два раза на разных языках программирования», с той поправкой, что точно известно, что покрыты все ветвления.
Думаю можно сказать и так.
Двойная реализация обладает синергетическим эффектом и снижает число багов гораздо существеннее, чем в 2 раза.
Для того, чтобы баг выжил, необходимо наличие ошибок сразу в 2 местах: как в коде программе, так и в коде самого формального верификатора.
Если вероятность бага в верификаторе 1%, а в программе 10%, то мы получаем общую надёжность программы в 99.9%
На практике же верификаторы многократно проверяются, в том числе и другими верификаторами, поэтому надёжность формальной верификации рекурсивно стремится вообще к 100%
Известность того, что покрыты все ветвления как раз и является ключевым преимуществом формальной верификации перед тестами.
Тестами можно покрыть только те сценарии, о которых знает тот кто их пишет, а критерий полноты покрытия определяется человеком либо эвристически.
В то время как верификация проверяет вообще абсолютно все, в её случае 100% покрытие будет уже доказанным.
Двойная реализация обладает синергетическим эффектом и снижает число багов гораздо существеннее, чем в 2 раза.
Для того, чтобы баг выжил, необходимо наличие ошибок сразу в 2 местах: как в коде программе, так и в коде самого формального верификатора.
Если вероятность бага в верификаторе 1%, а в программе 10%, то мы получаем общую надёжность программы в 99.9%
На практике же верификаторы многократно проверяются, в том числе и другими верификаторами, поэтому надёжность формальной верификации рекурсивно стремится вообще к 100%
Известность того, что покрыты все ветвления как раз и является ключевым преимуществом формальной верификации перед тестами.
Тестами можно покрыть только те сценарии, о которых знает тот кто их пишет, а критерий полноты покрытия определяется человеком либо эвристически.
В то время как верификация проверяет вообще абсолютно все, в её случае 100% покрытие будет уже доказанным.
Во, мне нравится формулировка: «У формальной верификации доказанное 100% покрытие тестами всех случаев для всех видов данных». Оно не утверждает, что программа без багов, оно не содержит схоластическое «соответствует спецификации» (потому что в голове в этот момент «спецификация» человеком, а на самом деле это код). Оно реально говорит о существенном преимуществе — гарантированном покрытии всех случаев тестами.
Сами тесты могут быть с багами. Но хотя бы они есть.
Сами тесты могут быть с багами. Но хотя бы они есть.
Вполне согласен.
На мой взгляд концептуально формальная верификация и покрытие кода тестами похожи и относятся к одной категории.
Если попробовать их сравнить, то я вижу 2 отличия:
1) Это как раз то, что формальная верификация дает доказанное 100% покрытие тестами.
2) Тесты пишет не человек, а формальный верификатор, который хоть и может ошибаться, но надёжность его стремится к 100% и многократно превосходит человеческую.
На мой взгляд концептуально формальная верификация и покрытие кода тестами похожи и относятся к одной категории.
Если попробовать их сравнить, то я вижу 2 отличия:
1) Это как раз то, что формальная верификация дает доказанное 100% покрытие тестами.
2) Тесты пишет не человек, а формальный верификатор, который хоть и может ошибаться, но надёжность его стремится к 100% и многократно превосходит человеческую.
Тесты пишет человек. На том самом «языке спецификаций» который с точки зрения написания ничем от мунспика bdd, например, не отличается. Что там из него генерируют машины уже не важно. Исходный код тестов — это спеицификация.
Я сторонник такого подхода, в котором тесты должны автоматически генерироваться из публичного описания программы на естественном, или, по крайней мере, понятном для обычного и не обладающего навыками программирования человека языке.
Это позволит исключить человеческий фактор из процесса написания тестов.
В идеале, формальная верификация должна доказывать что программа соответствует её публичному, человеческому описанию.
Это позволит исключить человеческий фактор из процесса написания тестов.
В идеале, формальная верификация должна доказывать что программа соответствует её публичному, человеческому описанию.
вы всего лишь один машиночитаемый язык заменяете на другой. Все языки программирования исходят из того, что «естественный» и «понятный для человека». С этим лозунгом писали фортран, си и т.д., сути проблемы это не меняет — это язык программирования (как бы он не маскировался под естественный) и цена ошибки или неоднозначности в нём — баг в программе.
Уже много раз была шутка про «купи в магазине бутылку молока, а если будут яйца, то возьми шесть».
Уже много раз была шутка про «купи в магазине бутылку молока, а если будут яйца, то возьми шесть».
Я не спорю с тем, что существующие «естественные и понятные для человека» языки программирования оставляют желать лучшего.
Надеюсь, мы увидим прогресс в направлении создания действительно понятных языков программирования, и формализации человеческой речи вообще.
На мой взгляд, вполне возможно (или будет возможно) генерировать человеко-понятные приказы или спецификации исходя из лишь из конечных целей.
Допустим, компьютеризированный холодильник обнаружил, что ему не хватает 1 бутылки молока и 6 яиц.
На примере этого он должен сгенерировать однозначное и понятное приказание для человека вида «Необходимо купить бутылку молока и 6 яиц, а если яиц не будет, то только молоко.».
И ответственность здесь лежит именно на холодильнике, это он должен генерировать адекватные описания, а не человек разбираться в непонятных.
Надеюсь, мы увидим прогресс в направлении создания действительно понятных языков программирования, и формализации человеческой речи вообще.
На мой взгляд, вполне возможно (или будет возможно) генерировать человеко-понятные приказы или спецификации исходя из лишь из конечных целей.
Допустим, компьютеризированный холодильник обнаружил, что ему не хватает 1 бутылки молока и 6 яиц.
На примере этого он должен сгенерировать однозначное и понятное приказание для человека вида «Необходимо купить бутылку молока и 6 яиц, а если яиц не будет, то только молоко.».
И ответственность здесь лежит именно на холодильнике, это он должен генерировать адекватные описания, а не человек разбираться в непонятных.
Я вам привёл пример спецификации, написанной на ествественном, понятном человеку языке, которая вызывает неоднозначности и баги.
С лёгкостью можно накрутить достаточно, чтобы баг остался в любом уровне фашизма при валидации, просто потому, что ествественный язык всегда оставляет пространство для неоднозначности, а как только вы его исключаете, язык перестаёт быть естественным.
Надо перестать пытаться натянуть сову на пень и признать, что любая спецификация — машиночитаемый язык программирования. К которому применимы все те же проблемы и решения, как и к любому другому языку.
С лёгкостью можно накрутить достаточно, чтобы баг остался в любом уровне фашизма при валидации, просто потому, что ествественный язык всегда оставляет пространство для неоднозначности, а как только вы его исключаете, язык перестаёт быть естественным.
Надо перестать пытаться натянуть сову на пень и признать, что любая спецификация — машиночитаемый язык программирования. К которому применимы все те же проблемы и решения, как и к любому другому языку.
Вы привели пример, когда один человек даёт задачу, или создаёт спецификацию, для другого.
На мой взгляд это выходит за рамки информационных технологий, а помогать людям взаимодействовать между собой будет лучше социологам и психологам.
Но я считаю, что проблема создания человеком понятной для компьютера спецификации, или же наоборот, создание компьютером понятной для человека в принципе решаема.
На настоящий момент я признаю то, что любые спецификации ещё очень далеки от естественных.
Но я искренне верю, что в будущем обязательно появятся спецификации, которые будут читаемы как людьми, и машинами.
Я сам увлекаюсь созданием таких спецификаций в том числе.
Кроме того, я считаю что нужно идти к решению этой проблемы с 2 концов: как повышать естественность языков, так и образованность людей, обучая их основам логики и программирования.
На мой взгляд это выходит за рамки информационных технологий, а помогать людям взаимодействовать между собой будет лучше социологам и психологам.
Но я считаю, что проблема создания человеком понятной для компьютера спецификации, или же наоборот, создание компьютером понятной для человека в принципе решаема.
На настоящий момент я признаю то, что любые спецификации ещё очень далеки от естественных.
Но я искренне верю, что в будущем обязательно появятся спецификации, которые будут читаемы как людьми, и машинами.
Я сам увлекаюсь созданием таких спецификаций в том числе.
Кроме того, я считаю что нужно идти к решению этой проблемы с 2 концов: как повышать естественность языков, так и образованность людей, обучая их основам логики и программирования.
Дело не в том, кому они будут понятны. Дело в том, можно ли в таких спецификациях написать код с багами. Очевидно, что можно. Особенно, если баг ведёт не к внутренней неконсистентности (это можно отследить), а к внешней (вне модели). Шутка про молоко — отличный пример.
Не спорю с тем, что пример отличный, но он относится только к взаимодействию 2 людей, что совершенно меняет всю картину и больше относится к социологии, чем IT.
Если и спецификацию, и код пишет машина, с применением формальных методов, то на данный момент вполне достижимо добиться практически 100% отсутствия багов.
И я верю, что в будущем, в дополнении к этому, удастся добиться и 100% естественности/понятности таких спецификаций как для людей, так и машин.
Надеюсь, что и мне удастся внести свой вклад в объединение этих двух миров.
Если и спецификацию, и код пишет машина, с применением формальных методов, то на данный момент вполне достижимо добиться практически 100% отсутствия багов.
И я верю, что в будущем, в дополнении к этому, удастся добиться и 100% естественности/понятности таких спецификаций как для людей, так и машин.
Надеюсь, что и мне удастся внести свой вклад в объединение этих двух миров.
Если и код и спецификацию пишет машина, то откуда она знает что писать? Вот это «что-то» и есть исходный код.
Машина может сгенерировать исходный код только имея входные и выходные данные.
Для этого обычно применяют нейросети или генетические алгоритмы, но SMT/SAT решатели тоже применяются для этой цели и в некоторых случаях превосходят все другие подходы.
И даже более того, машина в принципе может сгенерировать описание, спецификацию, входные данные и исходный код только лишь имея выходные данные в достаточном количестве.
Но это уже к синтезу программ и алгоритмов относится.
Для этого обычно применяют нейросети или генетические алгоритмы, но SMT/SAT решатели тоже применяются для этой цели и в некоторых случаях превосходят все другие подходы.
И даже более того, машина в принципе может сгенерировать описание, спецификацию, входные данные и исходный код только лишь имея выходные данные в достаточном количестве.
Но это уже к синтезу программ и алгоритмов относится.
А вот тут Остапа начало нести.
Удачи ездить на лифте, чей код и спецификация сгенерированы нейронной сетью.
Удачи ездить на лифте, чей код и спецификация сгенерированы нейронной сетью.
Благодарю, удача в этом нелёгком деле мне пригодится!
Остапом, однако, я себя не считаю, а все свои доводы и суждения буду подкреплять работающим кодом.
Нейронные сети уже достаточно хорошо изучены, и в эту сферу сложно привнести что-то новое.
Меня больше интересуют методы синтеза программ только лишь по входным и выходным данным конкретно с помощью SMT/SAT.
Это не моё изобретение, такой подход уже имеет место быть, хоть и не слишком известен.
В одной из следующей статей я намерен осветить и эту тематику, тоже на конкретных примерах.
Остапом, однако, я себя не считаю, а все свои доводы и суждения буду подкреплять работающим кодом.
Нейронные сети уже достаточно хорошо изучены, и в эту сферу сложно привнести что-то новое.
Меня больше интересуют методы синтеза программ только лишь по входным и выходным данным конкретно с помощью SMT/SAT.
Это не моё изобретение, такой подход уже имеет место быть, хоть и не слишком известен.
В одной из следующей статей я намерен осветить и эту тематику, тоже на конкретных примерах.
А, я понял о чём вы. Дайте мне ввод и вывод и я сгенерирую вам код.
… Это работает только в мире розовых пони и функций без сайд-эффектов. Как вы сайд-эффект в выводе опишите-то? Трепыхать светодиодом 3 милисекунды.
Что такое 3 милисекунды? Какой тип данных позволяет запретить выполнение кода дольше трёх милисекунд?
… Это работает только в мире розовых пони и функций без сайд-эффектов. Как вы сайд-эффект в выводе опишите-то? Трепыхать светодиодом 3 милисекунды.
Что такое 3 милисекунды? Какой тип данных позволяет запретить выполнение кода дольше трёх милисекунд?
Как ни странно, но в программировании немало и таких миров.
Кроме розовых пони, там порой обитают и единороги: стартапы или компании которые вышли на капитализацию свыше миллиарда долларов.
Приведу цитату из официального сайта той, самой безопасной в мире 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 летают не взирая на сайд-эффекты.
Кроме розовых пони, там порой обитают и единороги: стартапы или компании которые вышли на капитализацию свыше миллиарда долларов.
Приведу цитату из официального сайта той, самой безопасной в мире 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 летают не взирая на сайд-эффекты.
Я эту же задачу делал на Майкрософтовском (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]Простые и наглядные альтернативы очень радуют!
Я не претендую на академичность своей статьи, и сосредоточился на том чтобы сделать её понятной для максимального числа читателей.
Tla относится к той же категории языков, что и Coq либо Isabelle.
Они позволяют создавать формально доказанные программы.
А мой выбор Z3Prover обусловлен тем, что я больше смотрю на практический поиск уязвимостей, и в следующих статьях приступлю к трансляции программ с типичных языков в формальную логику.
Z3 подходит для этого лучше всего.
Я не претендую на академичность своей статьи, и сосредоточился на том чтобы сделать её понятной для максимального числа читателей.
Tla относится к той же категории языков, что и Coq либо Isabelle.
Они позволяют создавать формально доказанные программы.
А мой выбор Z3Prover обусловлен тем, что я больше смотрю на практический поиск уязвимостей, и в следующих статьях приступлю к трансляции программ с типичных языков в формальную логику.
Z3 подходит для этого лучше всего.
А никого не смущает, что решение, которое описано в тексте — неправильное?
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Момент с вторичной переправой капусты (которой уже нет на берегу) — это как?
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Момент с вторичной переправой капусты (которой уже нет на берегу) — это как?
Вы правы, и оказились наблюдательней меня!
Решение, которое выдала формальная верификация полностью корректно, в чём можно убедиться проверив запись в виде 0 и 1.
А вот моя текстовая интерпретация — нет.
Я всё-таки человек, и в отличии от формального верификатора иногда допускаю ошибки…
Вместо
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Должно быть
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Я исправлю статью, но оставлю хронику ошибки в этом комментарии.
Это наглядная демонстрация того, почему формальная верификация не является серебряной пулей.
Если сравнить с поиском уязвимостей, то это такой случай, где верификатор выдал мне конкретный и верный рецепт, но в итоге проникнуть в систему я не смог так как перепутал шаги.
Решение, которое выдала формальная верификация полностью корректно, в чём можно убедиться проверив запись в виде 0 и 1.
А вот моя текстовая интерпретация — нет.
Я всё-таки человек, и в отличии от формального верификатора иногда допускаю ошибки…
Вместо
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Должно быть
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Я исправлю статью, но оставлю хронику ошибки в этом комментарии.
Это наглядная демонстрация того, почему формальная верификация не является серебряной пулей.
Если сравнить с поиском уязвимостей, то это такой случай, где верификатор выдал мне конкретный и верный рецепт, но в итоге проникнуть в систему я не смог так как перепутал шаги.
We know each queen must be in a different row. So, we represent each queen by a single integer: the column position
Мы уже знаем правильный ответ, поэтому используем такую форму представления, где всего 40 тыс. возможных комбинаций, чтобы программа справилась с задачей.
Давайте «упростим» задачу. Сделаем не 8, а 9 ферзей. Любой ребенок, знакомый с шахматами, за секунду скажет, что задача не имеет решения. Правда, теперь мы не будем использовать то, что мы «знаем», что каждый ферзь находится в своем ряду, а представим каждого ферзя двумя координатами, как и положено в шахматах. С каждым ферзем свяжем не одно целое число, а набор координатных пар, соответствующих тем клеткам, которые ферзь бьет. И единственным ограничением будет то, что множество битых ферзями клеток не пересекается с множеством занятых ферзями клеток. Сможет ли замечательный верификатор за разумное время решить задачу?
Мы уже знаем правильный ответ, поэтому используем такую форму представления, где всего 40 тыс. возможных комбинаций, чтобы программа справилась с задачей.
Давайте «упростим» задачу. Сделаем не 8, а 9 ферзей. Любой ребенок, знакомый с шахматами, за секунду скажет, что задача не имеет решения. Правда, теперь мы не будем использовать то, что мы «знаем», что каждый ферзь находится в своем ряду, а представим каждого ферзя двумя координатами, как и положено в шахматах. С каждым ферзем свяжем не одно целое число, а набор координатных пар, соответствующих тем клеткам, которые ферзь бьет. И единственным ограничением будет то, что множество битых ферзями клеток не пересекается с множеством занятых ферзями клеток. Сможет ли замечательный верификатор за разумное время решить задачу?
У меня раньше был разряд по шахматам, и я пробовал писать свои шахматные программы.
Такая форма представления в виде 8 строчек и колонок сразу приходит в голову. Она позволяет проще проверять, какие поля бьёт слон, ладья или ферзь, да и по сути является способом представления геометрии доски в программе.
И в задаче с ферзями это будет банально самая лаконичная запись.
Если взять 64 клетки, то придётся гораздо дольше описывать сами понятия горизонталей и вертикалей.
Это я к тому, что никакой подгонки под задачу нет, а попросту было выбрано самое удобное и быстрое в написании представление.
Но ваша идея мне нравится, если будет свободная минутка, то постараюсь её опробовать и рассказать, справился ли верификатор или нет.
С точки зрения вычисления такая задача будет действительно сложней.
А пока проведём более простой эксперимент:
В такой задаче 40 320 (если не брать в учёт перестановки).
Это факториал от 8.
Если увеличить число ферзей до 20, это даст уже порядка 10^18 вариантов.
Z3Prover при этом всё так же справляется мгновенно.
Добавим нагрузки и увеличим их число до 30, что даст около 10^32 способов расстановки ферзей на доске.
Z3Prover задумался секунд на 5, но решение выдал.
Вот оно:
Наш замечательный верификатор справляется неплохо, поскольку он использует гораздо более мощные алгоритмы нежели обычный перебор.
Но у Z3Prover, конечно, тоже есть свои пределы, связанные главным образом с тем что в итоге он упирается в проблему P=NP.
При 40 ферзях дать быстрый ответ он уже не смог.
Такая форма представления в виде 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 ферзях дать быстрый ответ он уже не смог.
А использовать Z3 без питона как-нибудь можно?
Sign up to leave a comment.
Формальная верификация на примере задачи о волке, козе и капусте