URL: https://www.opennet.dev/cgi-bin/openforum/vsluhboard.cgi
Форум: vsluhforumID3
Нить номер: 128671
[ Назад ]
Исходное сообщение
"Google открыл код защищённой операционной системы KataOS"
Отправлено opennews , 15-Окт-22 10:43 
Компания Google объявила об открытии наработок, связанных с проектом KataOS, нацеленным на создание защищённой  операционной системой для встраиваемого оборудования. Системные компоненты KataOS написаны на языке Rust и выполняются поверх микроядра seL4, для которого на системах RISC-V предоставлено математическое доказательство надёжности, свидетельствующее о полном соответствии кода спецификациям, заданным на формальном языке. Код проекта открыт под лицензией Apache 2.0...

Подробнее: https://www.opennet.dev/opennews/art.shtml?num=57920

Содержание
Сообщения в этом обсуждении
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 10:43 
Genode какой-тл
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 10:45 
Опять пермессивщина
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 10:47 
вам шашечки?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Самый Лучший Гусь , 15-Окт-22 11:04 
GPL нам подавайте иначе это просто напросто фольшивка
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 13:52 
Нам не хочется бесплатно работать на хайпомакак в гугле. Это странно?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 14:28 
Так вы никогда и не работали.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 17:20 
Не хочется потому и не работали. Это разве странно?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Пенис , 15-Окт-22 20:45 
Берёшь и лицензируешь форк под GPL. Всего делов-то, но вонять ты горазд.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 11:54 
> вам шашечки?

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:04 
Вы так говорите, как будто это плохо))
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 12:01 
Да, пермиссивщина это плохо.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:03 
Эти все скучные буковки читайте сами. Где не скучные обои?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:04 
> Rust также предоставляет средства для защиты от целочисленных переполнений

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Анонн , 15-Окт-22 11:14 
Раст предоставляет защиту в дебаге и однозначное поведение в релизе. А не "хз как, пусть компилятор решает".
"Google открыл код защищённой операционной системы KataOS"
Отправлено Лолштоним , 15-Окт-22 20:39 
Как раз компилятор решает.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 23:20 
И разные компиляторы обрабатывают эту ситуацию по разному! В том-то и проблема
"Google открыл код защищённой операционной системы KataOS"
Отправлено анон , 16-Окт-22 02:01 
и сколько есть разных компиляторов rust?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 05:21 
каждую новую версию!
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 11:38 
Ноль. Потому что-то назвать обёртку вокруг llvm "комплилятором" это себя не уважать. Это просто линтер.
"Google открыл код защищённой операционной системы KataOS"
Отправлено анон , 16-Окт-22 13:12 
это даже для опеннета очень слабый наброс.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 13:20 
https://github.com/Rust-GCC/gccrs
https://github.com/bjorn3/rustc_codegen_cranelift
> Ноль. Потому что-то назвать обёртку вокруг llvm "комплилятором" это себя не уважать. Это просто линтер.

Наглядная демонстрация главного принципа Военов Супротив Раста: "Громкий, четкий, мощный пук заменяет аргументы!"

"Google открыл код защищённой операционной системы KataOS"
Отправлено Igraine , 16-Окт-22 13:47 
1) mrustc
2) rust-gcc
3) rustc
"Google открыл код защищённой операционной системы KataOS"
Отправлено анон , 16-Окт-22 23:33 
Интересный пример, в двух из трех репозиториев авторы сами чёрным по белому пишут что это очень ранняя стадия и совсем не готово для продакшна.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Прув , 15-Окт-22 11:18 
Ох уж эти иксперды с опеннета пишущие в комментах чушь…

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 12:22 
Любому человеку это кажется не очень то и безопасным.
"Google открыл код защищённой операционной системы KataOS"
Отправлено eganru , 15-Окт-22 12:28 
Это безопасно.
Почти в любом языке есть возможность сделать безопасную работу и проверку переполнений.

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

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

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 16:44 
Чушь не пори это полностью небезопасно.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Igraine , 15-Окт-22 21:55 
Но ведь в С и С++ если a и b целое со знаком, то переполнение неопределенно, условие всегда ложно и компилятор имеет право его удалить
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 14:20 
это чудесно, но что, если signed?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Маняним , 15-Окт-22 12:26 
> Ох уж эти иксперды с опеннета пишущие в комментах чушь…

