The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]

Сверхнадёжное ядро seL4 будет переведено в разряд открытых проектов

24.06.2014 23:55

Компания General Dynamics C4 Systems и австралийский исследовательский центр NICTA анонсировали скорый перевод микроядра seL4 (Secure Embedded L4) в категорию открытых проектов. Ядро seL4 нацелено на предоставление повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире.

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

  1. Главная ссылка к новости (https://news.ycombinator.com/i...)
  2. OpenNews: На базе гипервизора seL4 создана платформа для создания высокозащищённых систем
  3. OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
  4. OpenNews: Релиз открытой микроядерной ОС Genode 13.11
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/40075-sel4
Ключевые слова: sel4
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (100) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.3, Аноним (-), 00:31, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +22 +/
    ждём внесения ошибок сообществом!
     
     
  • 2.48, Аноним (-), 11:51, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –3 +/
    ...полутора землекопов. Сколько участников сообщества живет в сверхнадежном подземном бункере на глубине километра? Примерно столько же, если не меньше, будет коммитить в сверхнадежное ядро.
     

  • 1.5, Зевака (?), 00:41, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    А в чем заключалось математическое обоснование?
     
     
  • 2.9, pavlinux (ok), 01:00, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +8 +/
    > А в чем заключалось математическое обоснование?

    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.

    Короча, как у Ферма: "- Я нашёл поистине замечательное доказательство этого факта, но поля этой книги слишком малы, чтобы его уместить." :)

     
  • 2.46, sashka_ua (?), 11:17, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Обычно, математическое доказательство кода состоит в том, что доказывается, что программа в результате выполнения кода может иметь строго ограниченные набор желаемых состояний и не может выйти за пределы этого множества.

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

     
     
  • 3.78, Сергей (??), 16:34, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > не нивелирует багов компилятора, космических лучей, багов железа и вообще надеятся на абсолютную надежность ПО - глупость.

    Голову от падения кирпича оно тоже не спасёт.

     
     
  • 4.95, Серж (??), 18:25, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    А ежели кирпич уже упал? Спасёт?
     
     
  • 5.113, Сергей (??), 14:49, 26/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Да. А если принять внутрь и от изжоги помогает ;-)
     
  • 3.110, Аноним (-), 10:21, 26/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Гёдель смотрит с ухмылкой.
     
  • 3.114, yantux (??), 18:28, 26/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    На это надеяться не надо, это надо обеспечивать.
     
  • 2.50, Аноним (-), 11:53, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +7 +/
    > А в чем заключалось математическое обоснование?

    В том что если деградировать ядро до примитивного тасксвичера - в нем, конечно, багов не будет. Это даже можно формально доказать. Просто баги будут в других местах кода. Так что радости то с того, учитывая что само по себе такое "ядро" не умеет ни-че-го?

     
  • 2.79, Pasha (??), 17:01, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    В теории надежности, если кто-нибудь из отпостившихся "критиков" вообще знает что это такое.
    В случае системы с последовательным соединением элементов, надежность системы в целом будет определяться произведением надежностей(вероятность безотказной работы) каждого из звеньев системы. Это грубая формулировка, отражающая сущность повышения надежности системы за счет одного из звеньев. Самоучкам программистам и сисадминам, при всем моем  уважении к их роли в общем научно-техническом прогрессе, немного не хватает базового образования. Ищем на просторах тырнета "Теория надежности" и восполняем пробелы в образовании. Весьма полезная дисциплина.
     
     
  • 3.80, Pasha (??), 17:08, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Простой пример, если у вас операционка, которая работает "через раз" (надежность = 0.5), железо, которое работает "через раз" и пользовательская программа, работающая "через раз".
    То в результате надежность системы в целом будет 0.5*3 - 0.125, а если операционка очень надежная (0.99), то надежность системы будет 0.248. Т.е. в последнем случае система в целом будет надежнее практически в два раза, и разработчик посвятит свое время поиску косяков в куда меньшем количестве узлов отказа.
     
     
  • 4.81, Pasha (??), 17:10, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    P.S. В предыдущем "примере" 0.5*3 - ошибка. должно быть 0.5^3
     
  • 2.112, Anonymouse (?), 13:02, 26/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Доказали что ядро содержит те же ошибки что и спецификация.
     

  • 1.6, Аноним (-), 00:47, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего. Для Ъ хотелось бы какой-нибудь более подробной инфы.
     
     
  • 2.8, dr Equivalent (ok), 00:56, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Поэтому оно такое сверхнадежное.
     
  • 2.38, Нанобот (ok), 09:58, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    так и будет. и предназначено оно будет для решения специализированых задач на всяких-там микроконтроллерах. маловероятно, что в ближайшее время с него можно будет по интырнетам лазить
     
  • 2.51, Аноним (-), 11:54, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего.

    Ну так в hello world тоже багов не очень много. Хотя, конечно, от програмера зависит.

     

  • 1.7, pavlinux (ok), 00:47, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Ждём код, будем проверять :)
     
  • 1.10, Аноним (-), 01:01, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    для него даже багтрекер не нужен
     
     
  • 2.12, pavlinux (ok), 01:20, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +6 +/
    Ниже на писан код самой безопасной ОСь во Вселенной!

    --- cut here ---

    --- end cut here ---

     
     
  • 3.26, Аноним (-), 06:50, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +18 +/
    Я это вбросил в perl ... так оно мне linux на FreeBSD переустановило ...
    СволочЪ ты павлин :(
     

  • 1.11, Xasd (ok), 01:19, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным.

    тыг ведь видов ошибок можно допустить -- намного-много больше :-)

    как минимум -- вот например что часто бывает:

    * состояние гонки. в той или иной форме -- невероятно-частая ошибка.

    * некорректная проверка источника событий. (или вообще забывают проверять источник -- а сразу выполняют действие связанное с событием).

    * утечка ресурсов. например утечка может быть связана с неполным алгоритмом учёта состояния ресурсного объекта  (например: алгоритм -- учитывает не все возможные ситуации.. такое бывает СВЕХ-часто в ПО).

     
     
  • 2.14, pavlinux (ok), 01:24, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >... вот например что часто бывает

    PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf

     
     
  • 3.16, Xasd (ok), 01:26, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +4 +/
    >>... вот например что часто бывает
    > PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf

    нет :)

    я сразу комментировать

     
     
  • 4.17, pavlinux (ok), 01:32, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >>>... вот например что часто бывает
    >> 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 в ядро вкорячили.

     
  • 2.15, Аноним (-), 01:25, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    и ещё при верификации этой кодлой лентяев аспирантов можно допустить ещё больше ошибок. Главное же что статьи будут написаны и в журналы разосланы.
     
     
  • 3.18, kuku (?), 01:48, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Поддерживаю.
    Интересно: какой был бюджет этого исследования ?
    И что им обещали в конце исследования ?
    Насколько реально практическое применение этого ядра ?

    Люди годами пишут сложные ядра(например ядро Linux),
    а тут они взяли и написали ядро, которое не имеет ошибок.
    Как-то звучит "натянуто".
    Похоже эта теория "далека" от практики.

    Насколько оно уступает по сложности ядру Linux ?

     
     
  • 4.24, Аноним (-), 04:55, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD
     
     
  • 5.52, Аноним (-), 12:00, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > А ведь вам говорили, что ядро в виде монолитного куска кода плохая
    > идея XD

    Все относительно в матрице. Что есть монолитность, и как определить ее. Это всего лишь абстракция, а не реальная каменная субстанция. Что такое "кусок кода", опять абстракция.
    Даже если человеку отпилить руку, он необязательно умрет. вроде кажется что он монолитный на вид. Но не все что кажется на первый слепой взгляд монолитным на самом деле такое.

     
  • 5.70, Аноним (-), 15:58, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD

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

     
     
  • 6.84, Аноним (-), 17:39, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >> А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD
    > Да, было дело - Таненбаум критиковал когда-то. И где сейчас миникс и
    > где линукс? К слову, монолитность - понятие относительное.

    "Побеждает не самое технически совершенное решение. Пример - Чикака-95"

     
     
  • 7.104, Аноним (-), 20:41, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    технически совершенное решение побеждает всегда если оно есть. Реальность такова, что хоть как-то юзабильное монолитное GP ядро есть с некоторыми недостатками, а совершенного микроядра нет. Есть только ещё более убогие попытки сделать такое ядро.
     
  • 4.27, Аноним (-), 07:13, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Не имеет ошибок и ничего не умеет, а когда научится, проявятся и ошибки, и куча микроядерных проблем.
     
     
  • 5.36, Аноним (-), 09:20, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    А что должно уметь микроядро помимо выноса всего в пользовательское пространство?
     
     
  • 6.40, Аноним (-), 10:36, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > А что должно уметь микроядро помимо выноса всего в пользовательское пространство?

    Вот-вот отсутствие ошибок не является преимуществом микроядерной архитектуры как пытаются выдать. В формуле 2+2=4 трудно сделать ошибку, но и пользы от нее большой нет.

     
  • 6.44, Аноним (-), 10:53, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А что должно уметь микроядро помимо выноса всего в пользовательское пространство?

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

     
     
  • 7.66, Demo (??), 15:10, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Вы сознательно обманываете людей. Когда говорите о недостатках линукса

    Busted. Ты сам начал. До тебя о линуксе никто не вспоминал.

     
     
  • 8.68, Аноним (-), 15:34, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Так суть микроядра в том и состоит, что падение драйверов не рушит всю систему... текст свёрнут, показать
     
     
  • 9.71, Аноним (-), 15:59, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    В том же пингвине драйверы не так уж часто именно падают Чаще просто глючная ра... текст свёрнут, показать
     
  • 6.105, Аноним (-), 20:42, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А что должно уметь микроядро помимо выноса всего в пользовательское пространство?

    должно назначить виновного из юзерспейса за все дальнешие проблемы с системой.

     
  • 4.35, Аноним (-), 09:19, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    > Люди годами пишут сложные ядра(например ядро Linux),

    а тут они взяли и написали ядро

    L4 писали не годами? Срыв покровов.

     
  • 4.103, Аноним (-), 20:39, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Люди годами пишут сложные ядра(например ядро Linux),

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

    это разного уровня адра. Для критических систем ядра урезаны и узкоспециализированны, это тупо меньше SLOC.

     
     
  • 5.109, kuku (?), 01:10, 26/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    ... и железо там изготовлено из других материалов, по другой технологии и
    имеет логику самоконтроля на аппаратном уровне и помимо этого дублируется.
     

  • 1.13, Аноним (-), 01:23, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире.

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

     
     
  • 2.19, kuku (?), 01:51, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Когда человеком руководит страсть - он способен на многое,
    но он теряет здравомыслие.
     

  • 1.20, anonymus (?), 02:11, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    А сколько лет этому seL4? Когда оно было написано и проверено в последний раз?
     
     
  • 2.86, Аноним (-), 17:40, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > А сколько лет этому seL4? Когда оно было написано и проверено в
    > последний раз?

    Дурeнь, посмотри, КТО его использует. Тебе название General Dynamics ни о чем не говорит, не?

     
     
  • 3.106, Аноним (-), 20:46, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    это те самые перцы у которых f-16 при пересечении уровня моря в IL переворачивался вверх ногами? Да, говорит о многом. Но я точно не помню что там конкретно было, их f-16 или не их f-15
     

  • 1.23, chinarulezzz (ok), 03:55, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    >основание считать решения на базе seL4 самыми надёжными в мире

    оно на С/С++ написано?)

    P.S. Радует пополнение в мире опенсурса.

     
     
  • 2.98, pavlinux (ok), 19:13, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > оно на С/С++ написано?)

    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

     

  • 1.25, Crazy Alex (ok), 06:08, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Я, конечно, не в теме. Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной) модели железа, на котором это будет крутиться? Что, понятное дело, нереально.

    То есть, вероятно, математические доказательства корректности - это интересное упражнение, но для практики не больше ли пользы в хорошем покрытии юнит-тестами и основательном объеме fuzzy-тестирования?

     
     
  • 2.39, Ordu (ok), 10:29, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Не должно В идеале так надо было бы, конечно Но если играть в идеалистов, т... большой текст свёрнут, показать
     
     
  • 3.45, абыр (ok), 10:55, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.

    Зевая... серебряной пули нет.

     
     
  • 4.49, Ordu (ok), 11:51, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >> Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.
    > Зевая... серебряной пули нет.

    Я разве говорил что-то о серебряной пуле? Перечитайте и не говорите глупостей.

     
     
  • 5.65, абыр (ok), 14:44, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Подобную белиберду про грядущую ненужность программистов за последние тридцать лет по поводу чего только не писали. А пуля все не с места.
     
     
  • 6.73, Ordu (ok), 16:04, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ой, да ладно вам Настоящие программисты tm вымирали динозаврами уже не раз В... большой текст свёрнут, показать
     
  • 3.56, жабабыдлокодер (ok), 12:56, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ну, так спецификации программисты и будут писать. Те, кто вовремя переучатся, и молодняк, который этому сразу будет учиться. Разница то какая?
     
     
  • 4.58, Ordu (ok), 14:09, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ааа, вы про это Ну, во-первых, не надо особо зацикливаться на этой теме, я её о... большой текст свёрнут, показать
     

  • 1.28, Packuh (?), 07:20, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Оно было надежным пока было закрыто и никто о нем не знал. Ждем патчей. welcome to the real world.
     
  • 1.29, Packuh (?), 07:21, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    ах да и самый надежный секрет тот о котором знает только один.
     
  • 1.30, DmA (??), 07:37, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Микроядро математически прошедшее проверку  просто исполняет ядро Линукс как один и процессов. В ядре Линукс и драйвера и всё остальное , и его-то никто и не проверял! В России тоже был тендер, на 15 миллионов рублей, который должен был проверить ядро Линукс. Не знаю какие ам результаты
     
     
  • 2.37, Аноним (-), 09:22, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Не знаю какие там результаты

    В коде множество строчек, предположительно на Си

     
  • 2.96, Серж (??), 18:27, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Не знаю какие там результаты

    Освоено!


     
     
  • 3.97, Серж (??), 18:29, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >> Не знаю какие там результаты
    > Освоено!

    А остальные мелочи проверять всё равно никто не будет.

     

  • 1.31, milkman (?), 08:13, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    > Не знаю какие там результаты

    Сам написал: 15 миллионов рублей

     
  • 1.32, Ordu (ok), 08:55, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Любопытно. Прилагательное "математическое" как красная тряпка для местного населения. Любопытно почему, потому что никто не знает математики, или потому что все знают и раз по десять наступили на грабли неприменимости математики к реальной жизни?
     
     
  • 2.94, hummermania (ok), 17:57, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Всё как обычно - мгновенное и "глубоко компетентное" суждение о ранее незнакомом предмете при его поверхностном обзоре. Выше в комментах в PDF-ке в разделе References есть достаточно интересные документы. Особенно из свежих.
    Что нарылось при беглом обзоре некоторых из них:
      - С-шные функции перед реализацией пишутся на языке типа Haskell (есть на него ссылки в доках) - походу функциональный стиль рулит.
      - Любые конструкции языка приводящие к сайд-эффектам либо не используются вовсе, либо имеют ограниченное применение.
      - Работа с типами, выделением памяти, IPC, threading и пр. объекты проверяются матаппаратом и в случае нессответствия вручную оптимизируются (вроде так)
      - Для верификации кода юзают какой-то хитрый комплекс Isabella/HOL
      - Плюс еще очень много мат.теории - надо копать в доках до просветления.
    Может где-то и ошибаюсь, поправьте предметно...
     

  • 1.33, Аноним (-), 08:59, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство, как все надежно и круто, "на бумаге"
    сразу вспоминается про миникс, который круче чем яйца через 5 мин варки, "на бумаге"
     
     
  • 2.88, Аноним (-), 17:43, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство,
    > как все надежно и круто, "на бумаге"
    > сразу вспоминается про миникс, который круче чем яйца через 5 мин варки,
    > "на бумаге"

    Дeбил, GD знаешь, чем занимается? Ах, не знаешь, у них сайта нет.... Знаешь, почему?

     
     
  • 3.107, all_glory_to_the_hypnotoad (ok), 21:03, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Это ты дебил. Их деятельность практически ничем не знаменательна, обычная оборонка. Портачат там всего лишь чуть меньше, чем в остальных отраслях. Никакими сверхфантастическими проектами, которые сегодня кажутся сказкой, а лет через 50 будут обыденностью, там тоже не занимаются. Айти это не конёк оборонки, запомни, обезъяна.
     
  • 3.108, Аноним (-), 23:13, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    таки нет ? http://www.gdc4s.com/
    и почему же нет у них сайта ...
    феназепанчика тяпни
     

  • 1.34, iuy (?), 09:16, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Множество ошибок просто отсутствует!
     
  • 1.41, Аноним (-), 10:37, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    >выносом частей для управления ресурсами ядра в пространство пользователя

    Не понимаю, то есть драйвера будут выполняться что ли от простого пользователя? И как это повышает устойчивость к сбоям и безопасность?
    Заметил, что в инете десятки статей о преимуществах микроядра и почти ни одной о недостатках. Хотя сомнительно, что их нет. Это что-то вроде святого грааля или вечного двигателя?
    Очевидно одно: все эти "свежие идеи" вроде микроядра, все зависимости внутри одного пакета однозначно выгодны проприерастам. Подозреваю, что цель сделать все по на машине пользователя кроме наноядра максимально независимым от системы и самого пользователя. Так легче внедрять бэкдоры и продавать проприетарщину.

     
     
  • 2.55, angra (ok), 12:48, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    При падении драйвера ядро его перезапустит. Полезно, если в драйвере есть редко срабатывающий баг или переинициализация железа может помочь. На этом всё. Если драйвер вылетает из-за сбоя железа, который программно не исправить, то пользы от этого ровным счетом никакой. Про безопасность же в смысле security вообще речи не идет.


     
     
  • 3.57, Аноним (-), 13:41, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их сам могу останавливать/запускать в линуксе вручную или через скрипты и у меня ничего не падает, почему бы не реализовать эту функцию в ядре. Если конечно это ничему не повредит.

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

     
     
  • 4.69, Аноним (-), 15:43, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их
    > сам могу останавливать/запускать в линуксе вручную или через скрипты и у
    > меня ничего не падает, почему бы не реализовать эту функцию в
    > ядре. Если конечно это ничему не повредит.
    > Вот и напишите статью о недостатках микроядра, чтобы страдальцам виндовс и им
    > сочувствующим жизнь медом не казалась.

    Все монолитное ядро с драйверами работает в одном адресном пространстве, и если в драйвере изза ошибки что-то пишется не туда, то кернелепаник и бб, при чем тут перезапуск модулей?

     
  • 3.60, Аноним (-), 14:23, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –3 +/
    Ядро линукс построено вольно-невольно по аналогии с ЦНС, есть гематоэнцефалический барьер между кернелспейс и юзерспейс, Модули как навыки и знания, хранятся они не в желудке, а рядом с ядром. Представляю если бы одна моя мысль напрямую общалась с другой минуя координационный центр. Это называется шизофрения. :) Если у вас уже есть серьезный баг в мозгах то перезапуск не поможет и не нужен.
    Извиняюсь за лирическое отступление :))

     
  • 3.61, Аноним (-), 14:28, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Или вот еще такое сравнение. Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))


     
     
  • 4.62, Andrey Mitrofanov (?), 14:30, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))

    Бредишь? Про повышение привилегий под linux не слышал?

     
     
  • 5.63, Аноним (-), 14:32, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
    > Бредишь? Про повышение привилегий под linux не слышал?

    Не расстраивайся :)

     
  • 5.64, Аноним (-), 14:35, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
    > Бредишь? Про повышение привилегий под linux не слышал?

    В микроядре повышение привилегий стандартная процедура.

     
     
  • 6.67, Andrey Mitrofanov (?), 15:33, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    ...but in Soviet Russia, you deny to the microkernel.
     
  • 2.77, anonymous (??), 16:19, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Заметил, что в инете десятки статей о преимуществах микроядра и почти ни
    > одной о недостатках.

    Читайте внимательнее эти же статьи, основные недостатки, как минимум - просевшая производительность и увеличивающаяся сложность process interconnection.

     

  • 1.42, odity (?), 10:38, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Поясните дураку, а че они сделали ядро надежным,доказали математически, а торвальдс не сделал этого?
     
     
  • 2.53, angra (ok), 12:41, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Если брать аналогии, то почитай в википедии про "Гравитационная задача N тел". У этих ребят случай аналогичный задаче трех тел. А вот linux является аналогом задачи с на порядки большим количеством тел, причем количество тел продолжает постоянно увеличиваться, то есть на данном уровне развития математики не может быть решенным в аналитическом виде.
     
     
  • 3.59, Аноним (-), 14:14, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    По этой аналогии любая ос состоит из большого количества тел. И очередное микроядро - просто повод денег содрать и ничего более.


     
     
  • 4.72, Аноним (-), 16:01, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > По этой аналогии любая ос состоит из большого количества тел. И очередное
    > микроядро - просто повод денег содрать и ничего более.

    Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что баги при этом будут вне оного. Т.к. вся функциональность - вне оного. Правда большой вопрос насколько это является достоинством.

     
     
  • 5.89, Аноним (-), 17:45, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >> По этой аналогии любая ос состоит из большого количества тел. И очередное
    >> микроядро - просто повод денег содрать и ничего более.
    > Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что
    > баги при этом будут вне оного. Т.к. вся функциональность - вне
    > оного. Правда большой вопрос насколько это является достоинством.

    Raytheon смотрит на вас всех, как на гогно. Сечешь? ТАМ не нужна функциональность пингвина.

     

  • 1.43, Аноним (-), 10:39, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать?
     
     
  • 2.74, fi (ok), 16:04, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    скорей всего прикрутят к opensuse, как это было с прежним L4.
     
  • 2.90, Аноним (-), 17:45, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать?

    На Хеллфайрах работает. Ну и на других продуктах Raytheon.

     

  • 1.54, Аноним (-), 12:46, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если львиная доля безопасности обеспечивается вне ядра?
     
     
  • 2.91, Аноним (-), 17:46, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется
    > в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если
    > львиная доля безопасности обеспечивается вне ядра?

    Сайдуиндеру безопасность ПО ГСН ни к чему, как ты понимаешь. Да?

     
  • 2.100, Аноним (-), 20:07, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется
    > в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если
    > львиная доля безопасности обеспечивается вне ядра?

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

     

  • 1.75, DmA (??), 16:08, 25/06/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим на этом ядре процессом другое ядро( Linux) в которое никто и никогда из математиков не заглядывал :)
    Смешанная или смешная ОС получилась!
    Но если ядро будет падать каждые 10 минут, то и на этом супернадёжном ядре процесс с Линукс будет виснуть каждые 10 минут, вот только в случае с обычным сервером его перезапускать нужно в ручную, то тут можно настроить и всё будет происходить автоматически.Из часа такой комп проработает 50 минут пусть. А обычный Линукс только 10 минут из часа. Имеет право жить!
     
     
  • 2.76, Andrey Mitrofanov (?), 16:16, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим
    > на этом ядре процессом другое ядро( 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.

     
     
  • 3.92, Аноним (-), 17:46, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    >> пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим
    >> на этом ядре процессом другое ядро( 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?

     
     
  • 4.93, Andrey Mitrofanov (?), 17:54, 25/06/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Боюсь, чувак, это вы все смешны в вашем уютненьком. Вы вообще что-то
    > кроме оффтопика-пингвина видели IRL?

    Ефрейтор, *СРОЧНО* пройдите в первый отдел.

     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2024 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру