Hypervisor на базе ядра seL4

Есть ли какие-то готовые тулзы и маны для удобного запуска в таком гипервизоре Linux

Мануалов, к сожалению, я нигде подобных не видел, а вот коммерческие реализации на описанной тобой оригинальной технологии (L4) лицезрел ещё 13 лет назад:

https://forum.motofan.ru/index.php?s=&showtopic=161208&view=findpost&p=1793741

Для Ъ: Телефон Motorola EVOKE QA4 для американского рынка под CDMA, где вместо привычного BREW инженеры Motorola и Qualcomm изощрились и запустили Linux как сервис микроядра L4, а сверху поставили оболочку из GTK+ и X.Org

В таком виде оно и пошло на рынок. Исходники OSS-компонентов прошивки этого телефона можно скачать по ссылке выше. GUI-оболочка в них, конечно же, не входит.

Ну и для оригинального L4 имеется https://l4linux.org/, а вот есть ли подобное под seL4 – не знаю.

Если пока нет универсального гипервизора на базе seL4 типа ESXi, то может быть, хотя бы можно запустить скоростной софтовый эмулятор Box86 на ARM хосте с Genode+seL4, а уже в нем запустить обычный дистрибутив для X86, например, OpenBSD и/или Linux ?

https://genodl4arm.critical.com/

https://genode.org/documentation/platforms/index

https://box86.org/

Есть ли подобные скоростные эмуляторы для хостов x86?

Ведь именно гипервизорная функция с аппаратным ускорением не является безопасной в seL4 на x86 (да и очевидно аппаратная виртуализация x86 дырява на любом гипервизоре, чтобы там не говорили всякие разработчики XEN, Qubes, etc.), но если бы можно было каким-то образом запустить что-то похожее на Box86 на хосте x86 вместо ARM, то x86 стал бы немного безопаснее в том числе и для скоростной СОФТОВОЙ эмуляции (не аппаратной виртуализации) гостевух?

https://docs.sel4.systems/projects/sel4/verified-configurations.html

https://docs.sel4.systems/Hardware/

https://genodl4arm.critical.com/

Genode on seL4 on ARM
Genode Lab's Genode Operating System Framework
with Data61's seL4 Microkernel
running on physical ARM hardware.

https://www.opennet.ru/opennews/art.shtml?num=53129

Организация RISC-V Foundation сообщила о верификации работы микроядра seL4 на системах с архитектурой набора команд RISC-V. Верификация сводится к математическому доказательству надёжности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров RISC-V RV64, требующих повышенного уровня надёжности и гарантирующих отсутствие сбоев. Разработчики ПО, работающего поверх ядра seL4, могут быть полностью уверены, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и, в частности, её критические части.

Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86. Отмечается, что комбинация открытой аппаратной архитектуры RISC-V с открытым микроядром seL4 позволит добиться нового уровня безопасности, так как аппаратные составляющие в перспективе тоже могут быть полностью верифицированы, чего невозможно добиться для проприетарных аппаратных архитектур.

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

Напомним, что архитектура seL4 примечательна выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и т.п., вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора. Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.

Еще бы сравнить системы на базе seL4 с KasperskyOS:

https://os.kaspersky.com/wp-content/uploads/sites/11/2016/11/KasperskyOS-Whit...

https://habr.com/ru/post/437406/

Достижения HACMS основаны на старом верном друге инженера-программиста — модуляризации. Инновация в том, что формальные методы доказывают наблюдаемость интерфейсов и инкапсуляцию внутренностей модулей. Это гарантированное соблюдение модульности позволяет инженерам, которые не являются экспертами по формальным методам (как в компании «Боинг»), создавать новые или даже модернизировать существующие системы и достигать высокой устойчивости. Хотя инструменты пока не обеспечивают полного доказательства безопасности системы.

Формальная верификация

Доказательства математической корректности программ восходят, по крайней мере, к 1960-м годам, но долгое время их реальная польза для разработки программного обеспечения была ограничена масштабом и глубиной. Однако в последние годы произошёл ряд впечатляющих прорывов в формальной верификации на уровне кода реальных систем, от верифицированного компилятора C CompCert до верифицированного микроядра seL4 (см. научные статьи о нём), верифицированной системы конференц-связи CoCon, верифицированного ML-компилятора CakeML, верифицированных программ для доказательства теорем Milawa и Candle, верифицированной файловой системы с защитой от сбоев FSCQ, верифицированной распределённой системы IronFleet и верифированного фреймворка параллельного ядра CertiKOS, а также важных математических теорем, в том числе проблемы четырёх красок, автоматического доказательства гипотезы Кеплера и теоремы Фейта — Томпсона о нечётном порядке. Всё это настоящие системы. Например, CompCert — коммерческий продукт, микроядро seL4 используется в аэрокосмической и беспилотной авиации, в качестве платформы Интернета вещей, а система CoCon использовалась на многочисленных крупных научных конференциях.

http://gvsets.ndia-mich.org/documents/VEAC/2020/Cyber_1050_Performance Impact...

Hypervisor technologies are often presented as offering a high degree of separation at the cost of performance. Is this too expensive for embedded systems? The cost of performance has been shrinking year after year as new advancements in virtualization technologies are baked into processors. When a hypervisor couples hardware assisted virtualization with device emulation, it makes current systems portable, future proof, and extends the life of legacy systems. seL4 is a perfect fit for the high assurance embedded hypervisor space. The open source seL4 microkernel is the first formally verified microkernel built with security and performance in mind. The mathematical proof of seL4 provides unprecedented assurance at the lowest, most critical software level. This paper investigates the overheads associated with using seL4 as a hypervisor on ARM and x86 platforms, providing synthetic and real -world benchmarking methodology and results.

По отзывам пользователей Sculpt им удавалось запускать OpenBSD в старых релизах еще на VBox v5x, в новых пока не пробовали.

Причем в новых релизах Sculpt по их словам по прежнему можно легко установить старый VBox5 из pkg пакета.

Но Sculpt обычно собирается с ядром NOVA, с ядром seL4 почему-то мало кто даже пытается и то неудачно:

https://lists.genode.org/pipermail/users/2019-July/006829.html

Nanfang Hu nhu2000 at gmail.com Mon Jul 29 01:31:13 CEST 2019

Previous message (by thread): users Digest, Vol 15, Issue 17 Next message (by thread): Issues to build Sculpt with Sel4 kernel Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

I am trying to build Sculpt with Sel4 kernel.

sudo make -C build/x86_64 run/sculpt KERNEL=sel4 BOARD=pc

I run into error, «Could not allocate block in ext2 filesystem»

It seems that I have increased file system size. Where is the place to make that change?

Thanks Nanfang

Софтовая виртуализация VBox включается следующим образом:

VBoxManage modifyvm <VM_NAME> --hwvirtex off
VBoxManage modifyvm <VM_NAME> --vtxvpid off

https://docs.oracle.com/en/virtualization/virtualbox/6.0/admin/swvirt-details...