The OpenNET Project / Index page

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



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

Оглавление

Микроядро seL4 математически верифицировано для архитектуры ..., opennews (?), 10-Июн-20, (0) [смотреть все]

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


38. "Микроядро seL4 математически верифицировано для архитектуры ..."  –2 +/
Сообщение от vitalif (ok), 10-Июн-20, 15:22 
> при необходимости

ОЙ КАК ТОЛСТО...

Ответить | Правка | К родителю #32 | Наверх | Cообщить модератору

62. "Микроядро seL4 математически верифицировано для архитектуры ..."  +4 +/
Сообщение от erthink (ok), 10-Июн-20, 17:48 
> > при необходимости
> ОЙ КАК ТОЛСТО...

Видимо стоит уточнить для местных ихпёртов, которые (УВЫ) не читали, но осуждают.

Логика ядра верифицирована, но в реальных применениях это мало что даёт (смотрим на факапы Qualcomm и т.п.):
- без верификации всех "ассемблерных вставок" при использовании на конкретной платформе.
- без верификации логики служб и приложений (с учетом взаимодействия и средств контроля ОС).

Соответственно, "при необходимости" - относилось к верификации примитивов (связанных с "посадкой" ОС на какую-то конкретную платформу) и к верификации приложений.

TL;DR
Kaspersky OS предлагает контроль взаимодействия отдельных компонентов (служб, приложений) как с ядром, так и между собой - это принципиальное отличие от L4.
Грубо говоря, принципы безопасности/надежности L4 распространяются с ядра на все приложения, службы и систему в целом.

Ответить | Правка | Наверх | Cообщить модератору

67. "Микроядро seL4 математически верифицировано для архитектуры ..."  +2 +/
Сообщение от vitalif (ok), 10-Июн-20, 18:19 
Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не видел, а если даже откроют - то исходники не откроют. Но оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.

Примерно на уровне QP ОС.

L4 лучше хотя бы тем, что она реальна, а не иллюзорна.

Ответить | Правка | Наверх | Cообщить модератору

69. "Микроядро seL4 математически верифицировано для архитектуры ..."  +4 +/
Сообщение от erthink (ok), 10-Июн-20, 18:32 
> Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не
> видел, а если даже откроют - то исходники не откроют. Но
> оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.

Т.е. если вы не трогали луну руками, то её нет?

Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/
(если руки растут из нужного места).

Ответить | Правка | Наверх | Cообщить модератору

98. "Микроядро seL4 математически верифицировано для архитектуры ..."  +1 +/
Сообщение от Аноним (98), 10-Июн-20, 22:23 
Там есть исходный код ядра и его можно собрать и запустить со своими правками?
Ответить | Правка | Наверх | Cообщить модератору

99. "Микроядро seL4 математически верифицировано для архитектуры ..."  +/
Сообщение от erthink (ok), 10-Июн-20, 22:33 
> Там есть исходный код ядра и его можно собрать и запустить со
> своими правками?

Нет.
Но за подробностями лучше RTFM.

Ответить | Правка | Наверх | Cообщить модератору

135. "Микроядро seL4 математически верифицировано для архитектуры ..."  –1 +/
Сообщение от Аноним (161), 11-Июн-20, 10:55 
> Т.е. если вы не трогали луну руками, то её нет?

Разве это не принципиальный вопрос верификации?

> Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/

И что там дают? Уже собранную игрушку для написания хелловорлдов? Плюс "прямое согласие на сбор и обработку моих данных"

Ответить | Правка | К родителю #69 | Наверх | Cообщить модератору

200. "Микроядро seL4 математически верифицировано для архитектуры ..."  –1 +/
Сообщение от Аноним (-), 15-Июн-20, 06:31 
Как там грится? Джентльменамм верят на слово! И тут мне карта как поперла, как поперла!
Ответить | Правка | Наверх | Cообщить модератору

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

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




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

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