форумы  помощь  поиск  регистрация  майллист  вход/выход  слежка

Вариант для распечатки		Пред. тема | След. тема
Форум Разговоры, обсуждение новостей
Изначальное сообщение		[ Отслеживать ]

"Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от opennews (ok) on 25-Июн-14, 00:22
Компания General Dynamics C4 Systems (http://en.wikipedia.org/wiki/General_Dynamics_C4_Systems)  и австралийский исследовательский центр 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
Ответить | Правка | Cообщить модератору

Сообщения по теме

[Сортировка по времени | RSS]

3. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+22 +/–
Сообщение от Аноним (??) on 25-Июн-14, 00:31
ждём внесения ошибок сообществом!
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	48. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–3 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 11:51
	...полутора землекопов. Сколько участников сообщества живет в сверхнадежном подземном бункере на глубине километра? Примерно столько же, если не меньше, будет коммитить в сверхнадежное ядро.
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

5. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от Зевака on 25-Июн-14, 00:41
А в чем заключалось математическое обоснование?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	9. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+8 +/–
	Сообщение от pavlinux (ok) on 25-Июн-14, 01:00
	> А в чем заключалось математическое обоснование? 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. Короча, как у Ферма: "- Я нашёл поистине замечательное доказательство этого факта, но поля этой книги слишком малы, чтобы его уместить." :)
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

	46. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+3 +/–
	Сообщение от sashka_ua on 25-Июн-14, 11:17
	Обычно, математическое доказательство кода состоит в том, что доказывается, что программа в результате выполнения кода может иметь строго ограниченные набор желаемых состояний и не может выйти за пределы этого множества. Что не нивелирует багов компилятора, космических лучей, багов железа и вообще надеятся на абсолютную надежность ПО - глупость.
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

	78. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Сергей (??) on 25-Июн-14, 16:34
	> не нивелирует багов компилятора, космических лучей, багов железа и вообще надеятся на абсолютную надежность ПО - глупость. Голову от падения кирпича оно тоже не спасёт.
	Ответить | Правка | ^ к родителю #46 | Наверх | Cообщить модератору

	95. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Серж (??) on 25-Июн-14, 18:25
	А ежели кирпич уже упал? Спасёт?
	Ответить | Правка | ^ к родителю #78 | Наверх | Cообщить модератору

	113. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Сергей (??) on 26-Июн-14, 14:49
	Да. А если принять внутрь и от изжоги помогает ;-)
	Ответить | Правка | ^ к родителю #95 | Наверх | Cообщить модератору

	110. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 26-Июн-14, 10:21
	Гёдель смотрит с ухмылкой.
	Ответить | Правка | ^ к родителю #46 | Наверх | Cообщить модератору

	114. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от yantux (??) on 26-Июн-14, 18:28
	На это надеяться не надо, это надо обеспечивать.
	Ответить | Правка | ^ к родителю #46 | Наверх | Cообщить модератору

	50. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+7 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 11:53
	> А в чем заключалось математическое обоснование? В том что если деградировать ядро до примитивного тасксвичера - в нем, конечно, багов не будет. Это даже можно формально доказать. Просто баги будут в других местах кода. Так что радости то с того, учитывая что само по себе такое "ядро" не умеет ни-че-го?
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

	79. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+3 +/–
	Сообщение от Pasha (??) on 25-Июн-14, 17:01
	В теории надежности, если кто-нибудь из отпостившихся "критиков" вообще знает что это такое. В случае системы с последовательным соединением элементов, надежность системы в целом будет определяться произведением надежностей(вероятность безотказной работы) каждого из звеньев системы. Это грубая формулировка, отражающая сущность повышения надежности системы за счет одного из звеньев. Самоучкам программистам и сисадминам, при всем моем  уважении к их роли в общем научно-техническом прогрессе, немного не хватает базового образования. Ищем на просторах тырнета "Теория надежности" и восполняем пробелы в образовании. Весьма полезная дисциплина.
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

	80. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Pasha (??) on 25-Июн-14, 17:08
	Простой пример, если у вас операционка, которая работает "через раз" (надежность = 0.5), железо, которое работает "через раз" и пользовательская программа, работающая "через раз". То в результате надежность системы в целом будет 0.5*3 - 0.125, а если операционка очень надежная (0.99), то надежность системы будет 0.248. Т.е. в последнем случае система в целом будет надежнее практически в два раза, и разработчик посвятит свое время поиску косяков в куда меньшем количестве узлов отказа.
	Ответить | Правка | ^ к родителю #79 | Наверх | Cообщить модератору

	81. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Pasha (??) on 25-Июн-14, 17:10
	P.S. В предыдущем "примере" 0.5*3 - ошибка. должно быть 0.5^3
	Ответить | Правка | ^ к родителю #80 | Наверх | Cообщить модератору

	112. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Anonymouse on 26-Июн-14, 13:02
	Доказали что ядро содержит те же ошибки что и спецификация.
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

6. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Аноним (??) on 25-Июн-14, 00:47
Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего. Для Ъ хотелось бы какой-нибудь более подробной инфы.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	8. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+3 +/–
	Сообщение от dr Equivalent (ok) on 25-Июн-14, 00:56
	Поэтому оно такое сверхнадежное.
	Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

	38. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
	Сообщение от Нанобот (ok) on 25-Июн-14, 09:58
	так и будет. и предназначено оно будет для решения специализированых задач на всяких-там микроконтроллерах. маловероятно, что в ближайшее время с него можно будет по интырнетам лазить
	Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

	51. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 11:54
	> Подозреваю что поддерживает это свернадежное ядро чуть более чем ничего. Ну так в hello world тоже багов не очень много. Хотя, конечно, от програмера зависит.
	Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

7. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от pavlinux (ok) on 25-Июн-14, 00:47
Ждём код, будем проверять :)
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

10. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+3 +/–
Сообщение от Аноним (??) on 25-Июн-14, 01:01
для него даже багтрекер не нужен
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	12. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+6 +/–
	Сообщение от pavlinux (ok) on 25-Июн-14, 01:20
	Ниже на писан код самой безопасной ОСь во Вселенной! --- cut here --- --- end cut here ---
	Ответить | Правка | ^ к родителю #10 | Наверх | Cообщить модератору

	26. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+18 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 06:50
	Я это вбросил в perl ... так оно мне linux на FreeBSD переустановило ... СволочЪ ты павлин :(
	Ответить | Правка | ^ к родителю #12 | Наверх | Cообщить модератору

11. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Xasd (ok) on 25-Июн-14, 01:19
> Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным. тыг ведь видов ошибок можно допустить -- намного-много больше :-) как минимум -- вот например что часто бывает: * состояние гонки. в той или иной форме -- невероятно-частая ошибка. * некорректная проверка источника событий. (или вообще забывают проверять источник -- а сразу выполняют действие связанное с событием). * утечка ресурсов. например утечка может быть связана с неполным алгоритмом учёта состояния ресурсного объекта  (например: алгоритм -- учитывает не все возможные ситуации.. такое бывает СВЕХ-часто в ПО).
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	14. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от pavlinux (ok) on 25-Июн-14, 01:24
	>... вот например что часто бывает PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
	Ответить | Правка | ^ к родителю #11 | Наверх | Cообщить модератору

	16. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+4 +/–
	Сообщение от Xasd (ok) on 25-Июн-14, 01:26
	>>... вот например что часто бывает > PDFку прочел? http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf нет :) я сразу комментировать
	Ответить | Правка | ^ к родителю #14 | Наверх | Cообщить модератору

	17. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от pavlinux (ok) on 25-Июн-14, 01:32
	>>>... вот например что часто бывает >> 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 в ядро вкорячили.
	Ответить | Правка | ^ к родителю #16 | Наверх | Cообщить модератору

	15. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 01:25
	и ещё при верификации этой кодлой лентяев аспирантов можно допустить ещё больше ошибок. Главное же что статьи будут написаны и в журналы разосланы.
	Ответить | Правка | ^ к родителю #11 | Наверх | Cообщить модератору

	18. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от kuku on 25-Июн-14, 01:48
	Поддерживаю. Интересно: какой был бюджет этого исследования ? И что им обещали в конце исследования ? Насколько реально практическое применение этого ядра ? Люди годами пишут сложные ядра(например ядро Linux), а тут они взяли и написали ядро, которое не имеет ошибок. Как-то звучит "натянуто". Похоже эта теория "далека" от практики. Насколько оно уступает по сложности ядру Linux ?
	Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

	24. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 04:55
	А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD
	Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

	52. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 12:00
	> А ведь вам говорили, что ядро в виде монолитного куска кода плохая > идея XD Все относительно в матрице. Что есть монолитность, и как определить ее. Это всего лишь абстракция, а не реальная каменная субстанция. Что такое "кусок кода", опять абстракция. Даже если человеку отпилить руку, он необязательно умрет. вроде кажется что он монолитный на вид. Но не все что кажется на первый слепой взгляд монолитным на самом деле такое.
	Ответить | Правка | ^ к родителю #24 | Наверх | Cообщить модератору

	70. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 15:58
	> А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD Да, было дело - Таненбаум критиковал когда-то. И где сейчас миникс и где линукс? К слову, монолитность - понятие относительное.
	Ответить | Правка | ^ к родителю #24 | Наверх | Cообщить модератору

	84. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:39
	>> А ведь вам говорили, что ядро в виде монолитного куска кода плохая идея XD > Да, было дело - Таненбаум критиковал когда-то. И где сейчас миникс и > где линукс? К слову, монолитность - понятие относительное. "Побеждает не самое технически совершенное решение. Пример - Чикака-95"
	Ответить | Правка | ^ к родителю #70 | Наверх | Cообщить модератору

	104. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 20:41
	технически совершенное решение побеждает всегда если оно есть. Реальность такова, что хоть как-то юзабильное монолитное GP ядро есть с некоторыми недостатками, а совершенного микроядра нет. Есть только ещё более убогие попытки сделать такое ядро.
	Ответить | Правка | ^ к родителю #84 | Наверх | Cообщить модератору

	27. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 07:13
	Не имеет ошибок и ничего не умеет, а когда научится, проявятся и ошибки, и куча микроядерных проблем.
	Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

	36. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 09:20
	А что должно уметь микроядро помимо выноса всего в пользовательское пространство?
	Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

	40. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 10:36
	> А что должно уметь микроядро помимо выноса всего в пользовательское пространство? Вот-вот отсутствие ошибок не является преимуществом микроядерной архитектуры как пытаются выдать. В формуле 2+2=4 трудно сделать ошибку, но и пользы от нее большой нет.
	Ответить | Правка | ^ к родителю #36 | Наверх | Cообщить модератору

	44. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 10:53
	> А что должно уметь микроядро помимо выноса всего в пользовательское пространство? Вы сознательно обманываете людей. Когда говорите о недостатках линукса то берете все ядро вместе с драйверами и всеми модулями. И оцениваете его сбойность. Конечно по сравнению с лопатой у него вероятность сбоев выше. Но это же демагогия. Лопата линукс все равно не заменит. Вы сравниваете несопоставимые вещи. Сравнивать надо совокупность вашего микрочепухи с набором драйверов. авторы конечно молодцы, они доказали, что дваждыдва безошибочно.
	Ответить | Правка | ^ к родителю #36 | Наверх | Cообщить модератору

	66. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Demo (??) on 25-Июн-14, 15:10
	> Вы сознательно обманываете людей. Когда говорите о недостатках линукса Busted. Ты сам начал. До тебя о линуксе никто не вспоминал.
	Ответить | Правка | ^ к родителю #44 | Наверх | Cообщить модератору

	68. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 15:34
	Так суть микроядра в том и состоит, что падение драйверов не рушит всю систему
	Ответить | Правка | ^ к родителю #66 | Наверх | Cообщить модератору

	71. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 15:59
	> Так суть микроядра в том и состоит, что падение драйверов не рушит всю систему В том же пингвине драйверы не так уж часто именно падают. Чаще просто глючная работа с своей периферией. И в этом плане микроядро ничего не даст.
	Ответить | Правка | ^ к родителю #68 | Наверх | Cообщить модератору

	105. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 20:42
	> А что должно уметь микроядро помимо выноса всего в пользовательское пространство? должно назначить виновного из юзерспейса за все дальнешие проблемы с системой.
	Ответить | Правка | ^ к родителю #36 | Наверх | Cообщить модератору

	35. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+2 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 09:19
	> Люди годами пишут сложные ядра(например ядро Linux), а тут они взяли и написали ядро L4 писали не годами? Срыв покровов.
	Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

	103. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 20:39
	> Люди годами пишут сложные ядра(например ядро Linux), а тут они взяли и написали ядро, которое не имеет ошибок. это разного уровня адра. Для критических систем ядра урезаны и узкоспециализированны, это тупо меньше SLOC.
	Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

	109. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от kuku on 26-Июн-14, 01:10
	... и железо там изготовлено из других материалов, по другой технологии и имеет логику самоконтроля на аппаратном уровне и помимо этого дублируется.
	Ответить | Правка | ^ к родителю #103 | Наверх | Cообщить модератору

13. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Аноним (??) on 25-Июн-14, 01:23
> Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире. как же любят люди заблуждаться под покровом математики и технологий.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	19. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от kuku on 25-Июн-14, 01:51
	Когда человеком руководит страсть - он способен на многое, но он теряет здравомыслие.
	Ответить | Правка | ^ к родителю #13 | Наверх | Cообщить модератору

20. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от anonymus on 25-Июн-14, 02:11
А сколько лет этому seL4? Когда оно было написано и проверено в последний раз?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	86. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:40
	> А сколько лет этому seL4? Когда оно было написано и проверено в > последний раз? Дурeнь, посмотри, КТО его использует. Тебе название General Dynamics ни о чем не говорит, не?
	Ответить | Правка | ^ к родителю #20 | Наверх | Cообщить модератору

	106. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 20:46
	это те самые перцы у которых f-16 при пересечении уровня моря в IL переворачивался вверх ногами? Да, говорит о многом. Но я точно не помню что там конкретно было, их f-16 или не их f-15
	Ответить | Правка | ^ к родителю #86 | Наверх | Cообщить модератору

23. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
Сообщение от chinarulezzz (ok) on 25-Июн-14, 03:55
>основание считать решения на базе seL4 самыми надёжными в мире оно на С/С++ написано?) P.S. Радует пополнение в мире опенсурса.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	98. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от pavlinux (ok) on 25-Июн-14, 19:13
	> оно на С/С++ написано?) 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
	Ответить | Правка | ^ к родителю #23 | Наверх | Cообщить модератору

25. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Crazy Alex (ok) on 25-Июн-14, 06:08
Я, конечно, не в теме. Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной) модели железа, на котором это будет крутиться? Что, понятное дело, нереально. То есть, вероятно, математические доказательства корректности - это интересное упражнение, но для практики не больше ли пользы в хорошем покрытии юнит-тестами и основательном объеме fuzzy-тестирования?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	39. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Ordu (ok) on 25-Июн-14, 10:29
	> Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной) > модели железа, на котором это будет крутиться? Что, понятное дело, нереально. Не должно. :) В идеале так надо было бы, конечно. Но если играть в идеалистов, то вообще не стоит браться за написание программ, потому что никто не знает как писать программы без багов. В общем, если мы позиционируем себя как практиков, то мы должны признать, что неполная модель железа использованная в доказательстве, всё же лучше чем отсутствие этой самой модели. Правда да, тесты позволяют протестировать что-либо на реальном железе, но меня если честно, сильно сомневает способность тестов выявить какую-то "железную" проблему. Разве что документированную, многократно описанную, с существующим эксплоитом в паблике. Собственно: > 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? Математически же можно проверить все возможные случаи, несмотря на то, что количество этих случаев, равно бесконечности (практической бесконечности, поскольку все случаи проверить практикой невозможно). Конечно есть свои нюансы. Для того, чтобы доказать функциональную корректность кода, требуется предварительно написать спецификацию этого кода на формальном языке. Спецификация тоже может содержать ошибки. Но, поскольку и тесты также могут содержать ошибки, это нельзя считать недостатком метода по сравнению с написанием тестов. А вообще, это весьма перспективное направление. Варнинги компилятора придумали давно. Потом кому-то их показалось мало, и создали статистические анализаторы. Ребятам же показалось мало проверки кода по паттернам, и они попытались решить общий случай. Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.
	Ответить | Правка | ^ к родителю #25 | Наверх | Cообщить модератору

	45. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от абыр (ok) on 25-Июн-14, 10:55
	> Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры. Зевая... серебряной пули нет.
	Ответить | Правка | ^ к родителю #39 | Наверх | Cообщить модератору

	49. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Ordu (ok) on 25-Июн-14, 11:51
	>> Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры. > Зевая... серебряной пули нет. Я разве говорил что-то о серебряной пуле? Перечитайте и не говорите глупостей.
	Ответить | Правка | ^ к родителю #45 | Наверх | Cообщить модератору

	65. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от абыр (ok) on 25-Июн-14, 14:44
	Подобную белиберду про грядущую ненужность программистов за последние тридцать лет по поводу чего только не писали. А пуля все не с места.
	Ответить | Правка | ^ к родителю #49 | Наверх | Cообщить модератору

	73. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Ordu (ok) on 25-Июн-14, 16:04
	> Подобную белиберду про грядущую ненужность программистов за последние тридцать лет по поводу > чего только не писали. А пуля все не с места. Ой, да ладно вам. Настоящие программисты (tm) вымирали динозаврами уже не раз. Вот смотрите: 1. На заре эпохи компьютеров, все программисты имели серьёзное математическое или физическое образование. Они были самыми натуральными учёными, с научными публикациями, которые читали лекции первокурам и получали гранты. Зубробизоны. Их сегодня нет с нами. А те что остались, пишут такую чушь, что на их код без слёз взглянуть невозможно. 2. Затем программисты лабали исключительно на языке ассемблера и смотрели на высокоуровневых программистов как на дерьмо. Эти тоже практически вымерли. А код их сегодня выглядит макаронной мешаниной, в которой сам чёрт ногу сломит, о какой-либо поддержке этого кода не может быть и речи. 3. Выросло поколение пишущее на языках уровня C/Pascal. Эти сегодня затолканы в довольно-таки узкую нишу системного программирования. Есть примеры не вписывающиеся в эту нишу, но их, мягко говоря, не фонтан, и общие тенденции направлены на то, чтобы окончательно оставить сям системное программирование и ничего больше. 4. Сегодня мы имеем быдлокодеров на php/ruby и тп. Мы имеем C++ программистов, которые не зная ничего кроме C++ мнят себя гуру программирования и единственно правильными программистами. Есть джависты, которые (позорища!!!) жить не могут без сборки мусора. И, отмечу, все эти личности смотрят на C как на дерьмо, потому что там нет ООП/сборки мусора/динамической типизации/адекватной работы со строками/... выбирате любой пункт на вкус или впишите свой. 5. Предсказывая в будущее. Мир зохавают декларативные языки, позволяющие лишь описывать спецификацию программы. 95% сегодняшних программистов будут смотреть на тех, кто пишет на декларативных языках как на дерьмо, и считать их недопрограммистами. И все эти 95% вымрут как и предыдущие категории. Вымрут или будут загнаны в какие-то довольно узкие ниши. Оставшиеся в живых будут смотреть на код, который пишется сегодня, как на дерьмо, которое невозможно поддерживать, проще переписать. То есть, ведущиеся тридцать лет разговоры, на самом деле имели под собою почву и за эти тридцать лет программисты стали настолько иными, что можно уверенно говорить о том, что предыдущее поколение программистов вымерло. Конечно, можно возразить, и говорить о том, что никто не вымер, что вместо массового вымирания программистов, произошло приспособление программистов к новым условиям. Но это будет такой же полуправдой, как и утверждение о том, что популяция программистов пережила 2-3 массовых вымираний.
	Ответить | Правка | ^ к родителю #65 | Наверх | Cообщить модератору

	56. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от жабабыдлокодер (ok) on 25-Июн-14, 12:56
	Ну, так спецификации программисты и будут писать. Те, кто вовремя переучатся, и молодняк, который этому сразу будет учиться. Разница то какая?
	Ответить | Правка | ^ к родителю #39 | Наверх | Cообщить модератору

	58. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Ordu (ok) on 25-Июн-14, 14:09
	> Ну, так спецификации программисты и будут писать. Те, кто вовремя переучатся, и > молодняк, который этому сразу будет учиться. Разница то какая? Ааа, вы про это. Ну, во-первых, не надо особо зацикливаться на этой теме, я её озвучил, скорее ради лулзов, и, мне казалось, что объединение одним предложением плинтуса, быдлокодеров и динозавров, должно было донести мои намерения до сведения читателя. Во-вторых, как и при любой автоматизации, количество рабочих мест снижается. Кто-то переучивается и находит своё место в новой системе, кто-то переучивается, но места ему не хватает. В-третьих, надо признать, что автоматизация может привести к тому, что увеличится объём промышленности выпускаемой отраслью, что компенсирует снижение числа рабочих мест. В общем, не стоит особо зацикливаться на этой теме -- не знаю как вы, но я не могу предсказать к чему приведёт создание программы, пишущей программы и, поэтому, не готов серьёзно обсуждать эту тему.
	Ответить | Правка | ^ к родителю #56 | Наверх | Cообщить модератору

28. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Packuh on 25-Июн-14, 07:20
Оно было надежным пока было закрыто и никто о нем не знал. Ждем патчей. welcome to the real world.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

29. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от Packuh on 25-Июн-14, 07:21
ах да и самый надежный секрет тот о котором знает только один.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

30. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от DmA (??) on 25-Июн-14, 07:37
Микроядро математически прошедшее проверку  просто исполняет ядро Линукс как один и процессов. В ядре Линукс и драйвера и всё остальное , и его-то никто и не проверял! В России тоже был тендер, на 15 миллионов рублей, который должен был проверить ядро Линукс. Не знаю какие ам результаты
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	37. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 09:22
	> Не знаю какие там результаты В коде множество строчек, предположительно на Си
	Ответить | Правка | ^ к родителю #30 | Наверх | Cообщить модератору

	96. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Серж (??) on 25-Июн-14, 18:27
	> Не знаю какие там результаты Освоено!
	Ответить | Правка | ^ к родителю #30 | Наверх | Cообщить модератору

	97. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Серж (??) on 25-Июн-14, 18:29
	>> Не знаю какие там результаты > Освоено! А остальные мелочи проверять всё равно никто не будет.
	Ответить | Правка | ^ к родителю #96 | Наверх | Cообщить модератору

31. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+2 +/–
Сообщение от milkman on 25-Июн-14, 08:13
> Не знаю какие там результаты Сам написал: 15 миллионов рублей
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

32. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от Ordu (ok) on 25-Июн-14, 08:55
Любопытно. Прилагательное "математическое" как красная тряпка для местного населения. Любопытно почему, потому что никто не знает математики, или потому что все знают и раз по десять наступили на грабли неприменимости математики к реальной жизни?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	94. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от hummermania (ok) on 25-Июн-14, 17:57
	Всё как обычно - мгновенное и "глубоко компетентное" суждение о ранее незнакомом предмете при его поверхностном обзоре. Выше в комментах в PDF-ке в разделе References есть достаточно интересные документы. Особенно из свежих. Что нарылось при беглом обзоре некоторых из них:   - С-шные функции перед реализацией пишутся на языке типа Haskell (есть на него ссылки в доках) - походу функциональный стиль рулит.   - Любые конструкции языка приводящие к сайд-эффектам либо не используются вовсе, либо имеют ограниченное применение.   - Работа с типами, выделением памяти, IPC, threading и пр. объекты проверяются матаппаратом и в случае нессответствия вручную оптимизируются (вроде так)   - Для верификации кода юзают какой-то хитрый комплекс Isabella/HOL   - Плюс еще очень много мат.теории - надо копать в доках до просветления. Может где-то и ошибаюсь, поправьте предметно...
	Ответить | Правка | ^ к родителю #32 | Наверх | Cообщить модератору

33. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
Сообщение от Аноним (??) on 25-Июн-14, 08:59
маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство, как все надежно и круто, "на бумаге" сразу вспоминается про миникс, который круче чем яйца через 5 мин варки, "на бумаге"
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	88. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:43
	> маркетинговым впариванием попахивает =) 2 абзаца и в обоих про математическое доказательство, > как все надежно и круто, "на бумаге" > сразу вспоминается про миникс, который круче чем яйца через 5 мин варки, > "на бумаге" Дeбил, GD знаешь, чем занимается? Ах, не знаешь, у них сайта нет.... Знаешь, почему?
	Ответить | Правка | ^ к родителю #33 | Наверх | Cообщить модератору

	107. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от all_glory_to_the_hypnotoad (ok) on 25-Июн-14, 21:03
	Это ты дебил. Их деятельность практически ничем не знаменательна, обычная оборонка. Портачат там всего лишь чуть меньше, чем в остальных отраслях. Никакими сверхфантастическими проектами, которые сегодня кажутся сказкой, а лет через 50 будут обыденностью, там тоже не занимаются. Айти это не конёк оборонки, запомни, обезъяна.
	Ответить | Правка | ^ к родителю #88 | Наверх | Cообщить модератору

	108. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 23:13
	таки нет ? http://www.gdc4s.com/ и почему же нет у них сайта ... феназепанчика тяпни
	Ответить | Правка | ^ к родителю #88 | Наверх | Cообщить модератору

34. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
Сообщение от iuy on 25-Июн-14, 09:16
Множество ошибок просто отсутствует!
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

41. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от Аноним (??) on 25-Июн-14, 10:37
>выносом частей для управления ресурсами ядра в пространство пользователя Не понимаю, то есть драйвера будут выполняться что ли от простого пользователя? И как это повышает устойчивость к сбоям и безопасность? Заметил, что в инете десятки статей о преимуществах микроядра и почти ни одной о недостатках. Хотя сомнительно, что их нет. Это что-то вроде святого грааля или вечного двигателя? Очевидно одно: все эти "свежие идеи" вроде микроядра, все зависимости внутри одного пакета однозначно выгодны проприерастам. Подозреваю, что цель сделать все по на машине пользователя кроме наноядра максимально независимым от системы и самого пользователя. Так легче внедрять бэкдоры и продавать проприетарщину.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	55. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
	Сообщение от angra (ok) on 25-Июн-14, 12:48
	При падении драйвера ядро его перезапустит. Полезно, если в драйвере есть редко срабатывающий баг или переинициализация железа может помочь. На этом всё. Если драйвер вылетает из-за сбоя железа, который программно не исправить, то пользы от этого ровным счетом никакой. Про безопасность же в смысле security вообще речи не идет.
	Ответить | Правка | ^ к родителю #41 | Наверх | Cообщить модератору

	57. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 13:41
	В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их сам могу останавливать/запускать в линуксе вручную или через скрипты и у меня ничего не падает, почему бы не реализовать эту функцию в ядре. Если конечно это ничему не повредит. Вот и напишите статью о недостатках микроядра, чтобы страдальцам виндовс и им сочувствующим жизнь медом не казалась.
	Ответить | Правка | ^ к родителю #55 | Наверх | Cообщить модератору

	69. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 15:43
	> В монолитное ядро тоже можно вмонтировать функцию перезапуска модулей. Если я их > сам могу останавливать/запускать в линуксе вручную или через скрипты и у > меня ничего не падает, почему бы не реализовать эту функцию в > ядре. Если конечно это ничему не повредит. > Вот и напишите статью о недостатках микроядра, чтобы страдальцам виндовс и им > сочувствующим жизнь медом не казалась. Все монолитное ядро с драйверами работает в одном адресном пространстве, и если в драйвере изза ошибки что-то пишется не туда, то кернелепаник и бб, при чем тут перезапуск модулей?
	Ответить | Правка | ^ к родителю #57 | Наверх | Cообщить модератору

	60. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–3 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 14:23
	Ядро линукс построено вольно-невольно по аналогии с ЦНС, есть гематоэнцефалический барьер между кернелспейс и юзерспейс, Модули как навыки и знания, хранятся они не в желудке, а рядом с ядром. Представляю если бы одна моя мысль напрямую общалась с другой минуя координационный центр. Это называется шизофрения. :) Если у вас уже есть серьезный баг в мозгах то перезапуск не поможет и не нужен. Извиняюсь за лирическое отступление :))
	Ответить | Правка | ^ к родителю #55 | Наверх | Cообщить модератору

	61. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 14:28
	Или вот еще такое сравнение. Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :))))
	Ответить | Правка | ^ к родителю #55 | Наверх | Cообщить модератору

	62. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Andrey Mitrofanov on 25-Июн-14, 14:30
	>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :)))) Бредишь? Про повышение привилегий под linux не слышал?
	Ответить | Правка | ^ к родителю #61 | Наверх | Cообщить модератору

	63. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 14:32
	>>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :)))) > Бредишь? Про повышение привилегий под linux не слышал? Не расстраивайся :)
	Ответить | Правка | ^ к родителю #62 | Наверх | Cообщить модератору

	64. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 14:35
	>>Когда ядро линукс просто откажет, микроядро даст доступ к ракетам :)))) > Бредишь? Про повышение привилегий под linux не слышал? В микроядре повышение привилегий стандартная процедура.
	Ответить | Правка | ^ к родителю #62 | Наверх | Cообщить модератору

	67. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Andrey Mitrofanov on 25-Июн-14, 15:33
	...but in Soviet Russia, you deny to the microkernel.
	Ответить | Правка | ^ к родителю #64 | Наверх | Cообщить модератору

	77. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от anonymous (??) on 25-Июн-14, 16:19
	> Заметил, что в инете десятки статей о преимуществах микроядра и почти ни > одной о недостатках. Читайте внимательнее эти же статьи, основные недостатки, как минимум - просевшая производительность и увеличивающаяся сложность process interconnection.
	Ответить | Правка | ^ к родителю #41 | Наверх | Cообщить модератору

42. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
Сообщение от odity on 25-Июн-14, 10:38
Поясните дураку, а че они сделали ядро надежным,доказали математически, а торвальдс не сделал этого?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	53. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от angra (ok) on 25-Июн-14, 12:41
	Если брать аналогии, то почитай в википедии про "Гравитационная задача N тел". У этих ребят случай аналогичный задаче трех тел. А вот linux является аналогом задачи с на порядки большим количеством тел, причем количество тел продолжает постоянно увеличиваться, то есть на данном уровне развития математики не может быть решенным в аналитическом виде.
	Ответить | Правка | ^ к родителю #42 | Наверх | Cообщить модератору

	59. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 14:14
	По этой аналогии любая ос состоит из большого количества тел. И очередное микроядро - просто повод денег содрать и ничего более.
	Ответить | Правка | ^ к родителю #53 | Наверх | Cообщить модератору

	72. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 16:01
	> По этой аналогии любая ос состоит из большого количества тел. И очередное > микроядро - просто повод денег содрать и ничего более. Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что баги при этом будут вне оного. Т.к. вся функциональность - вне оного. Правда большой вопрос насколько это является достоинством.
	Ответить | Правка | ^ к родителю #59 | Наверх | Cообщить модератору

	89. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:45
	>> По этой аналогии любая ос состоит из большого количества тел. И очередное >> микроядро - просто повод денег содрать и ничего более. > Ну так они сделали примитивное микроядро, не умеющее вообще ничего. Логично что > баги при этом будут вне оного. Т.к. вся функциональность - вне > оного. Правда большой вопрос насколько это является достоинством. Raytheon смотрит на вас всех, как на гогно. Сечешь? ТАМ не нужна функциональность пингвина.
	Ответить | Правка | ^ к родителю #72 | Наверх | Cообщить модератору

43. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
Сообщение от Аноним (??) on 25-Июн-14, 10:39
А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	74. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–1 +/–
	Сообщение от fi (ok) on 25-Июн-14, 16:04
	скорей всего прикрутят к opensuse, как это было с прежним L4.
	Ответить | Правка | ^ к родителю #43 | Наверх | Cообщить модератору

	90. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:45
	> А на каком оборудовании оно может работать? GNU/Debian/seL4 на нем можно сделать? На Хеллфайрах работает. Ну и на других продуктах Raytheon.
	Ответить | Правка | ^ к родителю #43 | Наверх | Cообщить модератору

54. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
Сообщение от Аноним (??) on 25-Июн-14, 12:46
Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если львиная доля безопасности обеспечивается вне ядра?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	91. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:46
	> Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется > в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если > львиная доля безопасности обеспечивается вне ядра? Сайдуиндеру безопасность ПО ГСН ни к чему, как ты понимаешь. Да?
	Ответить | Правка | ^ к родителю #54 | Наверх | Cообщить модератору

	100. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Аноним (??) on 25-Июн-14, 20:07
	> Хм. Насколько я понял, в новости прямо сказано, что контроль доступа реализуется > в юзерспейс. Так какой толк от математически доказанной безопасности ядра, если > львиная доля безопасности обеспечивается вне ядра? Отдельные процессы не имеют прямого доступа друг к другу, поэтому тот факт, что какой-нибудь авторизатор крутится, условно, в отдельном процессе и под отдельным UID'ом, не делает его более уязвимым, чем если бы он был в ядре. Скорее даже наоборот, делает менее уязвимым, за счёт ограничения доступного ему пространства.
	Ответить | Правка | ^ к родителю #54 | Наверх | Cообщить модератору

75. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–4 +/–
Сообщение от DmA (??) on 25-Июн-14, 16:08
пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим на этом ядре процессом другое ядро( Linux) в которое никто и никогда из математиков не заглядывал :) Смешанная или смешная ОС получилась! Но если ядро будет падать каждые 10 минут, то и на этом супернадёжном ядре процесс с Линукс будет виснуть каждые 10 минут, вот только в случае с обычным сервером его перезапускать нужно в ручную, то тут можно настроить и всё будет происходить автоматически.Из часа такой комп проработает 50 минут пусть. А обычный Линукс только 10 минут из часа. Имеет право жить!
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	76. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+/–
	Сообщение от Andrey Mitrofanov on 25-Июн-14, 16:16
	> пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим > на этом ядре процессом другое ядро( 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.
	Ответить | Правка | ^ к родителю #75 | Наверх | Cообщить модератору

	92. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	–2 +/–
	Сообщение от Аноним (??) on 25-Июн-14, 17:46
	>> пишем микроядро,верифицируем его, если нужно наделяем крутыми свойствами, а  потом грузим >> на этом ядре процессом другое ядро( 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?
	Ответить | Правка | ^ к родителю #76 | Наверх | Cообщить модератору

	93. "Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..."	+1 +/–
	Сообщение от Andrey Mitrofanov on 25-Июн-14, 17:54
	> Боюсь, чувак, это вы все смешны в вашем уютненьком. Вы вообще что-то > кроме оффтопика-пингвина видели IRL? Ефрейтор, *СРОЧНО* пройдите в первый отдел.
	Ответить | Правка | ^ к родителю #92 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема