Ресурсы: техническое описание TLS, LaTeX - в картинки (img), криптографическая библиотека Arduino, шифр "Кузнечик" на ассемблере AMD64/AVX и ARM64
В блоге Cloudflare – подробности про поддержку ML-DSA DNS-сервисом 1.1.1.1 (я писал об этом пару дней назад). По ссылке (на сайт Cloudflare), собственно, в подробностях развёрнуты все те же моменты: переход DNS на TCP (потому что ответы с ML-DSA не пролезают в UDP) и внедрение соответствующих криптосистем в корне DNS. И есть новый пример зоны с ML-DSA в DNSSEC: valid.mldsa44.dnstest.dev.
Комментировать »
Anthropic (это Claude) на днях опубликовали, как заявляется, полную “формализацию” для Великой теоремы Ферма. Под “формализацией” тут надо понимать машинное описание всего набора необходимых теорем, за исключением нескольких базовых. С точки зрения алгоритмов, речь там про Lean-код, который подтверждает верность выводов – там заявлено 29511 сопутствующих теорем (это в терминах Lean, но, вообще, тут не так важно), то есть, заведомо необозримый кусок текста, и даже для машинной проверки – требуются сотни гигабайтов памяти (ОЗУ) и многие часы работы компьютера.
Но тут особенно интересен сопутствующий аспект: а именно, то, как новость подаётся. В тексте официальной новости несколько раз упоминаются другие, “человеческие” начинания на пути этой же “формализации”, но эти начинания, пока что, успеха не достигли, что тщательно подчёркивает текст новости. И это так, тут не поспорить. Достигла ли успеха машинная программа с миллионами строк и десятками тысяч “машинных теорем”? Тоже непонятно. Собственно, тут-то и кроется действующий конфликт: с завершающими заявлениями по долгоиграющим популярным темам вокруг теоретической математики начали выступать не университеты какие-нибудь, а коммерческие корпорации, поставляющие мощнейший вычислительный сервис, который принято называть LLM/AI. И выступают эти корпорации тут нынче регулярно: следом за “Ферма-формализацией” – свежее заявление по уравнениям Навье-Стокса от OpenAI (это проблема из раскрученного списка “Задачи тысячелетия”).
Комментировать »
IANA уже выделила для ML-DSA-44 номер 18 в индексе криптосистем DNSSEC. ML-DSA – это постквантовая криптосистема подписи, родственная ML-KEM, а цифры 4 в обозначении – это идентификатор используемого набора параметров, самого “короткого”. Применение данной квантовостойкой криптосистемы в DNSSEC описано в свежем черновике RFC (Westerbaan/Schmieg), и проверка ML-DSA-подписей уже есть в DNS-сервисе 1.1.1.1. Пример DNS-зоны с ML-DSA-подписью: only.alg18.westerbaan.name. (Большая редкость, понятно.)
Конкретно с этим алгоритмом основная проблема в том, что пусть 44-й вариант и самый “короткий”, но подпись всё равно занимает 2420 байта, а открытый ключ – 1312 байтов. То есть, для передачи данных всё равно потребуется TCP. Естественно, поддержка TCP необходима для работы DNS, но UDP всё ещё остаётся основным транспортом для простых DNS-ответов. Впрочем, возможно, что внедрение посткантовых криптосистем окончательно UDP вытеснит (конечно, UDP – быстрый протокол, но и для TCP есть Fast Open).
Тут можно заметить, что если у вас используется сервис DNS (рекурсивного резолвера) типа 1.1.1.1, то, скорее всего, к нему ваш системный резолвер уже и так подключается по TCP. И действительно, нынче сетевые реалии таковы, что DNS over TLS становится необходимостью, из-за подмены DNS-трафика. Ну а где TLS – там всё равно TCP. Однако не забывайте, что здесь речь-то идёт не о подключении клиента к рекурсивному резолверу, не о “последней миле”, а о том, как резолвер подключается к авторитативным серверам, о “внешем плече”. И вот там, чтобы получить ответ с ключами (DNSKEY) и подписями (RRSIG) ML-DSA, потребуется получить от авторитативных серверов по несколько килобайт данных. Если сравнить с ECDSA, то и трафик увеличивается в десятки раз, и TCP приобретает дополнительный вес. Ну и в типичной конфигурации валидацию DNSSEC-записей выполняет внешний резолвер, не системный.
Занятно, что внедрение ML-DSA в DNSSEC для зон ниже корневой, при том, что в корневой зоне используется не постквантовая криптосистема, – смысла имеет не так много, как можно подумать. Конечно, можно наладить собственную валидацию и проверять конкретные подписи, а ключам верить по значению. Но это не совсем то, чего ожидают от глобального дерева DNSSEC. А в корневой зоне сейчас RSA, а переходить – планируют на ECDSA.
Комментировать »
Дошли слухи, что и новая модель OpenAI GPT-6 Astra, даже в режиме Pro, считает, что причина (существования) дня и ночи на Земле – это вращение Земли вокруг своей оси. Занятно. Несомненно, это сейчас самая продвинутая модель из публично доступных. Но результат “по данному вопросу” – всё тот же. Вообще, тема про вращение Земли и день с ночью – одна из самых показательных. И вовсе не в отношении LLM, а в отношении понимания, знания и “наученности”. Я, кстати, часто к этой теме обращаюсь, и на dxdt тоже.
Почему выше слово “существования” дано в скобках? Потому что тут есть небольшая языковая особенность. Исходный вопрос – на английском, и он хоть и использует определённый артикль, но истолковать, действительно, можно по-разному. Однако толкования не спасают ситуацию: What is the cause of day and night on Earth? GPT-6 почему-то отвечает: Day and night are caused by Earth’s rotation on its axis (дословно: “День и ночь вызваны вращением Земли вокруг своей оси”). Дальше там идут неважные пояснения. Очевидно, это просто неверный ответ, как бы слова ни трактовались (в рамках разумного, конечно). К сожалению, этот неверный ответ – самый распространённый, поэтому-то он и тут вылезает. Но, надо отдать системе должное: если начать подсказывать, то верные ответы начинают вылезать тоже. Впрочем, эта записка немного о другом, а GPT тут лишь в качестве повода.
Как вообще нужно отвечать на вопрос о том, в чём причина существования дня и ночи на Земле? Отвечать нужно прямо и правильно: причина – в Солнце. Почему? Потому, что если убрать Солнце, – как светило, – из системы, то не будет ни дня, ни ночи. Кто-то может потребовать уточнений: дня, понятно, не будет без Солнца, но вот планета-то погрузится в вечную ночь. Как бы ни так! Ночь – это промежуток времени от заката до восхода, так что день – необходим для определения ночи. Нет Солнца – нет восхода. Нет и ночи.
Очевидно?
Почти.
Если начать закапываться в детали, то вылезут небольшие логические хитрости. Первая из них: Земля должна быть непрозрачной. Вот это как раз очевидно. На прозрачной хрустальной Земле солнечный свет просвечивает все стороны одновременно. Вторая хитрость: на непрозрачной Земле не должно быть такой атмосферы, которая рассеивает свет Солнца “по всей поверхности планеты”. Но это именно что неожиданные детали и уточнения. И если убрать Солнце, то даже на хрустальной Земле не будет ни дня, ни ночи.
Рассмотрим теперь другой вопрос: в чём причина смены дня и ночи? Правильный ответ: причина в том, что Солнце вращается вокруг Земли. Потому что если Солнце не вращается вокруг Земли, то на одной стороне той Земли всё время ночь, а на другой – всё время день.
(Откровенно говоря, меня всегда удивлял тот факт, что люди начинают почему-то вспоминать как, якобы, “вот Коперник доказал”, хотя Коперник ничего такого и не пытался доказывать. “Допустим, ваш Коперник прав”, – пояснял Шерлок Холмс. Но какая разница? Да никакой, действительно.)
Кажется, если всё время ночь на одной стороне планеты, тогда эту ночь нельзя будет назвать ночью, поскольку опять нет восхода Солнца. Но это только формально: если путешествовать по такой Земле, проложив подходящий маршрут, то в какой-то момент восход образуется из-за собственного движения путешественника.
Заметьте, Земля, вокруг которой Солнце не вращается, тем не менее вращается вокруг своей оси (в наивном смысле), если только она движется по орбите вокруг Солнца. Как так получается? Очень просто: чтобы всё время быть повернутой к Солнцу одной стороной – Земле нужно вращаться. Но, опять же, вращение тут – это вопрос системы координат. Тем не менее, за движение по орбите тут опять отвечает Солнце. Не было бы Солнца, не было бы данного орбитального движения, а лишь вечный не-день, который вращением не исправить.
Комментировать »
Ещё из серии “Забавные истории с LLM”. Снова Claude. Так как на пути программного кода возводятся неожиданные “кибербезопасные препоны” (cybersecurity guardrails), я тут на днях решил попробовать задачи из области теоретической математики: там есть Lean (это инструмент описания и проверки “компьютерных доказательств”), но не должно быть “кибербезопасных препон для безопасной безопасности”. На роль примера я наобум выбрал задачу 11.115 из “Коуровской тетради” (этот широко известный в узких кругах канонический список я упоминал ранее; как оказалось, не зря упоминал). Я набросал общее описание контрпримера к задаче, в меру собственного понимания, и попросил Claude найти конкретный контрпример и подготовить соответствующее доказательство на Lean.
Система Claude существует в нескольких LLM-воплощениях, доступны мне не все, но основные, как я понимаю, доступны. Сперва я задал запрос в Fable 5. Оно почему-то зациклилось и кружилось внутри себя, наступая периодически на “лимит вызова команд”, очень долго. Наверное, часа два. Никакого результата не выдало, но “кредиты” съело (неплохая “бизнес-модель”, кстати: показываем “юзеру” какие-то меняющиеся текстовые строки в браузере через Javascript и списываем за это “кредиты” в огромных количествах). Но не будем торопиться с выводами.
Потом я решил запустить в той же ветке Opus 5 Max. Как ни странно, Opus 5 Max довольно быстро нашло контрпример (да! и очень даже похожий на правду – см. ниже), но совсем не осилило Lean. Код Lean содержал какие-то вымышленные имена теорем, которых нет в библиотеках (я не очень хорошо понимаю Lean, но, думаю, тут всё именно так). Claude Opus 5 Max – объяснило, что на своей стороне не может компилировать Lean-код: нет среды и не хватает места, чтобы развернуть из пакетов. Но без машинного доказательства все рассуждения LLM, даже такой сверхмощной, о контрпримере, даже для такой простой задачи, – мне, к сожалению, не очень-то полезны (мой план-то был другим: попытаться вручную из корректного Lean-кода восстановить привычное математическое описание контрпримера).
Казалось бы, всё опять застопорилось.
Но нет. Внезапно Anthropic выпустили Fable 5.1. Буквально, вчера. Якобы, Fable 5.1 “сильно лучше в исследовательских задачах”, чем предыдущая Fable 5. Без особой надежды на успех, попробовал я в том же чате, со сломанным Lean, запустить Fable 5.1. Как ни странно, но оно бодро заявило, что сейчас в коде Lean оставит только те библиотеки (import), которые реально нужны для этого доказательства. Это логично. И, – возможно, – среда Lean c этими библиотеками влезет в доступные гигабайты контейнера на стороне Claude, так предположило Fable 5.1. После чего, как ни странно, действительно “урезало библиотеки” и действительно исправило ошибки в Lean-коде, так что стало понятно, что имеется в виду. В итоге, выдан файл с Lean-кодом, который уже компилируется и корректен со всех точек зрения, кроме того, что там могут быть неверные исходные допущения, но это я планирую проверить позже. Так вот.
(На всякий случай: если код и контрпример окажутся правильными, то, да, это будет решение для 11.115, которая пока что отмечена в тетради как открытая. Задачу я выбрал случайно, а критерием было то, что я сам смогу быстро написать условия на контрпример – поэтому-то и задача выбрана очень простая по формулировке и составу используемых объектов. Да, LLM-системы развиваются. Но тут и контрпример – какой-то подозрительно очевидный; если кому-то интересны супертехнические подробности, то вот: построим подгруппу на словах с чётными и нечётными степенями (это отображение в Z/2Z), и подгруппу на соотношениях с a^2. Код Lean я пока не публикую, поскольку не проверил, да и это всё может оказаться “подтягиванием” другого результата, который просто забыли упомянуть составители сборника.)
Комментировать »
Столкнулся тут с очередной маректинговой уловкой Anthropic. Называется, снова, Guardrails (“Ограждения/ограничения”).
Я уже некоторое время тестирую LLM-системы, чтобы понять, на что они реально годятся в плане “кодинга” (не “вайб”!). В рамках этого процесса я попросил Claude реализовать в программном коде некий, – не самый сложный, – сетевой протокол, интенсивно использующий криптографию. Я не стану приводить детали, они не имеют отношения к теме. И вот, исходя из опыта, я подготовил очень подробное описание и протокола, и программы: “промпт”, всё на английском, как положено. По тому “промпту” система Claude Opus 5 Max, – минут за двадцать-тридцать, то есть, прямо вот очень быстро, – сгенерировала требуемый программный код, больше тысячи эффективных строк (Go, но, опять же, речь не об этом). Не сказать, что код вызывает восхищение, но он, действительно, неплохой, как программный код, и практически идеально оформлен (комментарии, разбивка по файлам и пр.). Это всё необходимо признать.
Но, не будем торопиться. Переходим к маректинговой уловке. В коде, сгенерированном Claude, я нашёл несколько существенных ошибок, пара из которых – это прямые и серьёзные уязвимости. Да, это далеко не самые очевидные ошибки. Как я понимаю, при условии написания качественного и подробного входного “промпта” (на английском!), фокусов с банальными дефектами, – типа, забытой проверки подписи, – в ведущих LLM-системах нынче уже не наблюдается. В Claude (веб-интерфейс) есть режим “ревью кода”, где можно буквально к конкретной строке написать замечание. Что я и сделал: написал подробные замечания к коду, с вариантами исправлений. Обратите внимание: Claude – генерирует код, с нуля, по моему “промпту”; я – нахожу серьёзные ошибки, показываю на них, и прошу исправить.
Что происходит дальше? А дальше система сначала “думает”, потом пишет, что, мол: “хорошее ревью”; “все ошибки отмечены верно”, “я само нашло ещё две, пока разбиралось, как исправить”; “всё признаю, начинаю исправлять”. И потом – всё. Неожиданный финал: вылезает системное сообщение, что сработали “наши ограждения кибербезопасности” (ну, хорошо, “ограничения”, конечно) и система не будет продолжать обрабатывать предлагаемые исправления. “Зарегистрируйтесь в нашей программе по кибербезопасности!”.
То есть, эта штука сперва сама сгенерировала код с уязвимостями, а потом, когда я предложил внести исправления в этот код, заявила, что тут “кибербезопасность” и исправлять, поэтому, отказывается. Но с таким уязвимостями – код использовать нельзя. Заметьте, речь не идёт о создании инструмента для “пентестинга” или о написании утилиты для “фазинга” чужого протокола. Такого нет и близко – реализовывался протокол обмена пакетами данных по сети. Код написан Claude. Реализация содержит конкретные дыры. Исправлять за собой дыры – система упрямо отказывается, упирая на “безопасность”. В чём же здесь безопасность? Загадка. Видимо, в грубом маркетинге: мы сперва что-то сгенерируем, а потом откажемся продолжать поддержку без дополнительной регистрации/оплаты.
А с широко разрекламированной Fable 5 – всё ещё сильно хуже: там эти же “ограждения-барьеры”, в точно таком же контексте исправления дефектов сгенерированного кода, срабатывают вообще едва ли не постоянно; и результат система не выдаёт, но ещё и “кредиты” за использование ресурсов – исправно списывает (в огромном количестве).
Как говорится, кто бы сомневался!
Комментарии (2) »
Вроде, удалось продлить адрес dxdt.blog ещё на один год: учитывая все “странности” – успешность продления вовсе не была очевидной. Вообще, “забавно” было бы потерять ещё и dxdt.blog, куда сайт переехал.
Комментарии (5) »
Секунду координации (leap second) хотят отменить совсем. Одна из основных причин: по мнению Международного бюро мер и весов, есть большой шанс, что к 2035 году придётся вводить “отрицательную” секунду координации. То есть, раньше, для коррекции – секунду координации добавляли. Часы, работающие по “общепринятому” источнику частоты, ждали одну дополнительную секунду в сутках, чтобы их догнали астрономические события, связанные с вращением Земли. Расчётные сутки – удлинялись на секунду. Процесс должен компенсировать “убегание” метрологических источников частоты от представления о вращении Земли, как об историческом источнике понятия о сутках. Ну или наоборот – происходило “опережение”, тут уж как посмотреть: главное, что всегда есть некая накапливаемая разница, а знак её, вроде, не так важен. Ну, пока не возникает та самая “отрицательная” секунда координации.
Вопрос этот и сам по себе весьма спорный – вращение Земли не имеет строго определения, координация зависит от используемых методов подсчёта наблюдаемых событий и т.д., и т.п. Но это всё технические мелочи, по сравненению с тем, что в 2035 году эта же трактовка может привести к тому, что нужно будет реализовать “отрицательную” секунду, то есть, “перевести часы в обратную сторону” и одну секунду удалить из привычной минуты, и из суток. Представьте, что за 23:59:58 следует 00:00:00 следующих суток! Для точных компьютерных систем это выглядит пострашнее “проблемы 2000”. Из календаря исчезает секунда, поэтому, предположим, если где-то встретится TLS-сертификат, начало действия которого обозначено как 23:59:59, но дата приходится на сутки, когда произошла коррекция, то, получается, такого таймстемпа просто не существовало. И это даже посложнее, чем если кто-то написал 23:59:63. В последнем случае, хотя бы, можно заявить о нарушении формата, а вот 23:59:59 – никаких форматов не нарушает. Нарушает ли их 23:59:60, кстати? Отдельный вопрос. Как бы там ни было, но “отрицательную” секунду координации придётся дальше учитывать во всех вычислениях с преобразованием таймстемпов в календарное время. Тут и положительная-то секунда постоянно приводит к неприятностям, что уж там говорить об отрицательной.
Так что, вполне возможно, секунд координации больше не будет, остчёт секундного времени станет “равномерным”, но зато сделают сразу час координации. Ну а что – час? К нему, предположительно, нужно будет вернуться через несколько веков (именно: см. Draft Resolution C). Так-то. Было бы кому возвращаться.
Комментировать »
Как я понимаю, большинство читателей этого блога (dxdt.blog) читают его через RSS-поток. На веб-сраницах трафик тоже есть, – и он заметно больше, – но там, реально, основная часть – это запросы разных ботов, в том числе, LLM-систем. Узел под старым адресом блога, который был в домене .RU, сейчас возвращает универсальный редирект (HTTP 301) на dxdt.blog. Это распространяется и на запросы к RSS-ленте.
И вот смотрю я в логи этого “редиректора” (то есть, на старом адресе dxdt.ru), а там всё ещё немало так GET-запросов именно на RSS-поток. Причём, если верить данным RSS-агрегаторов, которые приходят на старый адрес за RSS, там у них сотни подписчиков. Я вижу, что, после редиректа, эти же RSS-агрегаторы приходят и на dxdt.blog. С одной стороны, неплохо, что они следуют редиректу. Однако, с другой стороны, то, что эти сервисы всё ещё ходят через “редиректор”, означает, что его адрес не был вытеснен новым, а это уже плохо, потому что, как только dxdt.ru будет удалён из DNS, этот трафик, скорее всего, потеряется, а ленты в агрегаторах отломятся.
Да, я вполне понимаю логику массовых сервисов “RSS-читалок”, которую они тут применяют. Естественно, желание сохранять старый адрес, даже если там HTTP 301, вполне разумное: мало ли, что там случилось на целевом веб-узле – администратор мог сделать 301 ненамеренно, по ошибке. То есть, это здравое поведение. Идеальным было бы запоминать новый адрес, полученный через HTTP 301, но переходить на него (исключительно) только после того, как предыдущий адрес совсем исчез. Но не факт, что так сделано. Понятно, что пользователи могут переподписаться с новым адресом – но тут нужно действие от пользователя: лент у пользователя много, ожидать, что он тщательно следит за адресом каждой ленты – слишком самонадеянно.
В общем, это я вот к чему написал: сообщение на dxdt.blog – один из двух доступных мне способов проинформировать читателей о замене адреса. Поэтому напоминаю – я перенёс сайт, теперь вместо dxdt.RU стало dxdt.BLOG, если вы читаете через RSS (а это тоже правильно), то вот новый URL RSS-потока: https://dxdt.blog/feed/
Пока есть возможность, я постараюсь старый адрес сохранять с редиректом. Через какое-то время (когда дойдут руки исправить ссылки внутри сайта) я планирую на dxdt.ru выложить по URL RSS-потока отдельную запись, информирующую о том, что поток переехал на другой адрес. Опять же, это всё – если будет возможность: с доменами .RU происходит какая-то неразбериха, что там ожидать – понять я уже не могу.
Ещё раз новый адрес RSS-потока: https://dxdt.blog/feed/
Спасибо, что читаете.
Comments Off on RSS и старый адрес .RU
Новый