<зануда>
Я лечусь (у врача) — это я лечу сам себя?
Я кусаюсь — я кусаю сам себя?
Я дерусь — драка с самим собой?
Я учусь (в школе/университете) — это я учу себя?
Не стоит переоценивать возвратность суффикса «сь».
</зануда>
Я бы решал эту задачу используя механизмы безопасности Windows — загрузка библиотек только из папки на которой явно прописаны допустимые права и вместо проверки хэшей, сразу бы сделал проверку подписи PE-файла, благо к этому довольно внятное АПИ, хоть и не без подводных камней. Если запускать сервис, то я вижу лучшим решением скопировать его в C:\Windows\system32 — стандартные библиотеки защищены от переписывания механизмами защиты ОС и если там можно будет подменять библиотеки, то у нас проблемы посерьезнее, чем внедрении dll в сервис.
Да, вы правы. Из недавнего — такие уязвимости были у NVIDIA и, вроде, у какого-то продукта Cisco.
А про состояние гонки — TOCTOU часто можно выиграть используя OpLock.
Да, спасибо, что упомянули список KnownDLLs и ключ CWDIllegalInDllSearch. Они слишком редко встречаются в боевых условиях, поэтому не стал заострять на них внимание.
Но все же, version.dll не входит в список KnownDLLs (по крайней мере на ближайших доступных мне машинах). И инъекция отлично работает (на гитхабе выложены билды dll, опыт ставится легко).
С одной стороны метод хороший, но довольно сложно его реализовать правильно. Дело в том, что если загрузка идет через секцию импорта, то проверять и считать что-либо уже поздно — библиотека уже загружена и выгружать ее бесполезно — код уже выполнен. Если загрузка происходит ручками, то у нас появлются варианты: можно намеренно испортить dll и тем самым сломать логику приложения, но что хуже, потенциально можно поставить OpLock на файл и подменить его после доступа на чтение. Получится, что сначала у файла посчитают контрольную сумму и она будет корректной, а загрузит приложение уже подмененный файл.
За секунду до окончания вы блокируете прием новых участников в список. Дальше перебором вставляете псевдо имейл (из-за звездочек все равно не проверить реальный он или нет) и рассчитываете алгоритм, получая какой-то номер. Если номер не «загаданный», то повторяете. Мощность перебора у вас больше количества участников, так что рано или поздно перебор выдаст такой имейл, чтобы результат был подходящий. Учитывая скорость перебора, возможный предрасчет md5, я думаю, что той самой секунды хватит, чтобы никто не влез, а ваш «псевдоучастник» добавился.
Простите, а что конкретно ваш алгоритм позволяет проверить? То, что конкретный участник правда проиграл или что у всех участников были равные шансы, даже если кто-то из участников знал чувствительные данные из внутрянки вашего сайта/алгоритма?
Если второе, то очень интересно. А если первое, то можете не утруждаться — таких алгоритмов можно с десяток за час придумать.
Там в принципе интересная ситуация. Художник (Михаил Беломлинский) действительно рисовал Бильбо с Леонова, но сделал это, как сейчас говорят, без разрешения правообладателя (самого Леонова). Причем это случилось как раз в момент, когда вся эта тема массово обсуждалась в печати, и даже сам Никулин писал о том, что его образ используют в куклах, пародиях.
Все благополучно разрешилось по факту — Беломлинский и Леонов встретились на каком-то мероприятии, где художник показал книгу с иллюстрациями. Леонову они очень понравились и вопрос можно было считать исчерпанным. В начале видео Леонов сам рассказывает об этой ситуации.
Я понимаю, что вы практик, а не теоретик, но обратите внимание, что "дешифрование" и "расшифрование" имеют разный смысл. Первое проходит без ключа и, фактически, означает атаку, а второе с ключом — типовая операция получения доступа.
Тут дело не столько в целостности повествования, сколько в том, что переход о котором я говорю, так сказать, важнее, чем все что есть в статье. Точнее мне это так видится, сейчас объясню почему.
Из статьи видно как солвер находит и не находит решения некоторой задачи описанной на формальном языке. Так вот тот переход, который опущен — это объяснение как переносить готовый код (с обвязкой в виде ОС, системных вызов и еще кучи чего) на формальную логику.
Возьмем условно банальный хартблид. Расскажите как можно через формальную верификацию найти его в коде. Поскольку на входе комбинаторный взрыв, то вангую ответ — никак. Вот если взять один файл, с 3 функциями, то наверное найдет. Ну как бы: знал бы где упал — соломки постелил бы.
Ладно это все то, о чем в статье нет. И вполне вероятно можно отмахнуться фразами типа в следующих статьях раскроете, хотя все же я почти уверен, что все сведется к «берем код без внешних вызовов, без работы с файловой системой, без сети и доказываем, что 2+2 никогда не вызовет переполнения стека».
Спасибо, что рассказываете об формальной верификации, это все реально интересно. Но попробуйте быть ближе к настоящему применению и если пишете о чем-то, то раскрывайте.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
к
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
В какой момент ядро Windows перешло во вполне детерминированную задачу о 8 ферзях, а ОС беспилотников Darpa в задачу о козе, волке и капусте.
Какие уязвимости могут быть в задаче о 8 ферзях?
Я бы попробовал высказать лемму, что если в алгоритме нет условных циклов, безусловных переходов и рекурсии (фактические есть только несколько циклов for с фиксированным счетчиком), то такая программа всегда остановит свою работу, ибо у нее просто нет способов зациклиться.
Что вы в итоге верифицировали?
Я лечусь (у врача) — это я лечу сам себя?
Я кусаюсь — я кусаю сам себя?
Я дерусь — драка с самим собой?
Я учусь (в школе/университете) — это я учу себя?
Не стоит переоценивать возвратность суффикса «сь».
</зануда>
очень наводит на мысли о том, что хочется хапнуть еще денег.
А про состояние гонки — TOCTOU часто можно выиграть используя OpLock.
Но все же, version.dll не входит в список KnownDLLs (по крайней мере на ближайших доступных мне машинах). И инъекция отлично работает (на гитхабе выложены билды dll, опыт ставится легко).
Если второе, то очень интересно. А если первое, то можете не утруждаться — таких алгоритмов можно с десяток за час придумать.
Все благополучно разрешилось по факту — Беломлинский и Леонов встретились на каком-то мероприятии, где художник показал книгу с иллюстрациями. Леонову они очень понравились и вопрос можно было считать исчерпанным.
В начале видео Леонов сам рассказывает об этой ситуации.
Я понимаю, что вы практик, а не теоретик, но обратите внимание, что "дешифрование" и "расшифрование" имеют разный смысл. Первое проходит без ключа и, фактически, означает атаку, а второе с ключом — типовая операция получения доступа.
Из статьи видно как солвер находит и не находит решения некоторой задачи описанной на формальном языке. Так вот тот переход, который опущен — это объяснение как переносить готовый код (с обвязкой в виде ОС, системных вызов и еще кучи чего) на формальную логику.
Возьмем условно банальный хартблид. Расскажите как можно через формальную верификацию найти его в коде. Поскольку на входе комбинаторный взрыв, то вангую ответ — никак. Вот если взять один файл, с 3 функциями, то наверное найдет. Ну как бы: знал бы где упал — соломки постелил бы.
Ладно это все то, о чем в статье нет. И вполне вероятно можно отмахнуться фразами типа в следующих статьях раскроете, хотя все же я почти уверен, что все сведется к «берем код без внешних вызовов, без работы с файловой системой, без сети и доказываем, что 2+2 никогда не вызовет переполнения стека».
Спасибо, что рассказываете об формальной верификации, это все реально интересно. Но попробуйте быть ближе к настоящему применению и если пишете о чем-то, то раскрывайте.
к
В какой момент ядро Windows перешло во вполне детерминированную задачу о 8 ферзях, а ОС беспилотников Darpa в задачу о козе, волке и капусте.
Какие уязвимости могут быть в задаче о 8 ферзях?
Я бы попробовал высказать лемму, что если в алгоритме нет условных циклов, безусловных переходов и рекурсии (фактические есть только несколько циклов for с фиксированным счетчиком), то такая программа всегда остановит свою работу, ибо у нее просто нет способов зациклиться.
Что вы в итоге верифицировали?
Обещать вот прям точно сделать разбор я не буду, поскольку это реально нетривиальная задача, но я попробую при случае.