Разработка операционной системы — задача, требующая глубоких знаний и опыта не только в программировании, но и в архитектуре компьютерных систем. Особое место занимают системы, создаваемые с упором на безопасность, надежность и формальную верификацию. CuBit представляет собой инновационный проект операционной системы общего назначения, написанной с использованием языка SPARK/Ada, который гарантирует высокий уровень надежности и безопасности за счет применения формальных методов доказательства отсутствия ошибок на этапе компиляции. Идея создания CuBit родилась из желания реализовать ОС, сочетающую возможности бытовых операционных систем с серьезными требованиями по безопасности, а также простотой кода, понятного и удобного для развития и поддержки. В отличие от популярных проектов вроде microkernel SeL4 или Muen separation kernel, которые ориентированы на хардкорную формальную верификацию микрокernel, CuBit планируется как полноценная многозадачная операционная система общего назначения.
Применение SPARK — подмножества языка Ada с полными возможностями формальной проверки — позволяет в значительной мере исключить класс ошибок, таких как выход за границы массива, арифметические переполнения и прочие ошибки времени выполнения, на момент компиляции. Это очень важно для системного программирования, где ошибки подобного рода могут привести к серьезным проблемам безопасности и отказам в работе. CuBit функционирует в 64-битном режиме на архитектуре x86-64, поддерживает запуск на нескольких ядрах вплоть до 128 логических процессоров и использует приоритетную предвосходящую многозадачность. Для адресации памяти реализованы виртуальные и физические менеджеры памяти, что обеспечивает гибкое управление ресурсами и способствует адаптации под разные аппаратные платформы. Хотя файловые системы и виртуальная файловая система (VFS) находятся еще в стадии разработки, проект постепенно движется к созданию полнофункционального ядра, способного поддерживать современные требования.
Одним из сложных и интересных аспектов разработки CuBit стало ограничение использования стандартных возможностей языка Ada, которые не подходят для системного программирования без загрузки дополнительного времени выполнения. Для этого в проекте применяется специальный набор директив компилятора, отключающих проверку выходов за границы и переполнений, а также запрещающих работу с плавающей точкой. Последнее связано как с техническими сложностями инициализации FPU, так и с оптимизацией скорости выполнения и минимизацией накладных расходов при переключении контекста между процессами. Дополнительно, по умолчанию отключается использование SSE-инструкций, которые могут быть непредсказуемы в исполнении и вызывать аппаратные исключения, если не инициализированы должным образом. Код ядра CuBit частично требует интеграции с ассемблерными вставками.
Для сборки используется ассемблер yasm с синтаксисом Intel, что удобно и понятно разработчику, предпочитающему данный стиль. В ядре реализованы функции для доступа к моделно-специфическим регистра, например, чтение MSR, которые необходимы для низкоуровневой настройки процессорных элементов и аппаратных функций. Чтобы сохранить возможности формальной верификации, вся ассемблерная часть выносится из SPARK-кода, поддерживая только спецификации контрактов в заголовках. Процесс линковки и загрузки ядра устроен таким образом, что объектный файл ядра представляет собой ELF-файл со стандартными секциями, однако с точным указанием физических и виртуальных адресов с помощью linker script. Ядро загружается в область верхних 2 гигабайт адресного пространства, чтобы избежать конфликтов с пользовательским пространством и упростить адресацию.
Стартовый код для дополнительных процессоров (AP) располагается в первых 64 килобайтах памяти в отдельной секции, обеспечивая возможность перехода от реал-мода к защищённому 64-битному режиму. Управление памятью построено на строго выверенных принятых решениях. CuBit сочетает два способа аллокации физической памяти – BootAllocator, представляющий собой статический битовый контейнер для начальной загрузки, а также BuddyAllocator — дружественный к фрагментации алгоритм, основанный на списках свободных блоков с размером степеней двойки. Несмотря на то, что использование циркулярных связанных списков и наложение структур данных на физическую память усложняют формальную проверку, это компромисс между практичностью и строгостью верификации, который обеспечивает высокую производительность и гибкость работы с памятью. Для динамического выделения объектов реализован SlabAllocator, который работает по принципу кучи фиксированного размера с быстрой работой за счет выделения и освобождения памяти из головы свободного списка.
Особенность состоит в поддержке GNAT-примитивов для простого хранения (Simple_Storage_Pool), что позволяет использовать привычный синтаксис new для создания объектов с минимальными накладными расходами времени выполнения и памяти. Этот механизм, пока еще экспериментальный, открывает перспективы для использования расширенных языковых конструкций, таких как tagged records и controlled types, в самом ядре операционной системы. Отдельное внимание уделено организации многоядерной архитектуры. Каждому ядру выделяется собственный стек фиксированного размера, разделенный на основную часть и вторичный стек Ada. Вторичный стек предназначен для поддержания специфичных для человека языковых конструкций и обеспечивается из общей области памяти.
Для идентификации текущего ядра и связи с его данными используется сегмент GS, что широко применяется в разработки ОС и драйверов. При запуске дополнительных процессоров их стеки инициализируются особым стартовым кодом, размещенным низко в памяти специально выделенной секцией. Планирование задач на текущем этапе представляет собой базовый round-robin со переключением контекста через сохранение и восстановление регистров процессора. Хотя эта часть ядра еще далека от совершенства, важным является тот факт, что концептуально реализован рабочий мультипроцессорный планировщик, способный развиваться и масштабироваться. При этом остается нерешенным вопрос моделирования пользовательских процессов с сохранением формальных свойств и доказательств корректности, что является сложной проблемой современной операционной системы для многопоточного окружения.
Особенность CuBit заключается в том, что разработчик не стремится создать клон Unix или Linux с полностью формальной проверкой. Вместо этого проект черпает вдохновение из разнообразных ОС — от легковесных встраиваемых систем, таких как Xinu и QNX, до крупных систем, включая BSD, Linux, Windows и VMS. Такой подход позволяет сохранять фокус на надежности, безопасности и практичности, не теряя гибкости архитектуры для будущего расширения и адаптации к требованиям современного программного обеспечения. Ни один проект операционной системы не обходится без обширной работы с документацией и поддержкой сообщества. Создатель CuBit придает большое значение полноте описаний кода и простоте участия новых разработчиков, чтобы привлечь внимание других профессионалов к развитию проекта.
Кодовая база открыта и доступна на GitHub, что особенно важно для роста и расширения функционала проекта. На сегодняшний день CuBit находится на ранней стадии разработки, однако он уже демонстрирует множество перспективных решений и интересных инженерных находок. Его применение языка SPARK/Ada для создания ОС открывает новые горизонты в области систем с повышенными требованиями к безопасности и формальному доказательству корректности. Такой подход перспективен для использования в авиационных, военных, финансовых и других критически важных направлениях, где целостность и предсказуемость работы на уровне ядра чрезвычайно важны. CuBit — пример того, как эволюция технологий и использование современных формальных методов позволяют создавать качественное стабильное программное обеспечение с высокой степенью доверия.
