LINUX.ORG.RU

Открыты исходники seL4!

 isabelle,


7

5

General Dynamics C4 Systems и NICTA рады объявить об открытии исходных кодов seL4 — первого в мире ядра операционной системы с доказанной корректностью:

  • бинарный код микроядра seL4 правильно реализует поведение, описанное в его абстрактной спецификации;
  • данные не могут быть изменены либо прочитаны без разрешения;
  • ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность.

Исходные коды доступны для широкой публики на GitHub.

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

★★★★★

Проверено: fallout4all ()
Последнее исправление: CYB3R (всего исправлений: 1)

интересно. надо будет посмотреть на досуге.

мдя, сколько же им пришлось париться с доказательствами!
думаю, воендосы на эту поделку будут падки.

Iron_Bug ★★★★★
()

BSD2 и GPL совместимы

Хм-м. FSF пишут, что BSD2 и GPL совместимы. Мне непонятно каким образом это может быть, если BSD2 ставит хоть какие-то условия, но пишут что так.

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

Не из Linux'а

Код из Linux'а таки попадает в xBSD, только этот код не под GPL. Наоборот тоже бывает.

Значит это код не из Linux'а. Автор может выпустить код под любой лицензией (если ему какой-нибудь договор не запрещает).

Camel ★★★★★
()
Ответ на: BSD2 и GPL совместимы от Camel

FSF пишут, что BSD2 и GPL совместимы. Мне непонятно каким образом это может быть, если BSD2 ставит хоть какие-то условия

Эти условия не противоречат GPL :)

«Пункт о рекламе» противоречит, с ним уже несовместимо. Но он настолько многим неудобен, что им редко пользуются.

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

(GPL)

Этот код коммитят в Linux. Просто под более либеральной лицензией.

Linux весь под GPL, причём строго второй версии. Попейте водички.

Camel ★★★★★
()

Корректность - для этого не нужно семи пядей, а вот будет ли «это» юзабельно на x64 для постройки нормальной ОСи - ещё вопрос. Hurd тоже много чем выделялся, однако дальше обочины не выезжал.

matumba ★★★★★
()
Ответ на: Public domain от Camel

Это public domain. Никакого кода «под более либеральной лицензией» вы пока не показали.

Где ты фразу «public domain» там нашел, упорок?

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

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

anonymous
()
Ответ на: Public domain от Camel

Это public domain.

«All Rights Reserved» - это уже точно не Public Domain :)

X-Pilot ★★★★★
()

математически доказанная корректность??? как???

I-Love-Microsoft ★★★★★
()
Ответ на: Нельзя требовать от Camel

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

alt-x ★★★★★
()
Ответ на: BSD2 и GPL совместимы от Camel

Хм-м. FSF пишут, что BSD2 и GPL совместимы. Мне непонятно каким образом это может быть, если BSD2 ставит хоть какие-то условия, но пишут что так.

На уровне файлов. Ни BSD, ни GPL не запрещают распространять проект в котором n файлов под BSD, и m файлов под GPL.

Может быть, можно даже извернуться и пометить код под разными лицензиями внутри одного файла, но на этот счёт я не уверен, и, в любом случае, это будет очень громоздко.

alt-x ★★★★★
()

a PC99-style Intel Architecture 32-bit x86 (ia32)

Что это такое??

На обычном x86 компьютере эту ось запустить не получится?

b0c0813f
()
Ответ на: Нельзя от Camel

Нельзя. Однажды BSD — всегда BSD.

Тебя обманули. BSD — лицензия позволяющая спокойно менять ее на другую, смотри как это делали MS с сетевым стеком, например.

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

воендосы на эту поделку будут падки

Нет, ведь это ядро:

реализует поведение, описанное в его абстрактной спецификации

а не в Уставе

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

Тебя обманули. BSD — лицензия позволяющая спокойно менять ее на другую

Бред

, смотри как это делали MS с сетевым стеком, например

Где я могу посмотреть исходник, в котором явно указана другая лицензия?

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

Так я не понял посоны, хоть на этой то оси крузис пойдет??

Корректность крузиса доказана математически?

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

BSD — лицензия позволяющая спокойно менять ее на другую

Упоролся что ли? Найди такое разрешение в тексте лицензии, это не должно представлять тебе труда, она короткая. А всё, что не разрешено явно, запрещено и охраняется законом.

unC0Rr ★★★★★
()

Осталось написать математически доказанные корректные драйвера под корректные, соответствующие спецификации на 100%, устройства. И полезную нагрузку, тоже доказанную, дописать надо. Первый половник из океана вычерпнут. Надо ли это все? Вот QNX просто работает, да и OpenWRT тоже.

A-234 ★★★★★
()
Ответ на: комментарий от happycorsair

