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

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

Сообщения

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

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

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

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

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

6. Сообщение от Цыган (?), 24-Авг-26, 22:17	+4 +/–
Красивое слово для толстосумов, чтобы выбить стипендии и гранты.
Ответить | Правка | Наверх | 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	+6 +/–
Если нужна простая и доступная аналогия - это fuse против kernel-mode на конских IOPS и небольших блоках.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1 Ответы: #15

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

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

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

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

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

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

17. Сообщение от Аноним10084 и 1008465039 (?), 24-Авг-26, 22:32	+1 +/–
* не должен ронять ОСь
Ответить | Правка | Наверх | 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	+1 +/–
Можно, но любая неверифицированная часть - снимает гарантию корректности, поэтому смысл? А делать целиком - ну разве что очень узкоспециализированное ядро под простое железо.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

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

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

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

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	+1 +/–
главное верить
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #27

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

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

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

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

39. Сообщение от Аноним (28), 25-Авг-26, 02:41	+/–
> Насколько я понимаю, в подобных системах на космических кораблях и подобном сверхвысоком > уровне критичности много дублируют. Грубо говоря, три бортовых компьютера делают вычисление, > выбирают правильный результат консенсусом, а ошибившегося могут в ребут отправить я как раз об этом, но тут есть свои приколы, если условно эти три коробочки одинаковые, то и воздействие на них (не предусмотренное и нарушающее их внутреннее состояние) будет одинаковое. Поэтому это не всегда помогает, ибо если реально есть внешнее воздействие на один, то оно же и воздействует на другие. В таких случаях эти условно три коробки должны быть как бы разной архитектуры, ну подобно механическим каким то датчикам (аналоговыми) или цифровым, то есть дублирование функциональное должно быть, а не архитектурное (конструктивное).
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #37

40. Сообщение от Норм (?), 25-Авг-26, 04:37	+1 +/–
Можно все что угодно. Разделение логическое больше чем реальное в плане железа и путей кода. Но линукс не получится. Не потому, что оно "монолитное", а потому что помойка, и кроме проблемы качества кода с указателями на войд, у него нету банально стабильного апи нонсенс. Верифицировать нечего, интерфейс не определен. Чудо что оно вообще работает.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

41. Сообщение от Норм (?), 25-Авг-26, 04:45	+3 +/–
Это очень хорошо, если все ляжет. На самом деле. Гораздо хуже, если оно вот сделает как вы в конце описали, и не ляжет. Я на FreeBSD видел ужас которого быть по идее не может, а он есть. Дров сетевухи выдал ошибку, а ос стала записывать ввод консоли в случайное место на диске. ZFS не востановился после такого понятно никак. Хотя большую часть данных смог вытянуть с трупика.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #26 Ответы: #46, #48

42. Сообщение от Аноним (42), 25-Авг-26, 06:09	+1 +/–
А практически - гуглите single event upset
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #13

44. Сообщение от Sm0ke85 (ok), 25-Авг-26, 07:21	–1 +/–
Интересно бы было увидеть/пощупать гну-дистрибутив на этом ядре, а то в линуксовое ядро потихоньку слоп заезжает с растом... Кстати, кто-нибудь в курсе на чем оно написано? (лицензия, я так понял, гпл2)
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #49, #72

45. Сообщение от Tron is Whistling (?), 25-Авг-26, 08:05	+/–
Да вот и я о том же. Выхлоп примерно схож, несмотря на то, что всё рельсами прибито. В итоге всё равно или сбой или человеческий фактор, но зато по одной половице ходили. По отраслям - в основном это биржевой и банковский сектор + сложные физические производства. Я как-то сунулся, там нужно больше регламенты знать чем реально строить, и больше в эти вещи не лезу, мне там тупо скучно. Свободным хирургом проще. Открыли, что надо - отрезали, что не надо - подшили, что не понравилось - тоже отрезали коту под стол, закрыли. Если что - ещё откроем :D
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #35 Ответы: #70

46. Сообщение от Tron is Whistling (?), 25-Авг-26, 08:09	+/–
Ну тут больше заточено на системы управления, которые могут ситуацию обнаружить и хотя бы перезапуститься через монитор, который с драйверами в целом не взаимодействует, только вотчдоги мониторит. Пока микроядро не легло, этот самый монитор будет пытаться переподнять всё, вплоть до железа, и через какой-нибудь дубовый встроенный прямо в SoC нешинный JTAG/RS232/CAN при этом слать индикацию, что ж0па случилась. Вполне реальная применимость именно рядом с машинерией - станки, автомобили, корабли, самолёты, etc. Где I/O по-минимуму, и надо просто _не торопясь_ контроллеры устройств мониторить + обрабатывать агрегированные от них сигналы.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #41 Ответы: #52

