Hacker News Digest

Формальная верификация ПО исторически требовала огромных усилий экспертов: на написание кода ядра seL4 ушло два человеко-года, а на его формальное доказательство — двадцать. Из-за этого метод применяли лишь в критичных системах вроде авионики Airbus. Теперь большие языковые модели меняют расклад: с помощью Claude удалось автономно доказать свойства безопасности на уровне ассемблера (архитектура RISC-V) более чем в 100 реальных открытых библиотеках — по заявлению авторов, это первая крупномасштабная попытка применить ИИ для формальной верификации production-кода на уровне ассемблера.

В частности, доказано, что программы всегда завершаются нормально и не падают при любом вводе объёмом до 64 МБ на многих точках входа фаззинга Google OSS-Fuzz, включая сбои, выявляемые санитайзером ASan. Попутно Claude нашёл баги, годами ускользавшие от обнаружения, несмотря на триллионы прогонов тестов. Авторы честно оговаривают границы: ASan ловит не все ошибки памяти, охвачены не все точки входа, а библиотеку могут неправильно использовать из вызывающего кода — для этого пришлось бы специфицировать требования к каждому публичному вызову.

Вывод: верификация пройдёт путь от «прикрученной сбоку» к встроенной, как статические типы и тестовые фреймворки, и вскоре станет такой же обыденной, как фаззинг.

Тред приводит примеры применения LLM для генерации формальных доказательств, но отмечает ограничения в масштабируемости и скепсис относительно индустриального внедрения. Успешные кейсы: — malisper с помощью LLM доказал эквивалентность 12 % кода PostgreSQL (≈70 k строк C), выявив расхождения в работе с плавающей точкой. — sestep использует агента для создания PR с Rocq-доказательствами, что ускоряет внедрение оптимизаций (SIMD, CUDA). — svcrunch проверил модель авторизации GoodMem через Alloy; red-team атаки не обнаружили уязвимостей. Критика и риски: — Для доверия результатам нужны точные модели RISC-V и процессов Linux, иначе проверка в Coq/Rocq не гарантирует соответствие реальному коду. — woggy, mjorgers и adyavanapalli подчеркивают, что формальная спецификация может не отражать реальное поведение программы. Olscore сравнивает это с проверкой дома по чертежу, который может не соответствовать замыслу. — j16sdiz и braiamp упоминают проекты OpenAI с Lean, где доказательства проходили проверку, но не давали заявленных результатов («псевдодоказательства»). Выводы и советы: — Практические барьеры (объем доказательств, необходимость ручного ревью) сохраняются. — usernametaken29 советует использовать LLM для сокращения кода, чтобы облегчить его формализацию. — passive и zeroeyz полагают, что автоматизация лишь снижает порог входа в fuzzing, но не решает базовых проблем верификации.

Выпуск Zig 0.17.0 стал результатом пяти месяцев работы 206 участников и 925 коммитов. Ключевое улучшение — переработка системы сборки с внедрением Build Server Protocol, что упрощает интеграцию с IDE и ускоряет разработку. ELF-линкер значительно улучшен, что делает инкрементальную компиляцию надёжной для всех пользователей на x86_64-linux. Обновлён уровень поддержки платформ: добавлен Tier 1 для Windows на ARM64, расширена поддержка Linux на RISC-V и улучшена работа на macOS. В языке удалён синтаксис умножения массивов, добавлены функции @bitCast с улучшенной безопасностью, @divCeil для точного округления вверх, @backingInt и @fromBackingInt для работы с перечислимыми типами, а также @SpirvType для Vulkan-разработки. Грамматика языка теперь формально специфицирована и протестирована фаззингом, что повышает надёжность парсинга. Перевод C-кода вынесен во внешний пакет, упрощая основной инструментарий. Zig остаётся ориентированным на создание надёжного, производительного и переиспользуемого кода, а развитие финансируется через Zig Software Foundation. Поддержка проекта через пожертвования помогает ускорить путь к версии 1.0.

