Papyrus P.Oxy.Hels.2Воскресное чтение манускриптов. И кусочков папирусов. Папирус P. Oxy. Hels. 2 (справа), а точнее – та его часть, которая доступна онлайн в виде фотографии, – представляет собой узкий вертикальный кусочек, содержащий окончания самых первых строк “Илиады” (1.1-22). Фрагменты слов на папирусе вполне можно прочитать и даже сравнить с едва ли не основным источником текста “Илиады” – с манускриптом Venetus A.

Venetus A датируют десятым веком (н.э.), хоть достоверно он “выявлен в источниках” только в 15 веке. Упомянутый же папирус – относится ко второму веку (тоже н.э.). Получается, что между данными источниками около восьми сотен лет. Немало. Начертания букв сильно отличаются. Кроме того, на папирусе совсем нет знаков пунктуации, пробелов и диакритических знаков. Вообще, при ближайшем рассмотрении, отсутствие дополнительных знаков представляется очень странным – экономия места не так велика, как необходимость перечитывать один и тот же фрагмент нараспев (для греческого), чтобы понять, что же тут написано. Но, как минимум, слова с кусочка папируса неплохо сходятся с текстом Venetus A.

На манускрипте между строками записаны комментарии к тексту, но и на папирусе межстрочный интервал более или менее постоянный, это позволяет маcштабировать изображения таким образом, что фрагмент текста папируса сходится с Venetus A построчно.

Например, на скриншоте ниже фрагменты папируса и манускрипта объединены так, что можно сравнить записи построчно. Это строки с первой (не уместилась начальная Μ на Venetus A) по седьмую. Конечно, слова могли отличаться, зато на папирусе β выглядит почти как в современных шрифтах, а вот буква β манускрипта больше похожа на рукописную русскую “и” – см. пятую строку папируса, часть слова βουλή (“замысел, воля”).

Manuscript and papyrus

Строки в конце кусочка папируса сходятся с Venetus A ещё лучше – см. следующий скриншот.

Manuscript and papyrus

Здесь кусочек папируса тоже положен рядом (справа). Однако, в этих строках не только Ἀχαιοὶ (“ахейцы”) присутствует на папирусе целиком (четвертая строка на скриншоте), но и если выровнять масштаб по межстрочному интервалу и сдвинуть папирус так, чтобы πάντα[ς] из второй строки фрагмента (на скриншоте) наложилась на πάντας (“всех”) Venetus A, то (ωνα) папируса совместится с (ωνα) в слове Ἀπόλλωνα (“Аполлона”) из текста Venetus A (предпоследняя строка на скриншоте), что хоть и понятно почему, но всё равно особенно занятно.

Manuscript and papyrus



Комментировать »

Занятно читать массовые рекомендации про “срочно удалите все сообщения из переписок в мессенджере” в свете новостей о популярном мессенджере Telegram.

Дело в том, что даже если удалённые на устройстве-клиенте сообщения действительно удалятся и на серверной стороне (если они там были, да), в том числе, из всех “бэкапов” разных уровней, то это вовсе не означает, что удалится и соответствующий трафик из сетевых дампов.

Telegram – центральный мессенджер, это означает, что нетрудно определить узлы, через которые проходят все сообщения. Даже если сервер сообщения удалил (не факт, но ладно), то соответствующий трафик, при необходимости, без проблем, в пассивном режиме, сохраняется на стороне подключения каждого дата-центра, ну, это как минимум. Каких-то уведомлений “арендатора” для того, чтобы поставить “сплиттер” в нужном месте, не требуется. Все сообщения восстанавливаются из трафика, если имеются нужные ключи.

(Дополнение: да, естественно, в удалении сообщений с устройства может быть польза, понятно; речь о другом; о том, что нужно использовать правильную “модель угроз”; удаление сообщений в приложении на устройстве – это удаление сообщений в приложении на устройстве, не более того: сообщения-то и с устройства при этом могут не удалиться, что уж говорить про прочие хранилища.)



