Компания General Dynamics C4 Systems (http://en.wikipedia.org/wiki/General_Dynamics_C4_Systems)&nb...и австралийский исследовательский центр NICTA (http://en.wikipedia.org/wiki/NICTA) анонсировали (http://sel4.systems/) скорый перевод микроядра seL4 (http://ssrg.nicta.com.au/projects/seL4/) (Secure Embedded L4) в категорию открытых проектов. Ядро seL4 нацелено на предоставление повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. Корректность реализации seL4 в своё время была доказана (http://www.opennet.me/opennews/art.shtml?num=23011) математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире.
29 июля под одной из свободных лицензий будут не только открыты исходные тексты ядра seL4, но и связанные с системой компоненты доказательства надёжности и сопутствующий код для построения высоконадёжных операционных систем. С технической стороны, ядро seL4 примечательно выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным.
URL: https://news.ycombinator.com/item?id=7938149
Новость: http://www.opennet.me/opennews/art.shtml?num=40075
ждём внесения ошибок сообществом!
...полутора землекопов. Сколько участников сообщества живет в сверхнадежном подземном бункере на глубине километра? Примерно столько же, если не меньше, будет коммитить в сверхнадежное ядро.
А в чем заключалось математическое обоснование?
> А в чем заключалось математическое обоснование?http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
While we have some ideas on how to construct verifi-
able systems on multiprocessors, they are outside the
scope of this paper and left for future work.Короча, как у Ферма: "- Я нашёл поистине замечательное доказательство этого факта, но поля этой книги слишком малы, чтобы его уместить." :)
Обычно, математическое доказательство кода состоит в том, что доказывается, что программа в результате выполнения кода может иметь строго ограниченные набор желаемых состояний и не может выйти за пределы этого множества.Что не нивелирует багов компилятора, космических лучей, багов железа и вообще надеятся на абсолютную надежность ПО - глупость.
> не нивелирует багов компилятора, космических лучей, багов железа и вообще надеятся на абсолютную надежность ПО - глупость.Голову от падения кирпича оно тоже не спасёт.
А ежели кирпич уже упал? Спасёт?
Да. А если принять внутрь и от изжоги помогает ;-)
Гёдель смотрит с ухмылкой.
На это надеяться не надо, это надо обеспечивать.
> А в чем заключалось математическое обоснование?В том что если деградировать ядро до примитивного тасксвичера - в нем, конечно, багов не будет. Это даже можно формально доказать. Просто баги будут в других местах кода. Так что радости то с того, учитывая что само по себе такое "ядро" не умеет ни-че-го?
В теории надежности, если кто-нибудь из отпостившихся "критиков" вообще знает что это такое.
В случае системы с последовательным соединением элементов, надежность системы в целом будет определяться произведением надежностей(вероятность безотказной работы) каждого из звеньев системы. Это грубая формулировка, отражающая сущность повышения надежности системы за счет одного из звеньев. Самоучкам программистам и сисадминам, при всем моем уважении к их роли в общем научно-техническом прогрессе, немного не хватает базового образования. Ищем на просторах тырнета "Теория надежности" и восполняем пробелы в образовании. Весьма полезная дисциплина.
Простой пример, если у вас операционка, которая работает "через раз" (надежность = 0.5), железо, которое работает "через раз" и пользовательская программа, работающая "через раз".
То в результате надежность системы в целом будет 0.5*3 - 0.125, а если операционка очень надежная (0.99), то надежность системы будет 0.248. Т.е. в последнем случае система в целом будет надежнее практически в два раза, и разработчик посвятит свое время поиску косяков в куда меньшем количестве узлов отказа.
P.S. В предыдущем "примере" 0.5*3 - ошибка. должно быть 0.5^3
Доказали что ядро содержит те же ошибки что и спецификация.
Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего. Для Ъ хотелось бы какой-нибудь более подробной инфы.
Поэтому оно такое сверхнадежное.
так и будет. и предназначено оно будет для решения специализированых задач на всяких-там микроконтроллерах. маловероятно, что в ближайшее время с него можно будет по интырнетам лазить
> Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего.Ну так в hello world тоже багов не очень много. Хотя, конечно, от програмера зависит.
Ждём код, будем проверять :)
для него даже багтрекер не нужен
Ниже на писан код самой безопасной ОСь во Вселенной!--- cut here ---
--- end cut here ---
Я это вбросил в perl ... так оно мне linux на FreeBSD переустановило ...
СволочЪ ты павлин :(
> Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным.тыг ведь видов ошибок можно допустить -- намного-много больше :-)
как минимум -- вот например что часто бывает:
* состояние гонки. в той или иной форме -- невероятно-частая ошибка.
* некорректная проверка источника событий. (или вообще забывают проверять источник -- а сразу выполняют действие связанное с событием).
* утечка ресурсов. например утечка может быть связана с неполным алгоритмом учёта состояния ресурсного объекта (например: алгоритм -- учитывает не все возможные ситуации.. такое бывает СВЕХ-часто в ПО).
>... вот например что часто бываетPDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
>>... вот например что часто бывает
> PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdfнет :)
я сразу комментировать
>>>... вот например что часто бывает
>> PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
> нет :)
> я сразу комментироватьBy design, we side-step addressing the verification
complexity of yield by using an event-based kernel
execution model, with a single kernel stack, and a
mostly atomic application programming interfaceКороча, они тоже udev в ядро вкорячили.
и ещё при верификации этой кодлой лентяев аспирантов можно допустить ещё больше ошибок. Главное же что статьи будут написаны и в журналы разосланы.
Поддерживаю.
Интересно: какой был бюджет этого исследования ?
И что им обещали в конце исследования ?
Насколько реально практическое применение этого ядра ?Люди годами пишут сложные ядра(например ядро Linux),
а тут они взяли и написали ядро, которое не имеет ошибок.
Как-то звучит "натянуто".
Похоже эта теория "далека" от практики.Насколько оно уступает по сложности ядру Linux ?
А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD
> А ведь вам говорили, что ядро в виде монолитного куска кода плохая
> идея XDВсе относительно в матрице. Что есть монолитность, и как определить ее. Это всего лишь абстракция, а не реальная каменная субстанция. Что такое "кусок кода", опять абстракция.
Даже если человеку отпилить руку, он необязательно умрет. вроде кажется что он монолитный на вид. Но не все что кажется на первый слепой взгляд монолитным на самом деле такое.
> А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XDДа, было дело - Таненбаум критиковал когда-то. И где сейчас миникс и где линукс? К слову, монолитность - понятие относительное.
>> А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD
> Да, было дело - Таненбаум критиковал когда-то. И где сейчас миникс и
> где линукс? К слову, монолитность - понятие относительное."Побеждает не самое технически совершенное решение. Пример - Чикака-95"
технически совершенное решение побеждает всегда если оно есть. Реальность такова, что хоть как-то юзабильное монолитное GP ядро есть с некоторыми недостатками, а совершенного микроядра нет. Есть только ещё более убогие попытки сделать такое ядро.
Не имеет ошибок и ничего не умеет, а когда научится, проявятся и ошибки, и куча микроядерных проблем.
А что должно уметь микроядро помимо выноса всего в пользовательское пространство?
> А что должно уметь микроядро помимо выноса всего в пользовательское пространство?Вот-вот отсутствие ошибок не является преимуществом микроядерной архитектуры как пытаются выдать. В формуле 2+2=4 трудно сделать ошибку, но и пользы от нее большой нет.
> А что должно уметь микроядро помимо выноса всего в пользовательское пространство?Вы сознательно обманываете людей. Когда говорите о недостатках линукса то берете все ядро вместе с драйверами и всеми модулями. И оцениваете его сбойность. Конечно по сравнению с лопатой у него вероятность сбоев выше. Но это же демагогия. Лопата линукс все равно не заменит. Вы сравниваете несопоставимые вещи. Сравнивать надо совокупность вашего микрочепухи с набором драйверов. авторы конечно молодцы, они доказали, что дваждыдва безошибочно.
> Вы сознательно обманываете людей. Когда говорите о недостатках линуксаBusted. Ты сам начал. До тебя о линуксе никто не вспоминал.
Так суть микроядра в том и состоит, что падение драйверов не рушит всю систему
> Так суть микроядра в том и состоит, что падение драйверов не рушит всю системуВ том же пингвине драйверы не так уж часто именно падают. Чаще просто глючная работа с своей периферией. И в этом плане микроядро ничего не даст.
> А что должно уметь микроядро помимо выноса всего в пользовательское пространство?должно назначить виновного из юзерспейса за все дальнешие проблемы с системой.
> Люди годами пишут сложные ядра(например ядро Linux),а тут они взяли и написали ядро
L4 писали не годами? Срыв покровов.
> Люди годами пишут сложные ядра(например ядро Linux),а тут они взяли и написали ядро, которое не имеет ошибок.
это разного уровня адра. Для критических систем ядра урезаны и узкоспециализированны, это тупо меньше SLOC.
... и железо там изготовлено из других материалов, по другой технологии и
имеет логику самоконтроля на аппаратном уровне и помимо этого дублируется.
> Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире.как же любят люди заблуждаться под покровом математики и технологий.
Когда человеком руководит страсть - он способен на многое,
но он теряет здравомыслие.
А сколько лет этому seL4? Когда оно было написано и проверено в последний раз?
> А сколько лет этому seL4? Когда оно было написано и проверено в
> последний раз?Дурeнь, посмотри, КТО его использует. Тебе название General Dynamics ни о чем не говорит, не?
это те самые перцы у которых f-16 при пересечении уровня моря в IL переворачивался вверх ногами? Да, говорит о многом. Но я точно не помню что там конкретно было, их f-16 или не их f-15
>основание считать решения на базе seL4 самыми надёжными в миреоно на С/С++ написано?)
P.S. Радует пополнение в мире опенсурса.
> оно на С/С++ написано?)Standard ML, Isabelle, местами C
Programming in C is not sufficient for implementing
a kernel. There are places where the programmer
has to go outside the semantics of C to manipulate
hardware directly. In the easiest case, this is achieved
by writing to memory-mapped device registers, as
for instance with a timer chip; in other cases one has
to drop down to assembly to implement the required
behaviour, as for instance with TLB flushes
Я, конечно, не в теме. Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной) модели железа, на котором это будет крутиться? Что, понятное дело, нереально.То есть, вероятно, математические доказательства корректности - это интересное упражнение, но для практики не больше ли пользы в хорошем покрытии юнит-тестами и основательном объеме fuzzy-тестирования?
> Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной)
> модели железа, на котором это будет крутиться? Что, понятное дело, нереально.Не должно. :)
В идеале так надо было бы, конечно. Но если играть в идеалистов, то вообще не стоит браться за написание программ, потому что никто не знает как писать программы без багов. В общем, если мы позиционируем себя как практиков, то мы должны признать, что неполная модель железа использованная в доказательстве, всё же лучше чем отсутствие этой самой модели. Правда да, тесты позволяют протестировать что-либо на реальном железе, но меня если честно, сильно сомневает способность тестов выявить какую-то "железную" проблему. Разве что документированную, многократно описанную, с существующим эксплоитом в паблике.
Собственно:
> Hardware management: the proof tries to make only the most minimal assumptions on the underlying
> hardware. It abstracts from cache consistency, cache colouring and TLB (translation lookaside
> buffer) management. The proof assumes these functions are implemented correctly in the assembly
> layer mentioned above and that the hardware works as advertised. The proof also assumes that
> especially these three hardware management functions do not have any effect on the behaviour of
> the C program. This is only true if they are used correctly.Взято отсюда: http://ertos.nicta.com.au/research/l4.verified/proof.pml
Причём эта ссылка достаточно древняя, например, сейчас они уже не доверяют компилятору, и проверяют также и сгенерированный машинный код на корректность: http://www.techworld.com.au/article/547841/nicta_release_dro...
> То есть, вероятно, математические доказательства корректности - это интересное
> упражнение, но для практики не больше ли пользы в хорошем покрытии юнит-тестами и
> основательном объеме fuzzy-тестирования?Нет, математическое доказательство полезнее. Потому что оно работает не с конкретными наборами входных данных, а с множествами этих самых наборов. Представь себе, в качестве примера, функцию высчитывающую корни квадратного уравнения, которая на входе принимает три числовых значения, на выходе даёт 0, 1 или 2 числовых значения. Сколько разных случаев можно проверить тестом? 5? 10? 100? 1000? 10000? Математически же можно проверить все возможные случаи, несмотря на то, что количество этих случаев, равно бесконечности (практической бесконечности, поскольку все случаи проверить практикой невозможно).
Конечно есть свои нюансы. Для того, чтобы доказать функциональную корректность кода, требуется предварительно написать спецификацию этого кода на формальном языке. Спецификация тоже может содержать ошибки. Но, поскольку и тесты также могут содержать ошибки, это нельзя считать недостатком метода по сравнению с написанием тестов.
А вообще, это весьма перспективное направление. Варнинги компилятора придумали давно. Потом кому-то их показалось мало, и создали статистические анализаторы. Ребятам же показалось мало проверки кода по паттернам, и они попытались решить общий случай. Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.
> Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.Зевая... серебряной пули нет.
>> Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.
> Зевая... серебряной пули нет.Я разве говорил что-то о серебряной пуле? Перечитайте и не говорите глупостей.
Подобную белиберду про грядущую ненужность программистов за последние тридцать лет по поводу чего только не писали. А пуля все не с места.
> Подобную белиберду про грядущую ненужность программистов за последние тридцать лет по поводу
> чего только не писали. А пуля все не с места.Ой, да ладно вам. Настоящие программисты (tm) вымирали динозаврами уже не раз. Вот смотрите:
1. На заре эпохи компьютеров, все программисты имели серьёзное математическое или физическое образование. Они были самыми натуральными учёными, с научными публикациями, которые читали лекции первокурам и получали гранты. Зубробизоны. Их сегодня нет с нами. А те что остались, пишут такую чушь, что на их код без слёз взглянуть невозможно.
2. Затем программисты лабали исключительно на языке ассемблера и смотрели на высокоуровневых программистов как на дерьмо. Эти тоже практически вымерли. А код их сегодня выглядит макаронной мешаниной, в которой сам чёрт ногу сломит, о какой-либо поддержке этого кода не может быть и речи.
3. Выросло поколение пишущее на языках уровня C/Pascal. Эти сегодня затолканы в довольно-таки узкую нишу системного программирования. Есть примеры не вписывающиеся в эту нишу, но их, мягко говоря, не фонтан, и общие тенденции направлены на то, чтобы окончательно оставить сям системное программирование и ничего больше.
4. Сегодня мы имеем быдлокодеров на php/ruby и тп. Мы имеем C++ программистов, которые не зная ничего кроме C++ мнят себя гуру программирования и единственно правильными программистами. Есть джависты, которые (позорища!!!) жить не могут без сборки мусора. И, отмечу, все эти личности смотрят на C как на дерьмо, потому что там нет ООП/сборки мусора/динамической типизации/адекватной работы со строками/... выбирате любой пункт на вкус или впишите свой.
5. Предсказывая в будущее. Мир зохавают декларативные языки, позволяющие лишь описывать спецификацию программы. 95% сегодняшних программистов будут смотреть на тех, кто пишет на декларативных языках как на дерьмо, и считать их недопрограммистами. И все эти 95% вымрут как и предыдущие категории. Вымрут или будут загнаны в какие-то довольно узкие ниши. Оставшиеся в живых будут смотреть на код, который пишется сегодня, как на дерьмо, которое невозможно поддерживать, проще переписать.
То есть, ведущиеся тридцать лет разговоры, на самом деле имели под собою почву и за эти тридцать лет программисты стали настолько иными, что можно уверенно говорить о том, что предыдущее поколение программистов вымерло. Конечно, можно возразить, и говорить о том, что никто не вымер, что вместо массового вымирания программистов, произошло приспособление программистов к новым условиям. Но это будет такой же полуправдой, как и утверждение о том, что популяция программистов пережила 2-3 массовых вымираний.
Ну, так спецификации программисты и будут писать. Те, кто вовремя переучатся, и молодняк, который этому сразу будет учиться. Разница то какая?
> Ну, так спецификации программисты и будут писать. Те, кто вовремя переучатся, и
> молодняк, который этому сразу будет учиться. Разница то какая?Ааа, вы про это. Ну, во-первых, не надо особо зацикливаться на этой теме, я её озвучил, скорее ради лулзов, и, мне казалось, что объединение одним предложением плинтуса, быдлокодеров и динозавров, должно было донести мои намерения до сведения читателя. Во-вторых, как и при любой автоматизации, количество рабочих мест снижается. Кто-то переучивается и находит своё место в новой системе, кто-то переучивается, но места ему не хватает. В-третьих, надо признать, что автоматизация может привести к тому, что увеличится объём промышленности выпускаемой отраслью, что компенсирует снижение числа рабочих мест. В общем, не стоит особо зацикливаться на этой теме -- не знаю как вы, но я не могу предсказать к чему приведёт создание программы, пишущей программы и, поэтому, не готов серьёзно обсуждать эту тему.
Оно было надежным пока было закрыто и никто о нем не знал. Ждем патчей. welcome to the real world.
ах да и самый надежный секрет тот о котором знает только один.
Микроядро математически прошедшее проверку просто исполняет ядро Линукс как один и процессов. В ядре Линукс и драйвера и всё остальное , и его-то никто и не проверял! В России тоже был тендер, на 15 миллионов рублей, который должен был проверить ядро Линукс. Не знаю какие ам результаты
> Не знаю какие там результатыВ коде множество строчек, предположительно на Си
> Не знаю какие там результатыОсвоено!
>> Не знаю какие там результаты
> Освоено!А остальные мелочи проверять всё равно никто не будет.
> Не знаю какие там результатыСам написал: 15 миллионов рублей
Любопытно. Прилагательное "математическое" как красная тряпка для местного населения. Любопытно почему, потому что никто не знает математики, или потому что все знают и раз по десять наступили на грабли неприменимости математики к реальной жизни?
Всё как обычно - мгновенное и "глубоко компетентное" суждение о ранее незнакомом предмете при его поверхностном обзоре. Выше в комментах в PDF-ке в разделе References есть достаточно интересные документы. Особенно из свежих.
Что нарылось при беглом обзоре некоторых из них:
- С-шные функции перед реализацией пишутся на языке типа Haskell (есть на него ссылки в доках) - походу функциональный стиль рулит.
- Любые конструкции языка приводящие к сайд-эффектам либо не используются вовсе, либо имеют ограниченное применение.
- Работа с типами, выделением памяти, IPC, threading и пр. объекты проверяются матаппаратом и в случае нессответствия вручную оптимизируются (вроде так)
- Для верификации кода юзают какой-то хитрый комплекс Isabella/HOL
- Плюс еще очень много мат.теории - надо копать в доках до просветления.
Может где-то и ошибаюсь, поправьте предметно...
маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство, как все надежно и круто, "на бумаге"
сразу вспоминается про миникс, который круче чем яйца через 5 мин варки, "на бумаге"
> маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство,
> как все надежно и круто, "на бумаге"
> сразу вспоминается про миникс, который круче чем яйца через 5 мин варки,
> "на бумаге"Дeбил, GD знаешь, чем занимается? Ах, не знаешь, у них сайта нет.... Знаешь, почему?
Это ты дебил. Их деятельность практически ничем не знаменательна, обычная оборонка. Портачат там всего лишь чуть меньше, чем в остальных отраслях. Никакими сверхфантастическими проектами, которые сегодня кажутся сказкой, а лет через 50 будут обыденностью, там тоже не занимаются. Айти это не конёк оборонки, запомни, обезъяна.
таки нет ? http://www.gdc4s.com/
и почему же нет у них сайта ...
феназепанчика тяпни
Множество ошибок просто отсутствует!
>выносом частей для управления ресурсами ядра в пространство пользователяНе понимаю, то есть драйвера будут выполняться что ли от простого пользователя? И как это повышает устойчивость к сбоям и безопасность?
Заметил, что в инете десятки статей о преимуществах микроядра и почти ни одной о недостатках. Хотя сомнительно, что их нет. Это что-то вроде святого грааля или вечного двигателя?
Очевидно одно: все эти "свежие идеи" вроде микроядра, все зависимости внутри одного пакета однозначно выгодны проприерастам. Подозреваю, что цель сделать все по на машине пользователя кроме наноядра максимально независимым от системы и самого пользователя. Так легче внедрять бэкдоры и продавать проприетарщину.
При падении драйвера ядро его перезапустит. Полезно, если в драйвере есть редко срабатывающий баг или переинициализация железа может помочь. На этом всё. Если драйвер вылетает из-за сбоя железа, который программно не исправить, то пользы от этого ровным счетом никакой. Про безопасность же в смысле security вообще речи не идет.
В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их сам могу останавливать/запускать в линуксе вручную или через скрипты и у меня ничего не падает, почему бы не реализовать эту функцию в ядре. Если конечно это ничему не повредит.Вот и напишите статью о недостатках микроядра, чтобы страдальцам виндовс и им сочувствующим жизнь медом не казалась.
> В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их
> сам могу останавливать/запускать в линуксе вручную или через скрипты и у
> меня ничего не падает, почему бы не реализовать эту функцию в
> ядре. Если конечно это ничему не повредит.
> Вот и напишите статью о недостатках микроядра, чтобы страдальцам виндовс и им
> сочувствующим жизнь медом не казалась.Все монолитное ядро с драйверами работает в одном адресном пространстве, и если в драйвере изза ошибки что-то пишется не туда, то кернелепаник и бб, при чем тут перезапуск модулей?
Ядро линукс построено вольно-невольно по аналогии с ЦНС, есть гематоэнцефалический барьер между кернелспейс и юзерспейс, Модули как навыки и знания, хранятся они не в желудке, а рядом с ядром. Представляю если бы одна моя мысль напрямую общалась с другой минуя координационный центр. Это называется шизофрения. :) Если у вас уже есть серьезный баг в мозгах то перезапуск не поможет и не нужен.
Извиняюсь за лирическое отступление :))
Или вот еще такое сравнение. Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))Бредишь? Про повышение привилегий под linux не слышал?
>>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
> Бредишь? Про повышение привилегий под linux не слышал?Не расстраивайся :)
>>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
> Бредишь? Про повышение привилегий под linux не слышал?В микроядре повышение привилегий стандартная процедура.
...but in Soviet Russia, you deny to the microkernel.
> Заметил, что в инете десятки статей о преимуществах микроядра и почти ни
> одной о недостатках.Читайте внимательнее эти же статьи, основные недостатки, как минимум - просевшая производительность и увеличивающаяся сложность process interconnection.
Поясните дураку, а че они сделали ядро надежным,доказали математически, а торвальдс не сделал этого?
Если брать аналогии, то почитай в википедии про "Гравитационная задача N тел". У этих ребят случай аналогичный задаче трех тел. А вот linux является аналогом задачи с на порядки большим количеством тел, причем количество тел продолжает постоянно увеличиваться, то есть на данном уровне развития математики не может быть решенным в аналитическом виде.
По этой аналогии любая ос состоит из большого количества тел. И очередное микроядро - просто повод денег содрать и ничего более.
> По этой аналогии любая ос состоит из большого количества тел. И очередное
> микроядро - просто повод денег содрать и ничего более.Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что баги при этом будут вне оного. Т.к. вся функциональность - вне оного. Правда большой вопрос насколько это является достоинством.
>> По этой аналогии любая ос состоит из большого количества тел. И очередное
>> микроядро - просто повод денег содрать и ничего более.
> Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что
> баги при этом будут вне оного. Т.к. вся функциональность - вне
> оного. Правда большой вопрос насколько это является достоинством.Raytheon смотрит на вас всех, как на гогно. Сечешь? ТАМ не нужна функциональность пингвина.
А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать?
скорей всего прикрутят к opensuse, как это было с прежним L4.
> А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать?На Хеллфайрах работает. Ну и на других продуктах Raytheon.
Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если львиная доля безопасности обеспечивается вне ядра?
> Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется
> в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если
> львиная доля безопасности обеспечивается вне ядра?Сайдуиндеру безопасность ПО ГСН ни к чему, как ты понимаешь. Да?
> Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется
> в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если
> львиная доля безопасности обеспечивается вне ядра?Отдельные процессы не имеют прямого доступа друг к другу, поэтому тот факт, что какой-нибудь авторизатор крутится, условно, в отдельном процессе и под отдельным UID'ом, не делает его более уязвимым, чем если бы он был в ядре. Скорее даже наоборот, делает менее уязвимым, за счёт ограничения доступного ему пространства.
пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а потом грузим на этом ядре процессом другое ядро( Linux) в которое никто и никогда из математиков не заглядывал :)
Смешанная или смешная ОС получилась!
Но если ядро будет падать каждые 10 минут, то и на этом супернадёжном ядре процесс с Линукс будет виснуть каждые 10 минут, вот только в случае с обычным сервером его перезапускать нужно в ручную, то тут можно настроить и всё будет происходить автоматически.Из часа такой комп проработает 50 минут пусть. А обычный Линукс только 10 минут из часа. Имеет право жить!
> пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а потом грузим
> на этом ядре процессом другое ядро( Linux) в которое никто и
> никогда из математиков не заглядывал :)
> Смешанная или смешная ОС получилась!Гугль смешной:
Windows NT is a hybrid MicroKernel
The Be OS is a hybrid microkernel and FreeBSD is not
Apple OS X is also a hybrid microkernel.
>> пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а потом грузим
>> на этом ядре процессом другое ядро( Linux) в которое никто и
>> никогда из математиков не заглядывал :)
>> Смешанная или смешная ОС получилась!
> Гугль смешной:
> Windows NT is a hybrid MicroKernel
> The Be OS is a hybrid microkernel and FreeBSD is not
> Apple OS X is also a hybrid microkernel.Боюсь, чувак, это вы все смешны в вашем уютненьком. Вы вообще что-то кроме оффтопика-пингвина видели IRL?
> Боюсь, чувак, это вы все смешны в вашем уютненьком. Вы вообще что-то
> кроме оффтопика-пингвина видели IRL?Ефрейтор, *СРОЧНО* пройдите в первый отдел.