про С

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

__builtin_*_overflow

"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 15-Окт-22 13:42 
А где в этой ветке хоть слово было про Си?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 16:45 
Омг
"Google открыл код защищённой операционной системы KataOS"
Отправлено Chlen22sm , 15-Окт-22 21:52 
Лучшая защита это прямые руки и умение в алгоритмы, а не клепание формочек на фреймворках.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Igraine , 15-Окт-22 22:03 
Покажите что вы там своими прямыми руками написали.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено анон , 16-Окт-22 13:31 
ага, просто пишите хороший код, а плохой не пишите.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:06 
>[оверквотинг удален]
> логически верифицированное ядро
> заслуживающими доверия
> особый уровень защиты
> подтверждения отсутствия сбоев
> верификации надёжности
> безопасных приёмов программирования
> минимизирующих ошибки
> Безопасная работа с памятью
> средства для защиты
> минимизации логических ошибок

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено швондер , 15-Окт-22 12:26 

Колючие глаза Римского через стол врезались в лицо администратора, и чем дальше тот говорил, тем мрачнее становились эти глаза. Чем жизненнее и красочнее становились те гнусные подробности, которыми уснащал свою повесть администратор... тем менее верил рассказчику финдиректор. Когда же Варенуха сообщил, что Степа распоясался до того, что пытался оказать сопротивление тем, кто приехал за ним, чтобы вернуть его в Москву, финдиректор уже твердо знал, что все, что рассказывает ему вернувшийся в полночь администратор, все – ложь! Ложь от первого до последнего слова.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 03:22 
> заслуживающими доверия

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:28 
Блин я только перешёл на Fuchsia
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 08:34 
Встречайте! Гладиаторские бои на гугл-арене! И пусть победит сильнейший!
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:32 
Fiasco.OC? Ты ли это?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:35 
Конкуренция это всегда хорошо, может хоть Гугл заставит Линуса шевелиться...
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 11:45 
Это просто чудесно:

> 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.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Alexey Torgashin , 15-Окт-22 11:56 
Пусть сначала этот гугл докажет что это не просто выкидыш , не просто перделка. От вторых мелко мягких . А реальная вещь. Реальная значит работает с реальными программами, которые должны появиться. Не только браузер и медиа плеер которые есть везде и всегда. А VSCode и аналоги, графические редакторы , редакторы видео и монтажа. Офис хорошо бы . И тп.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Самый умный из вас , 15-Окт-22 13:51 
Напиши плз контакты, как гуглу с тобой связаться, куда доказательства отправлять
"Google открыл код защищённой операционной системы KataOS"
Отправлено n00by , 15-Окт-22 17:09 
Так он написал имя. Гугл же всё про всех знает. ;)
"Google открыл код защищённой операционной системы KataOS"
Отправлено Бывалый смузихлёб , 15-Окт-22 11:59 
> Для дополнительной защиты все компоненты, кроме микроядра, изначально развиваются на языке Rust
> на языке Rust
> кроме микроядра
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 12:05 
Логично же. Его же придется переверифицировать заново. А так используют уже верифицированное.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 03:24 
Всё просто: верификатор не может верифицировать код раста.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Alexey Torgashin , 15-Окт-22 12:10 
Похоже я ошибся , ОС не для десктопа а для встраиваемых штук. Но это ещё вопрос кто и зачем возьмёт такую Ос. Для роутеров ? Ещё куда не шло. Для интернета вещей этого поганого, который нужен только для товарища майора чтобы следить , и хакеров ? Тогда нафиг . Для чего ещё?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 12:23 
Подскажу. Даже гугл её никуда не взял. Делай вывод.
"Google открыл код защищённой операционной системы KataOS"
Отправлено _kp , 17-Окт-22 09:55 
Часто подобные проекты изначально делают ради эксперимента, делают тесты, выводы, учитыают в других разработках. Забрасывают побочное изделие.
"Google открыл код защищённой операционной системы KataOS"
Отправлено eganru , 15-Окт-22 12:23 
Для определенного класса встраиваемых штук, тк. требования слишком высокие чтобы на средней руки MCU запускать.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 14:14 
> Для чего ещё?

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

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Бывалый смузихлёб , 15-Окт-22 16:16 
Ну и чем оно лучше того же миникса?

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 09:02 
> Ну и чем оно лучше того же миникса?