Комментарии (2) »

В современной типографике для древнегреческих текстов вопросительному знаку (“?”) графически соответствует точка с запятой (“;” – как и в новогреческом, где, формально, знак только так выглядит). В старых записях “знаков вопроса” не было. Пунктуация вообще появилась не сразу, а в старых текстах слова бывают записаны даже без пробелов.

Воскресное чтение манускриптов. Сегодня посмотрим на скриншот из манускрипта, известного как Clarke 39 (Codex Oxoniensis Clarkianus 39) – это записи сочинений Платона, на древнегреческом, конечно. Манускрипт датируют 895 годом, и там встречаются неожиданные варианты “знаков вопроса”. Фрагмент ниже (22r) относится к диалогу Платона “Критон”; уже это может показаться странным, но, в данном случае, не важно: речь пойдёт о более странных вещах – о пунктуации в средневековых манускриптах, поэтому в смысл диалога Платона не станем вдаваться.

Manuscript screenshot

Тут уже в первой строке фрагмента нетрудно найти знак, неотличимый от точки с запятой, что является большой редкостью для манускрипта девятого века н.э. Дальше – хорошо видны более экзотические варианты: двоеточие над “запятой”. На следующем скриншоте некоторые из них дополнительно отмечены зелёными стрелками.

Manuscript screenshot

В современной типографике текст между стрелками выглядит так: “τί φῄς; ταῦτα οὐχί καλῶς λέγεται;” (“Что думаешь? Это хорошо ли говорится?” – тут “точка с запятой” является вопросительным знаком).

Естественно, считается, что “запятая” тут – это вовсе не запятая, а указание на повышение тона, соответствующее вопросительной интонации, то есть, что-то вроде изогнутой стрелки. Это начертание могло послужить основой для современного знака “?”. Даже в этом манускрипте отдельный вопросительный знак используется крайне редко, далеко не во всех случаях вопросительных предложений. В древнегреческом языке вопрос можно построить при помощи специальных слов и с использованием диакритических знаков, но в неясных, – по мнению редактора, – случаях потребовалось отдельное уточнение (и оно иногда отличается от современного варианта текста). Две точки в этой записи служат для разделения высказываний участников диалога, для разделения предложений, а одна “верхняя” или “средняя” (не ясно) точка – может обозначать и окончание предложения, и паузу, так что вот эта точка тут больше и похожа на запятую, в современном понимании. Поэтому знак, указывающий на повышение тона, может быть приписан снизу как к одной точке, так и к двум.

Да, возможное отсутствие знаков препинания в исходном тексте сразу наводит на аналогию с современной перепиской, – допустим, – в мессенджерах на русском: “привет Сократ что делаешь”, “Здоров, Критон! Да вот, сижу тут, заточили меня, но есть некоторые свежие мысли” (Сократ почему-то использует знаки препинания, даже восклицательный знак, странно). Всё же, вряд ли сотрудник скриптория расшифровывал, размечая только что разработанными пунктуационными знаками, дамп базы древнего централизованного мессенждера: более распространённая точка зрения гласит, что сотрудник скриптория переписывал с папирусов и других манускриптов.

Посмотрим на увеличенный фрагмент.

Manuscript screenshot

Тут встречаются и многоуровневые “точки с запятой”, и простые “двоеточия”, так что всё сходится.

Вернёмся, впрочем, к первому фрагменту скриншота.

Manuscript screenshot

Если приглядеться, то там над первой “точкой с запятой” виден некий знак, похожий на проценты. Что он означает?

Это редакторский знак. Дело в том, что тут пропущен кусок текста, так что вопросительный знак (“;”) вообще оказался перенесён – он должен быть через восемь слов, но тоже после “δ᾽ οὔ” (как и на скриншоте), а недостающий фрагмент записан тут же, на полях (“οὐδὲ πάντων ἀλλὰ τῶν μέν, τῶν δ᾽ οὔ;”).