Zig 0.17.0 — значительный шаг вперёд в интеграции с IDE и стабильности сборки благодаря Build Server Protocol и улучшенному ELF-линкеру, подтверждённому практическим опытом. Однако остаются споры: жёсткая политика против ИИ в репозитории критикуется за баны за личные проекты, хотя команда утверждает, что блокировки касаются только официальных пространств и могут быть ошибочными. Нестабильность сборок из-за изменений в build.zig между версиями признаётся, но некоторые считают её неизлемой ценой быстрого развития. Zig называют наиболее продуманным языком для человека по сравнению с C, Go и Haskell, несмотря на малую экосистему. Поддержка целевых платформ остаётся сильной стороной, сравнимой с C, особенно для SPIR-V и WebGPU. Векторизация циклов по-прежнему отключена из-за сложностей с LLVM, что разочаровывает разработчиков численных задач. Поддержка io_uring отсутствует в 0.17.0 — команда отказалась от реализации на последнем этапе, вызывая недовольство у тех, кто нуждается в асинхронном вводе-выводе. Несмотря на официальную политику против ИИ, Zig привлекателен для LLM-ассистированных задач из-за хорошей поддаче генерации и анализу кода. Пользователи советуют избегать слишком новых релизов в продакшене из-за риска поломки build.zig, рекомендуя фиксировать зависимости или использовать стабильные версии. Баны за ИИ часто ошибочны — рекомендуется обращаться в команду по email. Сообщество видит Zig как «живой» язык с быстрыми изменениями и энтузиазмом, похожим на ранние Node.js или ES6, привлекающим тех, кто готов к нестабильности. Сомнения в достижении 1.0 до 2028 года coexist с надеждой, что стабилизация IR и работа над проверкой жизненного цикла памяти могут ускорить релиз.

Попытка запустить Linux на Mac mini с чипом M4 столкнулась с неожиданными трудностями из-за новой технологии SPTM — механизма защиты, который блокирует прямой доступ к аппаратным ресурсам, использовавшийся в ранних версиях Asahi Linux. В отличие от M1–M3, где можно было анализировать MMIO-трафик macOS, здесь требовалась глубокая модификация гипервизора m1n1, что вышло за рамки возможностей новичка. Однако автору удалось обойти проблему: отключив строгую безопасность загрузки, установив m1n1 через восстановление macOS и получив доступ к последовательному порту, он начал эксперименты с загрузкой ядра.

Первым барьером оказался заблокированный GXF — компонент, отвечающий за безопасность исключений, который на M4 отключён в режиме raw boot. Затем выяснилось, что регистр RVBAR, задающий точку входа для ядра, уже содержит корректное значение — попытки его перезаписать вызывали сбой. После долгого перерыва автор добился первого вывода через debug_putc, внедрив минимальное устройство дерева и включив earlycon. Ключевым прорывом стало обнаружение, что процессоры M4 теряют состояние при выполнении команды WFI (Wait For Interrupt), что приводило к зависанию. Исправление потребовало патча для m1n1 и ядра Linux, отключающего WFI в ранней стадии загрузки — после этого система начала выводить логи, и Linux наконец заработал.

Преимущества Apple‐устройств связаны с вертикальной интеграцией и оптимизацией аппаратного и программного обеспечения, а не только с более мощными характеристиками. Открытое железо вряд ли существенно изменит финансовый масштаб компании из‐за её огромного объёма продаж — даже если все желающие Linux‐пользователи купят самые дорогие Mac, это не окажет заметного влияния на доходы. Дискуссия о целесообразности открытости аппаратной части продолжается: одни считают, что это расширит рынок, другие уверены, что Apple намеренно продаёт только готовый пакет и не получит выгоды от открытости. Поддержка Linux на Mac остаётся сложной из‐за закрытых протоколов, в частности трекпада, хотя качество сенсора и тактильной отдачи остаётся ключевым фактором превосходства. Для запуска Linux рекомендуется поддерживать проекты вроде Asahi Linux и OEM‐производителей, работающих над драйверами и портами. Обратное проектирование чипов M4 и M6 активно использует инструменты искусственного интеллекта, ускоряя анализ и разработку драйверов.