Скажу, чтобы у тебя, знатного растохейтера лишний раз подгорело - всё, кроме микроядра, написано на расте, а не на анархистском си студентами в миниксе. По сути это почти как раз та самая "ОС на расте", которую вы от растаманов требуете и ржете над редокcом. Всякие загрузчики и "системдэ", менеджеры памяти, процессов, файловая и сетевая подсистемы, драйверы и т.п - всё на расте. Т.е. можно сказать что это и есть "ОС на расте", не считая микроядра, которое минимальный набор самых базовых функций выполняет. Ну просто микроядро верифицировано и там ошибок нет - можно и оставить.
Вот тем и лучше миникса - тот же самый студент, который с легкостью дырявый сишный усб\блютуз драйвер для миникса напишет, настолько же просто дырявый код в катаос не вкатит - раст будет сильно сопротивляться привычным студенческим ошибкам.

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 21:31 
> где софтварный сбой может стоит миллиарды

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Джон Макагонов , 15-Окт-22 12:29 
Меня уже не удивляет то,  что в передовых разработках применятся раст. Превосходство раста очевидно,  его величие - просто свершившейся факт. Даже скучно уже.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 13:08 
раст не полетел. Ему на смену уже идёт Карбон.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 15-Окт-22 13:55 
MS, Google, Amazon, Meta вовсю начали использовать Rust. Но анонимный воин супротив Раста не даст этим корпорациям себя обмануть. У него дома Rust не взлетел. :)))
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 03:27 
> Meta вовсю начали использовать Rust

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 16:01 
Именно поэтому — как узнают, что на расте написано, сразу бегут, пока пацаны с опеннета не засмеяли.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:22 
Она ещё не готова просто, о взлёте говорить пока рано. Про другие фирмы есть что сказать?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 09:31 
> раст не полетел. Ему на смену уже идёт Карбон.

Ты заврался донельзя. Всё перевернул.

Раст летит как раз хорошо и это видно по проектам, которые пилят гиганты, включая этот. Даже перечислять не буду, вам это без толку раз за разом перечислять. Как метать бисер сами знаете перед кем. Как не в коня корм. Проекты эти просто не для васянов, часть из них сложны, непонятны. Не музыкальные плееры, короче.

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

" Why build Carbon?

<в начале пишут что C++ древнее легаси-...овно, которое долго развивалось как бык поссал (вкривь и вкось) и что там куча технического долга и т.п и т.д. Но есть гигатонны полезного кода, который так просто не выкинешь. А потом пишут:>

Existing modern languages already provide an excellent developer experience: Go, Swift, Kotlin, Rust, and many more. Developers that can use one of these existing languages should. Unfortunately, the designs of these languages present significant barriers to adoption and migration from C++. These barriers range from changes in the idiomatic design of software to performance overhead.

Carbon is fundamentally a successor language approach, rather than an attempt to incrementally evolve C++.

"