Manuscript screenshot

Заканчивается этот комментарий вопросительным знаком, который, как мы разобрались, неотличим от точки с запятой (настолько неотличим, что приводит к занимательным случаям в Unicode; где, впрочем, предлагается “нормализовывать” всё в один символ, в “;”).



Комментировать »

Кстати, что касается постквантовых криптосистем от NIST и “квантовых компьютеров, взламывающих современные криптосистемы”, которые, якобы, “могут появиться через десять лет” (а могут и не появиться): есть ещё ничуть не менее распространённый штамп, утверждающий, в этом контексте, что “квантовые компьютеры кардинально быстрее решают задачу факторизации”. Факторизация – это разложение данного числа на простые множители. Однако речь в данном штампе почти всегда идёт про алгоритм Шора. Технически, это разные утверждения: о скорости факторизации и – про алгоритм Шора. Что не так важно. Куда как более показательно, что никакой “квантовый компьютер” пока что вообще не решал задачу факторизации, что уж там говорить про то, чтобы решать эту задачу “кардинально быстрее”.

Без преувеличений и “раздувания хайпа” надо было бы сказать, что алгоритм Шора описывает теоретическое “квантовое преобразование”, которое позволяет снизить сложность факторизации, проводимой классическим компьютером, до полиномиальной. И тот же математический аппарат, который порождает данное “квантовое преобразование”, пока что успешно используется при интерпретации некоторых физических экспериментов. Не более того. О каком-то “кардинально быстрее” – и речи-то пока что не идёт. А вот “постквантовая стойкость” – это, в рамках термина, именно предполагаемая стойкость именно к “алгоритму Шора”.

Понятно, что стандартизованная постквантовая криптосистема может оказаться уязвимой для классического криптоанализа (и, скорее всего, так и выйдет). При этом, несмотря на прижившиеся штампы в СМИ, пока никто не продемонстрировал, как именно можно было бы реализовать алгоритм Шора с полиномиальной сложностью, что называется, в железе. Потому что те немногие эксперименты с числом 15 или чуть большим числом, на которые ссылаются много лет, в принципе не позволяют проверить ключевую часть реализации алгоритма – квантовое преобразование Фурье.

Тем не менее, пробовать построить квантовый компьютер хотя бы на 2^1024 состояний – это полезно.



Комментарии (2) »

NIST выпустил первые стандарты по криптосистемам с постквантовой стойкостью. Как и ожидалось:

  • FIPS 203: обмен ключами (KEM) – Kyber, который в стандарте называется ML-KEM, где ML – это Module-Lattice (модули с решётками, а не “машинное обучение”);
  • FIPS 204, FIPS 205: подписи – CRYSTALS-Dilithium (ML-DSA, основной, 204) и Sphincs+ (SLH-DSA, дополнительный/резервный, 205).

(via)

P.S. Универсальных квантовых компьютеров пока нет и не видно, даже если присмотреться, но NIST в новости намекает, что, “как предсказывают некоторые эксперты”, квантовые компьютеры, способные взламывать современные криптографические алгоритмы, всё же могут появиться в течение десяти лет.



Комментировать »

Метаинформация о TLS-соединении. TLS-клиенты часто могут быть классифицированы (с точностью до типа и, реже, версии) по начальному сообщению TLS-сессии. Это позволяет при пассивном прослушивании узнавать трафик конкретных программ-клиентов (и не только, но сейчас речь только про клиентов и начало соединения).

Дело в том, что начальное сообщение, отправляемое клиентом, – ClientHello, – содержит много параметров и, соответственно, имеет структуру, которой хватает для эффективного построения отпечатков. Например, весьма подробное представление о том, как такой классификатор действует, можно составить, если внимательно посмотреть на выдачу моего тестового сервера TLS 1.3. Посмотреть можно непосредственно веб-браузером. При успешном соединении сервер вернёт страницу, где в подробностях показано то самое CLientHello, которое сервер получил от клиента. Вы можете подключиться браузером, обновить страницу несколько раз и увидеть, какие блоки данных не изменяются и, поэтому, служат основой для построения сигнатур.