ESP32-S31 от Espressif — это микроконтроллер с набором периферии, характерным для одноплатных компьютеров: гигабитный Ethernet MAC через RGMII, USB 2.0 High-Speed OTG хост, два слота SDIO, DVP-интерфейс для камеры, параллельный LCD-контроллер до 24-бит RGB, два I2S с синхронизацией Bluetooth-аудио, 14 ёмкостных сенсорных каналов, CAN FD и четыре блока MCPWM. На борту — два 320 МГц RISC-V ядра с FPU и 128-битным SIMD на одном из них, плюс отдельный 40 МГц низкопотребляющий ядро. Каждое основное ядро имеет 32 КБ L1-и кэша и делит 64 КБ данных кэша. Поддерживается до 64 МБ PSRAM через 250 МГц 8-бит DDR интерфейс и до 256 МБ флеш-памяти — значительный шаг вперёд по сравнению с ESP32-S3, где PSRAM и флеш делили шину.

Ключевое нововведение — настоящий MMU с виртуальной памятью и защитой, в отличие от упрощённой адресной трансляции в предыдущих моделях, что делает возможным запуск Linux. Несмотря на то, что datasheet ещё предварительный (версия 0.5) и содержит неточности (например, указана 80 МГц для PSRAM вместо реальных 250 МГц), энтузиасты уже получают рабочее Linux-окружение на ESP32-S31. Хотя запуск полноценного рабочего стола из-за ограниченной памяти пока невозможен, терминал и базовые утилиты работают без особых сложностей. Это первый шаг к тому, что ESP32 может со временем стать реальной альтернативой Raspberry Pi в сценариях, где важны низкое энергопотребление, встроенная беспроводная связь (Wi-Fi 6, Bluetooth 5.4, 802.15.4) и богатая периферия, даже если пока это остаётся скорее экспериментальной платформой.

ESP32-S31 с Linux может заменить SBC в IoT-задачах, но для критичных по задержкам задач (аудио, реальное время) FreeRTOS остаётся эффективнее из-за отсутствия предemption и меньшего оверхеда. Спор: Linux не может быть эффективнее firmware-блоха из-за предemption, но даёт готовые, тестируемые стеки сети и драйверов, критичные для IoT-устройств. Linux на ESP32 полезен не для производительности, а для упрощения портирования ПО и использования готовых решений (wpa_supplicant, USB-стек). XIP для RISC-V в Linux 7.1+ удалён, что усложняет запуск Linux на устройствах с 8 МБ RAM — Espressif использует ядро 6.18. Опыт на ESP32-P4: даже с 1 МБ flash и неиспользуемой PSRAM можно реализовать сложный TUI, фильтры звука и USB-устройства без джиттера — это невозможно на Linux. Разница между MCU и SBC стирается: ESP32-S31 с MMU и 16 МБ PSRAM конкурирует с SBC по функциональности, но не по энергопотреблению и предсказуемости. Цена модуля ESP32-S3 с 16 МБ NOR и 8 МБ PSRAM — $3.5 за 500+ шт., альтернатива Raspberry Pi для массового производства. Linux на ESP32 не подходит для экстремально ограниченных устройств — RTOS (Zephyr, FreeRTOS) и NetBSD предпочтительнее при отсутствии MMU или малом RAM. Для задач с камерой и AI (YOLO) ESP32-S31 недостаточен — требуется интеграция с ускорителями (Grove Vision AI). ESP32-S31 с периферией (RGMII, USB HS, DVP, I2S) подходит для эмуляции старых систем (ZX Spectrum, 386). Несмотря на мощность, ESP32-S31 остаётся 2.4 ГГц Wi-Fi — ограничение для современных сетевых приложений. Разнообразие моделей ESP32 (P4, S3, S31) затрудняет понимание доступных возможностей — нельзя полагаться на общее упоминание «ESP32». Для проектов с Python/Lua: SolarOS — альтернатива Linux, позволяющая разрабатывать на скриптовых языках без полной ОС. Linux на ESP32 не заменяет RTOS в задачах с жёсткими требованиями к детерминизму — назначение ядер RT-процессами не устраняет оверхед многопользовательской ОС. ESP32-S31 с MMU открывает путь к полноценным ОС, но выбор между RTOS и Linux должен основываться на требуемой функциональности, а не на мощности. Для домашнего сервера с высокой пропускной способностью ESP32-S31 не подходит — нужны NVMe, DDR4/DDR5, 2.5G Ethernet и NPU, выходящие за рамки его архитектуры.

