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

В 1980 году выпускники Университета Ватерлоо Гордон Белл и Дэн Додж основали Quantum Software Systems и начали разработку операционной системы QUNIX (позже переименованной в QNX). Их вдохновил опыт работы с Thoth — реальной ОС с синхронной передачей сообщений, написанной на высокоуровневых языках. Первая версия QUNIX 0.1 работала на самосборном компьютере с процессором Motorola 6809, а с появлением IBM PC в 1981 году они адаптировали систему под эту платформу.

QUNIX сочетала черты UNIX и CP/M: вместо стандартных каталогов вроде /bin использовались /cmds, /config, /sys. Команды отличались — например, help вместо man, task вместо ps. Это была первая микроядерная ОС для PC, ориентированная на надёжность в промышленных и коммуникационных системах. Интересная деталь: в ранних маркетинговых материалах график на мониторе был физически приклеен из-за отсутствия инструментов редактирования фото.

• Участники делятся личным опытом использования QNX в образовании (компьютеры ICON), робототехнике, на BlackBerry и в различных встраиваемых системах, отмечая её надёжность и элегантность.
• Многие вспоминают впечатляющую малую занимаемую память QNX и её демо-версию на дискетах, которая включала полноценную ОС с графическим интерфейсом и сетью.
• Обсуждаются сильные стороны ОС: изоляция процессов, реальное время и сетевая прозрачность, но также отмечаются недостатки, такие как накладные расходы на передачу сообщений.
• Упоминается использование QNX в индустрии (автомобильные инфотейнмент-системы VW/Audi, Skytrain в Ванкувере) и её влияние на дальнейшую карьеру в IT.
• Высказывается сожаление о упадке платформы и интерес к возможному открытию её исходного кода, а также ностальгия по эстетике интерфейса Photon.