Не спорю с тем, что пример отличный, но он относится только к взаимодействию 2 людей, что совершенно меняет всю картину и больше относится к социологии, чем IT.
Если и спецификацию, и код пишет машина, с применением формальных методов, то на данный момент вполне достижимо добиться практически 100% отсутствия багов.
И я верю, что в будущем, в дополнении к этому, удастся добиться и 100% естественности/понятности таких спецификаций как для людей, так и машин.
Надеюсь, что и мне удастся внести свой вклад в объединение этих двух миров.
Вы привели пример, когда один человек даёт задачу, или создаёт спецификацию, для другого.
На мой взгляд это выходит за рамки информационных технологий, а помогать людям взаимодействовать между собой будет лучше социологам и психологам.
Но я считаю, что проблема создания человеком понятной для компьютера спецификации, или же наоборот, создание компьютером понятной для человека в принципе решаема.
На настоящий момент я признаю то, что любые спецификации ещё очень далеки от естественных.
Но я искренне верю, что в будущем обязательно появятся спецификации, которые будут читаемы как людьми, и машинами.
Я сам увлекаюсь созданием таких спецификаций в том числе.
Кроме того, я считаю что нужно идти к решению этой проблемы с 2 концов: как повышать естественность языков, так и образованность людей, обучая их основам логики и программирования.
Я не спорю с тем, что существующие «естественные и понятные для человека» языки программирования оставляют желать лучшего.
Надеюсь, мы увидим прогресс в направлении создания действительно понятных языков программирования, и формализации человеческой речи вообще.
На мой взгляд, вполне возможно (или будет возможно) генерировать человеко-понятные приказы или спецификации исходя из лишь из конечных целей.
Допустим, компьютеризированный холодильник обнаружил, что ему не хватает 1 бутылки молока и 6 яиц.
На примере этого он должен сгенерировать однозначное и понятное приказание для человека вида «Необходимо купить бутылку молока и 6 яиц, а если яиц не будет, то только молоко.».
И ответственность здесь лежит именно на холодильнике, это он должен генерировать адекватные описания, а не человек разбираться в непонятных.
Я сторонник такого подхода, в котором тесты должны автоматически генерироваться из публичного описания программы на естественном, или, по крайней мере, понятном для обычного и не обладающего навыками программирования человека языке.
Это позволит исключить человеческий фактор из процесса написания тестов.
В идеале, формальная верификация должна доказывать что программа соответствует её публичному, человеческому описанию.
На мой взгляд концептуально формальная верификация и покрытие кода тестами похожи и относятся к одной категории.
Если попробовать их сравнить, то я вижу 2 отличия:
1) Это как раз то, что формальная верификация дает доказанное 100% покрытие тестами.
2) Тесты пишет не человек, а формальный верификатор, который хоть и может ошибаться, но надёжность его стремится к 100% и многократно превосходит человеческую.
Думаю можно сказать и так.
Двойная реализация обладает синергетическим эффектом и снижает число багов гораздо существеннее, чем в 2 раза.
Для того, чтобы баг выжил, необходимо наличие ошибок сразу в 2 местах: как в коде программе, так и в коде самого формального верификатора.
Если вероятность бага в верификаторе 1%, а в программе 10%, то мы получаем общую надёжность программы в 99.9%
На практике же верификаторы многократно проверяются, в том числе и другими верификаторами, поэтому надёжность формальной верификации рекурсивно стремится вообще к 100%
Известность того, что покрыты все ветвления как раз и является ключевым преимуществом формальной верификации перед тестами.
Тестами можно покрыть только те сценарии, о которых знает тот кто их пишет, а критерий полноты покрытия определяется человеком либо эвристически.
В то время как верификация проверяет вообще абсолютно все, в её случае 100% покрытие будет уже доказанным.
Не помешает.
Кроме того качество формальных верификаторов можно обеспечить проверкой того, что он находит в том числе все баги и уязвимости найденные как людьми, так и другими формальными верификаторами, в итоге надёжность стремится к 100%.
Я больше увлекаюсь практическим поиском уязвимостей, нежели формальным доказательством программ, поэтому интересуюсь в первую очередь Z3Prover и SMT/SAT решателями.
Но возможно я расскажу об этих языках в будущих статьях.
Насколько мне известно, ядро Windows имеет элементы, прошедшие формальную верификацию, но полного покрытия нет.
Оно приведено лишь в качестве примера, где используется формальная верификация, и не более того.
То что Microsoft признает такой подход и применяет его, свидетельствует о наличии в нём определённых преимуществ.
Если написать спецификацию в формате, понятном как человеку, так и компьютеру (например, в виде более строгой и ограниченной версии юридического языка исключающую двоякое трактование), а затем включить её внутрь формальной модели, то соответствие программы формальной спецификации вполне будет доказано.
Затем конечный пользователь программы может прочесть его описание, и сделать вывод, устраивает оно его или нет.
Если устраивает, то можно пользоваться. Если заметит опечатки или подозрительные цифры, можно отказаться от использования такой программы.
Я описывал не проблему коммуникации между заказчиком и разработчиком, а более конкретный и узкий случай переноса задуманной спецификации из мозга на бумагу.
Можно сформулировать это так, что спецификация считается корректной если выполняется 2 условия:
1) Спецификация полностью соответствует тому что делает программа, созданная на её основе.
2) Спецификация полностью отражает то, что задумал её создатель.
Формальная верификация позволяет на 100% обеспечить выполнение первого пункта, но полностью решить второй ей не под силу.
Я также считаю проблему создания верной спецификации гораздо более сложной, чем её проверка на соответствие того что делает программа, и готов признать, что инструменты позволяющие эти проблемы решить можно рассматривать даже как более мощные, чем формальная верификация, средства.
Кроме того, я увлекаюсь генетическим программированием и прочими технологиями для синтеза программ, и зачастую сталкиваюсь с проблемой как создания спецификации вручную, так и её автоматической генерации.
Я на своём опыте убедился, что эти задачи гораздо сложнее формальной верификации.
Вы правы, и оказились наблюдательней меня!
Решение, которое выдала формальная верификация полностью корректно, в чём можно убедиться проверив запись в виде 0 и 1.
А вот моя текстовая интерпретация — нет.
Я всё-таки человек, и в отличии от формального верификатора иногда допускаю ошибки…
Вместо
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Должно быть
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Я исправлю статью, но оставлю хронику ошибки в этом комментарии.
Это наглядная демонстрация того, почему формальная верификация не является серебряной пулей.
Если сравнить с поиском уязвимостей, то это такой случай, где верификатор выдал мне конкретный и верный рецепт, но в итоге проникнуть в систему я не смог так как перепутал шаги.
Простые и наглядные альтернативы очень радуют!
Я не претендую на академичность своей статьи, и сосредоточился на том чтобы сделать её понятной для максимального числа читателей.
Tla относится к той же категории языков, что и Coq либо Isabelle.
Они позволяют создавать формально доказанные программы.
А мой выбор Z3Prover обусловлен тем, что я больше смотрю на практический поиск уязвимостей, и в следующих статьях приступлю к трансляции программ с типичных языков в формальную логику.
Z3 подходит для этого лучше всего.
Я не согласен с тем что это желтизна.
На мой взгляд формальная верификация действительно является самым мощным средством поиска и устранения уязвимостей, и это подтверждается её применением в ядре Windows, беспилотниках Darpa и самом безопасном микроядре seL4.
Формальная верификация на самом деле позволяет найти все проблемы в программе, и доказать её соответствие спецификации.
А то, что она гарантированно способна находить баги в самой спецификации, я и не утверждал.
Да и вообще склонен думать, что полное решения проблемы багов связанных с неверной спецификацией либо невозможно, или очень далеко.
Не вижу способов, как полностью справиться с той ситуацией, в которой программист или заказчик задумал одно, а в ТЗ написал другое, потеряв или неточно передав часть своих мыслей в процессе переноса на бумагу. И на практике такое встречается сплошь и рядом.
Поэтому с тем, что формальная верификация серебряной пулей не является, я согласен.
Согласен, разница в цене и времени может сильно отличаться при разработке софта разного типа.
Если стоит задача разработать самое безопасное в мире микроядро операционной системы, как в случае seL4, то формальная верификация действительно будет дешевле других методов.
Что в принципе неудивительно, если разработка одной строчки кода даже до применения формальной верификации обходилась им в 1000$.
А стоимость создания верифицированного приложения по сравнению с обычным, в среднестатистических случаях программирования, как например, разработка веб-сайтов или создание мобильных приложений, будет уже от 10 раз дороже.
Это главная причина, по которой формальная верификация применяется довольно узко, и только там, где требуется максимальная надёжность и цена ошибки очень высока.
Так и есть, Coq или Isabelle гораздо лучше подойдут для создания верифицированного кода.
В то время как Z3Prover удобней использовать для проверки уже написанного кода на любых других языках программирования.
Существует много фреймворков для автоматического аудита на базе Z3, которые заточены под поиск уязвимостей и не ставят перед собой задачи 100% формального доказательства.
Это одна из самых серьезных проблем в формальной верификации, которая приводит к тому что создание программ с доказанной эффективностью обходится в 10 раз дороже: это сложнее и требует больше времени.
Но если правила игры или условия программы, системы или контракта написаны естественным языком, но предельно чётким и без двухсмысленностей, как юридический, но ещё строже, так чтобы и человек, и компьютер понимал, то становится вполне возможным включить саму спецификацию в формальную систему вместе с программой и доказать её корректность.
Тем не менее, в спецификации всё равно может быть ошибка в том плане, что авторы спецификации задумали одно, а описали другое, но это уже выходит за рамки таких методов.
Задача формальной верификации — доказать, что во-первых, программа полностью соответствует спецификации, и во-вторых, что она не допускает никаких других сценариев (в том числе уязвимостей), которые в спецификации не описаны.
И она с этим справляется.
Вы абсолютно правы!
Этот переход от перехода от кода к системе уравнений действительно является ключевым во всей концепции формальной верификации.
Именно этому моменту будет посвящена следующая статья, которая уже не за горами.
Я не хотел, чтобы первая статья показалась чрезмерно сложной для понимания.
Поэтому начал с упрощенного варианта, где вместо программы, на формальную логику переносится задача.
Хочу заверить, что принципы остаются теми же самыми, и следующая статья будет только дополнять эту новыми шагами.
В ней я расскажу о том как распарсить программу, превратить её в логическое выражение, сначала на языке самой программы.
А затем покажу, как сконвертировать это выражение в формальную логику.
Файлы, хранение данных и внешние вызовы я намерен затронуть в том числе.
Надеюсь, что моя статья несёт хоть какую-то полезность и в таком виде, так как статей по формальной верификации с примерами и кодом я на хабре не нашёл. (буду рад ошибиться)
Очень важно в формальной верификации то, что она ищет входные варианты гораздо более совершенным способом чем перебор, и находит нужные комбинации, даже если их 10^100.
Поэтому комбинаторного взрыва на входе она боится куда меньше чем брутфорс, и обнаружить даже Heartblead в принципе реально.
Благодарю вас за интересные и важные вопросы, которые помогают раскрыть статью.
Вначале статьи я обозначил, что расскажу несколько слов о том что такое формальная верификация, а затем приведу наглядные примеры, так, немного скомкано, переход и происходит…
Ядро Windows и задача о 8 ферзях связаны тем, что Z3Prover применяется в обоих случаях.
К тому же Z3Prover является разработкой от Microsoft Research, которым они же и ищут уязвимости в ядре.
Но вы правы, целостность повествования не столь хороша как хотелось бы.
В задаче о 8 ферзях уязвимостей нет, а сам пример был приведён главным образом для наглядной демонстрации механизмов и принципов работы Z3Prover, начиная с самых простых случаев.
Я показал принцип нахождения необходимой комбинации входных данных, в том случае, когда выходные данные и алгоритм известны.
Я согласен с вашей леммой о программе без условных циклов, переходов, которая всегда остановит свою работу.
Могу добавить, что некоторые языки программирования специально устанавливают такие ограничения, и таким образом все программы будут иметь конечную и предсказуемую сложность.
В следующей статье я как раз собираюсь написать о применении формальной верификации для нахождения уязвимостей в программах на таком языке, поскольку они прекрасно совместимы.
А итоге я верифицировал, что задача о волке, козе и капусты имеет решение за 8 шагов, а также то, что версия этой задачи со всеядным волком решения не имеет.
Если и спецификацию, и код пишет машина, с применением формальных методов, то на данный момент вполне достижимо добиться практически 100% отсутствия багов.
И я верю, что в будущем, в дополнении к этому, удастся добиться и 100% естественности/понятности таких спецификаций как для людей, так и машин.
Надеюсь, что и мне удастся внести свой вклад в объединение этих двух миров.
На мой взгляд это выходит за рамки информационных технологий, а помогать людям взаимодействовать между собой будет лучше социологам и психологам.
Но я считаю, что проблема создания человеком понятной для компьютера спецификации, или же наоборот, создание компьютером понятной для человека в принципе решаема.
На настоящий момент я признаю то, что любые спецификации ещё очень далеки от естественных.
Но я искренне верю, что в будущем обязательно появятся спецификации, которые будут читаемы как людьми, и машинами.
Я сам увлекаюсь созданием таких спецификаций в том числе.
Кроме того, я считаю что нужно идти к решению этой проблемы с 2 концов: как повышать естественность языков, так и образованность людей, обучая их основам логики и программирования.
Надеюсь, мы увидим прогресс в направлении создания действительно понятных языков программирования, и формализации человеческой речи вообще.
На мой взгляд, вполне возможно (или будет возможно) генерировать человеко-понятные приказы или спецификации исходя из лишь из конечных целей.
Допустим, компьютеризированный холодильник обнаружил, что ему не хватает 1 бутылки молока и 6 яиц.
На примере этого он должен сгенерировать однозначное и понятное приказание для человека вида «Необходимо купить бутылку молока и 6 яиц, а если яиц не будет, то только молоко.».
И ответственность здесь лежит именно на холодильнике, это он должен генерировать адекватные описания, а не человек разбираться в непонятных.
Это позволит исключить человеческий фактор из процесса написания тестов.
В идеале, формальная верификация должна доказывать что программа соответствует её публичному, человеческому описанию.
На мой взгляд концептуально формальная верификация и покрытие кода тестами похожи и относятся к одной категории.
Если попробовать их сравнить, то я вижу 2 отличия:
1) Это как раз то, что формальная верификация дает доказанное 100% покрытие тестами.
2) Тесты пишет не человек, а формальный верификатор, который хоть и может ошибаться, но надёжность его стремится к 100% и многократно превосходит человеческую.
Двойная реализация обладает синергетическим эффектом и снижает число багов гораздо существеннее, чем в 2 раза.
Для того, чтобы баг выжил, необходимо наличие ошибок сразу в 2 местах: как в коде программе, так и в коде самого формального верификатора.
Если вероятность бага в верификаторе 1%, а в программе 10%, то мы получаем общую надёжность программы в 99.9%
На практике же верификаторы многократно проверяются, в том числе и другими верификаторами, поэтому надёжность формальной верификации рекурсивно стремится вообще к 100%
Известность того, что покрыты все ветвления как раз и является ключевым преимуществом формальной верификации перед тестами.
Тестами можно покрыть только те сценарии, о которых знает тот кто их пишет, а критерий полноты покрытия определяется человеком либо эвристически.
В то время как верификация проверяет вообще абсолютно все, в её случае 100% покрытие будет уже доказанным.
Кроме того качество формальных верификаторов можно обеспечить проверкой того, что он находит в том числе все баги и уязвимости найденные как людьми, так и другими формальными верификаторами, в итоге надёжность стремится к 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% обеспечить выполнение первого пункта, но полностью решить второй ей не под силу.
Я также считаю проблему создания верной спецификации гораздо более сложной, чем её проверка на соответствие того что делает программа, и готов признать, что инструменты позволяющие эти проблемы решить можно рассматривать даже как более мощные, чем формальная верификация, средства.
Кроме того, я увлекаюсь генетическим программированием и прочими технологиями для синтеза программ, и зачастую сталкиваюсь с проблемой как создания спецификации вручную, так и её автоматической генерации.
Я на своём опыте убедился, что эти задачи гораздо сложнее формальной верификации.
Решение, которое выдала формальная верификация полностью корректно, в чём можно убедиться проверив запись в виде 0 и 1.
А вот моя текстовая интерпретация — нет.
Я всё-таки человек, и в отличии от формального верификатора иногда допускаю ошибки…
Вместо
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа капусты, возврат обратно в одиночку, переправа волка.
Должно быть
В нашем случае фермер поступил так: старт, отдых, отдых, переправа козы, переправа обратно, переправа капусты, возврат с козой, переправа волка, возврат обратно в одиночку, повторная доставка козы.
Я исправлю статью, но оставлю хронику ошибки в этом комментарии.
Это наглядная демонстрация того, почему формальная верификация не является серебряной пулей.
Если сравнить с поиском уязвимостей, то это такой случай, где верификатор выдал мне конкретный и верный рецепт, но в итоге проникнуть в систему я не смог так как перепутал шаги.
Я не претендую на академичность своей статьи, и сосредоточился на том чтобы сделать её понятной для максимального числа читателей.
Tla относится к той же категории языков, что и Coq либо Isabelle.
Они позволяют создавать формально доказанные программы.
А мой выбор Z3Prover обусловлен тем, что я больше смотрю на практический поиск уязвимостей, и в следующих статьях приступлю к трансляции программ с типичных языков в формальную логику.
Z3 подходит для этого лучше всего.
На мой взгляд формальная верификация действительно является самым мощным средством поиска и устранения уязвимостей, и это подтверждается её применением в ядре Windows, беспилотниках Darpa и самом безопасном микроядре seL4.
Формальная верификация на самом деле позволяет найти все проблемы в программе, и доказать её соответствие спецификации.
А то, что она гарантированно способна находить баги в самой спецификации, я и не утверждал.
Да и вообще склонен думать, что полное решения проблемы багов связанных с неверной спецификацией либо невозможно, или очень далеко.
Не вижу способов, как полностью справиться с той ситуацией, в которой программист или заказчик задумал одно, а в ТЗ написал другое, потеряв или неточно передав часть своих мыслей в процессе переноса на бумагу. И на практике такое встречается сплошь и рядом.
Поэтому с тем, что формальная верификация серебряной пулей не является, я согласен.
Если стоит задача разработать самое безопасное в мире микроядро операционной системы, как в случае seL4, то формальная верификация действительно будет дешевле других методов.
Что в принципе неудивительно, если разработка одной строчки кода даже до применения формальной верификации обходилась им в 1000$.
А стоимость создания верифицированного приложения по сравнению с обычным, в среднестатистических случаях программирования, как например, разработка веб-сайтов или создание мобильных приложений, будет уже от 10 раз дороже.
Это главная причина, по которой формальная верификация применяется довольно узко, и только там, где требуется максимальная надёжность и цена ошибки очень высока.
В то время как Z3Prover удобней использовать для проверки уже написанного кода на любых других языках программирования.
Существует много фреймворков для автоматического аудита на базе Z3, которые заточены под поиск уязвимостей и не ставят перед собой задачи 100% формального доказательства.
Но если правила игры или условия программы, системы или контракта написаны естественным языком, но предельно чётким и без двухсмысленностей, как юридический, но ещё строже, так чтобы и человек, и компьютер понимал, то становится вполне возможным включить саму спецификацию в формальную систему вместе с программой и доказать её корректность.
Тем не менее, в спецификации всё равно может быть ошибка в том плане, что авторы спецификации задумали одно, а описали другое, но это уже выходит за рамки таких методов.
Задача формальной верификации — доказать, что во-первых, программа полностью соответствует спецификации, и во-вторых, что она не допускает никаких других сценариев (в том числе уязвимостей), которые в спецификации не описаны.
И она с этим справляется.
Этот переход от перехода от кода к системе уравнений действительно является ключевым во всей концепции формальной верификации.
Именно этому моменту будет посвящена следующая статья, которая уже не за горами.
Я не хотел, чтобы первая статья показалась чрезмерно сложной для понимания.
Поэтому начал с упрощенного варианта, где вместо программы, на формальную логику переносится задача.
Хочу заверить, что принципы остаются теми же самыми, и следующая статья будет только дополнять эту новыми шагами.
В ней я расскажу о том как распарсить программу, превратить её в логическое выражение, сначала на языке самой программы.
А затем покажу, как сконвертировать это выражение в формальную логику.
Файлы, хранение данных и внешние вызовы я намерен затронуть в том числе.
Надеюсь, что моя статья несёт хоть какую-то полезность и в таком виде, так как статей по формальной верификации с примерами и кодом я на хабре не нашёл. (буду рад ошибиться)
Очень важно в формальной верификации то, что она ищет входные варианты гораздо более совершенным способом чем перебор, и находит нужные комбинации, даже если их 10^100.
Поэтому комбинаторного взрыва на входе она боится куда меньше чем брутфорс, и обнаружить даже Heartblead в принципе реально.
Благодарю вас за интересные и важные вопросы, которые помогают раскрыть статью.
Ядро Windows и задача о 8 ферзях связаны тем, что Z3Prover применяется в обоих случаях.
К тому же Z3Prover является разработкой от Microsoft Research, которым они же и ищут уязвимости в ядре.
Но вы правы, целостность повествования не столь хороша как хотелось бы.
В задаче о 8 ферзях уязвимостей нет, а сам пример был приведён главным образом для наглядной демонстрации механизмов и принципов работы Z3Prover, начиная с самых простых случаев.
Я показал принцип нахождения необходимой комбинации входных данных, в том случае, когда выходные данные и алгоритм известны.
Я согласен с вашей леммой о программе без условных циклов, переходов, которая всегда остановит свою работу.
Могу добавить, что некоторые языки программирования специально устанавливают такие ограничения, и таким образом все программы будут иметь конечную и предсказуемую сложность.
В следующей статье я как раз собираюсь написать о применении формальной верификации для нахождения уязвимостей в программах на таком языке, поскольку они прекрасно совместимы.
А итоге я верифицировал, что задача о волке, козе и капусты имеет решение за 8 шагов, а также то, что версия этой задачи со всеядным волком решения не имеет.