Комментарии 89
Даже если код является невзламываемым, это нельзя сказать о людях.
И о железе. Верифицированное ядро L4 точно также можно вскрыть, используя RowHammer, уязвимость в USB-контролере или IOMMU. Даже идеальная программа будет исполнятся на вполне реальном железе, а там такое количество глюков, недоработок, странностей и переходных процессов, что дыру можно найти практически всегда — были бы деньги и время на исследования.
P.S. Посмотрите вот это прекрасное видео о получении дампа прошивки графического планшета при помощи глитчинга.
P.S. Посмотрите вот это прекрасное видео о получении дампа прошивки графического планшета при помощи глитчинга.
Спасибо за ссылку на видео. Прикосновение к магии :)
Она девушка? Не подумайте, что я сексист, просто интересно. Везде про неё написано she/her/etc.
Но выглядит неоднозначно.
Но выглядит неоднозначно.
А по голосу и ухоженным ногтям не понятно разве? Так кстати есть момент, где её хорошо видно в отражении выключенного экрана.
https://www.youtube.com/watch?v=DykJTKvnSrw Девушка же
Цитируя ее сайт, «My full name is Micah Elizabeth Scott, but I used to be Micah Dowty prior to Fall 2010. My friends call me Beth.», она транссексуал. Судя по этому посту, она прошла операцию.
И да, это сексизм.
И да, это сексизм.
Просьба конкретизировать где вы видите сексизм в вопросе девушка ли автор видео? Если не сложно просьба так же ответить давно ли это у вас началось?
В данном случае сексизм заключается в самой постановке вопроса — «я не расист, но автор видео не негр ли случаем? Да, я понимаю, что это не имеет никакого отношения к теме видео, но просто показалось, что вдруг негр.» Нелепо же выглядит, не так ли?
Элизабет ведь снимает видео не о себе, а о чисто технических знаниях, но по некоторой причине некоторая часть аудитории оценивает все равно их через призму половой принадлежности автора. Почему это вообще должно быть важно? Что изменится в зависимости от половой принадлежности? Если Элизабет — женщина, она заслуживает другой оценки своего труда, нежели если бы она была мужчиной?
А что до «давно ли началось» — с детства родители приучили к тому, что стоит уважать чувства других людей, и нужно стремиться непредвзято оценивать слова и действия людей, отдельно от их личности, внешнего вида, гендера и сексуальной ориентации.
Элизабет ведь снимает видео не о себе, а о чисто технических знаниях, но по некоторой причине некоторая часть аудитории оценивает все равно их через призму половой принадлежности автора. Почему это вообще должно быть важно? Что изменится в зависимости от половой принадлежности? Если Элизабет — женщина, она заслуживает другой оценки своего труда, нежели если бы она была мужчиной?
А что до «давно ли началось» — с детства родители приучили к тому, что стоит уважать чувства других людей, и нужно стремиться непредвзято оценивать слова и действия людей, отдельно от их личности, внешнего вида, гендера и сексуальной ориентации.
В самой постановке вопроса я, если честно, вижу идиотизм (в бытовом смысле), порождённый как раз таки внедрением радфемского новояза в жизнь. Поэтому и выглядит нелепо.
В данном случае автор комментария не высказывает каких то дискриминирующих суждений, а вы уже предлагаете далеко идущие выводы. Вас это не смущает?
В данном случае автор комментария не высказывает каких то дискриминирующих суждений, а вы уже предлагаете далеко идущие выводы. Вас это не смущает?
Кошмар. Эдак скоро мы докатимся до того, что спросить у человека его имя будет восприниматься как оскорбление. Превратимся в безликую бесполую безымянную массу без каких-либо личностных характеристик. Зачем тогда люди вообще? Заложить всю драгоценную информацию в бездушные железяки, а самим тихо лечь и помереть.
Математическое доказательство верности кода — штука весьма заманчивая. Уверен, что мы ещё увидим значительные подвижки на этом фронте. Ценность для тестирования, для создания безошибочных программ трудно преувеличить, но вот в смысле хакерства даже на доказательство безошибочности положиться нельзя, потому что невозможно предусмотреть различные обходные пути нападения. Они попросту выходят за пределы области понятий, которыми оперируют такие доказательства. Вспомним тот же RowHammer.
RowHammer — явление вероятностное. Закрывается применением «космических» технологий — контрольных сумм и троированием с консенсусом.
Если заранее знать, от чего защищаться. Внезапно, может появиться возможность эксплуатации алгоритма консенсуса))
Это мы уже на уровень фантазии переходим. Собственно, любое рассуждение, где математический формализм начинают натягивать на реальность, немедленно перерастает в:
-Хорошо, ваша программа корректна, но докажите, что железо работает корректно
-(я долго перечисляю методы повышения надежности аппаратуры)
-докажите, что законы физики, на которые вы опираетесь, корректны
-(я долго перечисляю статфиз и прочие высокие эмпирии)
-докажите, что субъективная реальность реальна!
-… и мы плавно переходим плоскость философии, которая, как известно, является наукой неестественной, и объективной истины в которой — не найти.
-Хорошо, ваша программа корректна, но докажите, что железо работает корректно
-(я долго перечисляю методы повышения надежности аппаратуры)
-докажите, что законы физики, на которые вы опираетесь, корректны
-(я долго перечисляю статфиз и прочие высокие эмпирии)
-докажите, что субъективная реальность реальна!
-… и мы плавно переходим плоскость философии, которая, как известно, является наукой неестественной, и объективной истины в которой — не найти.
Тут даже не надо выходить на уровень физики.
Если дрон общается с оператором по радиоканалу и протокол шифруется алгоритмом AES256, то доказать корректность авторизации можно, только постулировав невзламываемость этого алгоритма (сейчас это математически не доказано).
И так во всём. Программа корректна, если… и если… И таких дыр (допущений, без которых доказательство невозможно) может быть десятки.
Если дрон общается с оператором по радиоканалу и протокол шифруется алгоритмом AES256, то доказать корректность авторизации можно, только постулировав невзламываемость этого алгоритма (сейчас это математически не доказано).
И так во всём. Программа корректна, если… и если… И таких дыр (допущений, без которых доказательство невозможно) может быть десятки.
Да ну, зачем такие сложности. Знаете, на чем держится вся арифметика? Вот на таком классном постулате — «Корректность аксиоматики арифметики подтверждается многолетним опытом ее использования».
Геометрия, например, корректна, если аксиоматика действительных чисел корректна.
Сплошная теорема Геделя о неполноте формальных систем.
При доказательстве вокруг компьютерных программ, например, возникают вопросы «А системный вызов точно работает согласно спецификации?», и так далее.
В итоге, формальное доказательство — это дорогой и мощный инструмент. Который должен использоваться наряду с остальными инструментами управления сложностью.
Геометрия, например, корректна, если аксиоматика действительных чисел корректна.
Сплошная теорема Геделя о неполноте формальных систем.
При доказательстве вокруг компьютерных программ, например, возникают вопросы «А системный вызов точно работает согласно спецификации?», и так далее.
В итоге, формальное доказательство — это дорогой и мощный инструмент. Который должен использоваться наряду с остальными инструментами управления сложностью.
Вы тут шутите, а на самом деле в правила могут быть не заложены нюансы криптографической системы. Например, может быть постулат, что неавторизованный пользователь не может послать пакет, зашифрованный корректным секретным ключом. А это неверно, достаточно перехватить один из старых пакетов, и отправить его позднее — и всё доказательство рассыпалось.
А если взять две одинаковые штуки, таких, что бы на выходе они давали непредсказуемо, но одинаково в обоих штуках изменяющийся сигнал, и компьютер оператора, измеряя свою штуку, передавал бы сигнал на дрон, а тот сверял его по своей штуке? В качестве штук можно было бы взять, например, заранее подготовленный список случайных чисел, или запись реликтового излучения, или еще что-то, что нельзя вычислить на третьей стороне.
мы плавно переходим плоскость философии, которая, как известно, является наукой
Философия — не наука.
Formal verification а в часности wp-calcul уже давно используют в «программировании по контракту», проблема в том что для многих алгоритмов доказательство их коректности сложнее и более ресурсоемко нежели расработка самих программ.
Я ничего не понял.
Вроде бы обсуждают заманчивую и интересную айтишную идею. Но ВСЕ примеры настолько гуманитарны и неточны, что непонятно даже приблизительно, каким образом там все происходит.
Окей, есть программа, которая заставит дрона долететь из точки А в точку Б. А если на пути внезапно построят дом? Хакеры это не те, кто просто ломают код. Это те, которые понимают как это работает и находят что программист не предусмотрел и как это можно использовать.
Вроде бы обсуждают заманчивую и интересную айтишную идею. Но ВСЕ примеры настолько гуманитарны и неточны, что непонятно даже приблизительно, каким образом там все происходит.
Окей, есть программа, которая заставит дрона долететь из точки А в точку Б. А если на пути внезапно построят дом? Хакеры это не те, кто просто ломают код. Это те, которые понимают как это работает и находят что программист не предусмотрел и как это можно использовать.
Как я понимаю смысл как раз в том, что программист не пишет программу «полета коптера из точки А в точку Б».
Он имеет дело с математическим объектом К (коптер), который имеет ряд характеристик. Среди характеристик есть такие как «географические координаты» — .g
Программа на самом верхнем уровне абстракции запишется как K.g = Б.g
Все. Больше программист ничего не пишет. Остальной код — дело правильно описанной математической модели коптера. В частности, где-то в этой модели есть описание, что при смене координат на минимальную величину Dg — необходимо поменять свойства «полет». Это свойство в свою очередь связано необходимостью поддерживать другие свойства в заданных диапазонах. Скажем уровень топлива должно быть всегда положительным и т.п. Также в свойствах модели описано занимаемое моделью пространство и просто указано что это пространство не должно содержать ничего кроме воздуха в таком то диапазоне характеристик (влажность, давление, смещение воздушных масс и т.п.)… В итоге получаем набор систем дифференциальных уравнений решив которые — получим алгоритм полета.
Описать такую модель для реальных объектов конечно очень сложно. Зато в результате — программисту не нужно думать «не построят ли по дороге дом», или «не сдует ли коптер ветром»?
Он просто напишет K.g = Б.g — программа посчитает и скажет — «нет данных для расчета, необходима информация о пространстве трассы». Программист подключает данные о трассе, и характеристиках пространства — и если данных достаточно — коптер летит.
Он все равно может не долететь — данные о трассе могут быть просто неверными. Но это уже проблема не в программе, а в исходных данных.
Ну и конечно этот пример — не подходит к статье. Ведь нельзя доказать математически, что модель коптера построена правильно… Поэтому в реальности подход применяют для чисто алгоритмических задач — скажем по криптографии, разделению уровней доступа и т.п. Там где возможно составить формальную модель.
Он имеет дело с математическим объектом К (коптер), который имеет ряд характеристик. Среди характеристик есть такие как «географические координаты» — .g
Программа на самом верхнем уровне абстракции запишется как K.g = Б.g
Все. Больше программист ничего не пишет. Остальной код — дело правильно описанной математической модели коптера. В частности, где-то в этой модели есть описание, что при смене координат на минимальную величину Dg — необходимо поменять свойства «полет». Это свойство в свою очередь связано необходимостью поддерживать другие свойства в заданных диапазонах. Скажем уровень топлива должно быть всегда положительным и т.п. Также в свойствах модели описано занимаемое моделью пространство и просто указано что это пространство не должно содержать ничего кроме воздуха в таком то диапазоне характеристик (влажность, давление, смещение воздушных масс и т.п.)… В итоге получаем набор систем дифференциальных уравнений решив которые — получим алгоритм полета.
Описать такую модель для реальных объектов конечно очень сложно. Зато в результате — программисту не нужно думать «не построят ли по дороге дом», или «не сдует ли коптер ветром»?
Он просто напишет K.g = Б.g — программа посчитает и скажет — «нет данных для расчета, необходима информация о пространстве трассы». Программист подключает данные о трассе, и характеристиках пространства — и если данных достаточно — коптер летит.
Он все равно может не долететь — данные о трассе могут быть просто неверными. Но это уже проблема не в программе, а в исходных данных.
Ну и конечно этот пример — не подходит к статье. Ведь нельзя доказать математически, что модель коптера построена правильно… Поэтому в реальности подход применяют для чисто алгоритмических задач — скажем по криптографии, разделению уровней доступа и т.п. Там где возможно составить формальную модель.
Я так понял, что любое вмешательство в код вызовет его неработоспособность. БПЛА тут приведены как идеальный случай единственного шифрованного канала управления. В реальной жизни, разумеется, есть мышки-клавиатуры-мониторы которые можно физически перехватить, и никакой код тут не поможет.
«Формальная верификация» штука далеко не новая
Вот, например, стоит обратить внимание
http://spinroot.com/gerard/pdf/icse_07.pdf
http://spinroot.com/gerard/pdf/IEEE_2007.pdf
Ну и сам проект spin, например
http://spinroot.com/spin/whatispin.html
Вот, например, стоит обратить внимание
http://spinroot.com/gerard/pdf/icse_07.pdf
http://spinroot.com/gerard/pdf/IEEE_2007.pdf
Ну и сам проект spin, например
http://spinroot.com/spin/whatispin.html
ИМХО, самая большая опасность — уверенность юзеров в том, что их код невозможно взломать, излишняя самоуверенность и раздолбайство, ведущее к снижению бдительности и далее к эпическому факапу и полному «П» при отсутствии плана действий в случае «ЧП». Типичная «ошибка Титаника».
«unum facit – aliud vastat»…
«unum facit – aliud vastat»…
Невзламываемый код — существует. Невзламываемые системы — нет.
Насколько реально (насколько дорого) взломать такую HSM систему или её аналог? http://www.realsec.com/en/wp-content/themes/base/includes/timthumb/timthumb.php?src=http://www.realsec.com/en/wp-content/uploads/2013/12/Cryptosec-PCI-v.1.1.jpg&w=800&h=600&zc=1
В карточке в энергозависимой памяти лежат ключи шифрования, взломом будет полное или частичное извлечение ключа. Батарейка снаружи корпуса, память — внутри корпуса, вместе с рядом датчиков физического вмешательства. При отключении батарейки или изменении сигналов от датчиков ключ стирается.
http://www.realsec.com/en/wp-content/uploads/2013/12/Datasheet-Cryptosec-PCI-v.1.1_English.pdf
Technical Specifications: 128 Kbytes of high-security internal memory (this memory is automatically deleted if a tampering attempt is detected).… Epoxy resin protective covering and reinforced metal casing made of 0.9 mm steel plate. Intrusion sensors (temperature, physical access, voltage, etc.).
• The module's firmware prevents output of confidential data.
• Access prevention to different parts of the cryptographic card using sensors that detect intrusions or anomalies and delete information (zeroization).
• All components are covered by an opaque epoxy resin and a metal casing to protect them all.
• TAMPER-RESPONSIVE: highest tamperization level.
. >>> State of the art anti-tamper mechanisms <<<
• Secure system for protection and key loading of externally generated keys through a secure direct connection using an asynchronous terminal.
• Possibility of assigning key ownership by users REALSEC.
В аппаратуре подобного уровня хранятся, к примеру, корневые ключи dnssec: https://www.cloudflare.com/dns/dnssec/root-signing-ceremony/ " tamper-proof hardware security module (HSM). The HSM is a physical computing device designed specifically for working with sensitive cryptographic material.… The goal is to eliminate any possibility of the root-signing key leaving the HSM after the ceremony ends. "
вопрос цены если объект взлома один то взломать мало реально, а если есть сотни образцов для тестирования… вскрыть не проблема — Механизм стирания тоже не проблема тк например длительное хранение данных может начать влиять на структуру материала вокруг и позволит считать данные даже после стирания по анализу структуры… ну это как пример… причем реально эта уязвимость может быть не учтена… отдельный вопрос обхода системы безопасности устройства…
можно конечно рассмотреть совсем параноидальные варианты с чипами «Оперативной памяти» в которых идет постоянная ротация места хранения ключей на базе рандомного алгоритма… но и тут есть варианты…
Думайте реально взломать можно все что сделано другим человеком…
можно конечно рассмотреть совсем параноидальные варианты с чипами «Оперативной памяти» в которых идет постоянная ротация места хранения ключей на базе рандомного алгоритма… но и тут есть варианты…
Думайте реально взломать можно все что сделано другим человеком…
НЛО прилетело и опубликовало эту надпись здесь
Курсы, где учат формальному доказательству — любой физмат вуз, желательно, не технический, а теоретический. (Для МГУ — мехмат, а не ВМК, например).
Работа Дейктры, на которую ссылается статья. Трудность тут в том, что для прочтения этой статьи с удовольствием, нужно иметь определенное представление о культуре математического рассуждения. Оно достигается курсу так ко второму обучения на профильной специальности.
Работа Дейктры, на которую ссылается статья. Трудность тут в том, что для прочтения этой статьи с удовольствием, нужно иметь определенное представление о культуре математического рассуждения. Оно достигается курсу так ко второму обучения на профильной специальности.
Можете поискать на тему «model checking» по-моему это об этом. Сама тема конечно «бородатая», но может это началось действительно второе дыхание…
Robotex, gbg.
В идеале нужно начать с изучения математической логики. (А изучение матлогики действительно неплохо бы с того, что поизучать математику вообще, приобрести математическое мышление, т. к. матлогика — это формализация стиля рассуждения, принятого в математике.)
По поводу МГУ. Я закончил мехмат МГУ. Из огромного числа прочитанных нам курсов было лишь два курса по матлогике (из них второй был необязательным). Матлогика, как мне показалось, трудно далась моим сокурсникам. Все старались её сдать и забыть как страшный сон. Так что типичный выпускник МГУ не знает о матлогике почти ничего. Если не считать тех, кто выбрал матлогику своей специальностью в МГУ, конечно.
Так что досточно просто изучить конспекты этих курсов. Достаточно первого из них, собственно, введение в матлогику. Вот конспекты, по которым учился я сам: http://lpcs.math.msu.su/vml2010.
Окей, что именно нужно из этих конспектов? Что нужно из матлогики? Я бы сказал, что нужно изучить логику первого порядка. Уметь «на бумажке» доказывать в ней простейшие утверждения. Необязательно изучить её по тем конспектам, можно по Википедии, желательно английской (first order logic), и прочим сайтам в интернете.
Дальше. Дальше нужно изучить какую-нибудь систему формальной логики для компьютера. Тут ключевые слова: формальная верификация доказательств, формальная логика, формальная математика. В МГУ про это уже не говорят, во всяком случае на специалитете. Я играл с Isabelle. Читайте доки на неё. Можно попробовать сразу начать с неё, без предварительного изучения матлогики, но, мне кажется, так не получится.
А вот после всего этого можно изучать, как, собственно, проверять код, используя эти системы. Здесь ключевые слова: формальная верификация программ. Посмотрите, например, проект L4.verified. Как я понимаю, они взяли код на си, преобразовали его в сущность, которую можно представить в Isabelle, а затем внутри Isabelle доказали как теорему, что этот код удовлетворяет спецификации.
Ещё посоветую сайт Фрейка: https://cs.ru.nl/~freek/ и вот этот блог: https://slawekk.wordpress.com/, но это уже обзорные и новостные ресурсы для тех, кто в теме.
По всем затронутым вопросам есть инфа в инете, в Википедии, может даже, что-то на Хабре.
Есть вопросы — пишите.
В идеале нужно начать с изучения математической логики. (А изучение матлогики действительно неплохо бы с того, что поизучать математику вообще, приобрести математическое мышление, т. к. матлогика — это формализация стиля рассуждения, принятого в математике.)
По поводу МГУ. Я закончил мехмат МГУ. Из огромного числа прочитанных нам курсов было лишь два курса по матлогике (из них второй был необязательным). Матлогика, как мне показалось, трудно далась моим сокурсникам. Все старались её сдать и забыть как страшный сон. Так что типичный выпускник МГУ не знает о матлогике почти ничего. Если не считать тех, кто выбрал матлогику своей специальностью в МГУ, конечно.
Так что досточно просто изучить конспекты этих курсов. Достаточно первого из них, собственно, введение в матлогику. Вот конспекты, по которым учился я сам: http://lpcs.math.msu.su/vml2010.
Окей, что именно нужно из этих конспектов? Что нужно из матлогики? Я бы сказал, что нужно изучить логику первого порядка. Уметь «на бумажке» доказывать в ней простейшие утверждения. Необязательно изучить её по тем конспектам, можно по Википедии, желательно английской (first order logic), и прочим сайтам в интернете.
Дальше. Дальше нужно изучить какую-нибудь систему формальной логики для компьютера. Тут ключевые слова: формальная верификация доказательств, формальная логика, формальная математика. В МГУ про это уже не говорят, во всяком случае на специалитете. Я играл с Isabelle. Читайте доки на неё. Можно попробовать сразу начать с неё, без предварительного изучения матлогики, но, мне кажется, так не получится.
А вот после всего этого можно изучать, как, собственно, проверять код, используя эти системы. Здесь ключевые слова: формальная верификация программ. Посмотрите, например, проект L4.verified. Как я понимаю, они взяли код на си, преобразовали его в сущность, которую можно представить в Isabelle, а затем внутри Isabelle доказали как теорему, что этот код удовлетворяет спецификации.
Ещё посоветую сайт Фрейка: https://cs.ru.nl/~freek/ и вот этот блог: https://slawekk.wordpress.com/, но это уже обзорные и новостные ресурсы для тех, кто в теме.
По всем затронутым вопросам есть инфа в инете, в Википедии, может даже, что-то на Хабре.
Есть вопросы — пишите.
НЛО прилетело и опубликовало эту надпись здесь
То, на что опирается Дейкстра, более глубокий раздел математики — это "Основания математики" (или, метаматематика). Для нее матлогика — это лишь инструмент.
Никакого более глубого уровня под матлогикой нет. Книга «Основания математики» Гильберта посвящена матлогике и тому, как с помощью этой матлогики построить более крепкие основания всей математики. Но нет никакого раздела математики под названием «основания математики», который был бы глубже матлогики.
По ссылке упоминается «метаматематическое доказательство». Такое доказательство всё равно было бы предметом матлогики. И такое доказательство невозможно, как упоминается дальше: «Его программа оказалась невыполнимой, как впоследствии установил К. Гёдель».
Я сейчас исхожу из общепринятых представлений о математике, которым меня научили в МГУ. И которому вы можете найти кучу подтверждений в интернете, в том числе в русской и английской Википедии.
По ссылке упоминается «метаматематическое доказательство». Такое доказательство всё равно было бы предметом матлогики. И такое доказательство невозможно, как упоминается дальше: «Его программа оказалась невыполнимой, как впоследствии установил К. Гёдель».
Я сейчас исхожу из общепринятых представлений о математике, которым меня научили в МГУ. И которому вы можете найти кучу подтверждений в интернете, в том числе в русской и английской Википедии.
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
procedure Search_List_Max (L : List_T; Pos : out Cursor; Max : out Component_T) with
SPARK_Mode,
Pre => not Is_Empty (L),
Post => (for all E of L => E <= Max) and then
(for some E of L => E = Max) and then
Has_Element (L, Pos) and then
Element (L, Pos) = Max
is
Cu : Cursor := First (L);
begin
Max := 0;
Pos := Cu;
while Has_Element (L, Cu) loop
pragma Loop_Invariant (for all Cu2 in First_To_Previous (L, Cu) => Element (L, Cu2) <= Max);
pragma Loop_Invariant (Max = 0 or else (for some Cu2 in First_To_Previous (L, Cu) => Element (L, Cu2) = Max));
pragma Loop_Invariant (Has_Element (L, Pos));
pragma Loop_Invariant (Max = 0 or else Element (L, Pos) = Max);
if Element (L, Cu) > Max then
Max := Element (L, Cu);
Pos := Cu;
end if;
Next (L, Cu);
end loop;
end Search_List_Max;
отсюда
Проблема в том, что за невзламываемость приходится платить ограниченностью функциональности — чем больше возможностей у программы, тем больше там места для уязвимостей, причём рост идёт экспоненциальный.
Так что когда мы доходим до чего-нибудь вроде браузеров — невзламываемость остаётся возможной только чисто теоретически.
Так что когда мы доходим до чего-нибудь вроде браузеров — невзламываемость остаётся возможной только чисто теоретически.
А как же проблемы с «задачей об остановке алгоритма?»
То есть
у нас есть алгоритм S и мы хотим доказать, что он делает D при начальных данных N за конечное время.
Но, Задача об остановке алгоритма утверждает, что такого алгоритма F(S,D,N), который остановился бы за конечное время при применимости алгоритма S к начальным данным N и конечному состоянию D, не существует…
То есть математическое доказательство путем построения такого алгоритма — невозможно.
То есть
у нас есть алгоритм S и мы хотим доказать, что он делает D при начальных данных N за конечное время.
Но, Задача об остановке алгоритма утверждает, что такого алгоритма F(S,D,N), который остановился бы за конечное время при применимости алгоритма S к начальным данным N и конечному состоянию D, не существует…
То есть математическое доказательство путем построения такого алгоритма — невозможно.
Нельзя проверить корректность произвольного алгоритма. Но в частном случае, можно доказать корректность какого-то одного конкретного. А если его корректность доказать не получается, по ходу доказательства может стать понятно: вот здесь, например, цикл, условие выхода из которого не всегда определено. Надо доопределить, и можно будет доказать корректность. Так и фиксятся ошибки.
Извините, но из приведенного примера ясно, что невозможно доказать даже для какого-то одного конкретного S. Вот нельзя и все. Математически строго — нельзя.
Т.е., вы хотите сказать, что я не смогу доказать конечность по времени алгоритма сложения двух целых чисел, принадлежащих множеству целых, которые могут быть представлены 64 битным двоичным значением?
Извините, но из приведенного примера ясно, что невозможно доказать даже для какого-то одного конкретного S. Вот нельзя и все. Математически строго — нельзя.
Ну вот у меня есть алгоритм из одной команды:
STOPА на чём вы его исполняете? На абстрактной машине Тьюринга? Тогда он останавливается по условиям задачи.
На реальном железе? Есть нюансы.
На реальном железе? Есть нюансы.
У оппонента было сомнение, можно ли проверить алгоритм как мат. абстракцию, не касаясь железных вопросов.
У вас очень вырожденный случай: вы берёте машину Тьюринга, сразу ставите её в терминальное состояние. Проблема остановки алгоритма гораздо более общая и этот пример к ней отношения не имеет.
А вот если коснуться железных вопросов, то даже тут всё станет не так однозначно.
А вот если коснуться железных вопросов, то даже тут всё станет не так однозначно.
тем не менее, этот вырожденный случай показывает, что существует класс алгоритмов, для которых можно привести математически обоснованное доказательсво их конечности исполнения во времени (в условиях идеального железа).
А теорема об останове говорит о невозможности такого доказательства для произвольного алгоритма. Другими словами (и это становится очевидно из самого её доказательства), утверждается, что существует семейство алгоритмов, для которых невозможно доказать их конечность исполнения во времени.
Но существование таких алгоритмов вовсе не означает, что любой алгоритм является таковым.
А теорема об останове говорит о невозможности такого доказательства для произвольного алгоритма. Другими словами (и это становится очевидно из самого её доказательства), утверждается, что существует семейство алгоритмов, для которых невозможно доказать их конечность исполнения во времени.
Но существование таких алгоритмов вовсе не означает, что любой алгоритм является таковым.
НЛО прилетело и опубликовало эту надпись здесь
Про перенос абстракции на железо, которое, в отличие от алгоритма, существует в реальном мире — уже сказали. Сомнения в возможности сделать строгую формализацию ОС общего назначения и всего работающего на ней софта — высказывали ещё в прошлом посте на эту тему.
У меня есть ещё одно соображение.
Существует область науки, в которой огромные государственные организации, привлекая лучших математиков, тратят миллиарды денег и тысячелетия человеко-времени, чтобы сделать алгоритмы, обеспеченные строгим математическим доказательством соотвествия заданным параметрам. Эта область называется Криптография.
Но, как мы видим, редко, но уязвимости находятся не только в реализации, но и в самих алгоритмах, параметры которых вроде-бы строго доказаны.
Возможно это намекает на то, что наличие уязвимостей и недочётов — фундаментальное свойство любых создаваемых человеком систем.
У меня есть ещё одно соображение.
Существует область науки, в которой огромные государственные организации, привлекая лучших математиков, тратят миллиарды денег и тысячелетия человеко-времени, чтобы сделать алгоритмы, обеспеченные строгим математическим доказательством соотвествия заданным параметрам. Эта область называется Криптография.
Но, как мы видим, редко, но уязвимости находятся не только в реализации, но и в самих алгоритмах, параметры которых вроде-бы строго доказаны.
Возможно это намекает на то, что наличие уязвимостей и недочётов — фундаментальное свойство любых создаваемых человеком систем.
но уязвимости находятся не только в реализации, но и в самих алгоритмах, параметры которых вроде-бы строго доказаны.Я про такое не слышал. То, о чём вы говорите, похоже на решение проблемы P=NP, а она, насколько я знаю, не решена.
Криптография отнюдь не ограничивается проблемой факторизации или дискретного логарифмирования. Есть сети фейстеля (DES, AES, ГОСТ-89), есть регистры сдвига с обратной связью и т.п. У каждого из них время от времени находятся проблемы в виде новых методов, позволяющих скинуть пару порядков с эффективной длины ключа.
Хорошо бы, кроме доказательства корректности ключевых элементов систем, остальное писать на языках, с развитыми системами типов и математически описанной семантикой. Падения десктопных приложений тоже доставляют массу неудобств.
Это уничтожит какие-то низкоуровневые оптимизации: битовые хаки, выкрутасы с переиспользованием памяти. Тот же firefox будет жрать памяти вдвое больше и рендерить в 5 раз медленнее — оно такое надо?
Компилятор уже сейчас справляется с оптимизацией часто лучше программиста, особено если последний не мешает ему низкоуровневыми хаками. И рендерит движек на Rust уже быстрее, чем на плюсах.
Rust хорош, т.к. взял всё от c++
Мой комментарий был, в основном, против языков с gc.
Насчёт семантики языка непонятно, можно ли ей формально верить.
Тот же c++ имеет
Кроме того, могут быть ошибки компилятора в трактовке семантики (формально проверить компилятор навряд ли будет возможно).
Поэтому семантическая разметка, что есть, что нет — проверять программу надо так, как будто её нет.
Мой комментарий был, в основном, против языков с gc.
Насчёт семантики языка непонятно, можно ли ей формально верить.
Тот же c++ имеет
const_cast и mutable, и поэтому нельзя рассчитывать на то, что, если согласно сигнатуре, функция принимает const-объект, то объект не поменяется.Кроме того, могут быть ошибки компилятора в трактовке семантики (формально проверить компилятор навряд ли будет возможно).
Поэтому семантическая разметка, что есть, что нет — проверять программу надо так, как будто её нет.
const_cast нужен для того, чтобы иметь возможность скормить константный объект функции, у которой прототип не содержит константного квалификатора, но про которую точно известно, что в объект она не пишет.
Если же пишет — будет UB, так в стандарте пишут.
Если же пишет — будет UB, так в стандарте пишут.
Ну сборка мусора не такое уж абсолютное зло с точки зрения производительности. Без сборки мусора трудно избежать фрагментации памяти. Потенциально, она может улучшить реактивность, так как освобождением памяти можно заняться когда нагрузка небольшая. В Erlang, где нет мутабельных структур, сборка мусора не блокирует систему и скорость реакции достигается очень высокая, несмотря на не слишком быструю VM.
Обычно проще проверить отдельно правильность разметки, и правильность программы с разметкой, чем правильность неразмеченной программы. Даже банальный вывод типов может оказаться ресурсоемким и неоднозначным, если не требовать объявлений типов хоть где-нибудь.
Верификация компилятора пока не достижима, но можно семантическую разметку протаскивать на уровень ассемблера и доказывать эквивалентность полученной программы исходному коду.
Обычно проще проверить отдельно правильность разметки, и правильность программы с разметкой, чем правильность неразмеченной программы. Даже банальный вывод типов может оказаться ресурсоемким и неоднозначным, если не требовать объявлений типов хоть где-нибудь.
Верификация компилятора пока не достижима, но можно семантическую разметку протаскивать на уровень ассемблера и доказывать эквивалентность полученной программы исходному коду.
Обычно вместе с gc приходит вторая особенность — при композиции объектов память под каждый выделяется отдельно, когда можно было выделить одним куском. Ухудшается memory locality. Если объект составить из двух других, они могут быть выделены далеко друг от друга + обращение к половинкам требует ещё одно чтение указателя.
Это, как раз, не проблема. Сборщики мусора обычно проводят еще и уплотнение памяти, в результате чего последовательные аллокации выделяют соседние блоки и каждая аллокация (если сборка мусора успевает все собрать), требует константного времени.
Основные проблемы — необходимость блокировок для работы с мутабельными структурами, утечки памяти, связанные с ссылками в неиспользуемых переменных и необходимость хрранения метаинформации.
Основные проблемы — необходимость блокировок для работы с мутабельными структурами, утечки памяти, связанные с ссылками в неиспользуемых переменных и необходимость хрранения метаинформации.
Странная статья. С первого взгляда бросаются в глаза множество глупейших ошибок в стратегии экспертов.
Может я чего-то в жизни не понимаю, но разве можно на основании неудачи одной команды делать вывод о надежности системы?
По моему количественные оценки тут вообще бессмысленны: даже если тысяча команд потерпят неудачу — 1001 может взломать. А если не взломает — есть и 1002, 1003 и так до плюс бесконечности.
И потом, разве можно утверждать, что какая-либо система надежна? Ошибки — это хаос, энтропия. Отсутствие ошибок — это абсолютный порядок, нулевая энтропия. Разве можно утверждать, что где-либо в реальности может существовать абсолютный порядок?
Разве можно недооценивать или переоценивать противника?
Хакеры, в традиционном понимании — это редкие гении, они по определению мыслят далеко за пределами разработчиков, и отыскивают ошибки там, куда ни один разработчик даже и не подумал взглянуть.
Именно поэтому хакеры находят ошибки — они видят ошибки там, где разработчики их не видят, иногда даже в упор.
Но даже гений не может утверждать, что ошибок нет.
Нельзя пригласить для оценки одного гения, и на основе его вывода заключить что другой гений также не осилит задачу.
К тому же с времен тех хакеров много воды утекло, и сейчас гении среди хакеров такая же редкость, как и среди обычных людей.
Так что делать какие-либо выводы на основе работы команды хакеров сейчас вдвойне глупо, и тянет не более, чем на попытку запудрить мозги покупателю: вот мол, хакеры не взломали, значит никто не взломает.
Это как с ведущими экспертами/собаководами и иже с ними в рекламе всяких блендаметов.
Разве можно, разрабатывая один(!) надежный компонент, распространять эту надежность на всю систему?
Система многокомпонентна, ошибка может быть в любом месте, а часто лежит вообще за пределами системы, куда разработчикам никак не могло прийти в голову заглянуть.
Самое ненадежное место в системе — взаимодействие с компонентами, в т.ч. с внешними. Это традиционно. Каждый пилит свой компонент, а стыкуются они кое-как. Ну а внешние потоки, а особенно петли данных, вообще чрезвычайно трудно проектировать без ошибок — там сам черт ногу сломит в этих кроссмодульных и кросс-системных взаимодействиях.
Умные девайсы часто прокалываются на ненадежном железе. Софт дорогой, миллион раз проверенный/перепроверенный, а железо собрано каким-нибудь.
А зачем нам надежное железо? Мы же специально для надежности и покупали дорогой софт, значит на железе можно сэкономить. И такая практика — везде, из-за чего регулярно случаются эпичные фэйлы на «подтвержденно надежных» системах: проверяли то совсем не то, что нужно было проверять, смотрели не туда, куда нужно было смотреть.
Особенно этим сейчас знамениты автопроизводители, чьи умные машины могут не стронуться с места по 1001 причине, большая часть из которых вообще несущественна, либо регулярно возникает самопроизвольно, совсем не так, как задумывалось, и никто с этим ничего поделать не может.
В общем умные системы часто на практике менее стабильны.
Разве можно все проверить?
По моему нет. По моему изначально нужно ориентироваться на то, что что-то пойдет не так.
Проверкам верить вообще нельзя, потому что иногда проверка — это рутина, которую поручают низкоквалифицированным сотрудникам, которые делают работу спустя рукава, а то и вообще ставят подпись не проверяя.
Этим славятся многие «эксперты», особенно на госслужбе.
Разве можно верить в безошибочность и непогрешимость чего-либо?
Из этой веры уже не раз вырастали самые эпичные и глупые ошибки в реализации, нередко стоящие многих жизней.
Из-за веры в непогрешимость системы, система находится на доверенном положении и проверяется слишком поздно, в последнюю очередь.
Нередко до ее проверки даже не доходит, т.к. часто ошибки находятся в других местах (а где их нет?), и на этом проверка заканчивается. Хотя проверена только часть системы.
А зачем проверять всю систему? Мы же нашли ошибку, не так ли? А то, что ошибок может быть больше одной — кто ж знал?
Может я чего-то в жизни не понимаю, но разве можно на основании неудачи одной команды делать вывод о надежности системы?
По моему количественные оценки тут вообще бессмысленны: даже если тысяча команд потерпят неудачу — 1001 может взломать. А если не взломает — есть и 1002, 1003 и так до плюс бесконечности.
И потом, разве можно утверждать, что какая-либо система надежна? Ошибки — это хаос, энтропия. Отсутствие ошибок — это абсолютный порядок, нулевая энтропия. Разве можно утверждать, что где-либо в реальности может существовать абсолютный порядок?
Разве можно недооценивать или переоценивать противника?
Хакеры, в традиционном понимании — это редкие гении, они по определению мыслят далеко за пределами разработчиков, и отыскивают ошибки там, куда ни один разработчик даже и не подумал взглянуть.
Именно поэтому хакеры находят ошибки — они видят ошибки там, где разработчики их не видят, иногда даже в упор.
Но даже гений не может утверждать, что ошибок нет.
Нельзя пригласить для оценки одного гения, и на основе его вывода заключить что другой гений также не осилит задачу.
К тому же с времен тех хакеров много воды утекло, и сейчас гении среди хакеров такая же редкость, как и среди обычных людей.
Так что делать какие-либо выводы на основе работы команды хакеров сейчас вдвойне глупо, и тянет не более, чем на попытку запудрить мозги покупателю: вот мол, хакеры не взломали, значит никто не взломает.
Это как с ведущими экспертами/собаководами и иже с ними в рекламе всяких блендаметов.
Разве можно, разрабатывая один(!) надежный компонент, распространять эту надежность на всю систему?
Система многокомпонентна, ошибка может быть в любом месте, а часто лежит вообще за пределами системы, куда разработчикам никак не могло прийти в голову заглянуть.
Самое ненадежное место в системе — взаимодействие с компонентами, в т.ч. с внешними. Это традиционно. Каждый пилит свой компонент, а стыкуются они кое-как. Ну а внешние потоки, а особенно петли данных, вообще чрезвычайно трудно проектировать без ошибок — там сам черт ногу сломит в этих кроссмодульных и кросс-системных взаимодействиях.
Умные девайсы часто прокалываются на ненадежном железе. Софт дорогой, миллион раз проверенный/перепроверенный, а железо собрано каким-нибудь.
А зачем нам надежное железо? Мы же специально для надежности и покупали дорогой софт, значит на железе можно сэкономить. И такая практика — везде, из-за чего регулярно случаются эпичные фэйлы на «подтвержденно надежных» системах: проверяли то совсем не то, что нужно было проверять, смотрели не туда, куда нужно было смотреть.
Особенно этим сейчас знамениты автопроизводители, чьи умные машины могут не стронуться с места по 1001 причине, большая часть из которых вообще несущественна, либо регулярно возникает самопроизвольно, совсем не так, как задумывалось, и никто с этим ничего поделать не может.
В общем умные системы часто на практике менее стабильны.
Разве можно все проверить?
По моему нет. По моему изначально нужно ориентироваться на то, что что-то пойдет не так.
Проверкам верить вообще нельзя, потому что иногда проверка — это рутина, которую поручают низкоквалифицированным сотрудникам, которые делают работу спустя рукава, а то и вообще ставят подпись не проверяя.
Этим славятся многие «эксперты», особенно на госслужбе.
Разве можно верить в безошибочность и непогрешимость чего-либо?
Из этой веры уже не раз вырастали самые эпичные и глупые ошибки в реализации, нередко стоящие многих жизней.
Из-за веры в непогрешимость системы, система находится на доверенном положении и проверяется слишком поздно, в последнюю очередь.
Нередко до ее проверки даже не доходит, т.к. часто ошибки находятся в других местах (а где их нет?), и на этом проверка заканчивается. Хотя проверена только часть системы.
А зачем проверять всю систему? Мы же нашли ошибку, не так ли? А то, что ошибок может быть больше одной — кто ж знал?
Да обычная пиар-статья, «много воды ни о чём», весь текст можно было уложить в три абзаца:
1. хакеры попробовали взломать алгоритм на формальной логике
2. исторический экскурс(Дейкстра и т.д.)
3. современное состояние формальной логики
1. хакеры попробовали взломать алгоритм на формальной логике
2. исторический экскурс(Дейкстра и т.д.)
3. современное состояние формальной логики
Попытка взлома — тестирование формального доказательства. Показывает, что в доказательстве грубых ошибок скорее всего нет.
«Программа — это такая последовательность из нулей и единичек, которая заставляет компьютер делать то, что хочет человек». Хотелось бы хоть какого-то содержания. Чем верифицировали, как формулировали требования? Может где-то есть код или научная статья по этому кейсу? Что существует такая штука, как формальная верификация — это не новость, спасибо.
Интересно было бы посмотреть на примеры, даже в случае с
Если список [7, 3, 5], он ожидает, что программа вернёт [3, 5, 7]. Но вывод программы [1, 2] удовлетворит спецификации – поскольку «это тоже отсортированный список, но только не тот список, которого вы, наверное, ожидали
Для каждого пункта j в списке убедиться, что j ≤ j + 1
Идеальный пример: сравниваем индексы вместо самих элементов. ^_^
(В оригинале тоже не особо внятно сформулировано.)
Интересно! Так ведь можно и обычные законы описать формально. Это превосходная возможность убрать фактор злоупотребления правом. По сути закон — это программа. А возможность разночтения — это и есть уязвимость в программе.
А не может ли случиться так, что математическая теория программы верна, но при написании кода программист допустил ошибку (даже банальную опечатку)? Тогда программа и её мат.модель разойдутся, что даёт почву для хака. Или я неправильно понял?
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Невзламываемый код существует