LINUX.ORG.RU

Представлена платформа для высокозащищенных систем на базе гипервизора seL4

 , , ,


0

2

После 7 лет работы Австралийский исследовательский центр NICTA и организация Open Kernel Lab представляют новую систему для обеспечения гарантированного уровня безопасности и отказоустойчивости. С точки зрения разработчиков это стало возможным благодаря:

  • Очень малому размеру микроядра-гипервизора и минималистичности функций. Как уже было сказано это микроядро-гипервизор seL4, которое в свою очередь базируется на открытом ядре OKL4
  • Математической проверки кода на устойчивость к сбоям
  • Жесткой изоляции процессов друг от друга и от ядра


Разработанная система позиционируется как решение для организации высокобезопасных систем для жизненно важных организаций таких как:

  • Медицинские центры(разработчики предлагают ее использовать как ОС для медоборудования )
  • Энергетические компании
  • Авиационные и другие транспортные компании

Кроме того разработчики считают что в перспективе эта система может послужить хорошей основой для систем электронной коммерции.
Список поддерживаемых архитектур:

  • ARM11
  • x86
  • Запуск в качестве гостя в Linux окружении

Здесь так же следует заметить, что при математическом доказательстве речь идет о проверке того, что система полностью удовлетворяет исходным спецификациям разработчика,следовательно, все равно сохраняются опасности от изначально неправильного проектирования
Исходные тексты, документация доступны для свободного использования, но в некоммерческих целях
Анонс маркетологов
Технические детали

>>> Подробности

★★★★★

Проверено: Shaman007 ()
Последнее исправление: Shaman007 (всего исправлений: 3)

Молодцы!

> The approach taken was to use literate Haskell to specify and implement the seL4 API. Haskell, as a functional programming language, is not a large paradigm shift for typical kernel programmers compared to more formal specification alternatives such as the B-method. Haskell is side-effect free functional programming language that allows us to explore implementation details of the kernel using a pseudo-imperative style with the help of Monads.

(это про верификацию). Молодцы, ничего не скажешь. Думаю, их ждёт светлое будущее :)

anonymous
()
Ответ на: Молодцы! от anonymous

Да вот только насколько это будет тормозить систему haskell же интерпретируемый

pylin ★★★★★
() автор топика
Ответ на: комментарий от silw

Как обычно не без ложки дегтя:

We are currently working towards supporting seL4 on multiprocessors. The true concurrency present on multiprocessors makes the formal verification aspects of seL4 extremely difficult. The challenge is to minimise the concurrency while still efficiently supporting multiprocessors.

Но ребята идут к успеху.

silw ★★★★★
()
Ответ на: комментарий от pylin

> Да вот только насколько это будет тормозить систему haskell же интерпретируемый

Это про верификацию

anonymous
()
Ответ на: комментарий от pylin

> haskell же интерпретируемый

haskell - это язык. ghc - это оптимизирующий компилятор этого языка машинный код. Есть разные компиляторы/интепретаторы

anonymous
()
Ответ на: комментарий от anonymous

Я вот к чему слой API самого ядра реализован через хаскелль, ведь seL4 это ядро, а так да у них еще довольно мощный фреймворк для верификации это им жирный + (плюс) ))

pylin ★★★★★
() автор топика
Ответ на: комментарий от tailgunner

Реализован при помощи, то есть насколько я понял хаскелль использовался разработчиками дял написания API к ядру

pylin ★★★★★
() автор топика
Ответ на: комментарий от pylin

Ну и как он будет тормозить систему? Английским по белому написано: «manually developing a high-performance C programming language implementation of seL4 for ARM processors».

tailgunner ★★★★★
()

Пока не появится на commoncriteria - новость ни о чем :]

vasily_pupkin ★★★★★
()
Ответ на: комментарий от silw

> Как обычно не без ложки дегтя

Тут конечно нужно вникнуть в то, что они там наproveвили. И хаскель тут кстати и в большую помощь.

Но вот есть конкуренцию не брали во внимание изначально «для упрощения модели», то IMHO жаль «круглых коней в вакууме», но можно закапывать. Если только у них нет гения математики в «кармане».

Хотя наверное предложат как раньше во FreeBSD - spl(IPL_seL4) на все ядро...

ly
()
Ответ на: комментарий от ly

Конечно надо вникать глубже, но >true concurrency в тексте наводит на мысль, что какая-то конкурентная модель у них есть, скорее всего, сильно упрощенная, но тем не менее.

silw ★★★★★
()

Куда катится этот мир? Сначала выкинули поддержку ARM из Pistachio, а затем сделали коммерческое ядро OKL4.

