The OpenNET Project / Index page

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

Google открыл код защищённой операционной системы KataOS

15.10.2022 10:01

Компания Google объявила об открытии наработок, связанных с проектом KataOS, нацеленным на создание защищённой операционной системы для встраиваемого оборудования. Системные компоненты KataOS написаны на языке Rust и выполняются поверх микроядра seL4, для которого на системах RISC-V предоставлено математическое доказательство надёжности, свидетельствующее о полном соответствии кода спецификациям, заданным на формальном языке. Код проекта открыт под лицензией Apache 2.0.

В системе обеспечена поддержка платформ на базе архитектур RISC-V и ARM64. Для симуляции работы seL4 и окружения KataOS поверх оборудования в процессе разработки используется фреймворк Renode. В качестве эталонной реализации предложен программно-аппаратный комплекс Sparrow, комбинирующий KataOS с защищёнными чипами на базе платформы OpenTitan. Предложенное решение позволяет совместить логически верифицированное ядро операционной системы с заслуживающими доверия аппаратными компонентами (RoT, Root of Trust), построенными с использованием платформы OpenTitan и архитектуры RISC-V. Помимо кода KataOS в дальнейшем планируется открытие и всех остальных компонентов Sparrow, включая аппаратную составляющую.

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

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

Для дополнительной защиты все компоненты, кроме микроядра, изначально развиваются на языке Rust с использованием безопасных приёмов программирования, минимизирующих ошибки при работе с памятью, приводящих к таким проблемам как обращение к области памяти после её освобождения, разыменование нулевых указателей и выход за границы буфера. На Rust в том числе написаны загрузчик приложений в окружении seL4, системные сервисы, фреймворк для разработки приложений, API для доступа к системным вызовам, менеджер процессов, механизм динамического распределения памяти и т.п. Для верифицированной сборки задействован инструментарий CAmkES, развиваемый проектом seL4. Компоненты для CAmkES также могут создаваться на языке Rust.

