The OpenNET Project / Index page

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

Для Linux предложен механизм верификации корректности работы ядра

07.08.2022 17:48

Для включения в состав ядра Linux 5.20 (возможно, ветка получит номер 6.0) предложен набор патчей с реализацией механизма RV (Runtime Verification), представляющего средства для проверки корректности работы на высоконадежных системах, гарантирующих отсутствие сбоев. Проверка производится во время выполнения через прикрепление обработчиков к точкам трассировки, сверяющих фактический ход выполнения с заранее определённой эталонной детерминированной моделью автомата, определяющего ожидаемое поведение системы.

Информация от точек трассировки переводит модель из одного состояния в другое, и если новое состояние не соответствует параметрам модели, генерируется предупреждение или ядро переводится в состояние "panic" (подразумевается, что высоконадёжные системы будут определять подобные ситуации и реагировать на них). Модель автомата, определяющая переходы из одного состояния в другое, экспортируется в формат "dot" (graphviz), после чего транслируется при помощи утилиты dot2c в представление на языке Си, которое загружается в форме модуля ядра, отслеживающего отклонения хода выполнения от предопределённой модели.

Сверка с моделью во время выполнения позиционируется как более легковесный и простой для реализации на практике способ подтверждения корректности выполнения на критически важных системах, дополняющий классические методы подтверждения надёжности, такие как проверка модели и математические доказательства соответствия кода спецификациям, заданным на формальном языке. Из достоинств RV называется возможность обеспечить строгую верификацию без отдельной реализации всей системы на языке моделирования, а также гибкое реагирование на непредвиденные события, например, для блокирования дальнейшего распространения сбоя в критически важных системах.

  1. Главная ссылка к новости (https://www.phoronix.com/news/...)
  2. OpenNews: Red Hat и Google представили Sigstore, сервис для криптографической верификации кода
  3. OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
  4. OpenNews: Микроядро seL4 математически верифицировано для архитектуры RISC-V
  5. OpenNews: Прототип отечественной ОС Phantom на базе Genode будет готов до конца года
  6. OpenNews: Новая криптографическая библиотека EverCrypt с математическим доказательством надёжности
Лицензия: CC-BY
Наводку на новость прислал Аноним
Тип: К сведению
Короткая ссылка: https://opennet.ru/57605-kernel
Ключевые слова: kernel, linux, verification
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (123) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним228 (?), 18:02, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +12 +/
    Vendorlock с мобилок на компьютеры???
     
     
  • 2.12, Аноним (-), 18:13, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +5 +/
    + DRM
     
     
  • 3.58, Аноним (58), 08:38, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    мммм вкуснатищаааа навалите побольше этого добра!
     
     
  • 4.85, Копираст (?), 19:42, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +5 +/
    На тебе ещё телеметрию!
     
  • 4.97, Аноним (-), 02:39, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > мммм вкуснатищаааа навалите побольше этого добра!

    А оно там, видите ли, конфигуряемо. И половина из этого сойдет за секурити фичи, если системой рулите вы. А если не вы - ваша проблема на самом деле вот в этом. Вы хотите на кривой козе обходить механизмы операционки? Обманывая законного владельца системы? Так это не работает.

     
     
  • 5.132, Аноним (132), 22:23, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Оно больше на SecureBoot похоже, только не на загрузку, а на всё исполнение.
     
     
  • 6.134, Аноним (-), 04:35, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Это как-то за уши притянуто, не для этого оно, это под реалтаймные управляющие системы. Это как предъявлять сталевару что из куска стали потом видите ли нож могут сделать и кого-то зарезать. Ну да, из каких-то кусков стали натурально сделают ножи. Некоторыми даже может и зарежут кого. Но вот сталевар к всему этому относится очень косвенно и уж точно не главный злодей.

    Что до секурбута - сам по себе он вообще фича как фича. В теории обеспечивает то что система служит легитиному владельцу, и не подчиняется левым персонажам. А то что вас используя фичу особо ушлые господа из ваших систем поперли - кто вам виноват что вы денег даете не тем кому следовало бы, а тем кто вас же за них и имеет?

     
  • 2.96, Аноним (-), 02:32, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    > Vendorlock с мобилок на компьютеры???

    Совсем больной? Это самодиагностика системы, полезно для управления промышленными процессами, бортовых компьютеров и тому подобного.

    А если тебе не нравятся что тебя ставят в стойло - отлично, придурок, давай денег тем кто тебя в стойло не ставит. Или как ты это себе представляешь? Заносить денег DRMщикам, на кривой козе хакать их DRM и плакаться что в новой версии все вулны заделали? Это не решение. Решение - дать денег тем кто тебя иметь не будет.

     
     
  • 3.128, Аноним (128), 14:09, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    в современном ойти это так не работает.
    иметь тебя будут и те, кому платишь и те, кому не платищь.
    ящик пандоры открыт ;)
     
     
  • 4.135, Аноним (-), 04:41, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > в современном ойти это так не работает.

    Все там работает, это я как краудфандивший некоторые штуки говорю. Да, может быть оно не такое мощное, а малосерийное произсодство дороже. Зато оно делает то что обещали. Да и нет ресурсов у стартаперов всякие Management Engine и прочие PSP наворачивать, они так факаперами станут.

    > иметь тебя будут и те, кому платишь и те, кому не платищь.

    Нет, вот именно меня иметь никто более не будет. Я стал разборчив кому и почему я денег даю. Даже если это и не лежит в ближайшем ларьке и/или требует немного поднапрясь мозг.

    > ящик пандоры открыт ;)

    Лично я открыл довольно интересные ящики пандоры, научившись собирать системы сам. Как ты представляешь поимение меня в этой парадигме? :)

     

  • 1.2, Бывалый смузихлёб (?), 18:05, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –5 +/
    .. а в итоге нечто подобное налепят на предустановленные «линуксы» - и привет огороженная от шаловливых ручонок пользователя ось. Огороженная даже более чем винда или ябблось
     
     
  • 2.60, 111 (??), 10:50, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Уверен, что эта штука будет отключаема: нужна верификация - включил в ядре, не нужна - выключил. И всего делов.
     
     
  • 3.62, Бывалый смузихлёб (?), 11:43, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    поначалу - да с антивирусом и обновлениями в винде тоже так думали поначалу ... большой текст свёрнут, показать
     
     
  • 4.63, Аноним (63), 11:48, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    ну кто проститутку снимает - тот её и трахает. Или не трахает - как пожелает арендатор, так и будет.
     
     
  • 5.98, Аноним (-), 02:48, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Точнее, кто имплементит систему - тому она по умолчанию и служит Захочет ли он ... большой текст свёрнут, показать
     
  • 4.86, Шаман (??), 19:44, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > ""слава богу", в линукс файндейшен сидят..."

    Вообще-то слава богам!

     
     
  • 5.94, Расмус Лердорф (?), 23:02, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Так-то, "слава багам, конечно!"
     
     
  • 6.99, Аноним (-), 02:49, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Так-то, "слава багам, конечно!"

    Багам не слава, им bisect :P

     
  • 3.75, Kuromi (ok), 15:45, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Ага, знаем мы как это будет. Делается это на примере кинца так: пропихиваем DRM в стандарты, пропихиваем везде, реализуем софт на линукс, но УПС, он работает плохо потмоу что в ядре нету нужных механизмов залочек, далее постепенно внедряем нужные механизмы в ядро, вы думаете "ну пофиг, ядро не обновлю",  но в момент Ч DRMный плагин вдруг говорит "Братан, а мне нужно ядро версии Х.Y и не старее" и внезапно ничего не работает. И да, идея не обновлять DRMный плагин тоже не прокатит потмоу что у них встроенный сертификат протухающий раз в 4 месяца (как в Widevine).

    Так что отключаемым оно может и будет, вот только при отключении все сразу перестанет работать.

     
     
  • 4.100, Аноним (-), 02:51, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Прикинь, в ядре линя конфигуряется практически все. При условии что ты владелец системы и можешь свой кернел притащить. А если не владелец - тогда извини, тебя там вообще быть не должно.
     
     
  • 5.121, microsoft (?), 10:46, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Ложь.
     
  • 5.130, Kuromi (ok), 14:53, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Прикинь, в ядре линя конфигуряется практически все. При условии что ты владелец
    > системы и можешь свой кернел притащить. А если не владелец -
    > тогда извини, тебя там вообще быть не должно.

    И что? Думаешь они не встроят в свои DRM проверку "нужных" фич? Будет просто говорить "Хмм, чувак, у тебя странное ядро, иди ка ты лесом, ставь нормальное". Суть в том что после "внедрежа" нужных им фич в ядро можно будет говорить "Так, в Линуксе все секурные фичи по умолчанию есть, поэтому это мейнстрим, а все кто кастомят - ССЗБ".

    Сейчас например Widewine DRM на Линуксе работает "хуже чем на других ОС", нету того уровня защиты что хочется правообладателям. Приходится утираться - ибо "ну не шмогла я". А вот когда протащат нужное...

     
     
  • 6.136, Аноним (-), 04:51, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    1 Это все придется в юзер мод софте делать 2 Имеючи контроль над ядром я в пр... большой текст свёрнут, показать
     
     
  • 7.144, Kuromi (ok), 05:46, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Не, ну позиция твоя ясна. Я не собираюсь её критиковать - твердые принципы это нынче редкость, но мы все понимаем, что большинство разменивает свободу на удобство.

    Ну и поправочка "3) Но для начала я не буду качать мутноблобный софт желающий чтобы моя система ему DRM предоставляла. Зачем мне малварь в системе?"

    Стоит зайти в любом браузеер, даже ФФ на какой нибудь платный онлайн кинотеатр и эта гадость сама подтянется. О времена, о нравы!

     
     
  • 8.146, Аноним (146), 08:43, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    И жаловаться оно при этом может только на себя Более того - если кто выбрал бе... текст свёрнут, показать
     
  • 3.120, microsoft (?), 10:44, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Отработал миску риса, маладца. Свободен.
     

  • 1.7, Ананимассс (?), 18:10, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +10 +/
    А кто верефицирует верификатор?
     
     
  • 2.24, A.Stahl (ok), 19:10, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +13 +/
    Верификатор второго порядка, очевидно.
     
     
  • 3.39, Иван Васильевич (?), 20:46, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +8 +/
    меня терзают смутные сомнения
     
     
  • 4.101, Аноним (-), 02:54, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > меня терзают смутные сомнения

    Сделай 2 верификатора и пусть они проверяют друг друга. Кроме стеба это до некоторой степени работает, хоть и со своими ограничениями.

     
  • 3.102, Sw00p aka Jerom (?), 03:44, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    неполнота!!!
     
  • 2.80, Neon (??), 18:35, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Да, древняя проблема: кто контролирует контролера.)
     
     
  • 3.143, Анон1234 (?), 05:40, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Самый лучший контролер норот, его не омманешь.
     
  • 3.154, Бывалый смузихлёб (?), 10:27, 11/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Да, древняя проблема: кто контролирует контролера.)

    В данном случае проблемы нет ведь известно кто - тот кто надо кто
    А потом окажется что контролёр контролёра находится на чьём-то уютном сервачке и проверяет онлайн чтобы кто-то сильно умный потными ручонками не влез куда ему не положено. А без подключения к интернету и аппарат толком не запустить ведь проверку не проходит. "Вот смеху то будет!"
    Разумеется, того контролёра никому (из посторонних) проверять не надо - "он и так правильный"

     
  • 2.83, Аноним (83), 19:32, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    TPM
     

  • 1.11, fuggy (ok), 18:12, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Кто будет гарантировать что в модели ошибок нет? Ведь чтобы написать сложный алгоритм, нужно такую же сложную модель в которой можно ошибиться.
     
     
  • 2.71, Аноним (71), 14:19, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Подожди Ты замахнулся слишком далеко Например, есть модуль ядра, который напис... большой текст свёрнут, показать
     
     
  • 3.82, fuggy (ok), 18:49, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если вызов паники заложен в модель, то это корректное поведение. Но если ошибся в модели, то производный код будет с той же ошибкой, то есть бессмысленный.
    Модель мы строим по готовому коду или сначала создаём модель, а потом её конвертируем в код? Мы проверяем что выполнение кода соответствует модели или код по модели написан правильно? Просто кажется что написать хороший код будет проще, чем написать хорошую модель.

    Так объясни, то есть мы берём код и проверяем что результат кода, будет идентичным результату, которая выдала модель. То есть проще говоря это тупо двойное резервирование. Мы тоже самое можем сделать, посчитать тот же самый код на втором процессоре и сравнить ответ. Тогда зачем такая заумная логика с моделями.

     
     
  • 4.108, Аноним (-), 06:30, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    В данном случае как я понимаю оно может проверять трейс выполнения в интересных точках и если он не совпал с эталоном - упс, у нас глюкавящая система. И ее лучше привести в определенное состояние, чем дать ей глюкать дальше. Для чего логично ее в панику отправить, вот это уже должно быть предусмотрено в высоконадежной системе.

    В частности в высоконадежных системах может быть допустим >1 линии защиты. Вон те микроконтроллеры заметив кончину основного мозга и сами по минимуму приведут процесс в безопасное состояние, например. Или оно на резервный перейдет. А если мозги вместо этого будут кормить вон те микроконтроллеры каким-то левым г-ном взятым с потолка, ничего хорошего уж точно не получится. А вот плохого сколько угодно.

     
     
  • 5.129, Аноним (129), 14:39, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > оно может проверять трейс выполнения в интересных точках и если он не совпал с эталоном - упс, у нас глюкавящая система.

    Сабж проверяет сам себя (и паникует). Если "глюкавящая система" проверяет сама себя, то это бессмысленная проверка.

     
     
  • 6.137, Аноним (137), 04:55, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Сабж проверяет сам себя (и паникует). Если "глюкавящая система" проверяет сама себя,
    > то это бессмысленная проверка.

    Не обязательно. Исход проверки либо "трейс совпал", либо "трейс не совпал". Если система сглючит и посчитает трейс несовпавшим хотя он совпадал, "все-равно надо было ее перегружать". А сглючить так чтобы посчитать несовпавший трейс совпавшим - это какая вообще вероятность? Да, те кто вон те выкладки писал - в теорию все же умели, в отличие от, и догадывались о некоторых соотношениях.

     
     
  • 7.147, Аноним (129), 09:50, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Не обязательно.

    "Отличная" гарантия для "высоко"-надежной системы.

     
     
  • 8.151, Аноним (-), 01:10, 11/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Насколько я понимаю - оно достаточно близко к идеалу, в плане обеспечения той ве... текст свёрнут, показать
     
  • 2.89, Аноним (129), 20:04, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Модель и реальность - это совершенно разные сущности (сущность - это часть реальности, парадоксик!)

    Проверяют реальность - многопоточный код с побочными эффектами в гетерогенной сети из железа, исполнителей этого кода - на соответствие модели.

     

  • 1.17, Аноним (-), 18:24, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +13 +/
    Опять вместо микроядра выбрали встроить какого-то шпиона контролирующего исполнения кода.
     
     
  • 2.26, A.Stahl (ok), 19:12, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • –3 +/
    Кода миллионы строк вместе
         Единый порыв -- монолит
    Лишь так в нашем прогрессе
         Ядро смердит и пердит
     
     
  • 3.27, Аноним (27), 19:19, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    "У кого что болит тот о том и говорит"
    Странно предлагать что именно болит у опеннет экспертов и как они с этим живут
     
     
  • 4.43, Аноним (43), 00:52, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    посмотри на "творения" этой бестолочи - все сразу ясно станет
     
     
  • 5.50, Аноним (58), 04:56, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    ты про игрушки стахаля? кинь ссыль тогда на это уг
     
  • 3.76, B.Stahl (?), 17:09, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    классные стихи выдал. пешыесчо как грится!
     

  • 1.20, Аноним (20), 18:39, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Годно.
     
     
  • 2.40, pashev.ru (?), 21:18, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    s/д/в/
     
     
  • 3.44, Аноним (43), 00:52, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    s/p/как/
     

  • 1.21, YetAnotherOnanym (ok), 18:42, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +9 +/
    > ядро переводится в состояние "panic"

    Вангую, что админы "высоконадежных системах, гарантирующих отсутствие сбоев" будут тупо отключать эту хрень, потому что залюбятся перестраивать "модель автомата" на каждый чих.

     
     
  • 2.23, Аноним (20), 18:54, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >потому что залюбятся перестраивать "модель автомата" на каждый чих.

    Разве она не будет строиться автоматически на основе исходного кода? В этом и смысл.

     
     
  • 3.29, Твайлайт Спаркл (ok), 19:36, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Нет, конечный автомат создаётся руками, после компилируется валидатор.

    Имхо, есть варианты применения, как инструмент для нахождения багов внутри ядра линукса и создания ещё более надёжного программного обеспечения. Что не может не радовать, если все наработки по ядру будут возвращаться в апстрим.

     
     
  • 4.69, Аноним (129), 13:53, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > инструмент для нахождения багов внутри ядра линукса и создания ещё более надёжного программного обеспечения

    Это оценочная функция для генератора разных версий ядра (оравы ядрописателей). Будут на проде, ой, в тестовом окружении оценивать надежность, с телеметрией, или паниковать при отсутствии.

     
     
  • 5.109, Аноним (-), 06:31, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Ты еще заагрись, блин, на телеметрию у космического аппарата или промышленного объекта, лолка.
     
     
  • 6.113, Аноним (129), 09:20, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Привет, аноним, отвечающий на несущественные части моих сообщений!
     
  • 6.115, aname (?), 09:53, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Это другое?
     
  • 6.117, Аноним (117), 10:36, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если это телеметрия от левых людей, то конечно надо заагриться, без шуток. Телеметрия должна быть в руках владельца.

    (жду коко про аренду и прочие слово-право-выкрутасы)

     
  • 2.57, Первая буква (?), 08:37, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Эта хрень будет тупо отключать отключения админов гарантируя отсутствие сбоев
     
     
  • 3.138, Аноним (137), 04:58, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Эта хрень будет тупо отключать отключения админов гарантируя отсутствие сбоев

    Не, это те кто реализуют системы будут отключать, если админы зарекомендуют себя достаточно бакланами чтобы это вело к проблемам. Ну то-есть как, если какой-то идиот уронит самолет поменяв прошивку, окей, в следующей версии ее подписями обвесят по самые небалуйся и оно скорее лететь откажется чем полетит с левой прошивкой.

     

  • 1.28, Аноним (-), 19:33, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    cool
     
  • 1.30, Аноним (-), 19:39, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Зачем?
     
  • 1.33, Аноним (33), 20:00, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    > верификации

    Слово "проверка" короче и, соответственно, имеет меньший углеродный след ))

     
     
  • 2.35, анон (?), 20:19, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Надо "алгоритм верификации корректности функционирования кёрнела".
    Так важнее звучит и понятнее многим волонтёрам на этом паблике.
     
  • 2.41, pashev.ru (?), 21:19, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • –4 +/
    А промолчал бы, было бы ещё меньше.
     
     
  • 3.45, Аноним (43), 00:54, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    так заткнись
     
  • 3.53, Аноним (33), 07:49, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Вот видите, товарищи. А было бы русскоязычное.. Кстати, а когда старые слова запрещают?
     
  • 2.105, Аноним (-), 05:53, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • –2 +/
    > Слово "проверка" короче и, соответственно, имеет меньший углеродный след ))

    Е#$%нувший промышленный процесс или упавший самолет тоже имеют углеродный (и не только) след. Может тебе еще и автоматы в щитке убрать, нехай у тебя при первом КЗ вся хата сразу выгорает. Зато не закоптим небо на производство пакетника.

     
     
  • 3.118, Аноним (117), 10:37, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Автоматы стоят для защиты линии от тебя, а не тебя от пожара.
     
     
  • 4.139, Аноним (137), 05:03, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Автоматы стоят для защиты линии от тебя, а не тебя от пожара.

    Да как бы тебе сказать, чудак? Сравни сечение проводов линии и сечение проводов у меня в доме. Моим проводам при КЗ поплохеет сильно раньше чем проводам линии, такая ерунда. Тупо закон ома.

     
  • 3.122, Аноним (-), 11:22, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Жёстео же тебя бомбит!
     

  • 1.37, Аноним (37), 20:41, 07/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Чего только не придумают чтоб Аду не учить.
     
     
  • 2.42, Аноним (42), 22:17, 07/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Bastards!
                     Опять и опять в бесконечность
                     Веселое утро глядит,
                     И радует сна быстротечность
                     И неба изменчивый вид.
                     Стоят неподвижно туманы
                     Над сочной, набухшей землей,
                     Цветущие майские страны
                     Они прикрывают собой.

    https://ru.wikipedia.org/wiki/Ада_Владимирова

     

  • 1.46, torvn77 (ok), 01:10, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    >Проверка производится во время выполнения через прикрепление обработчиков к точкам трассировки ...

    Я так скрипта на bash отлаживаю (echo point_name)

     
     
  • 2.110, Аноним (-), 06:36, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Я так скрипта на bash отлаживаю (echo point_name)

    Он тоже изобрел "дебажный printf". Хоть и хреновый. Но валидация поведения тут где? :)

    ps немного доразвитый "дебажный printf" имеет в реалтаймных системах свой пойнт, время же нельзя на паузу поставить, а вот такой flow околореалтаймно скидывать можно и относительно неинтрузивно, если понимая что делаешь.

     
     
  • 3.126, torvn77 (ok), 14:04, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >> Я так скрипта на bash отлаживаю (echo point_name)
    >Но валидация поведения тут где? :)

    Помимо этого я ещё вставляю  
    echo env_name=$env_name

    И вот так и идёт трек работы скрипта.  
    Автоматической валидации у меня конечно нет, смотрю глазами и обдумываю мозгами.

     
     
  • 4.152, Аноним (-), 01:16, 11/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Я в фирмварях использую что-то отдаленно напоминающее сабжевую идею. Там где функции опасные, есть дополнительные "check values" маркированые volatile (чтобы оптимизер не выпилил) и код проверяет почему он вообще здесь. Если ему не нравится повод по которому его вызвали - немедленная маркировка системы как "неисправной" и далее recovery/failsafe.

    Разумеется я не придумал этот фокус, базовый control flow enforce из safety guidelines. Шелскриптам столько не надо как правило: если что-то оформлено шелскриптом, надежностью заведомо не парились т.к. там много чего может пойти не так.

     

  • 1.47, all_glory_to_the_hypnotoad (ok), 01:30, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Очередной кривой и неработающий overengineering
     
  • 1.49, Аноним (49), 03:36, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Виндовый верифаер изобрели?
     
     
  • 2.116, aname (?), 10:02, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Будет иронично, если микрософты к этому свои клавиатуры приложили
     

  • 1.52, Аноним (52), 06:21, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    А смысл в этом Runtime Verification? Упало ядро в панику в рантайме - значит всё плохо, вот вам и вся верификация. Если бы было можно взять и запилить эталонную модель, превратить ядро в детерминированную машину состояний, то это бы сделали, скомпилировали и получили идеальное ядро, но это слишком сложная задача, потому что ну нельзя для монолитного ядра предсказать все возможные состояния и переходы между ними.
     
     
  • 2.65, kusb (?), 12:08, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А может это не надо если можно доказать, что один домен состояний гарантированно не влияет на другой...
     
  • 2.74, all_glory_to_the_hypnotoad (ok), 15:12, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    К монолитности ядра эта проблема не имеет никакого отношения. Проблема исключительно в сложности отдельно взятых компонент, для которых разработка формальной модели равносильна разработки кода без багов.
     
  • 2.106, Аноним (-), 06:04, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Обнаружение некорректной работы системы в сюжетно интересных точках и довольно б... большой текст свёрнут, показать
     
     
  • 3.123, all_glory_to_the_hypnotoad (ok), 11:31, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Для решения подобных проблем давно придумали assert и неотключаемый assert, не нужно городить дополнительные костыли сбоку много сложнее этих assert-ов.
     
     
  • 4.140, Аноним (-), 05:08, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Для решения подобных проблем давно придумали assert и неотключаемый assert, не нужно
    > городить дополнительные костыли сбоку много сложнее этих assert-ов.

    И как assert поможет от допустим DMA перезаписавнего блок памяти с переменными вон той программе? Assert вообще понятия не имел что в фоне кто-то еще что-то с памятью делал, он это просто не видел. Аналогично - с большей частью иных причин разрушения памяти, программных, аппаратных и программно-аппаратных.

    Сразу видно почему вебмакаки и хомяки не должны проектировать высоконадежные системы. Они в этом ничерта не смыслят.

     

  • 1.59, Онаним (?), 09:14, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    А механизм верификации корректности работы верификации где?
     
     
  • 2.81, Neon (??), 18:36, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А это следующий этап распила. А потом верификация верификатора следующего порядка и так  в рекурсии.)))
     
     
  • 3.92, kusb (?), 22:01, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если можно верифицировать физику и верификатора - по атомам, взаимодейтвиям и ниже - то многие могут успокоиться.
     
  • 3.93, anonymous (??), 22:24, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    При чём тут распил, болезней?
     
     
  • 4.103, myhand (ok), 05:10, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Он так привык.
     
  • 4.133, kusb (?), 23:14, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > При чём тут распил, болезней?

    Перечитай. Там другой распил. Получается тебе везде мерешится распил...

     

  • 1.61, darkshvein (ok), 11:18, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    патч проверяет наличие кода на Rust в ядре,
    и если оный не обнаружен - ядро работает корректно?
     
     
  • 2.88, Аноним (88), 19:51, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Конечно же нет.  
     

  • 1.64, Аноним (129), 12:03, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    > проверки корректности
    > высоконадежных системах

    Подмена понятий.

    Проверка не повышает и не понижает надежность.

    Проверка может только _оценить_ надежность.

    Если еще паниковать при проверке, то это точно не про надежность.

     
     
  • 2.67, _kp (ok), 13:23, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Ну если не смущает бородатые правила, ...

    - Чем больше функций в системе защиты, тем больше вероятность, что одна из них не работает так как надо.
    - Система обеспечения надежности выведет из строя другие системы.

    - Любая программа содержит дыры.  Следствие: даже системы защиты содержат дыры.
    - Обнаружить все дыры невозможно.

    - Установив систему защиты, не ждите благоприятных отзывов от сотрудников.
    - Нет такой плохой ситуации, которая не могла бы стать еще хуже.

     
     
  • 3.68, Аноним (129), 13:32, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > тем больше вероятность

    Чтобы работать с вероятностью надо знать вероятности. Бессмысленное, в общем случае ложное утверждение.

    И так далее по остальным "правилам"

     
     
  • 4.95, Аноним (-), 23:19, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Чтобы работать с вероятностью надо знать вероятности.

    Ну сходи почитай учебник теорвера, когда научишься с ней общаться, возвращайся продолжать беседу.

    > Бессмысленное, в общем случае ложное утверждение.

    Нет, всё правильно. Не зная вероятностей работать с ними не получится.

     
     
  • 5.114, Аноним (129), 09:22, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Привет, аноним из-под тора!
     
  • 4.124, _kp (ok), 11:51, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Бессмысленное, в общем случае ложное  утверждение.

    Вы шутки не любите? Зря. С серьёзным выражением лица делаются самые глупые ошибки.

    Законы Мерфи не выдуманы, глядя в потолок, а записаны по статистике проблем позникающих в реальных системах.
    И хоть в итоге оформлены как юмор, они всё равно более чем пригодны как инструкция для инженеров, конструкторов и проектировщиков.

    А главный их плюс, то, что в отличии от сухих пpавил, эти точно запоминаются. А уже зная что есть потенциальная проблема там, и там, смотрим что об этом в менее запоминающихся правилах пишут.

     

  • 1.66, user90 (?), 13:00, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Сложновато-с. в смысле для критики :) Молчу уж про реализацию..
     
  • 1.70, Аноним (70), 14:01, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    Да, да! Больше переключений контекста! Больше промахов кэша! Больше тормозов богу тормозов! Компы стали слишком быстрыми! Ура, товарищи! Бегом за новым железом!
     
  • 1.72, Максим (??), 14:57, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Неужели это настолько актуально? Часто ли ядро начинает работать неправильно и при этом не уходит в панику своими средствами?
     
  • 1.77, B.Stahl (?), 17:11, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    https://nitter.it/srostedt/status/1536184732655812608

    идеальный образ злодея-предателя выбрали. люблю американцев за драматический подход в политике - как будто в голливудском кино проживаешь

     
     
  • 2.84, Неизвестный (?), 19:32, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Сколько стоит ядро? 28 морей =)
    А за робота сколько заплатили за 5 лет?
     

  • 1.78, B.Stahl (?), 17:41, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    https://nitter.it/srostedt/status/1536184732655812608

    идеальный образ злодея-предателя выбрали. люблю американов за драматический подход в политике - как будто в голливудском кино проживаешь

     
  • 1.79, Neon (??), 18:34, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Старая проблема: а кто будет контролировать контролера ? Что он работает корректно ?
     
     
  • 2.87, Аноним (88), 19:50, 08/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Зачем его контролировать если выход годных улучшился да приемлемого уровня? 100% контроля быть не может.
     
  • 2.111, Аноним (-), 06:40, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Старая проблема: а кто будет контролировать контролера ? Что он работает корректно?

    Можно друг друга взаимно контролировать, допустим. А конкретно в этом механизме как оно может неверный вердикт вынести? Вероятность принять кривой трейс за верный крайне низкая если у системы проц хоть какие-то признаки жизни подает, а если правильный трейс за неправильный посчитан, ну, окей, оно все-равно глюкало и паника и далее ребут ему уж точно не помешает... :)))

     

  • 1.90, rshadow (ok), 20:17, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Я так понимаю они изобрели периодически запускать тесты ядра прям во время его же работы. Забавный метод, никогда еще такой ху*ни не видел.
     
     
  • 2.125, Аноним (129), 13:15, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Они изобрели поиск бозона Хиггса по трассам частиц.
     

  • 1.91, None (??), 20:47, 08/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Механизм "стадо - пастух"
     
  • 1.119, bOOster (ok), 10:41, 09/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Ну че, традиционное поделие для Линуксоидов. Прогресс, по их словам назвается :))) Вместо того чтобы улучшать качество кода, написанное программистом - придумываем чушь в виде каких-то проверок, с таким же убогим качеством кода и дырявой реализацией.  
     
     
  • 2.127, Аноним (127), 14:09, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    А вот лозунговый менеджер подъехал.  Мы тебя ждали (нет).
     
  • 2.131, Аноним (131), 15:30, 09/08/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Даже в Windows 11 есть контроль доступа к камере, микрафона и другие управления прав доступа - в Linux лет через 5 только поди появится)
     
     
  • 3.141, Аноним (-), 05:11, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Даже в Windows 11 есть контроль доступа к камере, микрафона и другие
    > управления прав доступа - в Linux лет через 5 только поди появится)

    Там еще телеметрия всякая, активации, онлайнакаунты, оно лучше юзера знает когда ребут пора и прочий "customer experience improvement". А тупому потребителю-индейцу как обычно дали клевое удобное и теплое одеяло. Правда, как обычно - тифозное.

    Ну а в линуксе одеяло можно себе самому сшить, тогда не надо гадать тифозное оно или нет.

     
  • 3.148, Аноним (129), 10:49, 10/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Даже в Windows 11 есть контроль доступа

    А в ядре линуксе есть eBPF. например, которым можно контролировать любой системный вызов. Или тебе нужно мышевозное пальцетыкательное окошко с единственной кнопкой "OK"?

     

  • 1.145, КО (?), 07:08, 10/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Коммитеры:
    @google.com
    @redhat.com
    @arm.com
    Ну, естессно.
     
     
  • 2.153, Аноним (-), 01:21, 11/08/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А в чем собственно трабл? Более того, RT_LINUX патчи интел стал продвигать. Они скупили их разработчиков, вот и... . А кто-то сомневается что у линуха найдется более 9000 применений в околореалтаймных системах с высокими требованиям к надежности? А зря! Бортовые компьютеры, автопилоты, управляющие системы и тому подобное добро. Очень странно что ARM хочет чтобы их чипы там были топчиком. Да и остальные не прочь поделить этот довольно вкусный кус пирога. Который к тому же в отличие от хайпа и пузырей - надолго и всерьез. От вон тех систем человечество в обозримом будущем не откажется.
     

  • 1.155, Аноним (155), 13:49, 15/08/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Чего только не придумают, лишь бы ядро на расте не переписывать
     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Спонсоры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

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