Т.е. карбон - заменитель Си++, а не раста. И если ты можешь писАть на расте - ты должен писАть на расте. Так авторы карбона и сказали, честно-честно. Там во фразе "Developers that can use one of these existing languages should" слова "can" и "should" даже выделены жирным шрифтом. Ну чтобы даже тебе понятно было. А вот если ты плюсовик замшелый, который ничего нового выучить не в состоянии, не готов менять парадигму мышления и у которого горы плюсового легаси-кода, требующего переписывании - добро пожаловать в карбон.

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 16:48 
Естесственно, Rust придуман не Google.
"Google открыл код защищённой операционной системы KataOS"
Отправлено eganru , 15-Окт-22 12:34 
Вообще такое ощущение, что новости специально пишут так, чтобы в комментах был жыр с хорошим запасом.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 15:22 
Зима приближается, нужно запасаться.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Друг Сергея , 15-Окт-22 13:06 
Kata Containers, KataOS, Rust и Go - что происходит?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 15-Окт-22 13:52 
Эволюция происходит. Софт усложняется. Люди ищут способы бороться с этой сложностью.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 21:32 
Я бы не сказал, что они что-то упростили...
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 11:28 
Нет ничего проще, надёжнее и безопаснее чем ANSI C, остальное пустой пиар
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 13:12 
> Нет ничего проще, надёжнее и безопаснее чем ANSI C, остальное пустой пиар

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:19 
Работа с памятью. Теперь можно гораздо меньше уделять ей внимания. Странно, что приходится объяснять это снова и снова.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 13:29 
Для дополнительной защиты все компоненты, кроме микроядра, изначально развиваются на языке Rust с использованием безопасных приёмов программирования...

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 15-Окт-22 13:50 
Линукс - для серверов и десктопа. А это для встройки. Разные ниши. В идеале и Линукс весь переписать на Rust полностью.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 14:29 
Только переписывание линукса на раст линуксу ничего не даст. Так что этого никогда не произойдет.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:17 
Вообще-то даст - дополнительную стабильность. Это уже огромный жирный плюс.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Бургер , 15-Окт-22 15:21 
>А это для встройки

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:26 
Вот именно. На помойку. Любая проблема с памятью и всё,  конец железке.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Бургер , 23-Окт-22 13:32 
> Вот именно. На помойку. Любая проблема с памятью и всё,  конец
> железке.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 11:27 
Они не отстанут пока не сломают Линукс окончательно
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 15-Окт-22 14:01 
Ожидаемо набежало стадо воинов супротив Rusta. Местные неосиляторы решили в очередной раз отметиться, высказав своё "фе" к тому, чего они не понимают, потому что неспособны.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 14:09 
Такое ощущение,что amd64 закапывают вслед за х86. Новости чуть ли не поголовно про АРМ и даже Линукс набрал растокодеров для этой архитектуры.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 22:01 
Гегемония интел-амд многим мешает
Гуглу в том сегменте заработать как? Строим новый
"Google открыл код защищённой операционной системы KataOS"
Отправлено ИмяХ , 15-Окт-22 15:11 
>>поверх микроядра seL4,
>>фреймворк Renode
>>инструментарий CAmkES

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 11:23 
Потому что цель это пиар раста.
Если бы цель была написание безопасностной и надёжной операционной системы они бы взяли ANSI C
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 13:10 

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 15:20 
Задавался. И написал. Называется L4.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 15:48 
> Задавался. И написал. Называется L4.

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


"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 09:41 
> безопасностной и надёжной операционной системы
>> Задавался. И написал. Называется L4.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 17:43 
Они взяли верифицированное микроядро и сверху накинули неверифицированную инфраструктуру Rust? Rust верифицировали?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 23:25 
А у вас есть верифицированная инфраструктура на си, чтобы накинуть поверх ядра? Что, нет? Как же так...
Вот и у них не было, а писать с нуля на шрешете они не захотели.
"Google открыл код защищённой операционной системы KataOS"
Отправлено anonymous , 16-Окт-22 13:29 
Примерно те же люди, которые сделали проект 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.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 19:42 
У них ничего не получится. Как обычно.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:30 
Сказал аноним в адрес корпорации с мультимиллиардным оборотом. :)
"Google открыл код защищённой операционной системы KataOS"
Отправлено user90 , 15-Окт-22 19:58 
А там не хрустело ли?
Да и какие дрова? Не под это сферическое оборудование, под реальное?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 20:38 
Васян с бодуна сделает опечатку в коде и всё это логически верифицированное можно отправлять на помойку.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 21:55 
Очередное распиаренное фуфло от гугла для жертв современного образования
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 15-Окт-22 22:40 
Это очень большая проблема что L4 предлагает большой выбор.
Всё должно быть компактно для разной архитектуры в ядре. Без вариантов можно и так и можно и подругому.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Neon , 16-Окт-22 01:05 
От логических ошибок программиста никакой Rust не спасет.)
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 17-Окт-22 09:50 
> От логических ошибок программиста никакой Rust не спасет.)

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 01:31 
Посочувствуем Гугле - кроме него, да пары отмороженых студентов, никто писать на Рже не будет. Если сейчас, со всеми доступными инструментами и туториалами этого никто делать не хочет, то дальше и подавно!

Есть такой "эффект новизны", когда объявляют новый язык и все, кому надо и не надо, набегают в него и начинают писать хелловорлды. Но у Раста этот пик ДАВНО ПОЗАДИ! Все, кто проникся языком, на нём и пишут. Все оба. :) Остальные махнули рукой и БОЛЬШЕ НИКОГДА в него не вернутся. Так что непонятно, на что надеются uдuоты, пропихивающие Раст во все щели - всё, клоуны, расходитесь - ваш Ржа не взлетел! Даже линynс ему не поможет, т.к. подавляющее большинство кода - Си, а растаманские модули попросту выкинут за отсутствием вменяемого количества разрабов.