Посмотрим на ситуацию чуть подробнее (рассматриваем случай TLS поверх TCP). Основу для построения сигнатур (отпечатков) может составлять последовательность байтов, которые представляют структуру TLS-сообщений. То есть, сообщения строятся из некоторого набора полей, а этим полям обязательно соответствуют конкретные заголовки.

Прежде всего, структура базового уровня: для TLS это будут TLS-записи, которые имеют свой простой заголовок фиксированного формата. Этот заголовок содержит обозначение типа и обозначение версии, а также – запись длины. С первыми параметрами (тип, версия) – всё очевидно, однако они, сами по себе, не дают нужной избирательности. Но уже сопоставление длины с соответствующей частью потока – даёт неплохой дополнительный признак: можно проверить, что заданное количество байтов укладывается в общий состав разбираемого потока.

Эта же идея важна и для разбора самого сообщения ClientHello, где она позволяет анализировать структуру следующего уровня, так как ClientHello вложено в TLS-запись. А состоит идея в том, что значения байтов, кодирующих предполагаемую длину, интерпретируются как смещение; полученное значение прибавляется к текущему адресу (в предварительно собранном потоке байтов) и значения байтов по вычисленному адресу сравниваются с ожидаемыми значениями, которые там оказались бы, если это действительно анализируется ClientHello. И если TLS-записи тут не добавляют много нового (они просто следуют одна за одной), то в ClientHello появляются вложенные поля данных (расширения) и более богатая структура, которая, тем не менее, устроена точно так же: значения байтов, интерпретируемые как целое число, задающее длину, должны строго сходиться, когда рассматриваются в виде цепочки. Заметьте, что до разбора самих значений полей данных дело ещё даже не дошло. Это важная особенность TLS: данный протокол не обладает скрытностью. Скрытный протокол выглядел бы случайным набором байтов со случайными же значениями. TLS, – особенно, на начальном этапе соединения, – выглядит как связанная строгими параметрами длины и типов байтовая структура (так, впрочем, и должно быть).

Для машины, разбирающей трафик, все эти записи “структур в байты” представляют собой наборы битов. Так что грамотно построенная ASIC-система может сопоставлять шаблоны с имеющимся потоком чрезвычайно быстро (ASIC – это аппаратная, интегральная схема, построенная под конкретную задачу; например, ASIC-и давно используются в производительных маршрутизаторах, потому что никакой универсальный процессор за ASIC-системой не угонится).

Итак, вернёмся к ClientHello. Помимо верхнеуровневой структуры из вложенных блоков, есть и содержание этих блоков. Например, сообщение ClientHello, в самом начале, после указания версии, полей Random и SessionID, содержит перечень шифронаборов, которые поддерживает клиент. (Это всё хорошо видно в выдаче тестового сервера.) Сокращённый пример: 0x1301, 0x1303, 0x1302, 0xC02B, 0xC02F… На уровне потока данных это всё просто последовательные значения байтов, по два байта на каждый идентификатор шифронабора (понятно, что данному блоку предшествуют байты с записью длины, что добавляет “узнаваемости”).

Так, для конкретной версии браузера перечень шифронаборов – узнаваем. В принципе, ничто не мешает клиенту менять состав и порядок пар байтов, обозначающих шифронаборы, но, например, Firefox передаёт фиксированный набор. Понятно, что строгая последовательность из 36 байтов – это уже достаточный идентифицирующий признак. (36 байтов получается так: 17 идентификаторов шифронаборов от Firefox, по два байта каждый, плюс два байта на запись длины.) Чуть более подробный пример, начальная часть ClientHello TLS 1.3:

 Type (тип сообщения, 0x01, один байт - подходит для сигнатуры);
 Len (длина сообщения, три байта - подходит для сигнатуры: должно соответствовать общей структуре);
 Version (версия, 0x0303, два байта - подходит для сигнатуры);
 Random ([...], 32 "случайных" байта - не подходит для сигнатуры);
 SessionID_Len (длина данных Session_ID, один байт, для TLS 1.3 - подходит для сигнатуры);
 SessionID (обычно, для TLS 1.3 от браузера тут будет 32 байта - не подходит для сигнатуры).
 CS_Len (длина данных списка шифронаборов, два байта - подходит для сигнатуры);
 CS (список двухбайтовых идентификаторов шифронаборов - подходит для сигнатуры).
 [...]

