Встраивание разрешено, конечно. Только многие понимают BSD как «стираю все копирайты, леплю GPL/whatever и радуюсь жизни». Использование кода под BSD в проекте под другой лицензией возможно, но это не является перелицензированием. Код так и остаётся под своей лицензией, изменить которую вправе только автор.

Ненужность крузиса доказана анониматически.

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

В посте, на который я отвечал, речь шла о «влиянии багов», а не о «падении». Кстати, обычные баги в драйвере (не падения) и в микроядерной системе повлияют на все программы.

эклипс, гном и половина терминалов упадут? или таки дождутся пока сеть не поднимется и не продолжат работу дальше?

Терминалы точно не продолжат, насчет Eclipse RSE тоже сомневаюсь.

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

Я тебе больше скажу - существуют tmpfs и ramdisk.

Ядро все из себя корректное а все остальное нет. Но беда в том, что это микроядро, само по себе абсолютно бесполезное. Вам еще надо доказать что юзверьспейс корректно использует это корректное ядро. А то получаются безупречно работающие подушки безопасности при заклинивающей на 120км/ч рулевой колонке. На маркетоидный развод похоже.

у парня какой-то нездоровый интерес к говну

Ядро все из себя корректное а все остальное нет. Но беда в том, что это микроядро, само по себе абсолютно бесполезное. Вам еще надо доказать что юзверьспейс корректно использует это корректное ядро. А то получаются безупречно работающие подушки безопасности при заклинивающей на 120км/ч рулевой колонке. На маркетоидный развод похоже.

Есть такое понятие, как уменьшение ущерба. Например некорректно работающая программа обычно не влияет на другие программы. А некорректно работающий драйвер может повлиять. Если продолжить аналогию с автомобилем, то цель микроядра - чтобы баг в климат-контроле не повесил весь бортовой компьютер, отключив тормоз и всё остльное.

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

Верно, потому что QNX - микроядро.

Толк в том, что вероятность багов в доказанном ядре практически нулевая (только если баг в одном месте и в ядре и в спецификации, что весьма маловероятно). А в ядре QNX вероятность багов ненулевая. К микроядерности это отношения не имеет.

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

По слухам, seL4 работает на миллиардах устройств и ни разу не взломана, так что какой-то толк есть. Но даже если это не так... тебе знакомо слово «исследования»?

Люди не пользуются ядром ОС, люди пользуются прикладными программами, которые пользуются сервисами ядра ОС и драйверами. Никого не волнует стабильная работа одного из компонентов, нужна стабильность работы в целом. Доказать это практически невозможно, только эмпирические наблюдения. Чем больше внедрений - тем больше наблюдений, а исследования это хорошо но далеко не достаточно.

По слухам...

А если без слухов:

The seL4 kernel is targeted at hardware that supports memory protection, which enables strong isolation functionality.

Ну какие миллиарды, о чем вы.

и ни разу не взломана

QNX тоже не взломан а работает еще больше где.

А если без слухов:

http://www.ok-labs.com/releases/release/open-kernel-labs-okl4-now-deployed-in... - поскольку технических деталей мало, без слухов не получится. И по этим слухам, стандартный ARMовский гипервизор (TrustZone?) сделан на seL4.

QNX тоже не взломан

Ы? QNX - обычная Unix-система, там все уязвимости обычные юниксовые. Голое микроядро нигде не используется.

а работает еще больше где.

Смешно.

Пасоны, а не знаете, чё это они вдруг открылись так-то? Каковая, значить, цель этова открытия? Академическая? Или чтобы набросились всем миром и потестили/критиканули? Привлекают разработчиков будущей ОСи?

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

5 лет разработчики доказывали заказчику, что программа полностью соответствует техническому заданию... /слёзы радости и гордости на глазах/ :-)

Понятно, вы OKL4 с seL4 перепутали.

Смешно.

Точно.

Понятно, вы OKL4 с seL4 перепутали.

Нет.

5 лет разработчики доказывали заказчику, что программа полностью соответствует техническому заданию...

Не 5, а все 10. Да и ничего не доказали. Спецификация - это расплывчатое определение.