"Google открыл код защищённой операционной системы KataOS"
Отправлено pashev.ru , 16-Окт-22 08:58 
> математическое доказательство надёжности, свидетельствующее о полном соответствии кода спецификациям

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 20:33 
> Но тут в комнату вошёл Гёдель...

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено red75prime , 18-Окт-22 01:11 
...посмотрел на что пытаются натянуть его теорему о неполноте, схватился за голову и убежал
"Google открыл код защищённой операционной системы KataOS"
Отправлено pashev.ru , 18-Окт-22 20:41 
> ...посмотрел на что пытаются натянуть его теорему о неполноте, схватился за голову
> и убежал

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено red75prime , 19-Окт-22 07:08 
Если это про то, что формализация арифметики может быть противоречивой, то про такое могут беспокоится только совсем выжившие из ума джедаи.
"Google открыл код защищённой операционной системы KataOS"
Отправлено pashev.ru , 19-Окт-22 13:55 
> Если это про то, что формализация арифметики может быть противоречивой, то про
> такое могут беспокоится только совсем выжившие из ума джедаи.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено pashev.ru , 19-Окт-22 13:56 
> Если это про то, что формализация арифметики может быть противоречивой, то про
> такое могут беспокоится только совсем выжившие из ума джедаи.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено red75prime , 20-Окт-22 14:44 
Если что-то доказано, то оно доказано и это можно проверить механически, и никакие теоремы о неполноте этому не мешают. А соответствует-ли теорема спецификации, написанной на естественном языке - вопрос внематематический. И Гёдель, Пенроуз или Хофштадтер, как и любые другие люди, тут могут только тыкнуть пальцем в несоответствие спецификации и её формализации (если оно есть).
"Google открыл код защищённой операционной системы KataOS"
Отправлено Myyx , 20-Окт-22 21:11 
>> Если что-то доказано, то оно доказано и это можно проверить механически

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

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 12:25 
> KataOS
> CAmkES
> seL4

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 15:54 
Держи карман шире!
"Google открыл код защищённой операционной системы KataOS"
Отправлено Лсдуз , 16-Окт-22 15:59 
думаешь поможет?
"Google открыл код защищённой операционной системы KataOS"
Отправлено пох. , 16-Окт-22 16:40 
Да ну нафиг, обычный карго-культ, это так не работает.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 21:31 
Это всё у них есть, что ещё они могут сделать?
"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 21:33 
> В качестве примера подобных приложений приводятся системы, манипулирующие изображениями людей и голосовыми записями.

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

"Google открыл код защищённой операционной системы KataOS"
Отправлено A , 17-Окт-22 17:37 
Скорее что тогда надо законодательство и практику менять так, что фото и видео не играют роли. В пользу какой-либо подписи через отпечаток связей нейронных клеток головного мозга.
"Google открыл код защищённой операционной системы KataOS"
Отправлено A , 17-Окт-22 17:38 
А вот если начал думать иначе, сменился отпечаток, сменились документы и заново все права получать... Ибо гад уже думает не как раньше было одобрено.

Мрак.

"Google открыл код защищённой операционной системы KataOS"
Отправлено Аноним , 16-Окт-22 22:55 
Вспомнилась ОС на Rust Redox. Есть GUI и микроядро
"Google открыл код защищённой операционной системы KataOS"
Отправлено истина в последней инстанции , 18-Окт-22 00:30 
Типа есть. Оно не работает от слова совсем.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Прохожий , 19-Окт-22 07:36 
Если ты пытался её запускать, то и неудивительно. С твоими-то когнитивными способностями.
А так вообще работает. И даже на реальном железе. Фотки на сайте можно посмотреть.
"Google открыл код защищённой операционной системы KataOS"
Отправлено Максим , 17-Окт-22 18:17 
Вот это правильно! Создавайте на Расте новые ОС, а Linux оставьте в покое, пожалуйста.
"Google открыл код защищённой операционной системы KataOS"
Отправлено fidoman , 18-Окт-22 20:42 
открытие наработок...связанных с проектом...нацеленным на...

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