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

Предоставленный текст - это страница репозитория GitHub для Catten, ядра экспериментальной операционной системы CharlotteOS. Однако в тексте отсутствует подробное описание самого проекта, его особенностей или технических деталей.

Страница содержит стандартное навигационное меню GitHub, но не включает информацию о целях разработки, используемых технологиях или текущем статусе проекта Catten. Для создания содержательного пересказа требуется более подробное описание проекта.

• Проект Charlotte OS стремится к современной архитектуре, но пока не реализованы драйверы для большинства оборудования, что делает его практически непригодным для ежедневного использования.
• Проект использует GPLv3 с дополнительным разрешением на линковку с проприетарными драйверами, что вызывает споры в сообществе.
• Проект написан на Rust и использует микроядро, что делает его уникальным среди существующих альтернатив.
• Проект не имеет собственной системы портов пакетов и полагается на переносе пакетов из других систем, что может вызвать проблемы.
• Проект не имеет собственной системы портов пакетов и полагается на переносе пакетов из других систем, что может вызвать проблемы.

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

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

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

OWhisper — это «Ollama для распознавания речи»: локальный или облачный STT-сервер, работающий в потоковом и пакетном режимах.

Появился из запросов пользователей Hyprnote «подключить свой STT, как LLM». Подходит для:

• быстрого локального прототипа;
• развёртывания крупных моделей на собственной инфраструктуре.

CLI — для локального запуска, Proxy — для облачных/крупных моделей.

FAQ

• Код: в репозитории Hyprnote (owhisper).
• Лицензия: GPLv3, планируется MIT.

• Пользователи просят стриминговый вывод, headless-режим и поддержку Linux; сборка уже есть, но тестировалась мало.
• Горячо обсуждается speaker diarization: пока нет, но это «на дорожной карте».
• Кто-то указывает, что проект использует внешние API (Deepgram) и не полностью локален, в отличие от Ollama.
• Автор отвечает: OWhisper умеет запускать локальные модели Whisper и Moonshine, работает как прокси к облачным провайдерам и выдаёт совместимый с Deepgram API.
• Поддерживаемые модели перечислены в CLI (owhisper pull --help) и скоро появятся на сайте.

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 из репозиториев и пересмотреть политику мейнтейнеров.