Главная мысль: RISC‑V захватывает рынок дешёвых микроконтроллеров не благодаря изысканной схеме команд, а потому, что открытый набор инструкций позволяет выпускать чипы по 10 ¢, а открытый инструментарий делает их доступными даже в отдалённых регионах.

Ключевые детали: компрессированные store‑offsets и отдельный Zicsr‑модуль действительно вызывают неудобства, но они лишь часть более широкой проблемы — отсутствие массового доступа к недорогим разработчикам. Для большинства стран «третьего мира» цена и логистика важнее эстетики ISA; один‑долларовый чип с бесплатной доставкой меняет правила игры, позволяя студентам и малым компаниям создавать собственные устройства.

Запомните: RISC‑V меняет Embedded‑пространство не за счёт «красивого» кода, а благодаря своей открытости, доступности и способности дать каждому шанс «зажечь» свой собственный транзисторный эксперимент.

Тред дополняет статью опытом эксплуатации и оспаривает утверждения о стоимости и доступности RISC-V. Автор @ndiddy отмечает, что оригинальная статья говорит о невозможности RISC-V конкурировать с ARM64, а ответ — о его пригодности для дешёвых микроконтроллеров — это разные темы. @kelnos сомневается, как RISC-V может быть дешевле в регионах с высокой стоимостью доставки, ведь она не зависит от типа чипа. @vlovich123 подтверждает: разница в 10 центов против доллара незначительна при доминирующей стоимости доставки. @HawtAds опровергает: в Нигерии и Бангладеш доставка не так дорога, как утверждается. @strenholme предполагает, что в будущем RISC-V может достигнуть или превзойти производительность ARM и x86_64, исходя из исторических тенденций.

RISC-V обещает захватить рынок недорогих микроконтроллеров, но не благодаря продуманному дизайну, а вопреки его недостаткам. Главная проблема — попытка универсального решения: одни требования предъявляются к суперкомпьютерам, другие — к дешёвым ядрам, где важны размер и задержка прерываний, а не производительность вычислений. Автор подчёркивает, что даже если RISC-V победит у 8051, это произойдёт лишь потому, что рынок микроконтроллеров требует простого, дешевого решения, а не потому что ISA идеально подходит.

В статье также критикуются «непрактичные» решения: излишняя сложность спецификации, отсутствие реального опыта разработчиков и «дизайн по комитету», где реальные пользователи остаются в стороне. Автор сравнивает это с ошибками ARM, где указание ядра недостаточно, а поставщикам операционных систем приходится адаптировать образы под бесчисленные платформы. Кроме того, упомянута неудача с векторным расширением — лучше использовать фиксированную ширину SIMD, как в традиционных решениях. Эти пункты подчеркивают, что RISC-V часто упускает из виду реальные инженерные ограничения в пользу теоретических возможностей.

RISC-V не идеален — у него есть недостатки, включая сложность из-за избыточности опций, что может вызывать проблемы с совместимостью и поддержкой. Однако его открытость и гибкость делают его привлекательным для разработчиков. Опыт @jacksons5f подтверждает: RISC-V можно успешно применять в продакшене. Несмотря на критику, экосистема активно развивается, а архитектура доказывает работоспособность в разных средах.

Платформенный процессор, система управления режимом SMM, C6‑DRAM и микрокод процессора можно «разблокировать», перепрограммируя переводы физических адресов DRAM.
skitter-creek-bath-salts вмешивается в нижние уровни иерархии памяти, переписывая регистры контроллера DRAM, чтобы любой виртуальный адрес *p мог указывать в произвольное место физической памяти. При разрушении адресных преобразований исчезают и защита, построенная на них: SEV, SGX, TDX, TrustZone, pKVM, CoVE, SMRAM и даже скрытые регионы PSP и ME становятся доступными.