Да и к тому же разработчики доказали заказчику, что часть(1%) минимального комплекса возможно соответствует, какой-то спецификации, которая хрен пойми что специфицирует. И похрен что недоказанных осталось 99% и похрен, что рост там экспоненциальный, а доказательство этого одного процента просто не имеет смысла. Герои. Через пару миллионов лет они «докажут» уже хоть что-то работающие.

Можно гордо назвать «ОС» «самой надёжной в мире» и впаривать лохам. Система работает.

Каждый раз смеюсь от названия сабжа.

Таки да.

А то получаются безупречно работающие подушки безопасности при заклинивающей на 120км/ч рулевой колонке.

Никаких проблем. Следуя твоей же аналогии. Мы спокойно въезжаем на скорости 120 в стену. А дальше кровь, кишки, рас...ный кузов... Но микроядро живет, отращивает новый кузов/движок/колеса, и система спокойно продолжает движение. Если стену жалко, то все еще проще: при заклинившей колонке, подрываем полный багажник динамита и... (см. предыдущий пункт).

Вся фишка микроядра в том, что если ТЗ предполагает чтобы пассажиры ничего не заметили, то можно сделать так чтобы они ничего не заметили. Не забесплатно, ессно. И совсем не задешево.

Вообще, seL4 проще чем какой-нибудь Xen. И это круто. Ибо гибкость. Для тех кому нужно больше, есть комплект юзерспейсных (с точки зрения микроядра) утилит. Он тоже запоенсорсен. И даже под BSD.

Есть также и линукс, адаптированный под запуск под seL4. Это решает проблему драйверов. Вообще, в L4 присутствуют только драйвера таймеров и контроллера прерываний (и еще последовательного порта в дебаг-версии). Правда, с видеодрайверами будет определенный облом, в том плане, если видюха корректно не пробрасывается под виртуалкой, то хрен больше одного раза ее запустишь. Но это проблемы видюх.

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

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

seL4 решает свю маленькую узкую задачу. Чтобы сделать на его основе систему практически полезную систему, поверх нее надо навернуть толстый слой софта. Неверифицированного.

Ну да, но жалко не стену жалко нас. Тоесть если рванет АЭС то мне по барабану что там ядро живое отработало, мне главное что дравер SCSI шины отказал и теперь усе.

Таки да.

Таки нет: http://www.ok-labs.com/releases/release/open-kernel-labs-provides-okl4-verifi...

«availability for download of OKL4 Verified (project name seL4)»

Неверифицированного

Дык. Верифицированный софт на деревьях не растет. И сам не размножается. Его нужно писать... А зачем? Главное — верифицированная пускалка. А «пускать» софт можно разными, и весьма экзотическими способами. Например, под верифицированной DBI системой.

Я уж молчу, про то что окружение (тоже верифицированное), сможет дать определенные гарантии, что запускаемый софт не сможет сделать что-то, что не разрешено его ролью. И микроядро здесь — весьма годный компромисс между дуболомством гипервизоров и тотальным попустительством «классических» ядер. Именно за счет гибкости, и настраиваемого уровня чистой и ничем не замутненной паранойи. Понятно дело, что *всё* окружение сделать верифицированным не выйдет. Но вот построить систему разумных компромиссов — вполне.

Верифицированный софт на деревьях не растет. И сам не размножается.

Неужели?

Главное — верифицированная пускалка.

Поверх которой пускается Linux со всеми его проблемами, да.

микроядро здесь — весьма годный компромисс между дуболомством гипервизоров и тотальным попустительством «классических» ядер

По-моему, ты вообще не понимаешь того, о чем говоришь.

Тоесть если рванет АЭС

Ну-ну. Не надо так пафосно. АЭС взрываются либо из-за конструктивных недостатков (Чернобыль), либо ссыкливого персонала (Фукусима). Система защиты многоуровневая, многоплановая и не завязанная на единый центр принятия решений.

Кроме того, если уж идти до конца, мне действительно похрен из-за чего взорвалась АЭС: из-за выхода из строя турбогенератора, отказа системы управления, или из-за того что персноал зассал и заглушенный реактор расплавился от процессов распада всякой высокоактивной радиоактивной срани (коей в любом уважающем себя реакторе просто дофига). Неудачный пример.

