Осталось менее 6 часов до открытия исходников ядра seL4, вместе со всеми доказательствами.
Хотел запилить новость, но стало лень. Пишу в толксы.
Некоторые детали:
Поддерживаемые архитектуры: arm (какая-то плата KZM) и x86_32.
Что доказывали: соответствие сишного кода спецификации. Только для arm. Для самой спецификации не доказывалось ничего. Например, не доказывалось отсутствие дыр в модели безопасности. Так что говорить о том, что доказана «корректность» не совсем правильно.
Чем пожертвовали в угоду простоте доказательства: ядро не преемптивно, smp не поддерживается.
В seL4 используются некоторые интересные идеи, отличающие это ядро от других ядер 4-го поколения, вроде L4ka::Pistachio.
Например, ядро не даёт доступа к физической памяти в том смысле что невозможно узнать куда будет отображена страница. Отсюда, вся работа с железом только с использованием IOMMU.
Также ядро не показывает thread ID. Посылка сообщения осуществляется не с использованием thread ID, а с использованием т.н. endpoing capability. Вообще, capability-based access controll — это краеугольный камень модели безопасности seL4. endpoint capability — это объект, с использованием которого можно посылать и получать сообщения. Сервер ждёт сообщений на своём endpoint-е, а поток, который хочет посылать серверу сообщения должен иметь копию endpoing cap. сервера в своём capability space. Откуда клиент возьмёт endpoint сервера? Либо этот endpoint будет засунут в capability space треда его родителем при конструировании оного capability space, либо клиент получит endpoing capability в каком-то другом сообщении. Механизм IPC позволяет пересылать capabilities в сообщениях. Что делать серверу, чтобы отличать клиентов, если недоступны thread ID? Для этого введена возможность пометок endpoint-ов. Сервер, беря оригинальный enpoint, применяет к нему операцию mint указывая какое-то число. Создаётся т.н. minted endpoint capability. Которую сервер отдаёт клиенту. Далее, когда сервер будет ждать сообщений на своём оригинальном endpoint-е, а клиент пошлёт сообщение через помеченный endpoint, то сервер получит число, которым он метил endpoint в специальном регистре. Конечно, не гарантируется что все запросы с данной пометкой приходят от одного потока, т.к. клиент может копировать свои endpoint-ы и передавать кому-то ещё.
Такая модель, на мой взгляд, имеет много плюсов. Во-первых, в отличие от идентификации по номерам потоков, с одним «соединением» (endpoint-ом) могут работать разные потоки клиента, не спрашивая у сервера отдельно разрешения на подключение для каждого потока, для тех моделей, где перед отправкой сообщений нужен handshake. Также эта модель, по сравнению с моделями где для отправки сообщений нужно знать только thread ID и не нужен handshake, ограничивает возможности совершения DoS-атак.
Взамен smp на x86_32 поддерживается node-based concurrency. Физическая память делится поровну между процессорами (я буду говорить о процессорах, даже если это ядра одного) и каждое ядро ОС выполняется на своём процессоре используя свой кусок физической памяти, как будто оно работает на однопроцессорной машине. Ядра друг о друге не знают ничего и друг с другом не общаются. Единственное, позволяется указать число страниц разделяемой памяти. Ядро ОС предоставляет доступ к т.н. Boot Structure, где сообщает номер процессора (ноды) и ссылки на разделяемые страницы. Гарантируется одинаковый порядок следования разделяемых страниц на всех ядрах. Но что делать с этими разделяемыми страницами — дело userspace-кода. Доступ к оборудованию через IOMMU имеет только boot-процессор.
Я бы много чего ещё мог написать. Заинтересовавшиеся могут обратиться к reference manual-у или спрашивать свои ответы в отдельных сообщениях.
Спасибо.