Эксперимент проведён на процессорах AMD Family 16h, где документация раскрывает регистры переводов, позволяющие менять маппинг без блокировки. Техника универсальна: схожие схемы переплетения, перемешивания и переключения используют все современные контроллеры памяти — от x86 до ARM и RISC‑V. Таким образом, «разблокировка» DRAM открывает путь к новым атакам и исследованиям, показывая, что даже самые защищённые области DRAM можно обойти, если знать, как «перепутать» их адресацию.

Тред обсуждает потенциальные последствия и ограничения эксплуатации подобных атак. Эксперты расходятся во мнениях: одни считают, что атаки могут обходить традиционные механизмы безопасности, другие — что современные системы уже их предотвращают. По опыту @zahlman, атаки возможны лишь при наличии root-доступа. @creshal утверждает, что они позволяют получить доступ к ранее недоступным областям системы. Эксперты советуют ограничивать доступ к таким возможностям только владельцам систем и действовать с осторожностью, учитывая риски для безопасности.

В предоставленном тексте отсутствует основное содержимое репозитория GitHub "jackdoe/pico2-swd-riscv", представлено только навигационное меню сайта. Судя по названию проекта, вероятно, это реализация интерфейса отладки SWD (Serial Wire Debug) для платформы на базе RISC-V, возможно, связанная с Raspberry Pi Pico 2. Однако без доступа к файлам проекта, README или описанию невозможно дать точное резюме.

Для создания качественного пересказа необходима информация о содержимом репозитория: описание проекта, схемы, исходный код, документация или обсуждения. Пожалуйста, предоставьте основное содержимое страницы проекта, и я подготовлю точное и ёмкое резюме в соответствии с вашими требованиями.

• Разработчики признают, что LLM-генерированный код лишает их ощущения «собственного» кода и ментальной модели, но считают это неизбежной ценой прогресса.
• Сообщество HN в очередной раз поднимает тему «вайб-кодинга» как симптома упадка ремесла и утраты смысла.
• В то же время, авторы поста отмечают, что даже при полном отказе от написания кода в пользу LLM, остаётся необходимость владеть базовыми навыками для верификации и рефакторинга.
• Обсуждение выходит за рамки самого феномена: участники затрагивают вопросы авторского права, лицензий и ответственности за сгенерированный код, а также то, как далеко может зайти эта тенденция.

Ironclad — это формально верифицируемый, реального времени, UNIX-подобный ядро операционной системы общего назначения и встраиваемых систем, написанное на SPARK и Ada. Проект полностью свободный и распространяется под лицензией GPLv3. Ключевые особенности включают POSIX-совместимый интерфейс, одновременное вытесняющее многозадачность, обязательный контроль доступа (MAC) и поддержку жёсткого реального времени.

Главное преимущество Ironclad — формальная верификация с помощью SPARK для критических компонентов, таких как криптография и MAC. Система полностью портативна и зависит только от GNU toolchain, что упрощает кросс-компиляцию. Проект поддерживает дистрибутивы для всех доступных архитектур, наиболее заметный из которых — Gloire. Ironclad всегда будет бесплатным для использования, изучения и модификации, а финансируется за счёт пожертвований и грантов от NLnet и Европейской комиссии.

• Участники сомневаются в степени формальной верификации Ironclad, сравнивая его с более строгими аналогами вроде seL4 и Tock, и указывают на отсутствие доказательства ключевых свойств ядра.
• Проект написан на SPARK и Ada, поддерживает x86_64 и RISC-V, но не ARM64; его лицензия включает бесплатную версию с возможностью коммерческого использования.
• Основные альтернативы: seL4 (быстрый и строго верифицируемый), Genode (POSIX-совместимый слой), Asterinas и Redox (Linux-совместимые ядра), а также ReactOS и SerenityOS.
• Критика включает медленную производительность по сравнению с seL4, отсутствие capability-based безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.