Между тем, на сайте l4hq.org чётко сказано:

http://www.l4hq.org/arch/arm/

Open Kernel Labs (OK) provides a comercial derivative of the L4Ka::Pistachio kernel for embedded systems called OKL4 and an operating system support layer, Iguana. It supports a variety of ARMv4, ARMv5 and ARMv6 processors and porting to other processors is possible in a short period of time.

Ну ничего, у меня старая версия Pistachio, которое поддерживает ARM.

alman ★★★
()

Забавно. Люди построили верификатор соответствия продукта дизайную Но пока только для продукта, запущенного на однопроцессорной системе.

Читаем по ссылке:

Future work

We are currently working towards supporting seL4 on multiprocessors. The true concurrency present on multiprocessors makes the formal verification aspects of seL4 extremely difficult. The challenge is to minimise the concurrency while still efficiently supporting multiprocessors.

А вот интересно, в принципе это возможно, верифицировать дизайн на параллельной системе если они уменьшают степень параллелизма?

gns ★★★★★
()

тормозня наверное страшная полчается, с плохой отзывчивостью (как и обычно у «правильных» систем) - что от электронной коммерции и торгов эту разработку и отодвинет.

tommy ★★★★★
()

>Список поддерживаемых архитектур:

ARM11

Хорошо

x86

Очень плохо, устаревший костылявый x86 надо искоренять а не поддерживать.

Запуск в качестве гостя в Linux окружении

Хорошо

anonymous
()

мои поздравления разработчикам! прекрасный проект

jtootf ★★★★★
()
Ответ на: комментарий от pylin

> OKL4 не коммерческое

Спорьте не со мной, а с вышеприведённой цитатой.

alman ★★★
()
Ответ на: комментарий от pylin

> Да вот только насколько это будет тормозить систему haskell же интерпретируемый

Проспись. // С уважением, Ваш К.О.

rtvd ★★★★★
()
Ответ на: комментарий от sdh

> Им LWKT от Диллана надо к этому ядру прикрутить, ка планировщик задач...

В L4 идеальный планировщик задач. Ничего прикручивать не нужно.

alman ★★★
()
Ответ на: комментарий от alman

Идеальный планировщик - LWKT, а сабжевый даже не проэктировался для многопроцессорных систем...

sdh
()
Ответ на: комментарий от alman

>Ну ничего, у меня старая версия Pistachio, которое поддерживает ARM.

Бери OKL4 3.х . Правда собирается SCons, но вполне себе сорцы открыты.OKL4 4.0 тоже дают вроде если попросить... А в фисташке что- то с комитами совсем негусто. Пока ИМХО OKL4 самая развивающаяся реализация L4.

yurkis
()

# базируется на ... Математической проверки

прелестно

# для свободного использования, но в некоммерческих целях

зачем это лишнее ", но"?

всего исправлений: 3

маловато будет

dilmah ★★★★★
()
Ответ на: комментарий от alman

Любую с достаточной документацией, jtag и вменяемым бутлоадером. RAM >= 64mib должно хватить за глаза. Требования по перефирии зависят от твоих нужд.

anonymous
()
Ответ на: комментарий от yurkis

>>Бери OKL4 3.х . Правда собирается SCons, но вполне себе сорцы открыты.OKL4 4.0 тоже дают вроде если попросить... А в фисташке что- то с комитами совсем негусто. Пока ИМХО OKL4 самая развивающаяся реализация L4.

для скачивания OKL4 надо то ли регацо то ли просто заполнять форму с данными. но на самом деле сорцы лежат в «открытом доступе» и их можно стянуть не тратя время на заполнение формы. и да, признаю, я честно украл^Wскачал сорцы OKL4 без указаний сведений о себе.

exception13 ★★★★★
()
Ответ на: комментарий от exception13

таки соврал. оказывается стягивал именно версию 3.0

exception13 ★★★★★
()
Ответ на: комментарий от gns

> А вот интересно, в принципе это возможно, верифицировать дизайн на параллельной системе если они уменьшают степень параллелизма?

Просто состояний ооочень много будет....

sv75 ★★★★★
()

B-method, OMG. Им осталось промелу использовать для верификации на SMP.

sv75 ★★★★★
()
Ответ на: комментарий от alman

> В $400 можно уложиться? Как с доставкой в регионы?

Уложиться можно запросто. Даже взять что-нить с LCD. Куча вариантов с доставкой worldwide

anonymous
()
Ответ на: комментарий от sv75