Хоть новую ОС лепи

и тут начинается самое главное - собственно ОС надо написать

хоть гипервизор на его основе

этих гипервизоров и так как говна за баней. Слишком далеки они от народа :)

anonymous
()

осталось доказать корректность железа на котором оно работает и будет порядок.

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

осталось доказать корректность железа на котором оно работает и будет порядок.

Нет осталось доказать корректность доказательства корректности и того кто доказывает корректность.

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

да да. и градус неадекватности чтобы не зашкаливал. не порти людям праздник, ты там лишний

zyoung
()
Ответ на: комментарий от A-234

Осталось написать математически доказанные корректные драйвера под корректные, соответствующие спецификации на 100%, устройства. И полезную нагрузку, тоже доказанную, дописать надо. Первый половник из океана вычерпнут. Надо ли это все? Вот QNX просто работает, да и OpenWRT тоже.

В микроядерной ОС драйвера не обязаны быть без багов. Баги драйвера не влияют на работу программ и устройств, не зависящих от этих драйверов. Кроме того драйвер всегда можно перезапустить. В случае монолитной ОС баг в драйвере легко кладёт всю систему на лопатки.

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

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

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

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

Если я правильно понимаю, то

Redistributions <...> must retain/reproduce the above copyright notice, this list of conditions and the following disclaimer

не требует сохранения фразы

Redistribution and use in source and binary forms, with or without modification, are permitted

Таким образом, лицензию сменить нельзя — но можно делать что угодно, лишь сохранив копирайт, текст про отказ от гарантий и текст о том, что эти вещи нужно сохранять.

Разве это запрещает встраивание BSD-лицензированного кода в GPL-лицензированный код?

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

микроядро seL4 является предельно минималистичным

Значит ли это, что оно почти ничего не умеет?

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

В микроядерной ОС драйвера не обязаны быть без багов.

Они нигде этого не обязаны.

Баги драйвера не влияют на работу программ и устройств, не зависящих от этих драйверов.

Ну да, ну да. Еще есть программы, не зависящие от драйвера сетевой карты? От сетевого стека? Я уже не говорю о драйвере диска.

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

Ну да, ну да. Еще есть программы, не зависящие от драйвера сетевой карты?

Ну в принципе полно, думаю.

Я уже не говорю о драйвере диска.

Да и без диска многие программы обходятся, если уже запущены и работают.

Кроме того бывает много других устройств, не таких важных, но чьи драйверы влияют на устройство. Банальный пример. У меня айфон, у него какие то проблемы с WiFi-модулем. Если я включаю WiFi, даже не пользуясь им он начинает глючить и в самый неподходящий момент тупо зависает весь телефон, хотя я этим WiFi в этот момент вообще не пользовался. В идеале ОС могла бы определить, что с WiFi что-то не так по аномальному поведению драйвера и выгрузить его, не прерывая работу устройства.

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

Ну да, ну да. Еще есть программы, не зависящие от драйвера сетевой карты?

Ну в принципе полно, думаю.

Да в принципе нет. Вот сейччас у меня запущены Gnome, браузер, Eclipse и несколько терминалов. Сеть не нужна только половине терминалов.

без диска многие программы обходятся, если уже запущены и работают.

Ну-ну.

Кроме того бывает много других устройств, не таких важных, но чьи драйверы влияют на устройство

Именно - «неважных». Вот от крахов в неважных драйверах микроядро и в самом деле хорошо защищено.

В идеале ОС могла бы определить, что с WiFi что-то не так по аномальному поведению драйвера и выгрузить его, не прерывая работу устройства.

В идеале - может быть. А в реальности на машине без IOMMU ни в чем нельзя быть уверенным, как бы изолирован не был драйвер.

tailgunner ★★★★★
()
Последнее исправление: tailgunner (всего исправлений: 1)
Ответ на: комментарий от hobbit

Скорее, хурдокапец...

Hurd полностью держит модель безопасности Юникс!

В микроядрах L4... от модели безопасности Юникс отказались из-за чрезмерно высокой цены в текущих реализациях.

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

без диска многие программы обходятся, если уже запущены и работают.

Ну-ну.

Вполне себе имел работающую vmware на машине со сдохшим диском.

spqr ★★★
()
Ответ на: комментарий от alt-x

BSD на то и BSD, блять, что её можно анально запроприетарить или анально загплить.

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

Можно поменять лицензию у форка.

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

Вот сейччас у меня запущены Gnome, браузер, Eclipse и несколько терминалов. Сеть не нужна только половине терминалов.

т.е. если у тебя выпадет сетевой шнур/ребутнется wi-fi роутер, то эклипс, гном и половина терминалов упадут? или таки дождутся пока сеть не поднимется и не продолжат работу дальше?

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