32-битные системы устарели, но ядро всё ещё их поддерживает из-за старого «железа» и ПО.
Arnd Bergmann: новые продукты уже 20 лет выходят на 64-битных платформах; встраиваемые устройства постепенно переходят с armv7 (32-бит) на armv8 (64-бит).

• Arm: 90 % встраиваемых систем; лишь три старые архитектуры до-armv7 ещё можно купить, но ядро держит десяток выведенных из производства. Поддержку можно выбрасывать «по половинам», когда исчезнут пользователи.
• Другие 32-битные архитектуры (arc, microblaze, nios2, openrisc, rv32, sparc/leon, xtensa) вытесняются RISC-V.
• nommu (armv7-m, m68k, superh, xtensa) никто не выпускает, их держат лишь ради существующих систем.

Для несовместимых 32-битных приложений — запуск 32-битного userspace на 64-битном ядре: экономит память, не требует 32-битного ядра.

Боль разработчиков:

• Высокая память (highmem) усложняет mm-подсистему; нужна, когда физической памяти > ~800 МБ.
• Ядро пока держит 32-битные машины до 16 ГБ, но таких почти нет; 4 ГБ встречаются (Chromebook), 2 ГБ — чаще, но «глупо»: память дороже CPU.

• Участники обеспокоены удалением поддержки nommu/32-бит: это уменьшает свободу, лишает возможности запускать Linux на старом или простом железе и делает ядро похожим на «дорожную карту» Apple/Windows.
• Некоторые предлагают форк «Linux Legacy» или переход на NetBSD/OpenBSD, которые по-прежнему поддерживают старые архитектуры.
• Для встраиваемых устройств без MMU считают более подходящими Zephyr, NuttX или Contiki, а не полноценный Linux.
• Поддержка big-endian почти мертва, но сохранится, пока IBM вкладывается в s390x.
• Старые ядра и LTS-дистрибутивы ещё десятилетие обеспечат безопасность и работу выброшенного железа.

Почему я перешёл на MiniPC

Пару лет экспериментов убедили: это моё будущее.

Плюсы

• Цена и заменяемость
  Заводская сборка и масштаб снижают цену. Поломки редки: нет вентиляторов, низкая температура, медленный износ.

• Компактность
  Прячется за ТВ, помещается на ладонь, легко переносится.

• Энергоэффективность
  20–50 Вт под нагрузкой, 6–12 Вт в idle. Для 24/7-сервисов выгодно и экологично. ARM/RISC-V обещают ещё меньше энергии.

• Специализация
  Один тип MiniPC не универсален, но набор из разных закрывает все задачи:

  • обычные — офис/браузер;
  • 4–6 LAN-портов — роутер, фаервол, VPN;
  • 4–6 M.2 — компактный NAS (до 20 ТБ);
  • мощный — хост контейнеров и «облако»;
  • Mac mini — macOS без отказа от Linux.

• Простота сборки
  «Монолит» из одного большого ПК требует редкой материнки, кучи PCI-устройств, корпуса с отсеками, сложной логистики и возвратов. Несколько MiniPC решают то же быстрее и дешевле.

• Участники активно обсуждают, как Mini-PC стали «новыми домашними серверами»: дешёвые, экономные (6–50 Вт), легко кластеруются под Proxmox/K8s и заменяют дорогое «энтерпрайз» железо.
• Популярны бывшие корпоративные NUC/HP/Lenovo и китайские 5560U/16 ГБ за $200–300; их ставят за TV, в туалет, за лазер, за StepMania — «дешевле, чем облако».
• Главные боли: шум (особенно в «геймерских» версиях), неремонтопригодность (паяная RAM/CPU, кастомные кулеры), высокий процент брака дешёвых китайцев и отсутствие апгрейдов.
• Мечтают о «тихом Mac-mini-размере» с RTX 4060/780M для игр, но физика (300 Вт TDP) и цена (~$2000) пока не позволяют; вариант — ПК в соседней комнате + длинный кабель/KVM.
• Valve, по мнению многих, была права с идеей Steam Machine, но рано и промахнулась в Linux-играх; новая попытка в 3–5 лет, возможно, совместит Proton, Mini-PC и приставочную форму.