После завершения доказательств функциональной корректности и целостности, компания Proofcraft установила доказательство того, что seL4 обеспечивает конфиденциальность на архитектуре AArch64 — формальное математическое доказательство того, что ядро не позволяет приложению, работающему поверх seL4, получать информацию без соответствующей авторизации.
Благодаря продолжающейся поддержке со стороны NCSC (Национального центра кибербезопасности Великобритании), этот результат завершает формальное доказательство того, что код реализации seL4 на AArch64 обеспечивает изоляцию безопасности приложений, работающих поверх ядра (при условиях, перечисленных здесь). Такая изоляция предотвращает распространение атак с некритичных приложений на критичные и их компрометацию.
Инженерия доказательств и теория на LICS'26
Статья The Algebra of Iterative Constructions авторства Кевина Батца, Бенджамина Люсьена Каминского, Лукаса Керера, Гервина Кляйна, Хеннинга Урбата и Тодда Шмида была представлена на 41-м ежегодном симпозиуме по логике в информатике (LICS) в Лиссабоне. Работа посвящена теоретической информатике — алгебраической абстракции и принципам рассуждения для итеративного построения неподвижных точек. Неподвижные точки — сквозная тема в информатике, с которой связаны такие известные результаты, как теорема Клини о неподвижной точке. Предложенная в статье алгебра позволяет формулировать подобные теоремы компактно и рассуждать о них абстрактно и упорядоченно, что можно эффективно реализовать в системах доказательства теорем вроде Isabelle/HOL — той самой, которую Proofcraft использует для верификации микроядра seL4.
Высоко автоматизированная реализация алгебры итераций в Isabelle/HOL, описанная в статье, стала результатом спонтанного сотрудничества главного научного сотрудника Proofcraft Гервина Кляйна и Бенджамина Каминского, начавшегося на встрече рабочей группы IFIP 2.3 (Programming Methodology) в Афинах в 2025 году. Этот пример показывает, что инженерия доказательств охватывает диапазон от прикладных задач до глубокой теории.
MCS-конфигурация seL4 верифицирована (для RISC-V)
Proofcraft достигла значимого этапа в дорожной карте верификации seL4, над которым работа велась годами: MCS-конфигурация seL4, обеспечивающая поддержку систем со смешанной критичностью, теперь доказанно корректна на архитектуре RISC-V.
Эта конфигурация — крупнейшая новая функция seL4, незаменимая для приложений реального времени со смешанной критичностью, например в автомобильной отрасли. Она включает масштабные изменения в реализации ядра и его API, поэтому верификация потребовала значительных усилий и долгое время оставалась приоритетом дорожной карты seL4.
Впервые завершена верификация функциональной корректности для seL4 с MCS. Функциональная корректность — крупнейшее и центральное доказательство в стеке верификации seL4. Доказательство ориентировано на архитектуру RISC-V и в дальнейшем будет перенесено на 64-битную архитектуру Arm в рамках программы DARPA PROVERS.
Динамический планировщик доменов для seL4
Proofcraft реализовала и формально доказала корректность более гибкого планирования доменов в seL4.
До этого изменения доказательства безопасности seL4, в частности доказательство соблюдения границ информационных потоков, требовали полностью статического расписания, компилируемого прямо в ядро. Это означало, что при использовании seL4 для контроля информационных потоков между приложениями разработчикам приходилось задавать фиксированный, заранее определённый объём времени для каждого домена на весь срок работы системы. Такая жёсткая политика затрудняла практическое применение контроля информационных потоков и поддержку SDK-подобной разработки, например с Microkit.
Proofcraft предложила новый runtime API seL4, позволяющий загружать полустатические расписания доменов. Это значит, что система с защитой информационных потоков может проходить разные фазы работы во время выполнения, каждая из которых может иметь свои требования к таймингу доменов. Например, на этапе загрузки системы можно использовать более длинные тайм-слоты, чтобы виртуальные машины успевали запуститься, не превышая выделенное доменное время, а на рабочем этапе — более короткие тайм-слоты, чтобы каждый домен оперативно реагировал на внешние воздействия. Кроме того, системы на базе SDK, такие как Microkit, могут использовать новый API для настройки расписания доменов на этапе загрузки.
Новый API seL4 реализован, верифицирован и доступен начиная с seL4 15.0.0.
Пленарный доклад Джун Андронич на весенней конференции CDIS в Стокгольме
21 мая 2026 года CDIS — шведский исследовательский центр киберзащиты и информационной безопасности — провёл весеннюю конференцию в Королевском технологическом институте KTH в Стокгольме.
Генеральный директор Proofcraft Джун Андронич выступила с одним из двух пленарных докладов наряду с Огюстом Мартенсом из Mistral AI. Джун рассказала об обзоре формальной верификации применительно к кибербезопасности, а также приняла участие в панельной дискуссии о цифровом суверенитете.
Proofcraft выступила на саммите Cyberagentur Milestone Research
В апреле 2026 года немецкое агентство Cyberagentur провело саммит Milestone Research, чтобы представить прогресс и результаты финансируемых им программ, включая программу исследований доверенного ПО (ÖvIT), получателем которой является Proofcraft в партнёрстве с Kry10.
Главный научный сотрудник Proofcraft Гервин Кляйн и главный научный сотрудник Kry10 Мартин Денель-Уайлд представили прогресс по проекту Dyvercon, направленному на обеспечение динамичности, производительности и доказуемости для сложных киберфизических систем. В частности, Гервин рассказал о работе Proofcraft по расширению доказательств seL4 для поддержки статической мультиядерной конфигурации, при которой приложения получают выгоду от использования нескольких процессорных ядер для повышения производительности, при этом на уровне ядра на каждом ядре процессора выполняется отдельный экземпляр seL4.
Кроме того, Гервин выступил с общим введением в формальную верификацию и обзором её применения на практике.
Proofcraft — спонсор саммита seL4 2026
Proofcraft поддерживает саммит seL4 2026 года в статусе серебряного спонсора.
Саммит seL4 — ежегодное международное мероприятие для участников из индустрии, государственных структур и университетов, интересующихся самым надёжно верифицированным ядром операционной системы в мире. Среди докладчиков и участников — создатели и разработчики технологии seL4, включая команду Proofcraft.
В этом году саммит seL4 пройдёт в Ванкувере, Канада, 1–3 сентября 2026 года.
5 лет Proofcraft. Пять лет ближе к верифицированному будущему
14 апреля 2021 года была основана компания Proofcraft. Спустя пять лет команда настолько погружена в работу над верифицированным будущим, что публикация новостей на некоторое время приостанавливалась.
За это время произошло многое, и это ещё не всё. Ниже собраны несколько накопившихся новостей с техническими результатами, которые Proofcraft успела представить за это время.
Во-первых, доказательства seL4 теперь поддерживаются на 100% платформ Arm, на которых может работать ядро. Благодаря этому существенному прогрессу в снижении зависимости от узкоспециализированных экспертов пользователи seL4 могут свободно выбирать между поддерживаемыми платформами Arm, всегда будучи уверены, что используют верифицированную кодовую базу. Эта работа выполняется в рамках программы DARPA PROVERS.
Во-вторых, seL4 на AArch64 теперь доказанно обеспечивает целостность: получено формальное математическое доказательство того, что ядро предотвращает несанкционированное изменение данных приложением, работающим поверх seL4. Работа над теоремами безопасности продолжается: благодаря постоянной поддержке NCSC команда близка к завершению доказательства свойства конфиденциальности, а вместе с ним — и всего стека доказательств безопасности для 64-битной архитектуры Arm.
Параллельно ведутся ещё три крупных проекта, финансируемых соответственно DARPA, Cyberagentur и NCSC.