47. Сообщение от Tron is Whistling (?), 25-Авг-26, 08:12	+/–
Вот да. Но в общем поэтому SpaceX и выстрелил.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #36 Ответы: #57

48. Сообщение от Аноним (48), 25-Авг-26, 08:15	+/–
А чё за сетевуха? Друг интересуется.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #41 Ответы: #50

49. Сообщение от Tron is Whistling (?), 25-Авг-26, 08:15	+/–
> Интересно бы было увидеть/пощупать гну-дистрибутив на этом ядре, а то в линуксовое > ядро потихоньку слоп заезжает с растом... Це вряд ли, это не для общего применения. Нишевая штука для специфичных задач вроде систем управления контроллерами. В теории можно под какой-нибудь хотя бы обрезок от qemu попробовать собрать и окружение для GNU, но кому оно сильно надо, учитывая, что если само окружение не доверенное и особенности модели с микроядром не учитывает, то большого толку от микроядра нет?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #44 Ответы: #51

50. Сообщение от Норм (?), 25-Авг-26, 08:18	+1 +/–
> А чё за сетевуха? Друг интересуется. Chelsio T540-CR
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #48 Ответы: #55

51. Сообщение от Sm0ke85 (ok), 25-Авг-26, 08:24	+/–
>Це вряд ли, это не для общего применения. Нишевая штука для специфичных задач вроде систем управления контроллерами. Там в описании вроде и сервера упомянаются, потому я и понадеялся. >В теории можно под какой-нибудь хотя бы обрезок от qemu попробовать собрать и окружение для GNU, но кому оно сильно надо, учитывая, что если само окружение не доверенное и особенности модели с микроядром не учитывает, то большого толку от микроядра нет? Все равно интересно что получилось бы))) Макось же на микроядре функционирует как-то, авось и эта штука получилась бы жизнеспособной, просто Линукс начал опасения вызывать, а тут была б альтернатива/конкурент, ведь оно, так понимаю, гпл)))
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #49 Ответы: #58

52. Сообщение от Норм (?), 25-Авг-26, 08:25	+/–
> Ну тут больше заточено на системы управления, которые могут ситуацию обнаружить и Это конкретное видимо да. А так QNX успешно как общего назначения ос работал. Тот же энтот, Redox. Зависит как чего и куда готовить. В монолитном линуксе много чего в кеш линии не влезает. Ну и с системдой пишущей вон гиг на диск от десятка мег логов, о всяком ио не приходится говорить. Кстати не просто так существовали и существую юзер спейс сетевые стеки. Лазить туда сюда в ядро линукса накладно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #46 Ответы: #54

53. Сообщение от Рулона Боева (?), 25-Авг-26, 08:31	+/–
Да, но это больше как юнит-тесты, проверяем корректность последовательности выходных сигналов платы при определенных последовательностях входных
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #16

54. Сообщение от Tron is Whistling (?), 25-Авг-26, 09:50	+/–
> А так QNX успешно как общего назначения ос работал. С QNX ныне почти все в производительных системах послезали - забодало. Оно реально дубовое и тормозное, даже для систем управления. > Тот же энтот, Redox. Штоэто. Оно никогда не работало, и скорее всего не будет. > В монолитном линуксе много чего в кеш линии не влезает. Микроядро эту ситуацию усугубляет в разы. > Кстати не просто так существовали и существую юзер спейс сетевые стеки. Лазить туда сюда в ядро линукса накладно. Именно. А с микроядрами так приходится лазить за всем абсолютно. И никак не обойти.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #52

55. Сообщение от Tron is Whistling (?), 25-Авг-26, 09:52	+/–
> Chelsio T540-CR Дай угадаю, IOMMU не было или выключен? Chelsio с их DMA вообще без IOMMU эксплуатировать нельзя.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #50