Это тоже вопрос. Как я понял. у них сейчас есть строго «последовательная» (однопоточная) модель ядра, писанная на хаскеле.

Далее, либо делать многопоточную модель (что убивает надежность доказательства из-за возможных дедлоков модели, например), либо действительно плодить состояния ядра и получаеть иголки в момент порождения состояний. Многопроцессорную систему с «многими тактовыми генераторами» трудно отмоделтировать честно, как мне кажется.

gns ★★★★★
()
Ответ на: комментарий от gns

О чём Вы говорите? О каком то доказательстве или о L4? Дедлоки в L4 возможны только если у архитектора системы руки кривые.

alman ★★★
()
Ответ на: комментарий от alman

Почитайте «подробности»:

The approach taken was to use literate Haskell to specify and implement the seL4 API. <....>

For validation, to enable the API to be used without requiring a real kernel implementation together with all the debugging complexities of managing real hardware, we created a simulator that implements the ARM processor user-level instruction set. The simulator enables ARM application binaries to be executed. When an exception would normally be generated resulting in execution transfer to the kernel running in privileged mode (a system call for example), the simulator invokes the Haskell kernel specification directly, which proceeds to resolve the exception and gives the illusion that the application is running on real hardware with a kernel implementing the API specification.

Так что я о верификации SEL4 API об эмулятор ядпа и процессора :)

gns ★★★★★
()
Ответ на: Молодцы! от anonymous

The approach taken was to use literate Haskell to specify and implement the seL4 API. Haskell, as a functional programming language, is not a large paradigm shift for typical kernel programmers compared to more formal specification alternatives such as the B-method.

другая ОС на Хаскелле: House M.D.

И да, seL4 имеет к нему отношение, но другая вещь, чем House/Osker: House/Osker это именно прототип ядра ОС на Haskell (упор на Хаскель), разработанный под общую спецификацию L4 (реквестирую тег в новость: L4), seL4 — это новое ядро под общую спецификацию L4 с успешно выполненной целью формальной верификации (упор на верификацию) (ау, где там BitC и ERTOS/Coyotos?)

anonymous
()
Ответ на: комментарий от gns

Так что я о верификации SEL4 API об эмулятор ядпа и процессора :)

У Яна Пьюмарты на эту тему есть интересные работы с VVM, Virtual Virtual Machine. Сейчас это немного развивается в проекте FONC см вики

Так что нужен не эмулятор процессора, а ОС под виртуальный процессор :)

anonymous
()
Ответ на: комментарий от pylin

> И в то же время: The approach taken was to use literate Haskell to specify and implement the seL4 API.

почитай про разницу между seL4 и House/Osker.

В House был прототип ОС на Хаскелле, публикация про «принципиально новый подход к созданию ОС» в подробностях рассматривала API ядра такой ОС, ADT, выделение памяти (в Haskell cборщик мусора, в House kmalloc был реализован через GC). Вывод из публикации: это принципиально возможно, но есть тонкости с реализацией.
В seL4 упор был сделан на формальную верификацию API L4. Для этого использовался Haskell. Уже верифицированное API не было особой необходимости реализовывать именно на Хаскелле, по формально проверенной модели было реализовано C++ (L4) API.

anonymous
()
Ответ на: комментарий от anonymous

> (ау, где там BitC и ERTOS/Coyotos?)

Шапиро растекается мыслью по древу, чо.

tailgunner ★★★★★
()
Ответ на: комментарий от silw

Конечно надо вникать глубже, но >true concurrency в тексте наводит на мысль, что какая-то конкурентная модель у них есть, скорее всего, сильно упрощенная, но тем не менее.

Конкуренцию при желании можно реализовать через CPS: CPS-C, а уже это представление или исходное до него — верифицировать, так что особо принципиальных проблем не вижу

anonymous
()
Ответ на: комментарий от alman

Куда катится этот мир? Сначала выкинули поддержку ARM из Pistachio, а затем сделали коммерческое ядро OKL4.

для АРМа есть неплохой Сodezero. Плохо, что его кроме АРМа толком нигде нет (в списке рассылки портируют вроде бы, но куда-то не туда)

anonymous
()
Ответ на: комментарий от gns

Далее, либо делать многопоточную модель (что убивает надежность доказательства из-за возможных дедлоков модели, например), либо действительно плодить состояния ядра и получаеть иголки в момент порождения состояний.

дедлоки должны быть невозможными — их отсутствие можно доказать теми же сетями Петри или пи-исчислением Dspace или в релевантной логике или в семантике Крипке (есть, к примеру, публикации про применение семантик Крипке при реализации сборщика мусора)

anonymous
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.