|
| | |
Компания General Dynamics C4 Systems и австралийский исследовательский центр NICTA открыли под свободными лицензиями исходные тексты микроядра seL4 (Secure Embedded L4), компоненты математического доказательства его надёжности и сопутствующий код для построения высоконадёжных операционных систем. Ядро открыто под лицензией GPLv2, а утилиты и работающий в пространстве пользователя код содержит как элементы под лицензией GPLv2, так и компоненты под лицензией BSD.
Микроядро seL4 нацелено на предоставление повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. В частности, Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) применяет seL4 для повышения защищённости программных систем, используемых в военных беспилотных летательных аппаратах.
Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире. Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заданным на формальном языке спецификациям. Таким образом, гарантируется надёжная изоляция между компонентами и отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным. Разработчики ПО, работающего поверх ядра seL4, могут быть полностью уверены, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и, в частности, её критические части.
Архитектура seL4 примечательна выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и т.п., вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора. Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.
Для разработчиков предлагается компоненто-ориентированная платформа для разработки приложений CAmkES, позволяющая моделировать и создавать системы на основе seL4 в виде коллекции взаимодействующих между собой компонентов. Также поставляется набор примеров и прототипов систем на основе seL4, подборка драйверов, библиотека для создания драйверов, порт Си-библиотеки Musl. Из поддерживаемых аппаратных архитектур отмечены ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86. Поддерживается запуск поверх микроядра seL4 ядра Linux, в данном случае seL4 выступает в роли гипервизора.
|
|
|
- Главная ссылка к новости (https://github.com/seL4...)
- OpenNews: Сверхнадёжное ядро seL4 будет переведено в разряд открытых проектов
- OpenNews: На базе гипервизора seL4 создана платформа для создания высокозащищённых систем
- OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
| | Тип: К сведению | | Ключевые слова: sel4, microkernel, (найти похожие документы) | При перепечатке указание ссылки на opennet.ru обязательно | | Реклама | |
id=adv>
| |
| |
2.4, уке, 09:47, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку] [к модератору]
| +31 +/– |
У меня инфа. Поддерживается железо:
F-16, M1 Abrams, Piranha, MX, SAPS, MASP, GDMX, TDRSS.
| | | |
3.39, Аноним, 14:12, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] | +/– | ссылку или бабабол ... весь текст скрыт [ показать] | | | |
3.52, Fantomas, 16:14, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +5 +/–Классно M1 Abrams, сервер, серверная и дизельгенератор в одном флаконе ... весь текст скрыт [ показать] | |
10.126, arisu, 14:17, 31/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– | |
вообще, всё наоборот: намного выгодней разломать врагов и оставить полезную технику на месте.
впрочем, если у кого-то будут технологии такого уровня, а у других нет, и защиты тоже нет — то ни о каких врагах речь уже не идёт, только о «чего изволите, бвана?»
| | | |
2.7, anonim, 09:49, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ показать ветку] [ к модератору] +4 +/– 2.8, Аноним, 09:50, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ показать ветку] [ к модератору] +2 +/–
1.10, Аноним, 09:53, 29/07/2014 [ответить] [смотреть все] [к модератору] +8 +/–
> даёт основание считать решения на базе seL4 самыми надёжными в мире.
Никто не спорит что примитивный тасксвичер можно написать без багов. Теперь удачи написать без багов обвязку, без которой все это примерно столь же полезно как выключенный компьютер.
8.57, cmp, 17:01, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] –2 +/–Железка и драйвер работают синхронно - перезапуск драйвера, в лучшем случае поте... весь текст скрыт [ показать] , arisu, 19:10, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/–
скажи, ты говоришь так же, как и пишешь — монотонно, укладывая в одно предложение кучу несвязаных словосочетаний? если нет, то какого же чёрта ты пишешь так, что читать тебя почти физически неприятно и хочется отоварить молотком по черепу?
8.58, Crazy Alex, 17:03, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +3 +/–Насколько я понимаю, единственный более-менее надежный вариант реакции - громко ... весь текст скрыт [ показать] , Аноним, 19:01, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/–По моим наблюдениям за ядром линукса это обычно так встает колом железка, а пот... весь текст скрыт [ показать] | |
9.115, Vkni, 22:07, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– |
> А если GPU не получилось перезапустить - радости то с работающего
> драйвера? Картинки то все-равно не будет. ЧСХ такое можно и с
> модульным монилитом понаблюдать для самых разных железок.
Понятно, что если железка-дрянь, то АппаратноПрограммныйКомплекс тоже будет плох. Тем не менее, сейчас операционные системы универсальны => желательно закладываться и на хорошие железки, чтобы на них ОС тоже была полезна.
А так, в своё время были мониторы, которые можно было убить программно, потом исчезли.
| | | |
7.104, arisu, 19:08, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–
> 20 процентов программы (кода) удовлетворят потребности 80% пользователей.
жаль только, что для разных пользователя эти двадцать процентов включают разные фичи.
6.66, chinarulezzz, 18:49, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/–Просто невнимательность, но не просто Не надо умных слов, друг Люди делают не ... весь текст скрыт [ показать] | |
8.113, Anonizmus, 21:14, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– |
> А это не оправдания, это капитанинг. Иногда, даже если не хочется делать
> баг - он может всpaться. Человеческий мозг - не цифровой компьютер,
> поэтому не обладает идеальной надежностью и 100% воспроизводимостью работы.
А кусок кремния таки прямо обладает [b]100%[/b] надежностью и воспроизводимостью... Тото у третьих пней предусматривался вариант работы в режиме напоминающем RAID 1.
| | | |
7.88, Ordu, 02:11, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–Про философию я соглашусь, она здесь неуместна, но игнорировать психологию совсе... весь текст скрыт [ показать] | |
8.93, pavlinux, 04:47, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | –1 +/– | |
> Кроме того, ограничения "вычислительных способностей" мозга -- это не вопрос ли психологии?
Нэт, это физиология изучает.
> Человек непосредственно, без всяких хитроумных заморок типа разделения
> задачи на подзадачи, может решать лишь весьма простые задачки.
Хвать уже муть писать, спутали всё. Алгоритмы с рефлексам, задачи с инстинктами.
Весь тред, да и все комменты в теме - х...ета полная, ничего общего не имеющая с реальностью.
Ну чесслово - глупее идиотов выглядят, только размышляющие идиоты.
| 
| | |
| |
9.100, Ordu, 13:53, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– | |
> Хвать уже муть писать, спутали всё. Алгоритмы с рефлексам, задачи с инстинктами.
Ну раскройте глаза нам глупым или, как говорится, GTFO.
Впрочем я уверен, что вы просто недостаточно интересовались причинами возникновения тех или иных ошибок, и уж во всяком случае не интересовались тем, что говорят об этом другие, в том числе и те, кто по роду своей деятельности изучает ошибки, которые мозг совершает *систематически*. Если интересно, то вот популярное изложение объясняющее на примерах, что такое когнитивное искажение: http://lesswrong.ru/w/Когнитивные_искажения
Обратите там внимание на опыт с рулеткой и прочие эксперименты демонстрирующие т.н. "якорение", и задайте себе после этого вопрос: можете ли вы вообще доверять своему мозгу? То есть другие когнитивные искажения тоже заслуживают внимания, но там хоть какие-то пути просматриваются как можно внести поправку, корректирующую деструктивное влияние мозга на процесс мышления, "якорение" же не позволяет даже этого.
| | | |
5.62, Аноним, 18:31, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/–Вот у лифта может быть дубовый алгоритм, который воможно провалидировать математ... весь текст скрыт [ показать] , pavlinux, 05:03, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–
>> Априори бажность - хорошая отговорка для тех кто проектирует лифты,
> Вот у лифта может быть дубовый алгоритм, который воможно провалидировать математически.
> Хотя у современных лифтов это уже не факт - в больших
> зданиях лифты принимают решения куда ехать исходя из количества людей и
> оптимальности поездки
Какая в пязду оптимальная поездка, на несвязаном графе с последовательными узлами?
3.23, Andrey Mitrofanov, 11:06, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–Ваши тоже _Все_ http lib ru ANEKDOTY errors txt_with-big-pictures html Че... весь текст скрыт [ показать] , Аноним, 10:15, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ показать ветку] [ к модератору] +/– 2.21, Mihail Zenkov, 10:53, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ показать ветку] [ к модератору] –1 +/– 3.41, Crazy Alex, 14:45, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–Угу А потом вам понадобится какая-то хитрая алгоритмика для экономии топлива А... весь текст скрыт [ показать] | |
6.95, pavlinux, 05:32, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– | |
> Речь шла о том, что усложнение систем - штука повсеместная и естественная.
Детский садик Ромашка.
Панимаешь в чём вся х..ня - доступные материалы - для говна,
говно не должно жить в каменном доме, с камином.
В доме говна - нужны системы кондиционирования и вентиляции.
Говно должно думать, что оно не говно. Для этого само говно,
производит для говна, продукцию из/на говне.
В основной массе, говно знающие, что делает говно, само верит
в то, что производит. И начинает думать, что если каждое говно
покупает, то, чем я хуже остального говна.
Говну не нужен дом из мрамора, гавну нужен просто дом.
Газбетон, ДСП, ПВХ, ... - типичный состав дома говна.
Так же говно, покупает лыжи Salomon за 1500$ и ботинки к ним за 3000$,
правда у говна даже нет 3-ого разряда по ОФП.
| 
| | |
6.97, Mihail Zenkov, 13:17, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–Везде очень по-разному Я в курсе про котлы вентиляцию etc Там также все неодно... весь текст скрыт [ показать] , Аноним, 03:02, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/– Невидимая рука рынка как бы намекает - зачем тратиться на топливную экономично... весь текст скрыт [ показать] , Vkni, 22:30, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–
> А всё потому, что по факту весь этот софт - монолитен. В том смысле, что для того,
> чтобы заменить, удалить или добавить любой компонент нужны приличные усилия и
> знания.
И вот тут мы опять смотрим на Хы с разными WM. :-)
| |
5.127, arisu, 14:27, 31/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– | |
> И вот тут мы опять смотрим на Хы с разными WM. :-)
а также на никсовую консоль и старый добрый принцип «одна задача — одна программа». но всё это неимоверно сложно для ЦА всяких DE.
| | | |
3.64, Аноним, 18:45, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +1 +/–А также выбросить GPU со спеками на 900 страниц, чипы беспроводной сети у которы... весь текст скрыт [ показать] , Mihail Zenkov, 13:27, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–
>> или делать их совершенно независимыми узлами,
> Как вы себе это представляете?
Точно также как строится микроядерная ОС.
Есть контроллер с основной программой, простой идеально отлаженный и проверенный. Он управляет остальными узлами. В случае зависания одного из узлов контроллер его перезапускает. В случае отказа узла, контроллер задействует дублирующий узел. Узлы естественно с hotplug.
3.85, Аноним, 00:44, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] +/–А допотопные версии зажигания были и вовсе механическими Ну вот вы и замените к... весь текст скрыт [ показать] | |
4.99, Mihail Zenkov, 13:42, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– |
> А допотопные версии зажигания были и вовсе механическими. Ну вот вы и
> замените компьютер на счеты, их хрен завесишь без аппаратных жульничеств.
Ненужно передергивать. Есть этап усовершенствования системы, после которого дальнейшее совершенствование практически ничего не дает кроме усложнения, снижения надежности и ремонтопригодности. Я привел реальный пример с ДВС. Механическое зажигание существенно проигрывает микроконтроллеру как по надежности, так и по точности. Но дальнейшие увеличение точности не дает ничего.
>> и еще успевать выводить статистику на экран.
> Зато считает с комариной скоростью, да и сколь-нибудь нормальный интерфейс пользователя
Для вывода интерфейса подключите планшет/телефон. Сохранится надежность там где она реально необходима и получите красивый интерфейс.
| | | |
| |
6.117, Mihail Zenkov, 03:11, 31/07/2014 [^] [ответить] [смотреть все] [к модератору] | –1 +/– |
> А тут тоже зависит от. Что понимать под ремонтом? Возможность сделать радиолампу
> на замену сгоревшей в гараже? Возможность перепаять транзистор? Замена стандартной микросхемы
> логики? Смена сбойнувшего проца? Вынимание сервера из стойки и замена на
> такой же, но исправный? Где та грань?...
Зависит от условий эксплуатации и целесообразности. Например на сервере многие части можно заменить на горячую, а в ноутбуке наоборот заменить видеокарту весьма проблемно. Конструкция настоящего джипа должна быть простой и очень надежной, позволять ремонт в поле, без стендов диагностики и сложного инструмента. Мотор гоночного болида наоборот настраивают на дорогих стендах и выбрасывают после гонки.
| | | |
| |
8.125, Mihail Zenkov, 13:52, 31/07/2014 [^] [ответить] [смотреть все] [к модератору] | +/– | |
> А вот прокладывать в обычной хате водопровод с троекратным резервированием по принципу "а вдруг сломается?!" - ну вы поняли.
Обычно в квартире ставят шаровый кран на вводе и перед каждой точкой разбора. Это дает возможность перекрыть потекший кран на кухне и продолжать пользоваться туалетом, а также менять разводку в квартире, не перекрывая во всем подъезде/доме воду.
| | | |
4.114, Anonizmus, 22:05, 30/07/2014 [ ^] [ ответить] [ смотреть все] [ к модератору] –1 +/–
Я вот до сих пор не могу понять почему массовые автомобили не выпускают из алюминия?..
2.50, an, 16:06, 29/07/2014 [ ^] [ ответить] [ смотреть все] [ показать ветку] [ к модератору] –1 +/–как я понимаю микрокод и аппаратный алгоритм процессора по сути компонент таск... весь текст скрыт [ показать] [ показать ветку]
1.14, bav, 10:19, 29/07/2014 [ответить] [смотреть все] [к модератору] +1 +/–
Гг. Осталось теперь математически доказать надежность всех остальных сервисов, которые делаю этот обглодышь минимально юзабельным.
1.15, Аноним, 10:21, 29/07/2014 [ответить] [смотреть все] [к модератору] +14 +/–
Ща поверх него запилят "сверхнадёжное" ПО на JavaScript и HTML5.
1.16, Аноним, 10:27, 29/07/2014 [ответить] [смотреть все] [к модератору] +8 +/–
Надо еще доказать корректность компилятора которым это все собирается.
1.18, IMHO, 10:32, 29/07/2014 [ответить] [смотреть все] [к модератору] +/–
еще одно ядро
1.19, хрю, 10:41, 29/07/2014 [ответить] [смотреть все] [к модератору] +2 +/–
там кода кот наплакал. код, конечно, легко читается и всё такое, но там ничего особо и нет. плюс оно, как я понимаю, не реалтайм.
1.22, Аноним, 10:54, 29/07/2014 [ответить] [смотреть все] [к модератору] –2 +/–
1.24, Аноним, 11:20, 29/07/2014 [ответить] [смотреть все] [к модератору] +/–Персиянские операторы Автобазы подтверждают ... весь текст скрыт [ показать] Ну что, ждем новости типа В ядре seL4 обнаружена критическая уязвимость ... весь текст скрыт [ показать]
1.34, Аноним, 13:34, 29/07/2014 [ответить] [смотреть все] [к модератору] –2 +/–где то уже читал про математическое доказательство и микроядро, и при чем недавн... весь текст скрыт [ показать]
Уверены они что система надежная?
http://xakep.ru/news/58149/
| |
5.109, Anonizmus, 20:48, 30/07/2014 [^] [ответить] [смотреть все] [к модератору] | –1 +/– |
> Ну, так все правильно - днем же звезд не видать. Как же
> с гороскопом без звезд-то работать. А стратеги, видно, те еще астрологи...
Вот немецкая разведка с помощью форса гороскопов сорвала отступление французских войск...
| | | |
1.43, my, 15:06, 29/07/2014 [ответить] [смотреть все] [к модератору] –1 +/–
Что-то не компилится.
> as: unrecognized option '-mcpu=cortex-a9'
1.45, Zenitur, 15:43, 29/07/2014 [ответить] [смотреть все] [к модератору] –1 +/–
Если там не Systemd то ненужно. Ведь всё, на чём нет Systemdб крутые хакеры объявляют устаревшим и не модным.
1.51, Пропатентный тролль, 16:09, 29/07/2014 [ответить] [смотреть все] [к модератору] –1 +/–
А была ли доказана безошибочность программ, которые использовались при провекри безошибочности?
1.59, Аноним, 17:12, 29/07/2014 [ответить] [смотреть все] [к модератору] –3 +/–Чем оно надёжнее проверенного Windows Core ... весь текст скрыт [ показать] Рилтайм от блекбери круче, инф100 1 да и кореос торт а не печенько рекламное ... весь текст скрыт [ показать]
Ваш комментарий
Read more |