При этом, скажем, браузер Chromium/Chrome добавляет к списку шифронаборов так называемые значения GREASE (для тестирования реализаций TLS), которые меняются от сеанса к сеансу. Но значения GRASE имеют строго определённый формат, так что их несложно распознать автоматом. Если взять такой клиент, как cURL, то состав ClientHello будет другим, в частности, другим будет список шифронаборов. Более того, по составу ClientHello нередко можно определить даже используемую библиотеку, реализующую TLS.

Естественно, не только шифронаборы подходят для построения сигнатуры. В ClientHello современных браузеров присутствует разнообразный набор расширений – это дописываемые в сообщение поля со своей структурой: они содержат заголовок с записью длины, дополнительные блоки внутри. Для TLS 1.3 расширения имеют определяющее значение. Внутри расширений передаются различные необходимые параметры, в частности, открытая часть протокола Диффи-Хеллмана и открытый ключ постквантовой криптосистемы X25519Kyber768. По составу и количеству расширений можно построить дополнительную сигнатуру. Так, уже наличие X25519Kyber768 едва ли не однозначно выдаёт современный веб-браузер. А ведь современный браузер ещё и укажет расширение ECH (Encrypted ClientHello). Firefox использует зафиксированный порядок расширений ClientHello, а браузер Chromium/Chrome – порядок следования расширений изменяет между сессиями. Однако даже в случае, когда порядок расширений разный, всё равно можно использовать перечень имеющихся расширений для построения сигнатуры.



Комментировать »

Предположим, имеется TLS-сертификат на веб-сайте, – то есть, выпущенный для доменного имени, – и соответствующий секретный ключ. Можно ли использовать этот секретный ключ для подписывания каких-то произвольных файлов, например, текстовых сообщений?

Да, это возможно. Технически, ключ вовсе не зафиксирован в роли “только для сайта”, так что ничего тут не мешает: достаточно взять какую-нибудь подходящую утилиту, которая может прочитать секретный ключ из файла (OpenSSL или другие варианты), и можно начать подписывать произвольные электронные документы. В процессе подписывания – открытый ключ и сертификат вообще не требуются. Естественно, каждое использование ключа (буквально – каждая операция) несёт с собой дополнительный риск утечки этого ключа. Однако, при штатной работе TLS, ключ “от сертификата” уже постоянно задействован именно для получения электронной подписи, так что тут нет места для каких-нибудь опасений относительно того, что ключ будет “использован не по назначению”. Однако для хитрых ошибок – место, всё же, появляется.

Так, если для подписи файлов применяется новая утилита, отличная от библиотеки, используемой TLS-реализацией веб-сервера, то возникает дополнительная вероятность утечки: либо непосредственно через эту утилиту, либо в процессе её вызова. Если этот дополнительный, относительно веб-сервера, процесс вдруг так устроен, что позволяет третьей стороне непосредственно подписывать произвольные данные, то даже без утечки ключа это ведёт к компрометации TLS-сервера: третья сторона может подменить сессию, перехватив соединение и подписав нужные параметры, которые подаст в виде файла на вход подписывающей утилиты. Так что осторожность – не помешает, а утечки ключей от одного TLS-сервера через другой, сконфигурированный с уязвимостью, – уже случались.

Проверка подписи для рассматриваемого способа использования проводится при помощи открытого ключа, опубликованного в TLS-сертификате. Тут возникает административный момент, связанный с политикой управления доверием, используемой приложением на проверяющей стороне. Это приложение может “верить в сертификат”, а может – “верить в сам ключ”.

В первом случае – допустимый контекст использования ключа задаёт сертификат и, так сказать, семантика применения этого сертификата. Например, приложение может в принципе принимать TLS-сертификаты (и ключи из них) только в контексте подписывания TLS-параметров при HTTPS-доступе к веб-серверу, и всё. Естественно, в сертификате предусмотрены дополнительные флаги и параметры, определяющие допустимые способы использования ключа. Их приложение тоже может учитывать каким-то своим способом (но, заметьте, использование ключа для подписи – в сертификате “от сайта” должно быть разрешено и так; см. выше).

Во втором случае, когда приложение “верит в сам ключ”, сертификат служит лишь контейнером для доставки этого ключа. “Верить в сам ключ” – означает, что доверие распространяется прежде всего на конкретное значение ключа, но при этом сам сертификат из рассмотрения может и не исключаться. Например, это обычная практика для корневых ключей в TLS для веб-сайтов и браузеров.

Впрочем, “побочное” использование ключей “от сайтов” для подписывания может подразумевать и то, что открытый ключ тоже используется вообще без учёта сертификата. Технически, опять же, ничего этому не мешает.



Комментировать »

Воскресное чтение манускриптов. В прошлом году, в заметке про кусочек папируса с фрагментом “Илиады”, я писал, что какие-то очень краткие фрагменты текстов, читаемые на папирусах, могли бы относиться к той же “Илиаде”, но их не получится так идентифицировать, поскольку недостаточно информации, а фрагменты выходят за пределы “эластичности” текста “Илиады”. Это довольно очевидное наблюдение. Тем не менее, посмотрим, можно ли на сканах манускриптов быстро найти что-то примерно подходящее, для иллюстрации. То есть, фрагменты текстов из нескольких слов, которые было бы не ясно куда отнести. Оказывается – найти можно. Для примера годится не слишком частая, но характерная фраза из записей сочинений Гомера. Скажем, кусочек из стиха, в котором упоминается Kubernetes – потому, что этот фрагмент тоже не так давно встречался на dxdt.ru, в записке про “Кибернетический след и цветовой сдвиг“. А именно: ἐνὶ οἴνοπι πόντῳ – “в тёмно-винном море”.

Ниже пара фрагментов манускриптов: Venetus A (“Илиада”, Гомер) и BnF.Grec.2771 (“Труды и дни”, Гесиод). Соответствующая фраза – выделена и там, и там.

Manuscript, screenshot

(Venetus A, 23:316)

Manuscript, screenshot

(BnF.Grec.2771, st. 622)

Первый манускрипт (Venetus A) датируется началом девятого (поправка, 2025/06/04: десятого) века, второй – десятым (всё н.э, понятно). То есть, между соответствующими манускриптами больше ста лет, согласно датировкам (поправка, 2025/06/04: меньше ста лет, конечно). При этом структура, оформление, а кроме того, что называется, “типографика” и начертания букв, очень и очень близки, что хорошо видно на скриншотах. Удачно, что интересующие нас слова в обоих случаях приходятся на конец строки. Попадись кому-то достаточно небольшой кусочек с записью только этих слов (как выделено на картинках, вместе с частями диакритических знаков и буквы из верхней строки) – различить источники по составу и по буквам текста вряд ли было бы возможно. Однако, если удалось бы прицепить какие-то ещё буквы (строки выше и ниже), то результат уже мог бы быть более избирательным.

Гесиод – из гомеровского периода, так что, наверное, ничего удивительного. Тем более, что приведённый фрагмент текста “про море” находится очень близко к описанию в “Трудах и днях” путешествия на “состязание поэтов”, которое нередко считают упоминанием состязания между самим Гесиодом и самим Гомером.



Комментировать »

В продолжение записки про ИИ Google и “серебряную медаль” Международной математической олимпиады. Там исходная задача, которую потом “решает” ИИ, прежде переводится людьми на входной язык системы машинных доказательств – то есть, на некоторый формальный язык, описывающий в определённых логических формулах целевое состояние, соответствующее задаче. Это не программа, как иногда пишут, а запись, грубо говоря, теоремы, соответствующей задаче, в формулах, которые возможно (при некоторых ограничениях) доказать в данной системе. Да, доказательство выполняется при помощи компьютерных вычислений, тем не менее, формальная запись задачи-теоремы не является программой, реализующей некий алгоритм – иначе не было бы смысла в поиске записей доказательств. И вот в “популярном изложении” необходимость такого перевода обосновывают тем, что нужно “переписать на языке, понятном системе”. Это, конечно, искажение. Но с ним связаны два важных момента.

Момент первый, – достаточно очевидный, – в том, что этот “суперпродвинутый” искусственный интеллект даже не способен прочитать условие задачи и, предположим, перевести его на формальный язык самостоятельно, хоть это и могло бы быть типичным вариантом запроса к ChatGPT. Так как для корректного перевода нужно хорошо понимать не только задачу, но и принципы построения формальных языков, выдача подобного ИИ-перевода для входа “системы ИИ” просто не подходит. Это понятно.

Есть и второй момент, который “замыливают” посильнее: перевод на формальный язык необходим для того, чтобы предлагаемые системой решения могли быть проверены на соответствие этому описанию машинным способом. То есть, так как предполагается, что будут подбираться тексты “доказательств” на формальном языке, необходим автоматический, машинный “проверятор” для этих доказательств – иначе, если решения потребуется согласовывать с человеком, то и работать это всё будет слишком медленно, поскольку образуется непреодолимый затык с проверкой решений. Так что необходима запись на формальном языке и проверяющая компьютерная система, а такая система в принципе не может проверять записи на естественном языке. Так что, понятно, это не решение олимпиадной задачи в том смысле, который тут принято присваивать слову “решение”.

Что же касается применения систем машинного (автоматического) доказательства в области теоретической (чистой) математики, то тут мнения, как говорится, сильно расходятся. Прежде всего потому, что теоретическая математика это не только не наука, но и вовсе не является такой уж “точной и строгой” областью, как, почему-то, нередко предполагают. Однако системы машинного доказательства очень полезны в некоторых прикладных математических направлениях. Например, для формальной проверки корректности (соответствия задаче) программного кода. Автоматические системы на этом направлении уже используются. Наверное, и автоматический генератор доказательств с перебором тут мог бы тоже пригодиться, как инструмент “фаззинга”. Но нужно учитывать, что во всех случаях речь, всё же, идет о компьютерных вычислениях, а не о математических операциях, поэтому соответствующие методы имеют существенные ограничения, как фундаментальные, так и вполне “локальные”, обусловленные ошибками на разных уровнях реализации.



Комментировать »

Исследователи, сравнивая в автоматизированном режиме (fuzzing) поведение различных микропроцессоров семейства RISC-V, обнаружили дефекты команд в линейке распространённых ЦПУ T-Head C910. Дефекты относятся к конкретной реализации и расширениям RISC-V, которые могут использовать разработчики совместимой аппаратуры.

Особенно интересно выглядит команда, позволяющая реализовать прямую запись данных в физическую память (ОЗУ) по произвольному адресу, минуя не только внутренний кеш, но и вообще все аппаратные ограничения на уровне процессора. Такой “гаджет”, конечно, позволяет добиться уверенной эскалации привилегий (и не только), в том числе, из любых контейнеров и прочих систем виртуализации. В качестве примера в исходной работе приводятся линуксы и модификация системного вызова getuid() таким образом, чтобы он всегда возвращал значение 0 (это, соответственно, root в линуксах). Очевидно, от типа ОС такой результат не зависит, так как речь про произвольный и прямой доступ в память.

(Новость OpenNet.)



Комментировать »


Комментировать »