| |
| 2.7, Tron is Whistling (?), 22:18, 24/08/2026 [^] [^^] [^^^] [ответить]
| +2 +/– |
Как и в любом микроядре - никак.
Постоянные переключения контекста, сбросы TLB и просто cache thrashing, со всеми вытекающими.
| | |
| 2.10, Tron is Whistling (?), 22:20, 24/08/2026 [^] [^^] [^^^] [ответить]
| +2 +/– |
Если нужна простая и доступная аналогия - это fuse против kernel-mode на конских IOPS и небольших блоках.
| | |
| |
| 3.15, Аноним10084 и 1008465039 (?), 22:30, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
Вот интересно, можно ли монолитное ядро с верификацией делать? В монолитке драйверы устройств смогут положить ОСь конкретно и плакали гарантии (если сами драйверы не верифицировать, но драйверы делать-то лениво, не то что ещё верифицировать...) В микроядре в теории, сколько помню, бажный драйвер не должен понять ОСь, впрочем как будто смысл идеальной ОСи, если железом она управляет через кривой драйвер... Но хоть что-то
| | |
| |
| 4.20, Tron is Whistling (?), 22:36, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
Можно, но любая неверифицированная часть - снимает гарантию корректности, поэтому смысл?
А делать целиком - ну разве что очень узкоспециализированное ядро под простое железо.
| | |
| 4.26, Tron is Whistling (?), 23:00, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
Тут двояко.
Если бажный драйвер попытается выйти из контекста своего юзерспейса - он получит по рукам.
Но это не значит, что всё его использующее не ляжет с ошибкой обращения к драйверу. В общем-то тоже может быть и зачастую будет фатал. Зависит от драйвера, и того, как написана реакция конечного софта на то, что драйвер ляжет. Микроядро при этом не ляжет, да, но вот юзерспейсу может поплохеть.
Если же бажный драйвер сконфигурит железо так, что оно например превратит шину в кашу или сделает замечательный DMA в память по рандомному адресу без IOMMU например - микроядро тут уже ничего сделать не сможет. А кое-где и IOMMU может не спасти.
| | |
|
|
|
| 1.2, Аноним (2), 22:00, 24/08/2026 [ответить] [﹢﹢﹢] [ · · · ]
| +/– |
Объясните дауну, что такое формальная верификация. Желательно на пальцах.
| | |
| |
| 2.4, Аноним (2), 22:06, 24/08/2026 [^] [^^] [^^^] [ответить]
| +1 +/– |
Для меня "формально" - это типо оно как бы есть но можно закрыть глаза.
А тут че то все молятся на нее
| | |
| |
| 3.19, Аноним10084 и 1008465039 (?), 22:35, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
Ну так сила в том, что можно по формальным правилам логики проверить корректность программы, сразу для всех допустимых входных данных. Никаких прогонов тестов, в которых можно что-то упустить - в принципе доказывается корректность работы
Ну это в идеальном случае, конечно
| | |
|
| 2.6, Цыган (?), 22:17, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
Красивое слово для толстосумов, чтобы выбить стипендии и гранты.
| | |
| |
| 3.28, Аноним (28), 23:07, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
> Красивое слово для толстосумов, чтобы выбить стипендии и гранты.
конечно, ровно таким макаром схлопнулся глубоководный аппарат Титан!
| | |
|
| 2.11, Аноним10084 и 1008465039 (?), 22:24, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
Если по простому - это значит, что записали допущения на входе и ожидаемый результат и доказали математически (не прогоном тестов, а именно вот как теоремы доказывают), что код при входных допущениях приводит к ожидаемому результату
Тут, конечно, остаётся проблема, что сама формальная спецификация (то, как записаны допущения и результат) должны не иметь ошибок + система проверки тоже хорошо чтобы багов не имело. Тем не менее, идея формальной верификации мне лично всегда импонировала
| | |
|
| 1.8, Мемоним (?), 22:18, 24/08/2026 [ответить] [﹢﹢﹢] [ · · · ]
| +/– | |
Дело конечно хорошее и правильное. Правда список принятых допущений делает немного грустить.
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ами машут ручкой.
| | |
| |
| |
| 3.13, Мемоним (?), 22:27, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
> Не, ну если железо того, то уже ничего не спасёт. Хоть с
> верификацией, хоть без.
Чисто теоретически, исходники железа тоже можно верифицировать. Только там объем доказательств не под силу даже самой мощной нейронке.
| | |
| |
| 4.31, Аноним (28), 23:19, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
> Только там объем доказательств не под силу даже самой мощной нейронке.
Индукцию применяют.
| | |
|
|
| 2.12, Аноним10084 и 1008465039 (?), 22:26, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
Так сказать, наполовину пуст или полон.
Мне вот лично кажется большим достижением то, что у них не прописано доверие компилятору - бинарный код тоже формально верифицируется. А ведь это большое дело!
| | |
| |
| 3.24, Tron is Whistling (?), 22:54, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
Чуть в сторону отступая - всегда поражало, как люди в тех конторах, где это реально нужно, работают (и нет, госконторы там конечно есть, но они в меньшинстве). Там, где шаг влево или шаг вправо - всё, приплыли. Сплошные нормы, регламенты, все эти перекрёстные проверки, исчерпывающие теоретические верификации и ещё дополнительные валидации к ним.
Я бы чокнулся, это нужно особый грейд садо-мазо в голове иметь. С уклоном в садо.
| | |
|
| 2.14, Аноним (30), 22:28, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
Ну так тут ничего удивительного нет. Разработчики ядра не могут ничего с железом сделать, они не отвечают за дыры в нём.
| | |
| |
| 3.18, Мемоним (?), 22:34, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– |
> Ну так тут ничего удивительного нет. Разработчики ядра не могут ничего с
> железом сделать, они не отвечают за дыры в нём.
Все так. Просто это надо всегда явно и жирно прописывать. А не вот так:
> Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев. | | |
| |
| 4.22, Tron is Whistling (?), 22:49, 24/08/2026 [^] [^^] [^^^] [ответить]
| +/– | |
> Все так. Просто это надо всегда явно и жирно прописывать. А не вот так:
Но зачем? Штука настолько нишевая, что те, кому надо - это прекрасно понимают. А остальным оно и незачем.
| | |
|
|
|
| 1.27, sage (??), 23:06, 24/08/2026 [ответить] [﹢﹢﹢] [ · · · ]
| +/– |
А тексты с доказательствами есть? Я только аннонсы на сайте вижу.
| | |
|
