The OpenNET Project / Index page

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

29.07.2014 09:20  Открыт код сверхнадёжного микроядра seL4

Компания 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 выступает в роли гипервизора.

  1. Главная ссылка к новости (https://github.com/seL4...)
  2. OpenNews: Сверхнадёжное ядро seL4 будет переведено в разряд открытых проектов
  3. OpenNews: На базе гипервизора seL4 создана платформа для создания высокозащищённых систем
  4. OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
Лицензия: CC-BY
Тип: К сведению
Ключевые слова: sel4, microkernel
При перепечатке указание ссылки на opennet.ru обязательно
Обсуждение Линейный вид | Ajax | Показать все | RSS
 
  • 1.2, evkogan, 09:39, 29/07/2014 [ответить] [смотреть все]
  • +/
    Сначала нужен список поддерживаемого оборудования
    И список портиротированного ПО
    У кого-то такая инфа?
     
     
  • 2.4, уке, 09:47, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]
  • +32 +/
    У меня инфа. Поддерживается железо:
    F-16, M1 Abrams, Piranha, MX, SAPS, MASP, GDMX, TDRSS.
     
     
  • 3.17, commiethebeastie, 10:27, 29/07/2014 [^] [ответить] [смотреть все]
  • +7 +/
    Демократичненько
     
  • 3.39, Аноним, 14:12, 29/07/2014 [^] [ответить] [смотреть все]
  • +/
    ссылку или бабабол
     
     
  • 4.54, Аноним, 16:33, 29/07/2014 [^] [ответить] [смотреть все]
  • +5 +/
    Да балабол, но все равно ржачно.
     
  • 3.52, Fantomas, 16:14, 29/07/2014 [^] [ответить] [смотреть все]  
  • +5 +/
    Классно M1 Abrams, сервер, серверная и дизельгенератор в одном флаконе ... весь текст скрыт [показать]
     
     
  • 4.61, Аноним, 17:23, 29/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Ога! Можно WoT гонять :)
     
     
  • 5.69, Аноним, 18:56, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Только тут подсказывают что для того чтобы гусеница за 30 секунд чинилась - надо... весь текст скрыт [показать]
     
     
  • 6.90, Аноним, 03:45, 30/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Не знаю как там у абраши и с наших православных танков 3 4 этого форума тупо тра... весь текст скрыт [показать]
     
     
  • 7.106, Аноним, 20:36, 30/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Так я и говорю - технологии надо сильно прокачать Ну там например выводок нанор... весь текст скрыт [показать]
     
     
  • 8.108, arisu, 20:43, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    да и самих врагов тоже, им пофигу, что ломать.
     
     
  • 9.120, Аноним, 04:34, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Это наверное опционально, низкоприоритетная задача Враги узрев такую разборку б... весь текст скрыт [показать]
     
     
  • 10.126, arisu, 14:17, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    вообще, всё наоборот намного выгодней разломать врагов и оставить полезную техн... весь текст скрыт [показать]
     
  • 4.111, Anonizmus, 20:53, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Боюсь стоимость владения вас не обрадует ... весь текст скрыт [показать]
     
  • 2.7, anonim, 09:49, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +4 +/
    >У кого-то такая инфа?

    Да, у кого-то есть.

     
  • 2.8, Аноним, 09:50, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +2 +/
    Ну беспилотники уже поддерживаются. Дело за малым.
     
  • 1.5, re, 09:47, 29/07/2014 [ответить] [смотреть все]  
  • +14 +/
    про титаник тоже так говорили
     
     
  • 2.9, Аноним, 09:50, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +18 +/
    Так все правильно - капитан и айсберг не были составными частями корабля, на них гарантия не распостранялась.
     
  • 2.37, Кевин, 13:59, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +4 +/
    каким бы надёжным не был сейф, его всегда можно бросить в вулкан (с)
     
  • 2.60, Аноним, 17:22, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +2 +/
    Т.е. не мне одному кажется, что математики что-то не учли???
     
     
  • 3.101, umbr, 15:35, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Учли, и пофиксили в следующих релизах Титаник, Олимпик и Британик так и плавали... весь текст скрыт [показать]
     
  • 2.84, Аноним, 00:43, 30/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    есть мнение, что говоруны эти были лицами заинтересованными
     
  • 1.10, Аноним, 09:53, 29/07/2014 [ответить] [смотреть все]  
  • +8 +/
    > даёт основание считать решения на базе seL4 самыми надёжными в мире.

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

     
     
  • 2.11, Аноним, 10:11, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • –1 +/
    То есть ты хочешь сказать, что все ваши поделки априорно бажные Я правильно теб... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.13, Аноним, 10:18, 29/07/2014 [^] [ответить] [смотреть все]  
  • +11 +/
    Я хочу сказать что все мало-мальски сложные программы апнриори бажные. И хрен вы их валидируете математически.
     
     
  • 4.29, chinarulezzz, 12:03, 29/07/2014 [^] [ответить] [смотреть все]  
  • +2 +/
    Зависит от инструмента, подхода к разработке, и человека К критическим задачам ... весь текст скрыт [показать]
     
     
  • 5.40, Crazy Alex, 14:33, 29/07/2014 [^] [ответить] [смотреть все]  
  • +2 +/
    К критическим задачам надо подходить скурпулезно Делая резервирование, проводя ... весь текст скрыт [показать]
     
     
  • 6.46, cmp, 15:54, 29/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    согласен, добавлю только, что эксперимент по созданию сверх надежного, но крайне... весь текст скрыт [показать]
     
     
  • 7.53, evkogan, 16:32, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Только одно, но ничто не мешает ядру не просто прибить драйвер, а перезапустить ... весь текст скрыт [показать]
     
     
  • 8.55, Аноним, 16:50, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Драйвер, может, и перезапустится, но перезапустится ли железка?
     
  • 8.57, cmp, 17:01, 29/07/2014 [^] [ответить] [смотреть все]  
  • –2 +/
    Железка и драйвер работают синхронно - перезапуск драйвера, в лучшем случае поте... весь текст скрыт [показать]
     
     
  • 9.79, Аноним, 23:58, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Особенно прикольно AMDшники GPU ресторят при сбоях Они пытаются восстановить со... весь текст скрыт [показать]
     
  • 9.105, arisu, 19:10, 30/07/2014 [^] [ответить] [смотреть все]  
  • +2 +/
    скажи, ты говоришь так же, как и пишешь 8212 монотонно, укладывая в одно пред... весь текст скрыт [показать]
     
  • 8.58, Crazy Alex, 17:03, 29/07/2014 [^] [ответить] [смотреть все]  
  • +3 +/
    Насколько я понимаю, единственный более-менее надежный вариант реакции - громко ... весь текст скрыт [показать]
     
  • 8.71, Аноним, 19:01, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    По моим наблюдениям за ядром линукса это обычно так встает колом железка, а пот... весь текст скрыт [показать]
     
     
  • 9.115, Vkni, 22:07, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Понятно, что если железка-дрянь, то АппаратноПрограммныйКомплекс тоже будет плох... весь текст скрыт [показать]
     
     
  • 10.121, Аноним, 08:58, 31/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    С железом тенденция ровно обратная - становится быстрее-выше-сильнее-навороченне... весь текст скрыт [показать]
     
  • 7.104, arisu, 19:08, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    жаль только, что для разных пользователя эти двадцать процентов включают разные ... весь текст скрыт [показать]
     
  • 6.66, chinarulezzz, 18:49, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Просто невнимательность, но не просто Не надо умных слов, друг Люди делают не ... весь текст скрыт [показать]
     
     
  • 7.80, Аноним, 23:59, 29/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    А это не оправдания, это капитанинг Иногда, даже если не хочется делать баг - о... весь текст скрыт [показать]
     
     
  • 8.113, Anonizmus, 21:14, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    А кусок кремния таки прямо обладает b 100 b надежностью и воспроизводимостью... весь текст скрыт [показать]
     
     
  • 9.122, Аноним, 08:59, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Так его люди делали, со всеми вытекающими ... весь текст скрыт [показать]
     
  • 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 Впрочем я уверен, что вы... весь текст скрыт [показать]
     
  • 8.134, chinarulezzz, 03:05, 01/08/2014 [^] [ответить] [смотреть все]  
  • +/
    не нужно думать что знания нашей психики завершены То что мы ошибаемся не означ... весь текст скрыт [показать]
     
  • 5.62, Аноним, 18:31, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Вот у лифта может быть дубовый алгоритм, который воможно провалидировать математ... весь текст скрыт [показать]
     
     
  • 6.70, chinarulezzz, 18:57, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    и свойственно _не_ ошибаться можно, они же знают что им свойственно Хорошо ... весь текст скрыт [показать]
     
     
  • 7.73, Аноним, 19:11, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Только когда вся программа и рантайм - размером с hello world, да еще транслятор... весь текст скрыт [показать]
     
     
  • 8.77, chinarulezzz, 19:33, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    тогда очевидно что программа должна стремиться к выполнению желательно одной фун... весь текст скрыт [показать]
     
     
  • 9.82, Аноним, 00:32, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Не обязательно Но программа должна быть или простой как топор, или должно быть ... весь текст скрыт [показать]
     
     
  • 10.133, chinarulezzz, 02:58, 01/08/2014 [^] [ответить] [смотреть все]  
  • +/
    не обязательно, но стремление хорошее, даже лучшее из возможных, принимая во вни... весь текст скрыт [показать]
     
  • 6.94, pavlinux, 05:03, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Какая в пязду оптимальная поездка, на несвязаном графе с последовательными узла... весь текст скрыт [показать]
     
     
  • 7.110, Аноним, 20:51, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ты недооцениваешь лифты Даже в простом лифте высотных зданий и офисов люди указ... весь текст скрыт [показать]
     
  • 3.23, Andrey Mitrofanov, 11:06, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ваши тоже _Все_ http lib ru ANEKDOTY errors txt_with-big-pictures html Че... весь текст скрыт [показать]
     
     
  • 4.63, Аноним, 18:40, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    ЧСХ, в каждой шутке есть доля правды ... весь текст скрыт [показать]
     
  • 2.12, Аноним, 10:15, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    зато дарповы гранты.
     
  • 2.21, Mihail Zenkov, 10:53, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • –1 +/
    Если отказаться от бесполезного bloatware kde gnome systemd etc с кучей модных... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.25, Аноним, 11:27, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Это объясняет и оправдывает тысячи дистров линя ... весь текст скрыт [показать]
     
  • 3.41, Crazy Alex, 14:45, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Угу А потом вам понадобится какая-то хитрая алгоритмика для экономии топлива А... весь текст скрыт [показать]
     
     
  • 4.72, Mihail Zenkov, 19:06, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Вот это и есть overengineering ибо дальнейшее усложнение алгоритмов повышает сло... весь текст скрыт [показать]
     
     
  • 5.81, Crazy Alex, 00:16, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Выигрыш - в том, что ты продашь больше машин, показав людям эту экономию или это... весь текст скрыт [показать]
     
     
  • 6.95, pavlinux, 05:32, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Детский садик Ромашка Панимаешь в чём вся х ня - доступные материалы - для го... весь текст скрыт [показать]
     
  • 6.97, Mihail Zenkov, 13:17, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Везде очень по-разному Я в курсе про котлы вентиляцию etc Там также все неодно... весь текст скрыт [показать]
     
  • 5.89, Аноним, 03:02, 30/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Невидимая рука рынка как бы намекает - зачем тратиться на топливную экономично... весь текст скрыт [показать]
     
  • 4.116, Vkni, 22:30, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    И вот тут мы опять смотрим на Хы с разными WM - ... весь текст скрыт [показать]
     
     
  • 5.127, arisu, 14:27, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    а также на никсовую консоль и старый добрый принцип 171 одна задача 8212 од... весь текст скрыт [показать]
     
  • 3.64, Аноним, 18:45, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    А также выбросить GPU со спеками на 900 страниц, чипы беспроводной сети у которы... весь текст скрыт [показать]
     
     
  • 4.75, Mihail Zenkov, 19:15, 29/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Да нужно выбрасывать или делать их совершенно независимыми узлами, дабы в случае... весь текст скрыт [показать]
     
     
  • 5.83, Аноним, 00:35, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Нужно Выбрасывайте, разрешаю Как вы себе это представляете Вот хочется вам ка... весь текст скрыт [показать]
     
     
  • 6.96, pavlinux, 05:47, 30/07/2014 [^] [ответить] [смотреть все]  
  • –3 +/
    gt оверквотинг удален Аноним, съибни, а Ну лошара же последний ... весь текст скрыт [показать]
     
     
  • 7.123, Аноним, 09:02, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Отправь СМСку с текстом не лох на короткий номер Ведь чем больше СМС ты пошл... весь текст скрыт [показать]
     
  • 6.98, Mihail Zenkov, 13:27, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Точно также как строится микроядерная ОС Есть контроллер с основной программой,... весь текст скрыт [показать]
     
     
  • 7.124, Аноним, 09:03, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ну да, то-есть сферическое железо в вакууме, которое никто никогда не увидит, кр... весь текст скрыт [показать]
     
  • 3.85, Аноним, 00:44, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    А допотопные версии зажигания были и вовсе механическими Ну вот вы и замените к... весь текст скрыт [показать]
     
     
  • 4.99, Mihail Zenkov, 13:42, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ненужно передергивать Есть этап усовершенствования системы, после которого даль... весь текст скрыт [показать]
     
     
  • 5.112, Аноним, 20:58, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    А тут тоже зависит от Что понимать под ремонтом Возможность сделать радиолампу... весь текст скрыт [показать]
     
     
  • 6.117, Mihail Zenkov, 03:11, 31/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Зависит от условий эксплуатации и целесообразности Например на сервере многие ч... весь текст скрыт [показать]
     
     
  • 7.118, Аноним, 04:05, 31/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Вот тут мы и приходим к самому главному Да, три гидролинии в самолете - имеют н... весь текст скрыт [показать]
     
     
  • 8.125, Mihail Zenkov, 13:52, 31/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    Обычно в квартире ставят шаровый кран на вводе и перед каждой точкой разбора Эт... весь текст скрыт [показать]
     
  • 4.114, Anonizmus, 22:05, 30/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Я вот до сих пор не могу понять почему массовые автомобили не выпускают из алюми... весь текст скрыт [показать]
     
     
  • 5.119, Аноним, 04:21, 31/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Потому что он мягкий как черти что, и при ДТП из юзера будет фарш Обратите вним... весь текст скрыт [показать]
     
     
  • 6.130, Аноним, 02:23, 01/08/2014 [^] [ответить] [смотреть все]  
  • +/
    Скорее, потому что дорогой Мягкость и разушаемость материалов при аварии наборо... весь текст скрыт [показать]
     
  • 2.50, an, 16:06, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • –1 +/
    как я понимаю микрокод и аппаратный алгоритм процессора по сути компонент таск... весь текст скрыт [показать] [показать ветку]
     
  • 1.14, bav, 10:19, 29/07/2014 [ответить] [смотреть все]  
  • +1 +/
    Гг. Осталось теперь математически доказать надежность всех остальных сервисов, которые делаю этот обглодышь минимально юзабельным.
     
     
  • 2.26, Аноним, 11:28, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • –2 +/
    Летают и работают А у вас в протоны датчики уебиметром заколачивают Чья б мыча... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.32, Гость, 12:33, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Что доказывает качество конструкции и огромный запас прочности, на фоне которого... весь текст скрыт [показать]
     
     
  • 4.33, rain87, 13:13, 29/07/2014 [^] [ответить] [смотреть все]  
  • +1 +/
    ровно до тех пор, пока датчик вверх ногами не прикувалдят
     
  • 3.65, Аноним, 18:47, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Конкретно с seL4 летает, вероятно очень мало всего А это аппаратный баг, от нег... весь текст скрыт [показать]
     
  • 1.15, Аноним, 10:21, 29/07/2014 [ответить] [смотреть все]  
  • +14 +/
    Ща поверх него запилят "сверхнадёжное" ПО на JavaScript и HTML5.
     
  • 1.16, Аноним, 10:27, 29/07/2014 [ответить] [смотреть все]  
  • +8 +/
    Надо еще доказать корректность компилятора которым это все собирается.
     
     
  • 2.35, Mirraz, 13:37, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +3 +/
    А ещё математически доказать 100 надёжность и корректность работы процессоров, ... весь текст скрыт [показать] [показать ветку]
     
  • 2.36, Аноним, 13:41, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +1 +/
    http compcert inria fr ... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.86, Аноним, 00:47, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    А что, сам на себе без багов он писаться не захотел А то он на ocaml завязан и ... весь текст скрыт [показать]
     
  • 1.18, IMHO, 10:32, 29/07/2014 [ответить] [смотреть все]  
  • +/
    еще одно ядро
     
  • 1.19, хрю, 10:41, 29/07/2014 [ответить] [смотреть все]  
  • +2 +/
    там кода кот наплакал. код, конечно, легко читается и всё такое, но там ничего особо и нет. плюс оно, как я понимаю, не реалтайм.
     
     
  • 2.20, IMHO, 10:48, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +1 +/
    ну так правильно, с тяжолым ядром в верх не полетишь, избавляются от груза
     
  • 2.68, Аноним, 18:54, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +3 +/
    Так в этом то и весь пойнт сверхнадежных - надо спихнуть все проблемы на других,... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.76, Mihail Zenkov, 19:27, 29/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Нет, здесь принцип не бери на себя большую ответственность, чем реально можешь п... весь текст скрыт [показать]
     
     
  • 4.87, Аноним, 00:48, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ну так я и говорю - для вычислений большинства человекам хватит деревянных счет ... весь текст скрыт [показать]
     
  • 1.22, Аноним, 10:54, 29/07/2014 [ответить] [смотреть все]  
  • –2 +/
    > GPLv2, так и компоненты под лицензией BSD

    Франкенштейн

     
  • 1.24, Аноним, 11:20, 29/07/2014 [ответить] [смотреть все]  
  • +/
    Персиянские операторы Автобазы подтверждают ... весь текст скрыт [показать]
     
  • 1.27, Аноним, 11:35, 29/07/2014 [ответить] [смотреть все]  
  • –2 +/
    Ну что, ждем новости типа В ядре seL4 обнаружена критическая уязвимость ... весь текст скрыт [показать]
     
     
  • 2.47, YetAnotherOnanym, 15:54, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +1 +/
    Да-да-да, вполне возможно, что ошибки не могут в спецификации ... весь текст скрыт [показать] [показать ветку]
     
  • 1.28, Какаянахренразница, 11:52, 29/07/2014 [ответить] [смотреть все]  
  • +3 +/
    > Открыт код сверхнадёжного микроядра seL4

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

     
  • 1.30, chinarulezzz, 12:08, 29/07/2014 [ответить] [смотреть все]  
  • +/
    Просто офигительная новость. Актуальное микроядро под GPL лицензией, да еще и нашедшее реальное применение - это то, что когда-то не хватило GNU.
     
     
  • 2.31, ШТО, 12:30, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +3 +/
    К сожалению, сейчас оно не подойдет для GNU, так как нужна лицензия GPLv3 , инач... весь текст скрыт [показать] [показать ветку]
     
  • 1.34, Аноним, 13:34, 29/07/2014 [ответить] [смотреть все]  
  • –2 +/
    где то уже читал про математическое доказательство и микроядро, и при чем недавн... весь текст скрыт [показать]
     
     
  • 2.38, Аноним, 14:03, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +7 +/
    > где то уже читал про математическое доказательство и микроядро, и при чем недавно ...

    если читал там, где "где-то" пишут без дефиса, а "причём" раздельно, то это был дилетантский бред

     
     
  • 3.44, Аноним, 15:39, 29/07/2014 [^] [ответить] [смотреть все]  
  • +3 +/
    Ну чего набросились, парень радуется, что читать научился Следующий этап - науч... весь текст скрыт [показать]
     
  • 1.42, trdm, 14:56, 29/07/2014 [ответить] [смотреть все]  
  • –1 +/
    Кажется беспилотник уже ломали в 2012 году.
    Уверены они что система надежная?
    http://xakep.ru/news/58149/
     
     
  • 2.56, Алексей, 16:59, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +1 +/
    По сути они заглушили сигналы GPS и подменили их своими Никакого взлома тут не ... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.91, Аноним, 04:23, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Хорошо бы, ибо - тупик - 124 да вот только в отличае от тебя - амеры не д... весь текст скрыт [показать]
     
     
  • 4.103, Аноним, 17:30, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Ну, так все правильно - днем же звезд не видать Как же с гороскопом без звезд-т... весь текст скрыт [показать]
     
     
  • 5.109, Anonizmus, 20:48, 30/07/2014 [^] [ответить] [смотреть все]  
  • –1 +/
    Вот немецкая разведка с помощью форса гороскопов сорвала отступление французских... весь текст скрыт [показать]
     
  • 1.43, my, 15:06, 29/07/2014 [ответить] [смотреть все]  
  • –1 +/
    Что-то не компилится.
    > as: unrecognized option '-mcpu=cortex-a9'
     
     
  • 2.48, Kodir, 15:58, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    Там надо исправить: '-mcpu=microwave'
     
     
  • 3.74, Аноним, 19:14, 29/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Судя по вышеизложеннному, -mcpu F-16 ... весь текст скрыт [показать]
     
  • 2.128, Аноним, 02:14, 01/08/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    Ну если ты пытаешься заставить ассемблер с компилировать код с оптимизацией под ... весь текст скрыт [показать] [показать ветку]
     
  • 1.45, Zenitur, 15:43, 29/07/2014 [ответить] [смотреть все]  
  • –1 +/
    Если там не Systemd то ненужно. Ведь всё, на чём нет Systemdб крутые хакеры объявляют устаревшим и не модным.
     
     
  • 2.49, Andrey Mitrofanov, 16:01, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    Пусть Поттер это генералу Динамиксу в лицо скажет! >/<
     
  • 1.51, Пропатентный тролль, 16:09, 29/07/2014 [ответить] [смотреть все]  
  • –1 +/
    А была ли доказана безошибочность программ, которые использовались при провекри безошибочности?
     
     
  • 2.78, Аноним, 22:06, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • –1 +/
    А была ли доказана безошибочность программ, которые использовались при проверке ... весь текст скрыт [показать] [показать ветку]
     
     
  • 3.92, Аноним, 04:24, 30/07/2014 [^] [ответить] [смотреть все]  
  • +/
    Нет не была. Почему тест крэшился :))))

     
  • 1.59, Аноним, 17:12, 29/07/2014 [ответить] [смотреть все]  
  • –4 +/
    Чем оно надёжнее проверенного Windows Core?
     
     
  • 2.67, Аноним, 18:52, 29/07/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +4 +/
    > Чем оно надёжнее проверенного Windows Core?

    Чем windows core.

     
  • 1.102, Аноним, 16:15, 30/07/2014 [ответить] [смотреть все]  
  • –1 +/
    Рилтайм от блекбери круче, инф100!1 да и кореос торт а не печенько рекламное
     
  • 1.107, Anonizmus, 20:43, 30/07/2014 [ответить] [смотреть все]  
  • –1 +/
    Это что попытка диверсии типа программы "Звездных войн"?

     
     
  • 2.129, Аноним, 02:17, 01/08/2014 [^] [ответить] [смотреть все] [показать ветку]  
  • +/
    Звери, а не люди провоцируют вероятного противника писать софт вместо того, что... весь текст скрыт [показать] [показать ветку]
     

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


      Закладки на сайте
      Проследить за страницей
    Created 1996-2017 by Maxim Chirkov  
    ДобавитьРекламаВебмастеруГИД  
    Hosting by Ihor