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

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

Сообщения

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

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

	3. "Выполнена формальная верификация безопасности микроядра seL4..."	–2 +/–
	Сообщение от Мемоним (?), 24-Авг-26, 22:04
	Плохо. Ни одного CVE.
	Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

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

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

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

8. "Выполнена формальная верификация безопасности микроядра seL4..."	+/–
Сообщение от Мемоним (?), 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. "Выполнена формальная верификация безопасности микроядра seL4..."	+/–
	Сообщение от Tron is Whistling (?), 24-Авг-26, 22:18
	Не, ну если железо того, то уже ничего не спасёт. Хоть с верификацией, хоть без.
	Ответить | Правка | Наверх | Cообщить модератору

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

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