Безопасная работа с памятью обеспечивается в Rust во время компиляции через проверку ссылок, отслеживание владения объектами и учёт времени жизни объектов (области видимости), а также через оценку корректности доступа к памяти во время выполнения кода. Rust также предоставляет средства для защиты от целочисленных переполнений, требует обязательной инициализации значений переменных перед использованием, применяет концепцию неизменяемости (immutable) ссылок и переменных по умолчанию, предлагает сильную статическую типизацию для минимизации логических ошибок.

  1. Главная ссылка к новости (https://opensource.googleblog....)
  2. OpenNews: Google представил открытый проект OpenTitan для создания заслуживающих доверия чипов
  3. OpenNews: Прототип отечественной ОС Phantom на базе Genode будет готов до конца года
  4. OpenNews: Открыт код сверхнадёжного микроядра seL4
  5. OpenNews: Проект Neptune OS развивает слой совместимости с Windows на базе микроядра seL4
  6. OpenNews: Микроядро seL4 математически верифицировано для архитектуры RISC-V
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/57920-kataos
Ключевые слова: kataos, opentitan, sel4
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (124) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним (1), 10:43, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    Genode какой-тл
     
  • 1.2, Аноним (2), 10:45, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Опять пермессивщина
     
     
  • 2.3, Аноним (3), 10:47, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    вам шашечки?
     
     
  • 3.6, Самый Лучший Гусь (?), 11:04, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +13 +/
    GPL нам подавайте иначе это просто напросто фольшивка
     
  • 3.44, Аноним (-), 13:52, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +9 +/
    Нам не хочется бесплатно работать на хайпомакак в гугле. Это странно?
     
     
  • 4.50, Аноним (50), 14:28, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Так вы никогда и не работали.
     
     
  • 5.72, Аноним (72), 17:20, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +5 +/
    Не хочется потому и не работали. Это разве странно?
     
  • 4.87, Пенис (?), 20:45, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Берёшь и лицензируешь форк под GPL. Всего делов-то, но вонять ты горазд.
     
  • 3.178, Аноним (178), 11:54, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > вам шашечки?

    Замечено, как только копрорасты хотят что-то выкинуть из объедков, почти прямиком на кладбище "открытых" проектов, по традиции это всё смазывается апачной лицензией.

    Совпадение?!...

     
  • 2.7, Аноним (7), 11:04, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Вы так говорите, как будто это плохо))
     
     
  • 3.21, Аноним (-), 12:01, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Да, пермиссивщина это плохо.
     

  • 1.4, Аноним (4), 11:03, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +7 +/
    Эти все скучные буковки читайте сами. Где не скучные обои?
     
  • 1.8, Аноним (8), 11:04, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –3 +/
    > Rust также предоставляет средства для защиты от целочисленных переполнений

    Кто пишет эту чушь? Раст не предоставляет средств для защиты от переполнения целочисленных переменных. Как минимум в продовой сборе софта.

     
     
  • 2.10, Анонн (?), 11:14, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –8 +/
    Раст предоставляет защиту в дебаге и однозначное поведение в релизе. А не "хз как, пусть компилятор решает".
     
     
  • 3.86, Лолштоним (ok), 20:39, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Как раз компилятор решает.
     
     
  • 4.108, Аноним (108), 23:20, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    И разные компиляторы обрабатывают эту ситуацию по разному! В том-то и проблема
     
     
  • 5.116, анон (?), 02:01, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    и сколько есть разных компиляторов rust?
     
     
  • 6.122, Аноним (122), 05:21, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    каждую новую версию!
     
  • 6.140, Аноним (140), 11:38, 16/10/2022 Скрыто ботом-модератором     [к модератору]
  • –2 +/
     
     
  • 7.150, анон (?), 13:12, 16/10/2022 Скрыто ботом-модератором     [к модератору]
  • +/
     
  • 7.151, Аноним (151), 13:20, 16/10/2022 Скрыто ботом-модератором     [к модератору]
  • +/
     
  • 6.154, Igraine (ok), 13:47, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    1) mrustc
    2) rust-gcc
    3) rustc
     
     
  • 7.169, анон (?), 23:33, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Интересный пример, в двух из трех репозиториев авторы сами чёрным по белому пишут что это очень ранняя стадия и совсем не готово для продакшна.

    Ну, время идёт, можно и подождать

     
  • 2.11, Прув (?), 11:18, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –4 +/
    Ох уж эти иксперды с опеннета пишущие в комментах чушь…

    Все там предоставляется, нужно только явно вызывать

    Смотри overflowing_*, saturating_*, checked_* и saturating_* -> например checked_add

     
     
  • 3.24, Аноним (8), 12:22, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Любому человеку это кажется не очень то и безопасным.
     
     
  • 4.29, eganru (?), 12:28, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Это безопасно.
    Почти в любом языке есть возможность сделать безопасную работу и проверку переполнений.



    if unlikely(a + b < a) assert("...")



    большого ума не требует

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

    Понятно, что не все и даже не 10 часть. Но гораздо лучше, чем ничего.

     
     
  • 5.65, Аноним (65), 16:44, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Чушь не пори это полностью небезопасно.
     
  • 5.93, Igraine (ok), 21:55, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Но ведь в С и С++ если a и b целое со знаком, то переполнение неопределенно, условие всегда ложно и компилятор имеет право его удалить
     
  • 5.182, Аноним (182), 14:20, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    это чудесно, но что, если signed?
     
  • 3.28, Маняним (?), 12:26, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    > Ох уж эти иксперды с опеннета пишущие в комментах чушь…

    про С

    > Все там предоставляется, нужно только явно вызывать

    __builtin_*_overflow

     
     
  • 4.38, Прохожий (??), 13:42, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А где в этой ветке хоть слово было про Си?
     
  • 4.66, Аноним (65), 16:45, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Омг
     
  • 2.91, Chlen22sm (?), 21:52, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +8 +/
    Лучшая защита это прямые руки и умение в алгоритмы, а не клепание формочек на фреймворках.
     
     
  • 3.96, Igraine (ok), 22:03, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –5 +/
    Покажите что вы там своими прямыми руками написали.

    И да, фреймворк это программная платформа, определяющая структуру программной системы. К формочкам фреймворк имеет очень косвенное отношение, разве что в фантазиях местных... посетителей

     
  • 3.153, анон (?), 13:31, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +8 +/
    ага, просто пишите хороший код, а плохой не пишите.
     

  • 1.9, Аноним (9), 11:06, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +9 +/
    >[оверквотинг удален]
    > логически верифицированное ядро
    > заслуживающими доверия
    > особый уровень защиты
    > подтверждения отсутствия сбоев
    > верификации надёжности
    > безопасных приёмов программирования
    > минимизирующих ошибки
    > Безопасная работа с памятью
    > средства для защиты
    > минимизации логических ошибок

    Надо брать определенно. А то уже устал сидеть на не заслуживающей доверия незащищенной операционной системе с небезопасной работой с памятью, максимизированными логическими ошибками, неверифицированной надежностью и без средств защиты от небезопасности (а также без особого уровня такой защиты).

     
     
  • 2.27, швондер (?), 12:26, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +4 +/

    Колючие глаза Римского через стол врезались в лицо администратора, и чем дальше тот говорил, тем мрачнее становились эти глаза. Чем жизненнее и красочнее становились те гнусные подробности, которыми уснащал свою повесть администратор... тем менее верил рассказчику финдиректор. Когда же Варенуха сообщил, что Степа распоясался до того, что пытался оказать сопротивление тем, кто приехал за ним, чтобы вернуть его в Москву, финдиректор уже твердо знал, что все, что рассказывает ему вернувшийся в полночь администратор, все – ложь! Ложь от первого до последнего слова.
     
  • 2.118, Аноним (122), 03:22, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +6 +/
    > заслуживающими доверия

    Вот ^^^ это ^^^ - самое главное! Самый чётко определённый термин, доказанный математически.

     

  • 1.12, Аноним (12), 11:28, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    Блин я только перешёл на Fuchsia
     
     
  • 2.172, Аноним (172), 08:34, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Встречайте! Гладиаторские бои на гугл-арене! И пусть победит сильнейший!
     

  • 1.13, Аноним (13), 11:32, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Fiasco.OC? Ты ли это?
     
  • 1.14, Аноним (14), 11:35, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    Конкуренция это всегда хорошо, может хоть Гугл заставит Линуса шевелиться...
     
  • 1.15, Аноним (15), 11:45, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    Это просто чудесно:

    > The initial Sparrow target platform was intended to have 4MiB of memory. A production build of the included services fit in <3MiB of memory but due to the overhead of CAmkES and the rootserver boostrap mechanism actually require ~2x that to reach a running state.

    Почему так - они точно не знают. Предлагают переписать всё на расте.

     
  • 1.18, Alexey Torgashin (?), 11:56, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Пусть сначала этот гугл докажет что это не просто выкидыш , не просто перделка. От вторых мелко мягких . А реальная вещь. Реальная значит работает с реальными программами, которые должны появиться. Не только браузер и медиа плеер которые есть везде и всегда. А VSCode и аналоги, графические редакторы , редакторы видео и монтажа. Офис хорошо бы . И тп.

    Это же относится к ОС Геноде которая непонятно что и непонятно зачем .

     
     
  • 2.42, Самый умный из вас (?), 13:51, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +7 +/
    Напиши плз контакты, как гуглу с тобой связаться, куда доказательства отправлять
     
     
  • 3.71, n00by (ok), 17:09, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Так он написал имя. Гугл же всё про всех знает. ;)
     

  • 1.19, Бывалый смузихлёб (?), 11:59, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    > Для дополнительной защиты все компоненты, кроме микроядра, изначально развиваются на языке Rust
    > на языке Rust
    > кроме микроядра
     
     
  • 2.22, Аноним (7), 12:05, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Логично же. Его же придется переверифицировать заново. А так используют уже верифицированное.
     
     
  • 3.119, Аноним (122), 03:24, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Всё просто: верификатор не может верифицировать код раста.
     

  • 1.23, Alexey Torgashin (?), 12:10, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Похоже я ошибся , ОС не для десктопа а для встраиваемых штук. Но это ещё вопрос кто и зачем возьмёт такую Ос. Для роутеров ? Ещё куда не шло. Для интернета вещей этого поганого, который нужен только для товарища майора чтобы следить , и хакеров ? Тогда нафиг . Для чего ещё?
     
     
  • 2.25, Аноним (8), 12:23, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +4 +/
    Подскажу. Даже гугл её никуда не взял. Делай вывод.
     
     
  • 3.177, _kp (ok), 09:55, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Часто подобные проекты изначально делают ради эксперимента, делают тесты, выводы, учитыают в других разработках. Забрасывают побочное изделие.
     
  • 2.26, eganru (?), 12:23, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Для определенного класса встраиваемых штук, тк. требования слишком высокие чтобы на средней руки MCU запускать.
     
  • 2.49, Аноним (49), 14:14, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Для чего ещё?

    Для вещей, где софтварный сбой может стоит миллиарды.

    > Для роутеров?

    Вряд ли. В любом случае не для домашних роутеров. Цена сбоя домашнего роутера близка к нулю. Поэтому в нём лучше из железа выжать максимум и засунуть всё в монолитное ядро.

     
     
  • 3.60, Бывалый смузихлёб (?), 16:16, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Ну и чем оно лучше того же миникса?

    А для остальных случаев - есть как минимум йокто для линуксоморды и ртос вроде сейфРтос или азурРтос( бывшая треадИкс ) для собственно управляющего мк

    Я, кстати, наверняка пропустил упоминание что сабж - компактная РТОС( ОСРВ ) ведь иначе непосредственно ей не может рулиться что-либо, если ошибка в ней может стоить миллиарды

     
     
  • 4.173, Аноним (172), 09:02, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Скажу, чтобы у тебя, знатного растохейтера лишний раз подгорело - всё, кроме мик... большой текст свёрнут, показать
     
  • 3.89, Аноним (89), 21:31, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > где софтварный сбой может стоит миллиарды

    Не похоже, что сабж такой уж дорогой.
    Для чего ещё? Нам мало где требуется надёжный софт?
    Например, тот же транспорт, медицина.

     

  • 1.30, Джон Макагонов (?), 12:29, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –6 +/
    Меня уже не удивляет то,  что в передовых разработках применятся раст. Превосходство раста очевидно,  его величие - просто свершившейся факт. Даже скучно уже.
     
     
  • 2.35, Аноним (35), 13:08, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –6 +/
    раст не полетел. Ему на смену уже идёт Карбон.
     
     
  • 3.46, Прохожий (??), 13:55, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –3 +/
    MS, Google, Amazon, Meta вовсю начали использовать Rust. Но анонимный воин супротив Раста не даст этим корпорациям себя обмануть. У него дома Rust не взлетел. :)))
     
     
  • 4.120, Аноним (122), 03:27, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Meta вовсю начали использовать Rust

    Тогда понятно, почему у их Вселенная не взлетела, а народ разбегается уже после первого месяца.

     
     
  • 5.162, Аноним (162), 16:01, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Именно поэтому — как узнают, что на расте написано, сразу бегут, пока пацаны с опеннета не засмеяли.
     
  • 5.199, Прохожий (??), 07:22, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Она ещё не готова просто, о взлёте говорить пока рано. Про другие фирмы есть что сказать?
     
  • 3.174, Аноним (172), 09:31, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Ты заврался донельзя Всё перевернул Раст летит как раз хорошо и это видно по п... большой текст свёрнут, показать
     
  • 3.183, Аноним (183), 16:48, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Естесственно, Rust придуман не Google.
     

  • 1.31, eganru (?), 12:34, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +6 +/
    Вообще такое ощущение, что новости специально пишут так, чтобы в комментах был жыр с хорошим запасом.
     
     
  • 2.58, Аноним (58), 15:22, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Зима приближается, нужно запасаться.
     

  • 1.33, Друг Сергея (?), 13:06, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Kata Containers, KataOS, Rust и Go - что происходит?
     
     
  • 2.45, Прохожий (??), 13:52, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Эволюция происходит. Софт усложняется. Люди ищут способы бороться с этой сложностью.
     
     
  • 3.90, Аноним (90), 21:32, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Я бы не сказал, что они что-то упростили...
     
     
  • 4.132, Аноним (140), 11:28, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Нет ничего проще, надёжнее и безопаснее чем ANSI C, остальное пустой пиар
     
     
  • 5.149, Аноним (151), 13:12, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Нет ничего проще, надёжнее и безопаснее чем ANSI C, остальное пустой пиар

    "Talk is cheap, show me your code!" (c)

     
  • 4.198, Прохожий (??), 07:19, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Работа с памятью. Теперь можно гораздо меньше уделять ей внимания. Странно, что приходится объяснять это снова и снова.
     

  • 1.36, Аноним (36), 13:29, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +5 +/
    Для дополнительной защиты все компоненты, кроме микроядра, изначально развиваются на языке Rust с использованием безопасных приёмов программирования...

    Вот растаманы, пользуйтесь, а линукс в покое оставьте!

     
     
  • 2.40, Прохожий (??), 13:50, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Линукс - для серверов и десктопа. А это для встройки. Разные ниши. В идеале и Линукс весь переписать на Rust полностью.
     
     
  • 3.53, Аноним (35), 14:29, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Только переписывание линукса на раст линуксу ничего не даст. Так что этого никогда не произойдет.
     
     
  • 4.197, Прохожий (??), 07:17, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Вообще-то даст - дополнительную стабильность. Это уже огромный жирный плюс.
     
  • 3.57, Бургер (?), 15:21, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    >А это для встройки

    окей, окей, Yocto и остальные на помойку, тк анон опенета решил, что Linux для серверов и десктопа.

    embedded девелоперы, расходимся.

     
     
  • 4.200, Прохожий (??), 07:26, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Вот именно. На помойку. Любая проблема с памятью и всё,  конец железке.
     
     
  • 5.208, Бургер (?), 13:32, 23/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Вот именно. На помойку. Любая проблема с памятью и всё,  конец
    > железке.

    ноотопы в помощь

     
  • 2.131, Аноним (140), 11:27, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Они не отстанут пока не сломают Линукс окончательно
     

  • 1.47, Прохожий (??), 14:01, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Ожидаемо набежало стадо воинов супротив Rusta. Местные неосиляторы решили в очередной раз отметиться, высказав своё "фе" к тому, чего они не понимают, потому что неспособны.
     
  • 1.48, Аноним (48), 14:09, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Такое ощущение,что amd64 закапывают вслед за х86. Новости чуть ли не поголовно про АРМ и даже Линукс набрал растокодеров для этой архитектуры.
     
     
  • 2.95, Аноним (95), 22:01, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Гегемония интел-амд многим мешает
    Гуглу в том сегменте заработать как? Строим новый
     

  • 1.56, ИмяХ (?), 15:11, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    >>поверх микроядра seL4,
    >>фреймворк Renode
    >>инструментарий CAmkES

    А это всё на каких языках написано? И почему нет пары абзацев о достоинствах этого языка?

     
     
  • 2.128, Аноним (140), 11:23, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Потому что цель это пиар раста.
    Если бы цель была написание безопасностной и надёжной операционной системы они бы взяли ANSI C
     
     
  • 3.148, Аноним (151), 13:10, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/

    > Если бы цель была написание безопасностной и надёжной операционной системы они бы взяли ANSI C

    Т.е. за 50 лет существования сишки никто такой целью не задавался?

     
     
  • 4.158, Аноним (158), 15:20, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Задавался. И написал. Называется L4.
     
     
  • 5.159, Аноним (151), 15:48, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Задавался. И написал. Называется L4.

    Называется "слышал звон".


     
  • 5.175, Аноним (172), 09:41, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > безопасностной и надёжной операционной системы
    >> Задавался. И написал. Называется L4.

    L4 - микроядро. Микроядро - не операционная система, а ее часть. Пусть и важная.

     

  • 1.74, Аноним (-), 17:43, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Они взяли верифицированное микроядро и сверху накинули неверифицированную инфраструктуру Rust? Rust верифицировали?
     
     
  • 2.110, Аноним (108), 23:25, 15/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А у вас есть верифицированная инфраструктура на си, чтобы накинуть поверх ядра? Что, нет? Как же так...
    Вот и у них не было, а писать с нуля на шрешете они не захотели.
     
     
  • 3.152, anonymous (??), 13:29, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Примерно те же люди, которые сделали проект seL4, сделали проект CakeML - a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself. А что сделали инженеры Google? Пока что просто написали неверифицированный код на Rust, но бахвалятся безопасностью проекта. Да ещё только под RISC-V и ARM64. И запускают это на своих вендорлокнутых железяках. А всем остальным предлагают веровать в безопасность этих решений. Спасибо, пусть оставят внутри своей корпорации как и Zircon, который в пару шагов эксплуатировали реята из Positive Technologies.
     

  • 1.82, Аноним (82), 19:42, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    У них ничего не получится. Как обычно.
     
     
  • 2.201, Прохожий (??), 07:30, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Сказал аноним в адрес корпорации с мультимиллиардным оборотом. :)
     

  • 1.83, user90 (?), 19:58, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    А там не хрустело ли?
    Да и какие дрова? Не под это сферическое оборудование, под реальное?
     
  • 1.85, Аноним (85), 20:38, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Васян с бодуна сделает опечатку в коде и всё это логически верифицированное можно отправлять на помойку.
     
  • 1.92, Аноним (92), 21:55, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    Очередное распиаренное фуфло от гугла для жертв современного образования
     
  • 1.103, Аноним (103), 22:40, 15/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Это очень большая проблема что L4 предлагает большой выбор.
    Всё должно быть компактно для разной архитектуры в ядре. Без вариантов можно и так и можно и подругому.
     
  • 1.113, Neon (??), 01:05, 16/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    От логических ошибок программиста никакой Rust не спасет.)
     
     
  • 2.176, Аноним (172), 09:50, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > От логических ошибок программиста никакой Rust не спасет.)

    Ну так гиганты статистику выкладывали - от 70% спасёт, от 30% ("логических", хотя они все наверное логические) - нет.

    А если начнете требовать 100% и возражать что "если хоть 1% остается то нинужна", то тогда на дорогах и зебры со светофорами не нужны, да и вообще ПДД - всё равно находятся дятлы которые на красный проезжают/пробегают и носятся как будто на всей планете больше никого не осталось.

     

  • 1.115, Аноним (115), 01:31, 16/10/2022 Скрыто ботом-модератором [﹢﹢﹢] [ · · · ]     [к модератору]
  • –3 +/
     
  • 1.123, pashev.ru (?), 08:58, 16/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    > математическое доказательство надёжности, свидетельствующее о полном соответствии кода спецификациям

    Осталось доказать надёжность спецификаций. Но тут в комнату вошёл Гёдель...

     
     
  • 2.165, Аноним (122), 20:33, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +2 +/
    > Но тут в комнату вошёл Гёдель...

    Для справки: (1948 год) ...на собеседовании Гёдель попытался доказать, что Конституция США формально-логически неполна и не гарантирует защиты от установления диктатуры, но был вежливо остановлен.

     
  • 2.192, red75prime (?), 01:11, 18/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    ...посмотрел на что пытаются натянуть его теорему о неполноте, схватился за голову и убежал
     
     
  • 3.193, pashev.ru (?), 20:41, 18/10/2022 [^] [^^] [^^^] [ответить]  
  • –2 +/
    > ...посмотрел на что пытаются натянуть его теорему о неполноте, схватился за голову
    > и убежал

    Так и не понял ты, юный падаван, суть математики.

     
     
  • 4.196, red75prime (?), 07:08, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если это про то, что формализация арифметики может быть противоречивой, то про такое могут беспокоится только совсем выжившие из ума джедаи.
     
     
  • 5.203, pashev.ru (?), 13:55, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Если это про то, что формализация арифметики может быть противоречивой, то про
    > такое могут беспокоится только совсем выжившие из ума джедаи.

    Так и не понял ты, юный падаван, суть математики.

     
  • 5.204, pashev.ru (?), 13:56, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    > Если это про то, что формализация арифметики может быть противоречивой, то про
    > такое могут беспокоится только совсем выжившие из ума джедаи.

    Скачай и прочитай «Гёдель, Эшер, Бах: эта бесконечная гирлянда». А также «Новый ум короля».

     
     
  • 6.205, red75prime (?), 14:44, 20/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если что-то доказано, то оно доказано и это можно проверить механически, и никакие теоремы о неполноте этому не мешают. А соответствует-ли теорема спецификации, написанной на естественном языке - вопрос внематематический. И Гёдель, Пенроуз или Хофштадтер, как и любые другие люди, тут могут только тыкнуть пальцем в несоответствие спецификации и её формализации (если оно есть).
     
     
  • 7.207, Myyx (?), 21:11, 20/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    >> Если что-то доказано, то оно доказано и это можно проверить механически

    точно. проверить и проинтерпретировать. да?

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

     

  • 1.146, Аноним (146), 12:25, 16/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    > KataOS
    > CAmkES
    > seL4

    Названия просто трындец. Предлагаю им сделать имя пользователя по умолчанию - ЛСДУ3.

     
     
  • 2.160, Аноним (160), 15:54, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Держи карман шире!
     
  • 2.161, Лсдуз (?), 15:59, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    думаешь поможет?
     
     
  • 3.163, пох. (?), 16:40, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Да ну нафиг, обычный карго-культ, это так не работает.

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

     
     
  • 4.166, Аноним (122), 21:31, 16/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Это всё у них есть, что ещё они могут сделать?
     

  • 1.167, Аноним (167), 21:33, 16/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    > В качестве примера подобных приложений приводятся системы, манипулирующие изображениями людей и голосовыми записями.

    Никого такие заявления не напрягают ? За такое надо замуровывать пока не поздно. А то потом гуголь наберет кредитов на имя любого человека. Они чем нибудь думают ?

     
     
  • 2.186, A (?), 17:37, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Скорее что тогда надо законодательство и практику менять так, что фото и видео не играют роли. В пользу какой-либо подписи через отпечаток связей нейронных клеток головного мозга.
     
     
  • 3.187, A (?), 17:38, 17/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    А вот если начал думать иначе, сменился отпечаток, сменились документы и заново все права получать... Ибо гад уже думает не как раньше было одобрено.

    Мрак.

     

  • 1.168, Аноним (168), 22:55, 16/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Вспомнилась ОС на Rust Redox. Есть GUI и микроядро
     
     
  • 2.190, истина в последней инстанции (?), 00:30, 18/10/2022 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Типа есть. Оно не работает от слова совсем.
     
     
  • 3.202, Прохожий (??), 07:36, 19/10/2022 [^] [^^] [^^^] [ответить]  
  • +/
    Если ты пытался её запускать, то и неудивительно. С твоими-то когнитивными способностями.
    А так вообще работает. И даже на реальном железе. Фотки на сайте можно посмотреть.
     

  • 1.188, Максим (??), 18:17, 17/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Вот это правильно! Создавайте на Расте новые ОС, а Linux оставьте в покое, пожалуйста.
     
  • 1.194, fidoman (ok), 20:42, 18/10/2022 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    открытие наработок...связанных с проектом...нацеленным на...

    Хороший ход, не публикуя завершённый проект, получить активность энтузиастов, которые расскажут про все дыры.

     

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



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

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