56. Сообщение от Айтышнык в полёте (?), 25-Авг-26, 09:52	+/–
Я лпишу как это делается в гражданской авиации по стандарту РФ КТ-178С.егг можно найти в инете и почитать для понятия глубины всех наших глубин. Вот представь что выдается ТЗ на программный продукт. Но выдается не одному прогеру и тестировщику, а целой организации, где програмисты и тестировшики не самые важные люди. Из ТЗ делают специалисты системные требования, которые лписывают в целом ПО и его окружения и на чем ПО жолжна запускаться при каких условиях окружения (железка, набор системных библиотек, частоты, объем памяти, переферия, температура, условия безопасности и т.п.). Требования оформлены должны быть лпределённым способом, написаны в соответствии с стандартом на составление системных требований(например каждое требование уникально, каждое требование предъявляет только одно условие к ПО, непротиворечивость друг другу, полноту всех требований к устройству и т.п.) далее из них делают требования высокого уровня и разрабатывают архитектуру и из них делают требования низкого уровня, которые так же написаны в соответствии со стандартами. После того как они 6аписаны и верифицированы независимыми разработчиками требований. В общем только после этого приступают к коду. Код пишут не абы как а как реализацию этих требований низкого уровня с трассировкой на них. После этого за дело беруться верификаторы которые сверяют на сколько код соответствует требованиям низкого уровня. Вся сверка происходит в соответствии с протоколом который написан в соответствии со стандартом на ПО где расписаны те цели которые должно ПО достичь. (Например: есть ли код который написан не в соответствии с ТНУ и не оправдан системными требованиями и требованиями к архитектуре ПО. Код написан в соответствии со стандартами кодирования? (А это например MISRA или  PEP) Ну и прочее. Та же трассировка является одним из вопросов.) Оформляется протокол он проходит независимым колегой ревью и вот можно сказать что код прошел формальную верификацию. Тоесть это кусочек только всего огромного процесса прослеживаемости от идеи и задачи до реализации.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2

57. Сообщение от Айтышнык в полёте (?), 25-Авг-26, 09:58	+/–
А вы вкурсе что существует организация по безопасности полетов в США. Аналог нашей РосАвиации? Так вот к ним не придешь просто со словами: у нас все намази, зуб даю. SpaceX выстрелила из-за организации работ а делают они это все по тем де стандартам что и НАСА иначе им никто не разрешит ничего в воздух запускать. Американские и Европейские стандарты это самые надежные и проверенные. Если самолет получает сертификацию либо ьам либо там то почти любая страна без вопросов выдает летное национальное свидетельство. Все знают что эти ребята уже во все врзможные места с микроскопом залезли ьез ващелина и проверили очень тщательно. Но идеала не существует и обмануть всеравно можно. Но лучше низ никто не умеет проверять
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #47 Ответы: #61, #65, #66

58. Сообщение от Tron is Whistling (?), 25-Авг-26, 09:59	+1 +/–
> Макось же на микроядре функционирует как-то, Ну как, функционирует... Попробуйте её вне полтора моделей поддерживаемого железа запустить... Можно, но пляски с бубном и куча граблей разложена.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #51 Ответы: #69

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

60. Сообщение от Жироватт (ok), 25-Авг-26, 10:09	+/–
> Ну, мы ента, вместо того, чтобы реально тестировать на чётких тестах и делать фаззинг для всего остального прогоняем по исходному коду особую программу, которая строит полный граф выполнения, от запуска (всех точек запуска со всеми параметрами) до завершения и проверили, что формально там граф выполнения выполняет только прошедший проверку компилятором код. Также наша чюдо-программа смотрит спеки интерфейсов и допускает только безопасное подмножество интеропа: тип-в-тип и принудительно проверяет указатели. Еще очень сильно ругается на вывод типа, на неявные объявления и оптимизации. Выглядит красиво, распечаток много, бумажка с печатью, инвесторам нраица. А вот проверять то, что программа выдаёт осмысленный ли результат - не наша зона ответственности Как-то так
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2

61. Сообщение от Жироватт (ok), 25-Авг-26, 10:15	+/–
Настолько все хорошо, что новые боинги падают, а инженеры, которые рассказывают, как wetback'и кувалдометрами прибивают неподошедшее по нормам в фюзеляжу - саморасстреливаются из дробовика в спину?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #57 Ответы: #71

64. Сообщение от Смузихеб забывший пароль (?), 25-Авг-26, 10:43	+/–
с микрокодом ещё веселей
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #21

65. Сообщение от Смузихеб забывший пароль (?), 25-Авг-26, 10:52	+/–
Спейс-икс "выстрелил" т.к был карманной конторой того кого надо Помимо полностью безграничного бюджета Вплоть до того доходило, что с ними наса практически бесплатно делилась наработками, патентами и даже высококвалифицированным профильным персоналом. С одной стороны С другой - сша "доходчиво" объясняли на самом высоком уровне всем кто пользовался услугами по запуску сторонних контор из других стран почему им следовало бы пользоваться услугами именно конкретной конторы, "а то вдруг хуже может стать" Возможно ли подобное для реальной обычной мелкой конторки-стартапа с ограниченным бюджетом и потребностью в персонале, который штучный и через сайт поиска работы не найдёшь не считая огромной горы требований к оснащению ?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #57 Ответы: #68

