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

"Выполнена формальная верификация безопасности микроядра seL4 для архитектуры AArch64"	+/–
Сообщение от opennews (??), 24-Авг-26, 21:44
Завершена работа над математической формальной верификацией надёжности и безопасности  работы микроядра seL4  на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и  гарантирующих отсутствие сбоев... Подробнее: https://www.opennet.ru/opennews/art.shtml?num=66127
Ответить | Правка | Cообщить модератору

Сообщения

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

1. Сообщение от Аноним (1), 24-Авг-26, 21:44	+/–
Как там с производительностью?
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #3, #7, #10

2. Сообщение от Аноним (2), 24-Авг-26, 22:00	+/–
Объясните дауну, что такое формальная верификация. Желательно на пальцах.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #4, #6, #11

3. Сообщение от Мемоним (?), 24-Авг-26, 22:04	–3 +/–
Плохо. Ни одного CVE.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

4. Сообщение от Аноним (2), 24-Авг-26, 22:06	+/–
Для меня "формально" - это типо оно как бы есть но можно закрыть глаза. А тут че то все молятся на нее
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2 Ответы: #19

5. Сообщение от Аноним (5), 24-Авг-26, 22:16    Скрыто ботом-модератором	+/–
Quis custodiet ipsos custodes? Где формальное доказательство того, что верификация непорочна?
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #29

6. Сообщение от Цыган (?), 24-Авг-26, 22:17	+2 +/–
Красивое слово для толстосумов, чтобы выбить стипендии и гранты.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2 Ответы: #28

7. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:18	+1 +/–
Как и в любом микроядре - никак. Постоянные переключения контекста, сбросы TLB и просто cache thrashing, со всеми вытекающими.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

8. Сообщение от Мемоним (?), 24-Авг-26, 22:18	+/–
Дело конечно хорошее и правильное. Правда список принятых допущений делает немного грустить. https://sel4.systems/Verification/assumptions.html Особенно > Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions. Тут Intelы с AMDами машут ручкой.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #9, #12, #14, #38

9. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:18	+1 +/–
Не, ну если железо того, то уже ничего не спасёт. Хоть с верификацией, хоть без.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8 Ответы: #13

10. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:20	+3 +/–
Если нужна простая и доступная аналогия - это fuse против kernel-mode на конских IOPS и небольших блоках.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1 Ответы: #15

11. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:24	+/–
Если по простому - это значит, что записали допущения на входе и ожидаемый результат и доказали математически (не прогоном тестов, а именно вот как теоремы доказывают), что код при входных допущениях приводит к ожидаемому результату Тут, конечно, остаётся проблема, что сама формальная спецификация (то, как записаны допущения и результат) должны не иметь ошибок + система проверки тоже хорошо чтобы багов не имело. Тем не менее, идея формальной верификации мне лично всегда импонировала
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2

12. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:26	+/–
Так сказать, наполовину пуст или полон. Мне вот лично кажется большим достижением то, что у них не прописано доверие компилятору - бинарный код тоже формально верифицируется. А ведь это большое дело!
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8 Ответы: #23, #24

13. Сообщение от Мемоним (?), 24-Авг-26, 22:27	+/–
> Не, ну если железо того, то уже ничего не спасёт. Хоть с > верификацией, хоть без. Чисто теоретически, исходники железа тоже можно верифицировать. Только там объем доказательств не под силу даже самой мощной нейронке.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #9 Ответы: #16, #21, #31

14. Сообщение от Аноним (30), 24-Авг-26, 22:28	+/–
Ну так тут ничего удивительного нет. Разработчики ядра не могут ничего с железом сделать, они не отвечают за дыры в нём.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8 Ответы: #18

15. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:30	+1 +/–
Вот интересно, можно ли монолитное ядро с верификацией делать? В монолитке драйверы устройств смогут положить ОСь конкретно и плакали гарантии (если сами драйверы не верифицировать, но драйверы делать-то лениво, не то что ещё верифицировать...) В микроядре в теории, сколько помню, бажный драйвер не должен понять ОСь, впрочем как будто   смысл идеальной ОСи, если железом она управляет через кривой драйвер... Но хоть что-то
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #10 Ответы: #17, #20, #26, #30

16. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:31	+/–
А я слышал железнячники вроде какие-то верификации у себя проводят, чтобы сложные железки собирать, разве нет?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #13

17. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:32	+/–
* не должен ронять ОСь
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

18. Сообщение от Мемоним (?), 24-Авг-26, 22:34	+/–
> Ну так тут ничего удивительного нет. Разработчики ядра не могут ничего с > железом сделать, они не отвечают за дыры в нём. Все так. Просто это надо всегда явно и жирно прописывать. А не вот так: > Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #14 Ответы: #22

19. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:35	+/–
Ну так сила в том, что можно по формальным правилам логики проверить корректность программы, сразу для всех допустимых входных данных. Никаких прогонов тестов, в которых можно что-то упустить - в принципе доказывается корректность работы Ну это в идеальном случае, конечно
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #4

20. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:36	+/–
Можно, но любая неверифицированная часть - снимает гарантию корректности, поэтому смысл? А делать целиком - ну разве что очень узкоспециализированное ядро под простое железо.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

21. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:37	+/–
Можно. Зависит от сложности. Z80 проще, x86 уже трудно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #13

22. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:49	+/–
> Все так. Просто это надо всегда явно и жирно прописывать. А не вот так: Но зачем? Штука настолько нишевая, что те, кому надо - это прекрасно понимают. А остальным оно и незачем.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #18

23. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:51	+/–
Да, конкретно для этой ниши верификация соответствия бинарника исходнику - почти обязательна.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #12

24. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:54	+/–
Чуть в сторону отступая - всегда поражало, как люди в тех конторах, где это реально нужно, работают (и нет, госконторы там конечно есть, но они в меньшинстве). Там, где шаг влево или шаг вправо - всё, приплыли. Сплошные нормы, регламенты, все эти перекрёстные проверки, исчерпывающие теоретические верификации и ещё дополнительные валидации к ним. Я бы чокнулся, это нужно особый грейд садо-мазо в голове иметь. С уклоном в садо.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #12 Ответы: #25, #32, #36

25. Сообщение от Tron is Whistling (?), 24-Авг-26, 22:54    Скрыто ботом-модератором	+/–
То есть простите, с уклоном в мазо. Которое к себе обращено короче.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #24

26. Сообщение от Tron is Whistling (?), 24-Авг-26, 23:00	+/–
Тут двояко. Если бажный драйвер попытается выйти из контекста своего юзерспейса - он получит по рукам. Но это не значит, что всё его использующее не ляжет с ошибкой обращения к драйверу. В общем-то тоже может быть и зачастую будет фатал. Зависит от драйвера, и того, как написана реакция конечного софта на то, что драйвер ляжет. Микроядро при этом не ляжет, да, но вот юзерспейсу может поплохеть. Если же бажный драйвер сконфигурит железо так, что оно например превратит шину в кашу или сделает замечательный DMA в память по рандомному адресу без IOMMU например - микроядро тут уже ничего сделать не сможет. А кое-где и IOMMU может не спасти.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

27. Сообщение от sage (??), 24-Авг-26, 23:06	+/–
А тексты с доказательствами есть? Я только аннонсы на сайте вижу.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #34

28. Сообщение от Аноним (28), 24-Авг-26, 23:07	–1 +/–
> Красивое слово для толстосумов, чтобы выбить стипендии и гранты. конечно, ровно таким макаром схлопнулся глубоководный аппарат Титан!
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6

29. Сообщение от Аноним (28), 24-Авг-26, 23:09    Скрыто ботом-модератором	+/–
> Quis custodiet ipsos custodes? Где формальное доказательство того, что верификация непорочна? неполна вероятно, как и любая формальная система.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #5

30. Сообщение от Аноним (30), 24-Авг-26, 23:17    Скрыто ботом-модератором	+/–
Уже есть частично верифицированное - Ironclad.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

31. Сообщение от Аноним (28), 24-Авг-26, 23:19	+/–
> Только там объем доказательств не под силу даже самой мощной нейронке. Индукцию применяют.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #13

32. Сообщение от Аноним (28), 24-Авг-26, 23:21    Скрыто ботом-модератором	+/–
> Я бы чокнулся, это нужно особый грейд садо-мазо в голове иметь. С > уклоном в садо. это же не в одно рыло, и тем более все по четко расписанному плану.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #24 Ответы: #33

33. Сообщение от Tron is Whistling (?), 24-Авг-26, 23:24	+/–
Да хоть бы и не в одно. Всё равно люто. Лишний раз чихнуть - по протоколу.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #32 Ответы: #35

34. Сообщение от Аноним (34), 25-Авг-26, 00:09	+/–
главное верить
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #27

35. Сообщение от Аноним (28), 25-Авг-26, 00:53	+/–
> Да хоть бы и не в одно. Всё равно люто. Лишний раз > чихнуть - по протоколу. И тут даже не все можно предвидеть и формализовать, к примеру допускаем ли мы ситуацию когда во время процесса сложения двух чисел, числа изменились (под воздействием радиации)? Что тогда? Есть вход, есть коробочка (операция, функция, вычислитель - не важно) и есть выход. Вот и формальное доказательство нам должно давать гарантии, что при каждом входе будет ожидаемых выход, а также должно содержать доказательство ситуаций воздействия на эту коробочку.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #33 Ответы: #37

36. Сообщение от Аноним10084 и 1008465039 (?), 25-Авг-26, 01:08	+/–
Читал про NASA и совсем чуть-чуть про авиа-инженерию - меня скорее даже поражало, как они умудряются при этих всех регламентах что-то делать и даже относительно безопасно делать (да, про провалы NASA и прочих Боингов я в курсе, они не без греха, но если бы там писали ПО так, как пишут в простом сайтостроении - не летали бы ни самолёты, ни корабли вообще) Обычно когда в коммерческой разработке пытаются что-то там зарегламентировать и перепроверить, становится медленно, неэффективно и дорого. Впрочем, бюджет NASA и впрямь был огромен, может секрет во многом и в нём
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #24

37. Сообщение от Аноним10084 и 1008465039 (?), 25-Авг-26, 01:10	+/–
Насколько я понимаю, в подобных системах на космических кораблях и подобном сверхвысоком уровне критичности много дублируют. Грубо говоря, три бортовых компьютера делают вычисление, выбирают правильный результат консенсусом, а ошибившегося могут в ребут отправить
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #35

38. Сообщение от Аноним (5), 25-Авг-26, 01:17	+/–
Верификация верифицирует в зоне своей ответственности. Иначе придётся доказывать заодно и то, что вселенная существует. И как она существует.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8

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

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