Поверх которой пускается Linux со всеми его проблемами, да.

Во-первых, линуксов пускать можно много. Во-вторых, критичный софт может быть и не под линуксом, что не помешает ему пользоваться сервисами линукса типа драйверов Wi-Fi или TCP/IP стека.

По-моему, ты вообще не понимаешь того, о чем говоришь.

Я говорю про конкретную задачу: сделать юзабельную систему по принципу QubeOS.

Я говорю про конкретную задачу: сделать юзабельную систему по принципу QubeOS.

Ты говоришь про какую-то существенную разницу (для этой задачи) между гипервизором и микроядром. А ее нет. Более того, интерфейс L4 не намного богаче интерфейса гипервизора.

А ее нет

Есть. Главным образом в том, что гипервизор не предполагает простого написания собственных юзерспейс (с точки зрения гипервизора) процессов. Микроядро — предполагает.

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

интерфейс L4 не намного богаче интерфейса гипервизора

ИМХО, даже беднее.

что гипервизор не предполагает простого написания собственных юзерспейс (с точки зрения гипервизора) процессов. Микроядро — предполагает.

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

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

Как я понимаю, еще меньше. Гипервизор, наверное, можно считать микроядром... Но тогда — весьма специфической реализацией.

Hurd тоже много чем выделялся, однако дальше обочины не выезжал.

http://www.opennet.ru/opennews/art.shtml?num=40297

«В частности, Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) применяет seL4 для повышения защищённости программных систем, используемых в военных беспилотных летательных аппаратах.»

Внесите царя

Что за царь?

Carb_blog, Carb_blog4, Carb_blog5

А ты не думал, что между 1-м и 4-м есть 2-й и 3-й. Риально, да?

Что за царь?

голем из говна

А ты не думал, что не настолько интересен, чтобы следить за всеми инкарнациями?

«В частности, Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) применяет seL4 для повышения защищённости программных систем, используемых в военных беспилотных летательных аппаратах.»

Оборонка сша почти полностью состоит из частных разработок, а частные разработки состоят из маркетинга на 99%.

Да и темболее, что защищать в беспилотнике? Линию связи? Она никак не связана с говноядром. От глушилки и сбития это не спасает. Автопилотирование тоже никак не связанно с говноядром, да и антиреверс тоже.

Дак в чем же заключается перспектива разработки DARPA? Я тебе скажу - грантополучательство и разводка лохов.

Причем тут следить? Тут дело не в слежении, а в отсутствии мышления. Тыж 0(1) 4 5 нашел. Это задачка на выявление последовательности уровня детсада.

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

Гуляй, Вася

,

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

В кои-то веки ЛОР тортить опять стал, а они банят. Ну что за недалёкость...

Есть же игнор, специально для монашек. Убиваете ресурс, посаны.

Vsl хотя бы производил впечатление человека, который понимает, о чём говорит. И ругань у него была затейливее. Это же какой-то негодный клон. Я не предлагаю устроить клуб джентльменов и коллективно пить чай, оттопырив пальчик, но всему есть предел

Это маркетоидный бред. Суть в том что на seL4 нету миллиардов устройств.

В Чернобыле конструктивные недостатки наложились на вопиющий дилетантизм персонала. И этот персонал _намеренно_ поотключал всю защиту до которой смог дотянуться.
Вы говорите что до сих пор все RTOS справлялись с управлением сложными ответственными объектами и без скурпулезного тестирования ядра? Ну так и я о том же. Бессмысленно тратить время на эту ерунду, исследовать нужно стабильную работу системы в целом а не микроядрышка которое только тем и занято что делает безопасные memcopy.

Суть в том что на seL4 нету миллиардов устройств.

Суть в том, что микроядро от OKL и seL4 - если и не один проект, то очень связаны. А что конкретно стоит в миллиардах устройств, точно знают очень мало людей, поэтому я прямо говорил - «по слухам». Но я ничего не путаю.

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

Проект не один, а как они связаны мне найти не удалось. Судя по составу OKL4 в seL4 входит только микровизор. Частей вроде OKL4 Linux и т.п. в составе seL4 нету.

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