Весною 2015 года команда хакеров пыталась взломать беспилотный военный вертолёт под названием Little Bird («Птичка»). Вертолёт, схожий с пилотируемой версией любимого спецназом США летательного аппарата, находился на территории компании Boeing в Аризоне. У хакеров была фора: в начале их работы они обладали доступом к одной из подсистем управляющего компьютера. Им оставалось лишь взломать основной бортовой полётный компьютер и получить контроль над БПЛА.
В самом начале проекта команда хакеров «Red Team» могла взломать систему вертолёта почти так же просто, как ваш домашний WiFi. В последующие месяцы инженеры DARPA применили новый механизм безопасности, программную систему, не подверженную насильственной экспроприации. Ключевые параметры системы Little Bird невозможно взломать при помощи существующих технологий, а её коду можно доверять, как математическим доказательствам. И хотя команде дали шесть недель доступа к БПЛА, и доступ к компьютерной системе превышал возможности доступа реальной команды хакеров, они не смогли взломать защиту «Птички».
«Они не смогли взломать или нарушить ход операции»,- говорит Кэтлин Фишер, профессор информатики из Университета Тафтса и управляющая проектом «высоконадёжных военных киберсистем» (High-Assurance Cyber Military Systems, HACMS). «В результате представители DARPA встали и сказали, о, боже мой, вы на самом деле можем использовать такую технологию в важных системах».
Технология, противостоящая хакерам, это стиль программирования под названием формальное подтверждение. В отличие от обычного кода, написанного неформально и оцениваемого обычно только по его работоспособности, формально подтверждённое ПО выглядит, как математическое доказательство: каждое утверждение логически вытекает из предыдущего. Всю программу можно проверить с той же уверенностью, что и математическую теорему.
«Вы пишете математическую формулу, описывающую поведение программы и, используя инструмент для проверки доказательства, который проверяет правильность этого утверждения»,- говорит Брайан Парно, исследующий формальное подтверждение и безопасность в Microsoft Research.
Стремление создавать формально подтверждённые программы существовало почти так же давно, как и сама область информатики. И очень долго это оставалось невозможным, но достижения прошедших десяти лет в области «формальных методов» подвинули этот подход ближе к общепринятой практике. Сегодня формальное подтверждение ПО изучают в получающих финансирование академических группах, в военных проектах США и технологических компаниях, например, Microsoft и Amazon.
Интерес возрастает вместе с увеличением количества жизненно важных задач, проходящих через онлайн. Когда компьютеры изолированно существовали в домах и офисах, ошибки программирования были лишь неудобством. Теперь же они открывают дыры в безопасности на машинах в сети, позволяющие любым сведущим людям проникать в компьютерные системы.
«В ХХ-м веке, когда у программы была ошибка, это было плохо, она могла упасть, ну и бог с ней»,- говорит Эндрю Аппель [Andrew Appel], профессор информатик из Принстонского университета и лидер в области подтверждения программ. Но в ХХI-м веке ошибка может открыть «хакерам путь для получения контроля над программой и кражи ваших данных. Из терпимой ошибки она превратилась в уязвимость, что намного хуже»,- говорит он.
Кэтлин Фишер
Мечты об идеальных программах
В октябре 1973 года Эдсгер Дейкстра придумал идею создания кода без ошибок. Ночью, находясь в отеле на одной из конференции, он вдруг подумал о том, как сделать программирование более математическим. Объясняя идею позже, он сказал «С возбуждённым сознанием я вылез из постели в 2:30 утра, и писал более часа». Этот материал стал началом его плодотворной книги 1976 года «Дисциплина программирования», которая вместе с работами Чарльза Хоара (подобно Дейкстре, получившего премию Тьюринга), определила взгляды на использование доказательства правильности при написании программ.
Но информатика не последовала вслед за этой идеей, в основном потому, что в течение многих лет казалось непрактичным, или даже невозможным, определять функцию программы при помощи правил формальной логики.
Формальное определение – это способ определить то, что конкретно делает программа. Формальное подтверждение – способ доказать без всяких сомнений, что программный код идеально соответствует этому определению. Представьте, что вы пишете программу для робомобиля, везущего вас к продуктовому магазину. На уровне операций вы определяете движения, которыми располагает робомобиль для достижения цели – он может поворачивать, тормозить или ускоряться, включаться или выключаться в начале и конце пути. Ваша программа будет состоять из этих основных операций, построенных в нужном порядке так, чтобы в итоге вы приехали к магазину, а не в аэропорт.
Традиционный способ проверки работоспособности программы – это тестирование. Программисты дают программе много данных на вход (юнит-тесты), чтобы убедиться, что она ведёт себя, как надо. Если ваша программа задаёт алгоритм движения робомобиля, можно протестировать её поездки между множеством разных точек. Такое тестирование обеспечивает корректную работу программ в большинстве случаев, чего достаточно для большинства приложений. Но юнит-тесты не гарантируют, что ПО будет всегда работать правильно – нельзя проверить программу на всех возможных входных данных. Даже если алгоритм сработает для всех пунктов назначения, всегда есть возможность, что она поведёт себя не так в редких условиях – или, как говорят, в «граничных условиях» – и откроет дыру в безопасности. В реальных программах такие ошибки могут быть простыми, например, переполнение буфера, при котором программа копирует чуть больше данных, чем надо, и перезаписывает часть памяти компьютера. Такую по виду безвредную ошибку тяжело устранить, и она обеспечивает дыру для хакерской атаки – слабая дверная петля, открывающая путь в замок.
«Одна дыра где-либо в софте, и это уже уязвимость. Очень сложно проверить все пути для всех возможных входных данных»,- говорит Парно.
Настоящие спецификации сложнее, чем поездка в магазин. Программистам, например, может понадобиться программа, нотариально заверяющая и проставляющая дату получения документов в порядке их получения. В этом случае спецификация должна указывать, что счётчик всегда увеличивается, и что программа никогда не должна допускать утечку ключа, используемого для подписи.
На человеческом языке это описать легко. Превратить спецификацию в формальный язык, понятный компьютеру, гораздо тяжелее – что и объясняет основную проблему написания программ.
«Состряпать формальную спецификацию, понятную для компьютера, сложно по сути,- говорит Парно. – Легко на верхнем уровне сказать „не допускай утечек пароля“, но нужно подумать, как превратить это в математическое определение».
Другой пример – программа, сортирующая список номеров. Программист в попытках формализовать спецификацию для неё может придумать такое:
Для каждого пункта j в списке убедиться, что j ? j + 1
Но и в этой формальной спецификации – убедиться, что каждый элемент в списке меньше или равен следующему – есть ошибка. Программист подразумевает, что выходные данные будут содержать изменённые входные. Если список [7, 3, 5], он ожидает, что программа вернёт [3, 5, 7]. Но вывод программы [1, 2] удовлетворит спецификации – поскольку «это тоже отсортированный список, но только не тот список, которого вы, наверное, ожидали»,- говорит Парно.
Иначе говоря, тяжело превратить идею того, что должна делать программа, в формальную спецификацию, исключающую любую неправильную интерпретацию того, чего вы хотите от программы. И приведённый пример описывает простейшую программу сортировки. Теперь представьте описание чего-то гораздо более абстрактного, например, защиту пароля. «Что это значит математически? Для такого определения может понадобиться записать математическое описание того, что означает „хранить секрет“, или, что означает для алгоритма шифрования быть безопасным,- говорит Парно. – Все эти вопросы мы рассматривали, и продвинулись в их изучении, но они могут быть чрезвычайно хитры для реализации».
Блочная безопасность
По сути, необходимо написать как спецификации, так и дополнительные комментарии, необходимые для того, чтобы ПО могло делать заключения о коде. Программа, включающая её формальное подтверждение, может в пять раз превышать размер обычной программы, написанной с той же целью.
Эту ношу можно немного облегчить при помощи подходящих инструментов – языков программирования и вспомогательных программ, помогающих программистам создавать пуленепробиваемые программы. Но в 1970-х их не существовало. «Многие аспекты науки и технологии тогда ещё не выросли достаточно, поэтому к 1980-м многие области информатики потеряли к этому интерес»,- говорит Аппель, ведущий исследователь группы DeepSpec, разрабатывающей формально подтверждённые компьютерные системы.
Несмотря на улучшение инструментов, на пути подтверждения программ возник ещё один барьер: не было уверенности в том, что оно вообще было нужно. Хотя энтузиасты метода говорили о том, что небольшие ошибки могут приводить к большим проблемам, остальные обращали внимание на то, что в основном компьютерные программы работают достаточно неплохо. Иногда падают, да – но потерять немножко несохранённых данных, или иногда перезапускать систему кажется небольшой платой за отсутствие необходимости кропотливо переводить каждый кусочек программы на язык формальной логики. Со временем даже те, кто находился у истоков программного подтверждения, начали сомневаться в его пользе. В 1990-х даже Хоар признал, что спецификации могут быть трудозатратным решением несуществующей проблемы. В 1995 он писал:
Десять лет назад исследователи формальных методов (а среди них я ошибался сильнее всего) предсказывали, что мир программирования с благодарностью примет помощь формализации… Оказалось, что мир недостаточно сильно страдал от проблем, которые наше исследование пыталось решать.
Потом появился интернет, который сделал для ошибок в коде то же, что авиаперелёты сделали для инфекций: когда все компьютеры связаны друг с другом, неудобные, но терпимые ошибки могут привести к нарастающим проблемам безопасности.
«Мы вот что не полностью понимали,- говорит Аппель. – Существуют программы, открытые всем хакерам интернета, и если в такой программе есть ошибка, она может стать уязвимостью».
К тому времени, когда исследователи начали понимать серьёзность угроз для безопасности, представляемых интернетом, подтверждение программ было готово вернуться. Для начала исследователи достигли прогресса в фундаментальных частях формальных методов. Это улучшение вспомогательных программ, таких, как Coq и Isabelle; разработка логических систем (теории зависимых типов), обеспечивающих платформу разработки, помогающую компьютерам оценивать код; «операционная семантика» – язык, обладающий правильными словами, позволяющими выразить то, что требуется от программы.
«Начиная со спецификации на человеческом языке, вы сталкиваетесь с двусмысленностями,- говорит Джанетт Винг, вице-президент Microsoft Research. – Любой естественный язык содержит двусмысленности. В формальной спецификации вы записываете точное описание на основе математики, для объяснения того, что вы хотите от программы».
Джанетт Винг из Microsoft Research
Кроме того, исследователи формальных методов пересмотрели свои цели. В 1970-х и 1980-х они хотели создать полностью проверенные компьютерные системы, от электронных схем до программ. Сегодня большинство исследователей работают над небольшими, но наиболее критичными или уязвимыми частями систем – например, над операционными системами или криптографическими протоколами.
«Мы не утверждаем, что докажем корректность всей системы на 100%, вплоть до электронных схем,- говорит Винг. – Такие заявления нелепы. Мы точны в том, что мы можем или не можем сделать».
Проект HACMS показывает, как можно достичь больших гарантий безопасности, описав одну небольшую часть компьютерной системы. Первой целью проекта было создание невзламываемого квадрокоптера для развлечений. Шедшее в комплекте с квадриком ПО было монолитным – то есть, получив доступ к одной его части, хакер получал доступ ко всем остальным. Два года команда HACMS занималась разделением кода в управляющем компьютере на части.
Команда переписала архитектуру ПО, используя то, что Фишер называет «строительными блоками высокой уверенности» – инструменты, позволяющие программистом доказывать чистоту кода. Один из них обеспечивает доказательство того, что получив доступ в одну из частей, нельзя путём эскалации привилегий добраться до остальных.
Позднее программисты установили такой софт на «Птичку». В тесте с командой Red Team ей предоставили доступ в одну из частей системы, контролировавшей какую-то часть вертолёта, например, камеру – но не основные функции. Неудача хакеров была математически гарантирована. «Они доказали машинно-проверяемым способом, что хакеры не смогут выйти за пределы раздела системы, так что это неудивительно, – говорит Фишер. – Это совпадает с теоремой, но всегда полезно провести проверку».
В последующий за проверкой год DARPA применяла инструменты и технологии проекта к другим областям военной технологии, например, к спутникам и автоматическим грузовикам. Новые инициативы совпадают с тем, как формальное подтверждение распространялось в последние десять лет: каждый успешный проект поощряет следующий. «Отговорки на тему сложности этого принципа уже не проходят»,- говорит Фишер.
Проверить интернет
Безопасность и надёжность – две основных цели, вдохновляющих формальные методы. С каждым днём необходимость в улучшениях становится всё более очевидной. В 2014-м году небольшая программная ошибка, которую формальное описание словило бы, открыло путь для ошибки Heartbleed, грозившей сломать интернет. Через год парочка «легальных» хакеров подтвердила худшие опасения по поводу автомобилей, подключённых к интернету, получив удалённый контроль над Jeep Cherokee.
С повышением ставок исследователи формальных методов ставят всё более амбициозные цели. Группа DeepSpec под руководством Аппеля (также работавшего над HACMS) пытается построить такую сложную полностью проверенную систему, как веб-сервер. В случае успеха проект, получивший грант от Государственного научного фонда в $10 миллионов, соберёт вместе множество меньших успешных проектов последнего десятилетия. Исследователи создали несколько подтверждённых безопасных компонентов вроде ядра операционной системы. «Чего пока не было сделано, так это объединения этих компонентов по имеющим спецификации интерфейсам»,- говорит Аппель.
В Microsoft Research у программистов есть два амбициозных проекта. Первый, Everest, стремится создать подтверждённую версию HTTPS, протокола, обеспечивающего безопасность веб-браузеров, который Винг называет «ахиллесовой пятой интернета».
Второй – создание подтверждённых спецификаций сложных кибер-физических систем, таких, как БПЛА. У проекта существуют значительные сложности. В то время как обычные программы работают с отдельными недвусмысленными этапами, программы, управляющие движением дронов, используют машинное обучение для принятия вероятностных решений, основанных на непрерывном потоке данных об окружении. Далеко не очевидно, как можно принимать логические решения с такой степенью неточности, или описать их в виде формальной спецификации. Но только за последние десять лет формальные методы продвинулись довольно далеко, и Винг, управляя проектом, оптимистично считает, что исследователи смогут решить все эти проблемы.
Комментарии (73)
OldFisher
04.11.2016 13:02+5Математическое доказательство верности кода — штука весьма заманчивая. Уверен, что мы ещё увидим значительные подвижки на этом фронте. Ценность для тестирования, для создания безошибочных программ трудно преувеличить, но вот в смысле хакерства даже на доказательство безошибочности положиться нельзя, потому что невозможно предусмотреть различные обходные пути нападения. Они попросту выходят за пределы области понятий, которыми оперируют такие доказательства. Вспомним тот же RowHammer.
gbg
04.11.2016 16:16RowHammer — явление вероятностное. Закрывается применением «космических» технологий — контрольных сумм и троированием с консенсусом.
qw1
04.11.2016 21:51Если заранее знать, от чего защищаться. Внезапно, может появиться возможность эксплуатации алгоритма консенсуса))
gbg
04.11.2016 22:00Это мы уже на уровень фантазии переходим. Собственно, любое рассуждение, где математический формализм начинают натягивать на реальность, немедленно перерастает в:
-Хорошо, ваша программа корректна, но докажите, что железо работает корректно
-(я долго перечисляю методы повышения надежности аппаратуры)
-докажите, что законы физики, на которые вы опираетесь, корректны
-(я долго перечисляю статфиз и прочие высокие эмпирии)
-докажите, что субъективная реальность реальна!
-… и мы плавно переходим плоскость философии, которая, как известно, является наукой неестественной, и объективной истины в которой — не найти.qw1
04.11.2016 22:08Тут даже не надо выходить на уровень физики.
Если дрон общается с оператором по радиоканалу и протокол шифруется алгоритмом AES256, то доказать корректность авторизации можно, только постулировав невзламываемость этого алгоритма (сейчас это математически не доказано).
И так во всём. Программа корректна, если… и если… И таких дыр (допущений, без которых доказательство невозможно) может быть десятки.gbg
04.11.2016 22:27Да ну, зачем такие сложности. Знаете, на чем держится вся арифметика? Вот на таком классном постулате — «Корректность аксиоматики арифметики подтверждается многолетним опытом ее использования».
Геометрия, например, корректна, если аксиоматика действительных чисел корректна.
Сплошная теорема Геделя о неполноте формальных систем.
При доказательстве вокруг компьютерных программ, например, возникают вопросы «А системный вызов точно работает согласно спецификации?», и так далее.
В итоге, формальное доказательство — это дорогой и мощный инструмент. Который должен использоваться наряду с остальными инструментами управления сложностью.qw1
04.11.2016 23:41Вы тут шутите, а на самом деле в правила могут быть не заложены нюансы криптографической системы. Например, может быть постулат, что неавторизованный пользователь не может послать пакет, зашифрованный корректным секретным ключом. А это неверно, достаточно перехватить один из старых пакетов, и отправить его позднее — и всё доказательство рассыпалось.
saboteur_kiev
04.11.2016 13:22+8Я ничего не понял.
Вроде бы обсуждают заманчивую и интересную айтишную идею. Но ВСЕ примеры настолько гуманитарны и неточны, что непонятно даже приблизительно, каким образом там все происходит.
Окей, есть программа, которая заставит дрона долететь из точки А в точку Б. А если на пути внезапно построят дом? Хакеры это не те, кто просто ломают код. Это те, которые понимают как это работает и находят что программист не предусмотрел и как это можно использовать.
Quiensabe
05.11.2016 06:46Как я понимаю смысл как раз в том, что программист не пишет программу «полета коптера из точки А в точку Б».
Он имеет дело с математическим объектом К (коптер), который имеет ряд характеристик. Среди характеристик есть такие как «географические координаты» — .g
Программа на самом верхнем уровне абстракции запишется как K.g = Б.g
Все. Больше программист ничего не пишет. Остальной код — дело правильно описанной математической модели коптера. В частности, где-то в этой модели есть описание, что при смене координат на минимальную величину Dg — необходимо поменять свойства «полет». Это свойство в свою очередь связано необходимостью поддерживать другие свойства в заданных диапазонах. Скажем уровень топлива должно быть всегда положительным и т.п. Также в свойствах модели описано занимаемое моделью пространство и просто указано что это пространство не должно содержать ничего кроме воздуха в таком то диапазоне характеристик (влажность, давление, смещение воздушных масс и т.п.)… В итоге получаем набор систем дифференциальных уравнений решив которые — получим алгоритм полета.
Описать такую модель для реальных объектов конечно очень сложно. Зато в результате — программисту не нужно думать «не построят ли по дороге дом», или «не сдует ли коптер ветром»?
Он просто напишет K.g = Б.g — программа посчитает и скажет — «нет данных для расчета, необходима информация о пространстве трассы». Программист подключает данные о трассе, и характеристиках пространства — и если данных достаточно — коптер летит.
Он все равно может не долететь — данные о трассе могут быть просто неверными. Но это уже проблема не в программе, а в исходных данных.
Ну и конечно этот пример — не подходит к статье. Ведь нельзя доказать математически, что модель коптера построена правильно… Поэтому в реальности подход применяют для чисто алгоритмических задач — скажем по криптографии, разделению уровней доступа и т.п. Там где возможно составить формальную модель.saboteur_kiev
05.11.2016 19:38Вот именно. Непонятно, почему считается, что модель коптера (то есть компоненты программы) изначально неуязвимы.
locutus
04.11.2016 14:23+1«Формальная верификация» штука далеко не новая
Вот, например, стоит обратить внимание
http://spinroot.com/gerard/pdf/icse_07.pdf
http://spinroot.com/gerard/pdf/IEEE_2007.pdf
Ну и сам проект spin, например
http://spinroot.com/spin/whatispin.html
ARD8S
04.11.2016 14:28ИМХО, самая большая опасность — уверенность юзеров в том, что их код невозможно взломать, излишняя самоуверенность и раздолбайство, ведущее к снижению бдительности и далее к эпическому факапу и полному «П» при отсутствии плана действий в случае «ЧП». Типичная «ошибка Титаника».
«unum facit – aliud vastat»…
PaulAtreides
04.11.2016 14:33+3Невзламываемый код — существует. Невзламываемые системы — нет.
a5b
04.11.2016 22:35Насколько реально (насколько дорого) взломать такую 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. "
Robotex
04.11.2016 15:50Сколько лет уже программирую, а о таком в первый раз слышу. А можно где-то подробнее об этом почитать? Есть какие-нибудь курсы? Хочу освоить эту область знаний
gbg
04.11.2016 16:23+1Курсы, где учат формальному доказательству — любой физмат вуз, желательно, не технический, а теоретический. (Для МГУ — мехмат, а не ВМК, например).
Работа Дейктры, на которую ссылается статья. Трудность тут в том, что для прочтения этой статьи с удовольствием, нужно иметь определенное представление о культуре математического рассуждения. Оно достигается курсу так ко второму обучения на профильной специальности.
PavelVainerman
04.11.2016 19:18Можете поискать на тему «model checking» по-моему это об этом. Сама тема конечно «бородатая», но может это началось действительно второе дыхание…
safinaskar
04.11.2016 19:36+3Robotex, gbg.
В идеале нужно начать с изучения математической логики. (А изучение матлогики действительно неплохо бы с того, что поизучать математику вообще, приобрести математическое мышление, т. к. матлогика — это формализация стиля рассуждения, принятого в математике.)
По поводу МГУ. Я закончил мехмат МГУ. Из огромного числа прочитанных нам курсов было лишь два курса по матлогике (из них второй был необязательным). Матлогика, как мне показалось, трудно далась моим сокурсникам. Все старались её сдать и забыть как страшный сон. Так что типичный выпускник МГУ не знает о матлогике почти ничего. Если не считать тех, кто выбрал матлогику своей специальностью в МГУ, конечно.
Так что досточно просто изучить конспекты этих курсов. Достаточно первого из них, собственно, введение в матлогику. Вот конспекты, по которым учился я сам: http://lpcs.math.msu.su/vml2010.
Окей, что именно нужно из этих конспектов? Что нужно из матлогики? Я бы сказал, что нужно изучить логику первого порядка. Уметь «на бумажке» доказывать в ней простейшие утверждения. Необязательно изучить её по тем конспектам, можно по Википедии, желательно английской (first order logic), и прочим сайтам в интернете.
Дальше. Дальше нужно изучить какую-нибудь систему формальной логики для компьютера. Тут ключевые слова: формальная верификация доказательств, формальная логика, формальная математика. В МГУ про это уже не говорят, во всяком случае на специалитете. Я играл с Isabelle. Читайте доки на неё. Можно попробовать сразу начать с неё, без предварительного изучения матлогики, но, мне кажется, так не получится.
А вот после всего этого можно изучать, как, собственно, проверять код, используя эти системы. Здесь ключевые слова: формальная верификация программ. Посмотрите, например, проект L4.verified. Как я понимаю, они взяли код на си, преобразовали его в сущность, которую можно представить в Isabelle, а затем внутри Isabelle доказали как теорему, что этот код удовлетворяет спецификации.
Ещё посоветую сайт Фрейка: https://cs.ru.nl/~freek/ и вот этот блог: https://slawekk.wordpress.com/, но это уже обзорные и новостные ресурсы для тех, кто в теме.
По всем затронутым вопросам есть инфа в инете, в Википедии, может даже, что-то на Хабре.
Есть вопросы — пишите.gbg
04.11.2016 20:24То, на что опирается Дейкстра, более глубокий раздел математики — это "Основания математики" (или, метаматематика). Для нее матлогика — это лишь инструмент.
safinaskar
05.11.2016 13:59+1Никакого более глубого уровня под матлогикой нет. Книга «Основания математики» Гильберта посвящена матлогике и тому, как с помощью этой матлогики построить более крепкие основания всей математики. Но нет никакого раздела математики под названием «основания математики», который был бы глубже матлогики.
По ссылке упоминается «метаматематическое доказательство». Такое доказательство всё равно было бы предметом матлогики. И такое доказательство невозможно, как упоминается дальше: «Его программа оказалась невыполнимой, как впоследствии установил К. Гёдель».
Я сейчас исхожу из общепринятых представлений о математике, которым меня научили в МГУ. И которому вы можете найти кучу подтверждений в интернете, в том числе в русской и английской Википедии.
Robotex
04.11.2016 19:14+1Хотелось бы хоть какой-то пример верифицированной программы
el_gato
06.11.2016 11:01+1with 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;
отсюда
SinsI
04.11.2016 19:22+1Проблема в том, что за невзламываемость приходится платить ограниченностью функциональности — чем больше возможностей у программы, тем больше там места для уязвимостей, причём рост идёт экспоненциальный.
Так что когда мы доходим до чего-нибудь вроде браузеров — невзламываемость остаётся возможной только чисто теоретически.
bear11
04.11.2016 21:39А как же проблемы с «задачей об остановке алгоритма?»
То есть
у нас есть алгоритм S и мы хотим доказать, что он делает D при начальных данных N за конечное время.
Но, Задача об остановке алгоритма утверждает, что такого алгоритма F(S,D,N), который остановился бы за конечное время при применимости алгоритма S к начальным данным N и конечному состоянию D, не существует…
То есть математическое доказательство путем построения такого алгоритма — невозможно.
qw1
04.11.2016 21:58Нельзя проверить корректность произвольного алгоритма. Но в частном случае, можно доказать корректность какого-то одного конкретного. А если его корректность доказать не получается, по ходу доказательства может стать понятно: вот здесь, например, цикл, условие выхода из которого не всегда определено. Надо доопределить, и можно будет доказать корректность. Так и фиксятся ошибки.
bear11
04.11.2016 22:27-1Извините, но из приведенного примера ясно, что невозможно доказать даже для какого-то одного конкретного S. Вот нельзя и все. Математически строго — нельзя.
pacaya
04.11.2016 22:54Т.е., вы хотите сказать, что я не смогу доказать конечность по времени алгоритма сложения двух целых чисел, принадлежащих множеству целых, которые могут быть представлены 64 битным двоичным значением?
bear11
04.11.2016 23:10Да, для одного алгоритма, идя по нему, похоже сможете (или нет). Но если вы будете считать этот подход системой и применять его без изменения и адаптации к другим алгоритмам, будут попадаться крепкие орешки, не поддающиеся системе.
qw1
04.11.2016 23:47Совершенно верно. В данном случае нам не надо доказательство применять к другим алгоритмам. Нам нужно доказать корректность ровно одного алгоритма: того, который запишем в прошивку беспилотника.
qw1
04.11.2016 23:44+1Извините, но из приведенного примера ясно, что невозможно доказать даже для какого-то одного конкретного S. Вот нельзя и все. Математически строго — нельзя.
Ну вот у меня есть алгоритм из одной команды:
Неужели нельзя доказать, что он останавливается?STOPPaulAtreides
05.11.2016 11:53А на чём вы его исполняете? На абстрактной машине Тьюринга? Тогда он останавливается по условиям задачи.
На реальном железе? Есть нюансы.qw1
05.11.2016 13:24У оппонента было сомнение, можно ли проверить алгоритм как мат. абстракцию, не касаясь железных вопросов.
PaulAtreides
05.11.2016 15:21-1У вас очень вырожденный случай: вы берёте машину Тьюринга, сразу ставите её в терминальное состояние. Проблема остановки алгоритма гораздо более общая и этот пример к ней отношения не имеет.
А вот если коснуться железных вопросов, то даже тут всё станет не так однозначно.pacaya
05.11.2016 15:33+2тем не менее, этот вырожденный случай показывает, что существует класс алгоритмов, для которых можно привести математически обоснованное доказательсво их конечности исполнения во времени (в условиях идеального железа).
А теорема об останове говорит о невозможности такого доказательства для произвольного алгоритма. Другими словами (и это становится очевидно из самого её доказательства), утверждается, что существует семейство алгоритмов, для которых невозможно доказать их конечность исполнения во времени.
Но существование таких алгоритмов вовсе не означает, что любой алгоритм является таковым.PaulAtreides
05.11.2016 16:11-2Теорема об останове — это общий случай. Наличие частных случаев ни о чём не говорит. Так же, как, например, существование чётного простого числа не говорит о том, что существует ещё хотя бы одно.
pacaya
05.11.2016 16:16+1Если бы была теорема о том, что таких чисел не существует (простых четных), то существование такого числа было бы прямым и простым опровержением теоремы.
PaulAtreides
05.11.2016 12:17Про перенос абстракции на железо, которое, в отличие от алгоритма, существует в реальном мире — уже сказали. Сомнения в возможности сделать строгую формализацию ОС общего назначения и всего работающего на ней софта — высказывали ещё в прошлом посте на эту тему.
У меня есть ещё одно соображение.
Существует область науки, в которой огромные государственные организации, привлекая лучших математиков, тратят миллиарды денег и тысячелетия человеко-времени, чтобы сделать алгоритмы, обеспеченные строгим математическим доказательством соотвествия заданным параметрам. Эта область называется Криптография.
Но, как мы видим, редко, но уязвимости находятся не только в реализации, но и в самих алгоритмах, параметры которых вроде-бы строго доказаны.
Возможно это намекает на то, что наличие уязвимостей и недочётов — фундаментальное свойство любых создаваемых человеком систем.qw1
05.11.2016 13:27но уязвимости находятся не только в реализации, но и в самих алгоритмах, параметры которых вроде-бы строго доказаны.
Я про такое не слышал. То, о чём вы говорите, похоже на решение проблемы P=NP, а она, насколько я знаю, не решена.PaulAtreides
05.11.2016 15:38Криптография отнюдь не ограничивается проблемой факторизации или дискретного логарифмирования. Есть сети фейстеля (DES, AES, ГОСТ-89), есть регистры сдвига с обратной связью и т.п. У каждого из них время от времени находятся проблемы в виде новых методов, позволяющих скинуть пару порядков с эффективной длины ключа.
qw1
05.11.2016 19:09А вопрос то был в чём. Существовали ли «строго доказанные» алгоритмы и параметры, в которых потом нашли дыры? Я бы хотел ознакомится с теми «доказательствами».
potan
06.11.2016 01:16Хорошо бы, кроме доказательства корректности ключевых элементов систем, остальное писать на языках, с развитыми системами типов и математически описанной семантикой. Падения десктопных приложений тоже доставляют массу неудобств.
qw1
06.11.2016 10:34Это уничтожит какие-то низкоуровневые оптимизации: битовые хаки, выкрутасы с переиспользованием памяти. Тот же firefox будет жрать памяти вдвое больше и рендерить в 5 раз медленнее — оно такое надо?
potan
06.11.2016 15:42-1Компилятор уже сейчас справляется с оптимизацией часто лучше программиста, особено если последний не мешает ему низкоуровневыми хаками. И рендерит движек на Rust уже быстрее, чем на плюсах.
qw1
06.11.2016 16:31Rust хорош, т.к. взял всё от c++
Мой комментарий был, в основном, против языков с gc.
Насчёт семантики языка непонятно, можно ли ей формально верить.
Тот же c++ имеетconst_castиmutable, и поэтому нельзя рассчитывать на то, что, если согласно сигнатуре, функция принимает const-объект, то объект не поменяется.
Кроме того, могут быть ошибки компилятора в трактовке семантики (формально проверить компилятор навряд ли будет возможно).
Поэтому семантическая разметка, что есть, что нет — проверять программу надо так, как будто её нет.gbg
06.11.2016 18:15const_cast нужен для того, чтобы иметь возможность скормить константный объект функции, у которой прототип не содержит константного квалификатора, но про которую точно известно, что в объект она не пишет.
Если же пишет — будет UB, так в стандарте пишут.qw1
06.11.2016 18:52Именно так, UB может и послужить причиной открытия уязвимости.
Я веду к тому, что анализ в доказательстве не может опираться на семантическую разметку (владение, const и т.п.). Написано const — а ты не доверяй, смотри что фактически происходит в функции, как будто const нет.potan
06.11.2016 20:39Правильнее требовать от разработчиков использования подмножества языка, не допускающее неопределенного поведения. Ну или такой язык.
potan
06.11.2016 20:36Ну сборка мусора не такое уж абсолютное зло с точки зрения производительности. Без сборки мусора трудно избежать фрагментации памяти. Потенциально, она может улучшить реактивность, так как освобождением памяти можно заняться когда нагрузка небольшая. В Erlang, где нет мутабельных структур, сборка мусора не блокирует систему и скорость реакции достигается очень высокая, несмотря на не слишком быструю VM.
Обычно проще проверить отдельно правильность разметки, и правильность программы с разметкой, чем правильность неразмеченной программы. Даже банальный вывод типов может оказаться ресурсоемким и неоднозначным, если не требовать объявлений типов хоть где-нибудь.
Верификация компилятора пока не достижима, но можно семантическую разметку протаскивать на уровень ассемблера и доказывать эквивалентность полученной программы исходному коду.qw1
07.11.2016 23:37Обычно вместе с gc приходит вторая особенность — при композиции объектов память под каждый выделяется отдельно, когда можно было выделить одним куском. Ухудшается memory locality. Если объект составить из двух других, они могут быть выделены далеко друг от друга + обращение к половинкам требует ещё одно чтение указателя.
potan
07.11.2016 23:51Это, как раз, не проблема. Сборщики мусора обычно проводят еще и уплотнение памяти, в результате чего последовательные аллокации выделяют соседние блоки и каждая аллокация (если сборка мусора успевает все собрать), требует константного времени.
Основные проблемы — необходимость блокировок для работы с мутабельными структурами, утечки памяти, связанные с ссылками в неиспользуемых переменных и необходимость хрранения метаинформации.qw1
08.11.2016 20:38Я не об этом. Попробуйте заставить какой-нибудь node.js расположить подряд в памяти все координаты точек из объекта
struct Triangle { Point3D a,b,c; }, чтобы они попали в одну кеш-линию. Уплотнение тут не поможет.
0x131315
06.11.2016 04:22Странная статья. С первого взгляда бросаются в глаза множество глупейших ошибок в стратегии экспертов.
Может я чего-то в жизни не понимаю, но разве можно на основании неудачи одной команды делать вывод о надежности системы?
По моему количественные оценки тут вообще бессмысленны: даже если тысяча команд потерпят неудачу — 1001 может взломать. А если не взломает — есть и 1002, 1003 и так до плюс бесконечности.
И потом, разве можно утверждать, что какая-либо система надежна? Ошибки — это хаос, энтропия. Отсутствие ошибок — это абсолютный порядок, нулевая энтропия. Разве можно утверждать, что где-либо в реальности может существовать абсолютный порядок?
Разве можно недооценивать или переоценивать противника?
Хакеры, в традиционном понимании — это редкие гении, они по определению мыслят далеко за пределами разработчиков, и отыскивают ошибки там, куда ни один разработчик даже и не подумал взглянуть.
Именно поэтому хакеры находят ошибки — они видят ошибки там, где разработчики их не видят, иногда даже в упор.
Но даже гений не может утверждать, что ошибок нет.
Нельзя пригласить для оценки одного гения, и на основе его вывода заключить что другой гений также не осилит задачу.
К тому же с времен тех хакеров много воды утекло, и сейчас гении среди хакеров такая же редкость, как и среди обычных людей.
Так что делать какие-либо выводы на основе работы команды хакеров сейчас вдвойне глупо, и тянет не более, чем на попытку запудрить мозги покупателю: вот мол, хакеры не взломали, значит никто не взломает.
Это как с ведущими экспертами/собаководами и иже с ними в рекламе всяких блендаметов.
Разве можно, разрабатывая один(!) надежный компонент, распространять эту надежность на всю систему?
Система многокомпонентна, ошибка может быть в любом месте, а часто лежит вообще за пределами системы, куда разработчикам никак не могло прийти в голову заглянуть.
Самое ненадежное место в системе — взаимодействие с компонентами, в т.ч. с внешними. Это традиционно. Каждый пилит свой компонент, а стыкуются они кое-как. Ну а внешние потоки, а особенно петли данных, вообще чрезвычайно трудно проектировать без ошибок — там сам черт ногу сломит в этих кроссмодульных и кросс-системных взаимодействиях.
Умные девайсы часто прокалываются на ненадежном железе. Софт дорогой, миллион раз проверенный/перепроверенный, а железо собрано каким-нибудь.
А зачем нам надежное железо? Мы же специально для надежности и покупали дорогой софт, значит на железе можно сэкономить. И такая практика — везде, из-за чего регулярно случаются эпичные фэйлы на «подтвержденно надежных» системах: проверяли то совсем не то, что нужно было проверять, смотрели не туда, куда нужно было смотреть.
Особенно этим сейчас знамениты автопроизводители, чьи умные машины могут не стронуться с места по 1001 причине, большая часть из которых вообще несущественна, либо регулярно возникает самопроизвольно, совсем не так, как задумывалось, и никто с этим ничего поделать не может.
В общем умные системы часто на практике менее стабильны.
Разве можно все проверить?
По моему нет. По моему изначально нужно ориентироваться на то, что что-то пойдет не так.
Проверкам верить вообще нельзя, потому что иногда проверка — это рутина, которую поручают низкоквалифицированным сотрудникам, которые делают работу спустя рукава, а то и вообще ставят подпись не проверяя.
Этим славятся многие «эксперты», особенно на госслужбе.
Разве можно верить в безошибочность и непогрешимость чего-либо?
Из этой веры уже не раз вырастали самые эпичные и глупые ошибки в реализации, нередко стоящие многих жизней.
Из-за веры в непогрешимость системы, система находится на доверенном положении и проверяется слишком поздно, в последнюю очередь.
Нередко до ее проверки даже не доходит, т.к. часто ошибки находятся в других местах (а где их нет?), и на этом проверка заканчивается. Хотя проверена только часть системы.
А зачем проверять всю систему? Мы же нашли ошибку, не так ли? А то, что ошибок может быть больше одной — кто ж знал?hardegor
06.11.2016 10:12Да обычная пиар-статья, «много воды ни о чём», весь текст можно было уложить в три абзаца:
1. хакеры попробовали взломать алгоритм на формальной логике
2. исторический экскурс(Дейкстра и т.д.)
3. современное состояние формальной логики
potan
06.11.2016 15:45Попытка взлома — тестирование формального доказательства. Показывает, что в доказательстве грубых ошибок скорее всего нет.
ertaquo
Даже если код является невзламываемым, это нельзя сказать о людях.
CodeRush
И о железе. Верифицированное ядро L4 точно также можно вскрыть, используя RowHammer, уязвимость в USB-контролере или IOMMU. Даже идеальная программа будет исполнятся на вполне реальном железе, а там такое количество глюков, недоработок, странностей и переходных процессов, что дыру можно найти практически всегда — были бы деньги и время на исследования.
P.S. Посмотрите вот это прекрасное видео о получении дампа прошивки графического планшета при помощи глитчинга.
realscorp
Спасибо за ссылку на видео. Прикосновение к магии :)
Lsh
Она девушка? Не подумайте, что я сексист, просто интересно. Везде про неё написано she/her/etc.
Но выглядит неоднозначно.
qw1
А по голосу и ухоженным ногтям не понятно разве? Так кстати есть момент, где её хорошо видно в отражении выключенного экрана.
qw1
Точнее, не в выключенном, а на чёрном фоне, метка времени 00:32:32
Lsh
Честно говоря, голос меня и смутил. Несколько низковатый. Мне подумалось, что она раньше была парнем.
EndUser
https://www.youtube.com/watch?v=DykJTKvnSrw Девушка же
mwizard
Цитируя ее сайт, «My full name is Micah Elizabeth Scott, but I used to be Micah Dowty prior to Fall 2010. My friends call me Beth.», она транссексуал. Судя по этому посту, она прошла операцию.
И да, это сексизм.
nomadmoon
Просьба конкретизировать где вы видите сексизм в вопросе девушка ли автор видео? Если не сложно просьба так же ответить давно ли это у вас началось?
mwizard
В данном случае сексизм заключается в самой постановке вопроса — «я не расист, но автор видео не негр ли случаем? Да, я понимаю, что это не имеет никакого отношения к теме видео, но просто показалось, что вдруг негр.» Нелепо же выглядит, не так ли?
Элизабет ведь снимает видео не о себе, а о чисто технических знаниях, но по некоторой причине некоторая часть аудитории оценивает все равно их через призму половой принадлежности автора. Почему это вообще должно быть важно? Что изменится в зависимости от половой принадлежности? Если Элизабет — женщина, она заслуживает другой оценки своего труда, нежели если бы она была мужчиной?
А что до «давно ли началось» — с детства родители приучили к тому, что стоит уважать чувства других людей, и нужно стремиться непредвзято оценивать слова и действия людей, отдельно от их личности, внешнего вида, гендера и сексуальной ориентации.
nomadmoon
В самой постановке вопроса я, если честно, вижу идиотизм (в бытовом смысле), порождённый как раз таки внедрением радфемского новояза в жизнь. Поэтому и выглядит нелепо.
В данном случае автор комментария не высказывает каких то дискриминирующих суждений, а вы уже предлагаете далеко идущие выводы. Вас это не смущает?
PHmaster
Кошмар. Эдак скоро мы докатимся до того, что спросить у человека его имя будет восприниматься как оскорбление. Превратимся в безликую бесполую безымянную массу без каких-либо личностных характеристик. Зачем тогда люди вообще? Заложить всю драгоценную информацию в бездушные железяки, а самим тихо лечь и помереть.