Hacker News Digest

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 безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.

F-Droid уже 15 лет предоставляет безопасный каталог свободных приложений для Android, проверяя исходный код на отсутствие скрытых функций вроде трекеров и рекламы. Каждое приложение собирается из открытого кода и подписывается, гарантируя прозрачность и защиту от вмешательства. В отличие от коммерческих магазинов, где распространены шпионские программы, F-Droid обеспечивает конфиденциальность — например, погодные приложения не передают данные брокерам.

Новая политика Google требует от разработчиков централизованной регистрации с оплатой, верификацией личности и привязкой идентификаторов приложений. Это угрожает существованию F-Droid, который не может ни принудить авторов к регистрации, ни присвоить их идентификаторы. Реализация правил лишит пользователей тысяч проверенных приложений и подорвет доверие к открытому ПО.

• Участники выражают серьёзную озабоченность новыми правилами Google, которые угрожают существованию независимых магазинов приложений, таких как F-Droid, и возможности сторонней установки (sideloading).
• Многие видят в этом шаге конец открытости Android, усиление контроля корпораций над пользователями и потенциальную угрозу цифровым свободам, включая развитие открытого ПО.
• Обсуждаются возможные последствия: уход разработчиков с платформы, необходимость перехода на альтернативные ОС (например, GrapheneOS, PureOS), а также потенциальные конфликты с лицензиями вроде GPLv3.
• Высказывается мнение, что проблема требует законодательного решения на уровне государств (особенно ЕС) для защиты права пользователей запускать любое ПО на своих устройствах.
• Некоторые видят выход в развитии прогрессивных веб-приложений (PWA) и мобильных версий Linux как альтернативы закрытым экосистемам.

StarDict — кроссплатформенный словарь GPLv3 — при работе в X11 по умолчанию пересылает выделенный пользователем текст по нешифрованному HTTP на два китайских сервиса: YouDao и dict.cn.

Проблема обнаружена Винсентом Лефевром 4 августа 2025 года при подготовке к Debian 13. Пакет stardict-plugin, который ставится автоматически, содержит плагин YouDao. Функция «scan» (включена по умолчанию) отслеживает выделение мышью и отправляет текст на серверы без шифрования.

На Wayland уязвимости нет: система блокирует чтение чужих выделений, но и «scan» не работает.

Сопровождающий Debian Сяо Шэн Вэнь считает поведение допустимым: функции можно отключить. Лефевр возражает: конфиденциальные возможности не должны быть активны по умолчанию.

Описание пакета упоминает «scan», но не говорит, что YouDao — онлайн-сервис. Сяо предложил вынести сетевые плагины в отдельный пакет, но сомневается в необходимости.

Аналогичные проблемы сообщались в 2009 и 2015 годах; тогда отключили сетевые словари по умолчанию, но плагин YouDao (добавлен в 2016) игнорирует эту настройку.

• Пакет StarDict по умолчанию отправляет выделенный текст на китайские серверы по нешифрованному HTTP.
• Мейнтейнер Debian отмахнулся: «в описании пакета всё написано, RTFM».
• Пользователи возмущены: словарь можно было сделать полностью локальным (≈ 400 МБ), а поведение — опциональным.
• Уязвимость годами игнорировалась, баг-репорты закрывались как «небаг».
• Сообщество требует исключить StarDict из репозиториев и пересмотреть политику мейнтейнеров.