66. Сообщение от Аноним (66), 25-Авг-26, 11:55	–1 +/–
> Так вот к ним не придешь просто со словами: у нас все намази, зуб даю. Боинг именно так и делал, пока его самолёты не начали падать. Соответствие регламентам FAA проверялось сотрудниками боинга, которые отчитывались в FAA, мол, у нас всё намази, зуб даю.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #57

67. Сообщение от Аноним10084 и 1008465039 (?), 25-Авг-26, 11:56	+/–
https://github.com/seL4/l4v/ тут должны лежать вроде
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #27 Ответы: #74

68. Сообщение от Аноним (-), 25-Авг-26, 12:05	+/–
> Спейс-икс "выстрелил" т.к был карманной конторой того кого надо Помимо полностью безграничного бюджета > Вплоть до того доходило, что с ними наса практически бесплатно делилась наработками, патентами и даже высококвалифицированным профильным персоналом. Ты сейчас рассказываешь о событиях после 2008, до 2008 года бюджет был сильно ограничен, и вся эта контора висела на волоске перед четвёртым запуском Falcon 1. Из государственных контор на их стороне в период с 2001 по 2008 были только вояки, но я не знаю ничего про то, чтоб они секретами делились в то время. Они помогли последний Falcon 1 самолётом доставить, потому что сроки реально все выходили и денег на продолжение деятельности уже не было. Тогда было так, что либо успешный запуск, попадание в программу NASA, что будет означать покупку будущих запусков с авансом прямо сейчас; либо дасвиданья спасеих, подавай на банкротство. Но в то же время FAA им тогда вставляла палки в колёса, отказываясь выдавать им лицензии на запуски, собственно из-за чего они и запускали с острова в Тихом Океане. У них по-моему первый запуск из-за этого и обломался: слишком долго ихняя ракета стояла на площадке, её солью разъело. И из-за этого для последнего запуска пришлось просить вояк о транспортном самолёте, чтоб ракету туда доставить за дни, а не за месяцы, как было бы при транспортировке кораблями. > Возможно ли подобное для реальной обычной мелкой конторки-стартапа с ограниченным бюджетом и потребностью в персонале, который штучный и через сайт поиска работы не найдёшь не считая огромной горы требований к оснащению? Да. Штучный персонал был подобран штучно. У Eric Berger есть книга Liftoff, описывающая первые 7 лет функционирования Space X, в частности откуда взялся этот штучный персонал. Если тебе интересен ответ на твой вопрос, то открой книги и почитай, а не выдумывай из головы.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #65

69. Сообщение от aname (ok), 25-Авг-26, 12:54	+/–
Будто в линухе пляски с бубном и грабли закончились. лол
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #58

70. Сообщение от Аноним (28), 25-Авг-26, 13:44	+/–
> Я как-то сунулся, там нужно больше регламенты знать чем реально строить, и > больше в эти вещи не лезу, мне там тупо скучно. Свободным > хирургом проще. Открыли, что надо - отрезали, что не надо - > подшили, что не понравилось - тоже отрезали коту под стол, закрыли. > Если что - ещё откроем :D Свободная (исследовательская) наука, как раз для таких. Академическая - сектантство!
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #45

71. Сообщение от Аноним (28), 25-Авг-26, 13:45	+/–
> Настолько все хорошо, что новые боинги падают, а инженеры, которые рассказывают, как > wetback'и кувалдометрами прибивают неподошедшее по нормам в фюзеляжу - саморасстреливаются > из дробовика в спину? Напомните ему про дырку в космическом аппарате, которая жвачкой была заделана :)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #61

72. Сообщение от нах. (?), 25-Авг-26, 13:49	+/–
на ЭТОМ невозможен никакой дистрибутив, потому что это не ядро. Внезапно. Микроядро - это DBUS, сколько раз еще вам повторять?! Это dbus возведенный в абсолют и вынесенный в ring0. ВСЁ! Остальное ты пишешь - САМ. У l4 и деривативов даже управления памятью нет.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #44

73. Сообщение от нах. (?), 25-Авг-26, 13:56	+/–
> IOMMU никак не поможет если к примеру загадить pci шину сошедшим с ума устройством. Ну или просто повиснуть в надежном-безопастном-юзерлевел драйвере диска. Ну работает у тебя дбас. А диска-то у тебя нет. Семь бед - один ресет. И запомните, что далеко не все устройства (почти никакие в общем случае) в писюке гарантированно можно оживить без физического ресета.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #26

74. Сообщение от sage (??), 25-Авг-26, 15:47	+/–
Да, похоже на то. Интересно, но нифига не понятно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #67

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

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