The OpenNET Project / Index page

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

форумы
правила/FAQ
поиск
регистрация
вход
слежка
RSS


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

Оглавление

Линус Торвальдс не исключил возможность интеграции поддержки Rust в ядро Linux 5.20, opennews (ok), 22-Июн-22, (0) [смотреть все]

Сообщения [Сортировка по времени | RSS]


310. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (310), 23-Июн-22, 19:08 
Почему в ядро Linux включают именно:
    протекающий, ненадежный, неверифицируемый Rust,
    a не безопасный, надежный, верифицируемый SPARK
?!!
Ответить | Правка | Наверх | Cообщить модератору

328. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от warlock66613email (ok), 23-Июн-22, 23:33 
Вам ответить отвлечённо или прагматично?

Потому что на Rust приятно писать код. А на SPARK упорешься. Потому что Rust как современный язык отвечает требованиям, предъявляемым современному языку (репозиторий пакетов, вменяемая система сборки, избавление программиста от обезъяньей работы вроде копипаста заголовков методов в интерфейсную часть модуля, и др.), а SPARK — штука древняя. Потому что Rust целенаправленно создавался и создаётся под подобные задачи, и из коробки имеет достойный FFI с Си.

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

Ответить | Правка | Наверх | Cообщить модератору

381. "Линус Торвальдс не исключил возможность интеграции поддержки..."  –1 +/–
Сообщение от Аноним (381), 25-Июн-22, 03:38 
> репозиторий пакетов, вменяемая система сборки

Прямо перечислил априори не нужное

> избавление программиста от работы головой

Фиксанул, не благодари

Ответить | Правка | Наверх | Cообщить модератору

387. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (358), 25-Июн-22, 10:22 
>> избавление программиста от работы головой
> Фиксанул, не благодари

Как что-то плохое. Хотя страх всяких сишников можно понять, ведь повторяется история с станками жаккара.

Ответить | Правка | Наверх | Cообщить модератору

493. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (-), 27-Июн-22, 17:49 
Сишники видите ли обычно системщики. А это свободный и гордый народ, знающий себе цену. Предпочитающие некую автономию и самодостаточность, без лизания ботинок гугла, майкрософта и амазона. А ваше светлое будущее с лизанием ботинок вон тем - выглядит довольно так себе.

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

Ответить | Правка | Наверх | Cообщить модератору

532. "Линус Торвальдс не исключил возможность интеграции поддержки..."  –1 +/–
Сообщение от Аноним (532), 06-Окт-22, 13:05 
> Потому что на Rust приятно писать код.

Ну ты и Петросян!

Ответить | Правка | К родителю #328 | Наверх | Cообщить модератору

533. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от warlock66613email (ok), 07-Окт-22, 19:12 
Я понимаю, что хаскелистам смешно, да. Но мне на Rust приятнее во всех отношениях и проще. Хотя Хаскелл в чём-то удобнее, я согласен.
Ответить | Правка | Наверх | Cообщить модератору

329. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +2 +/–
Сообщение от yet another anonymous (?), 24-Июн-22, 00:00 
Потому что ядро --- важный и значимый ресурс. Подмять его под себя через инфраструктуру, средства разработки или как ещё --- очень логичная стратегия.
Ответить | Правка | К родителю #310 | Наверх | Cообщить модератору

335. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 24-Июн-22, 02:54 
Пфф, а то, что ядро написано на протекающем, ненадёжном, неверифицируемом C, тебя не смущает? Нужно срочно переписать ядро на SPARK! Ну как срочно... на это уйдёт лет 100, учитывая многословность синтаксиса, а также сколько бойлерплейта и контрактов придётся писать к каждой функциональной строчке кода. Код будет в 10 раз больше и никому не нужен, но зато абсолютно безопасен и надёжен. Впрочем, любой код будет абсолютно безопасен, если его не запускать.
Ответить | Правка | К родителю #310 | Наверх | Cообщить модератору

340. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от yet another anonymous (?), 24-Июн-22, 07:47 
s/SPARK/Rust/g

И что, что-то по сути поменялось в месседже?

Ответить | Правка | Наверх | Cообщить модератору

350. "Линус Торвальдс не исключил возможность интеграции поддержки..."  –1 +/–
Сообщение от burjui (ok), 24-Июн-22, 10:19 
Если думать не головой, а задницей, то нет.
Ответить | Правка | Наверх | Cообщить модератору

359. "Линус Торвальдс не исключил возможность интеграции поддержки..."  –1 +/–
Сообщение от Аноним (154), 24-Июн-22, 14:35 
> Если думать не головой, а задницей, то нет.

Ну так покажи эту разницу тем, кто думает задницей...

Или ты то же из таких?

Ответить | Правка | Наверх | Cообщить модератору

360. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анончик (?), 24-Июн-22, 14:48 
А то! 4.332
Ответить | Правка | Наверх | Cообщить модератору

369. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 24-Июн-22, 21:10 
Я уже задолбался кому-то что-то объяснять на этом ресурсе. Тем более бессмысленно объяснять что-то тем, кто думает задницей. Никто даже документацию прочитать не в состоянии, не то что попробовать написать что-то более-менее сложное на языке перед тем, как гадить в комменты про "вырвиглазный синтаксис" и прочую чепуху. Сами идите, пишите на обоих языках, а потом сравнивайте объём кода, трудозатраты и КПД своей работы. А заодно подумайте, почему ни один из формально верифицируемых языков даже близко не пошёл в массы.
Ответить | Правка | К родителю #359 | Наверх | Cообщить модератору

371. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анончик (?), 24-Июн-22, 21:37 
Не нужно ничего объяснять, лучше расскажи, почему ни один из формально верифицируемых языков даже близко не пошёл в массы. Послушаем умного человека.
Ответить | Правка | Наверх | Cообщить модератору

372. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 24-Июн-22, 22:35 
Потому что на них, внезапно, сложно и долго писать. Или ты думал, что там просто компиляторы очень умные, сами угадывают твои намерения, и верификация даётся бесплатно? Чтобы верифицировать твой код, ты сначала должен опписать критерии верификации - то есть, "контракты" в терминологии SPARK. И тебе придётся каждую строчку кода обложить пачкой контрактов, далеко не всегда тривиальных, и тебе это очень быстро надоест, потому что успеешь постареть, пока напишешь хоть какой-то функционал. Для космических аппаратов и ядерных электростанций это приемлемо, а для менее критичного софта - нет. Никто не будет ждать 2 года, пока ты напишешь супернадёжный медиаплеер. И даже SPARK не защитит от логических ошибок, пока контракты пишет человек.
Ответить | Правка | Наверх | Cообщить модератору

401. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 18:53 
Ответ: массового заказчика нет.

SPARK уже занял свою нишу. Заказчик должен платить за надежность, безопасность и верифицируемость ПО.

Есть надежная, безопасная и верифицируемая ОС: https://muen.sk

Кажется стандарт в гражданской авиации. Даже в РФ бортовое ПО на ADA-SPARK пишут?

Кроме атомной энергетики, военные SPARK любят в своих АСУ.

Сегодня просто уникальный исторический момент. Прошло около 45 лет со дня заказа разработки этого языка программирования, сменилось несколько поколений программистов и на конец в GNU смогли написать свободный компилятор RUST. Вхождение в мир надежного, безопасного и верифицируемость ПО стоит не десятки миллиардов долларов, а 0.0$

Я категорически против зоопарка. Убежден, что Linux должен писался на C и ASM, как это было изначально. А добавление любого другого языка в ядро Linux только запустить его, затруднит поддержку и использование. А конкретно Rust вместо безопасности добавит новые классы уязвимостей.

Ответить | Правка | Наверх | Cообщить модератору

407. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 20:03 
>Вхождение в мир надежного, безопасного и верифицируемость ПО стоит не десятки миллиардов долларов, а 0.0$

Из крайности - в крайность. Типичный опеннетный эксперт.
>0.0$

Это если не писать контракты в том же SPARK. Правда, тогда и код не скомпилируется. А контрактов придётся писать больше, чем кода. Так что совсем не 0$.
> А конкретно Rust вместо безопасности добавит новые классы уязвимостей.

На каком основании вы сделали такой вывод?

Ответить | Правка | Наверх | Cообщить модератору

499. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (499), 27-Июн-22, 19:47 
>> А конкретно Rust вместо безопасности добавит новые классы уязвимостей.
> На каком основании вы сделали такой вывод?

Новый язык, другой компилятор, от других людей, новые дыры:
https://www.cvedetails.com/vulnerability-list.php?vendor_id=...
https://www.developer-tech.com/news/2022/jan/24/rust-vulnera.../
Намного усложнитса поддержка и аудит кода.
И это еще не те новые классы уязвимостей которые я иметь ввиду.

Вся модель безопасности ОС держится на правеле: что исполняется не должно изменятся, а что изменяется не должно исполнятся (согласовано учеными конца 1960-тых и принято в стандарт 1983). В помощь инструкции проца NX, PAE.

С этого следуют требования к защите памяти:

CONFIG_PAX_MPROTECT=y
- changing the executable status of memory pages that were
   not originally created as executable,
- making read-only executable pages writable again,
- creating executable pages from anonymous memory,
- making read-only-after-relocations (RELRO) data pages writable again.

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

Рассуждения: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/lin...

Executable code and read-only data must not be writable
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Any areas of the kernel with executable memory must not be writable. While this obviously includes the kernel text itself, we must consider all additional places too: kernel modules...

Это же относится и ко всему прикладному ПО без исключений и копромисов на JIT, PBF, ... и прочью дрянь. Принципиальный вопрос о толерантности к Rust, в прикладном ПО, зависит от строгого следования этим правилам.

Ответить | Правка | Наверх | Cообщить модератору

508. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 29-Июн-22, 02:05 
Вы так и не привели ни одного примера "новых классов уязвимостей", которые якобы привнесёт именно Rust.
Ответить | Правка | Наверх | Cообщить модератору

522. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (-), 01-Июл-22, 00:13 
> Вы так и не привели ни одного примера "новых классов уязвимостей", которые
> якобы привнесёт именно Rust.

Кодер подумал что безопасТно и забил на использование мозга. Маркетологи гамадрила корп сказали же что безопасТно!

Ответить | Правка | Наверх | Cообщить модератору

525. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 01-Июл-22, 00:51 
Зато голословно заявлять про какие-то мифические "новые классы" (что мля?) уязвимостей - это явный признак полного использования мозга. Жаль только, что мозг используется, а результат такой, как будто нет - получается, энергия расходуется впустую. "безопасТно", "гамадрила корп" и прочие "хрусты" - это всё, на что способен мозг типичного хейтерка с Опеннета, потому что он ещё не окончил школу, но зато уделал одноклассников на уроках информатики своими обширными познаниями в разработке на Turbo Pascal и C, на котором он не делает ошибок, потому что ничего не пишет.
Ответить | Правка | К родителю #522 | Наверх | Cообщить модератору

531. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (531), 05-Окт-22, 17:49 
Не голословно. Для GNU/Linux придется использовать этот компилятор Rust: https://www.opennet.ru/opennews/art.shtml?num=57491 стандартный компилятор добавит новые классы уязвимостей.
Ответить | Правка | К родителю #525 | Наверх | Cообщить модератору

375. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (375), 24-Июн-22, 23:27 
Как может данная прослойка обеспечить безопасность, если у нее 70% кода unsafe? Т.е фактически, будет вызываться из безопасного кода, небезопасные функции из прослойки. Да о чем можно говорить, когда этому подтверждение недописанный драйвер android от гугла.
Если моя логика абсолютна не верна, то как тогда?
Ответить | Правка | К родителю #369 | Наверх | Cообщить модератору

376. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от yet another anonymous (?), 24-Июн-22, 23:50 
Там продвигаются более интернсные вещи, хотя на них обращают внимание сильно меньше. Это
   - сборочная система
   - легкий update компилятора
   - пакетная система с автоподгрузкой из сетки by demand в процессе сборки

Демпфировать это, в принципе, можно, но en masse это неустранимо (см. npm, pip, доустановка deb-пакетов на лету в CI, аналогичное подтягивание docker'ов, ...).

Ответить | Правка | Наверх | Cообщить модератору

402. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 18:56 
> пакетная система с автоподгрузкой из сетки by demand в процессе сборки

Это смерть безопасности.

Ответить | Правка | Наверх | Cообщить модератору

523. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (-), 01-Июл-22, 00:20 
>    - сборочная система

Лизать ботинки гугла, амазона и майкрософт с их Единственно Правильной Экосистемой - вообще баг а не фича.

>    - легкий update компилятора

Безопасным curl | sh? :) Где ремотным джентльменам верят на слово.

>    - пакетная система с автоподгрузкой из сетки by demand
> в процессе сборки

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

Ответить | Правка | К родителю #376 | Наверх | Cообщить модератору

377. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 00:03 
Как же вы достали уже с этим, сил нет... Неужели самим непонятно, что любой потенциальный косяк работы с памятью будет локализован в этих блоках unsafe? Весь остальной код гаратированно ни при чём. А это значит, что аудит на предмет некорректных обращений к памяти (а это основной источник уязвимостей, особенно с получением root доступа) нужно проводить только для unsafe блоков. Никто и никогда не обещал полной безопасности обращений к памяти при наличии unsafe кода, однако локализация небезопасных операций в соответствующих блоках очень сильно сужает область поиска потенциальных и актуальных багов. Практически невозможно, даже тысячей глаз, прочитать миллион строк кода и найти там все переполнения буфера и т.п.. С 10к строк это сделать гораздо проще.
Ответить | Правка | К родителю #375 | Наверх | Cообщить модератору

382. "Линус Торвальдс не исключил возможность интеграции поддержки..."  –1 +/–
Сообщение от Аноним (381), 25-Июн-22, 03:44 
> косяк работы с памятью

Проблемы квалификации программиста, а не языка как такового. Хотя, глядя на то что творится в IT и какие макаки-гуманитарии туда идут, за будущее не страшно, т.к. выдумки о скайнете так и останутся выдумками.

Ответить | Правка | Наверх | Cообщить модератору

383. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +1 +/–
Сообщение от burjui (ok), 25-Июн-22, 05:19 
По твоей логике в мире нет ни одного квалифицированного программиста, потому ошибки совершают абсолютно все.
Ответить | Правка | Наверх | Cообщить модератору

389. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +1 +/–
Сообщение от Аноним (358), 25-Июн-22, 10:37 
> Проблемы квалификации программиста, а не языка как такового

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

Ответить | Правка | К родителю #382 | Наверх | Cообщить модератору

404. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 19:19 
> Неужели самим непонятно, что любой потенциальный косяк работы с памятью будет локализован в этих блоках unsafe

Тебя обманули и ты вводишь в заблуждение других.

В ядро Linux, уже очень давно, лет 20 как, можно компилятором gcc собрать безопасно:
  гарантии безопасной работы с памятью получить МОЖНО!!!
  гарантии надежности НЕТ.
  автоматической математической верификации корректности на уровне исходныых текстов НЕТ.

Гарантии безопасности работы ядра Linux с памятью:
config_pax_kernexec
config_grkernsec_randstruct

Безопасность работы с памятью в ядрах некоторых UNIX, Linux, NetBSD, частично OpenBSD уже есть! И все на C. Она достигнута логически следуя правилу: все, что исполняется не должно изменятся, а что изменяется не должно исполнятся. Используя инструкции процессоров (постранично) или даже полностью софтварно (посегментно). Эксплуатация переполнения буфера невозможна! Цена использования C: невозможность дать гарантии надежности при дачи гарантий безопасности работы с памятью.

Ответить | Правка | К родителю #377 | Наверх | Cообщить модератору

406. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 19:44 
Еще одна большая сакральная тайна которую пропагандисты Rust скрывают, чтобы вас всех обмануть:

Ядра некоторых UNIX, Linux, NetBSD, Apple OS X, частично OpenBSD и MS Windows дают гарантии безопасной работы с памятью для всего прекладного ПО! Даже, для того, что написан на дырявом C и текущем Rust:

Для Linux включите опции ядра:

config_pax_noexec
config_pax_pageexec    (надеюсь ваш проц инструкцию NX держит)
config_pax_mprotect

И получаем гарантии безопасности и корректности работы с памятью сразу всего прикладного ПО, на любом языке программирования, собранного любым компилятором!!!

Цена: нет гарантий надежности. В авиации, атомной энергетике, ... необходима надежность.

Ни Rust ни C надежности и верификации вам не дадут.

Ответить | Правка | Наверх | Cообщить модератору

408. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 20:14 
>> Неужели самим непонятно, что любой потенциальный косяк работы с памятью будет локализован в этих блоках unsafe
>Тебя обманули и ты вводишь в заблуждение других.

Аргументы будут или пука в лужу, по вашему мнению, достаточно?

>все, что исполняется не должно изменятся, а что изменяется не должно исполнятся.

Такой способ безопасной работы с памятью не бесплатен, а имеет накладные расходы во время выполнения кода, в отличие от статической верификации.

Ответить | Правка | К родителю #404 | Наверх | Cообщить модератору

410. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 20:41 
> Аргументы будут или пука в лужу, по вашему мнению, достаточно?

В луже с растом сейчас сидишь ты.

Аргументируют:

config_pax_noexec
config_pax_pageexec    (надеюсь ваш проц инструкцию NX держит)
config_pax_mprotect
config_pax_kernexec


1. Дает гарантии корректной и безопасной работы с памятью ядра Linux и всего прикладного ПО не зависимо от язака написания и используемого компилятора.

2. Накладные расходы при постраничной проверке памяти равны 0 для следующих архитектур процессоров: alpha, avr32, ia64, parisc, sparc, sparc64, x86_64, i386 и старше с поддержкой инструкции NX. А для ppc, ppc64 накладные расходы мизерны.

Прочти в учебнике раздел о "Проактивной защите".

И всем обратить внимание на РЕАЛИЗАЦИЮ защиты пямяти в разных ОС.

Правильная защита памяти: Linux+PAX, NetBSD, Apple OS X, ...

Не правильная защита памяти: OpenBSD, MS Windows, ...

Ответить | Правка | Наверх | Cообщить модератору

413. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 21:59 
>Накладные расходы при постраничной проверке памяти равны 0 для следующих архитектур процессоров: alpha, avr32, ia64, parisc, sparc, sparc64, x86_64, i386 и старше с поддержкой инструкции NX.

Здесь был неправ, признаю.

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

Ответить | Правка | Наверх | Cообщить модератору

423. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (423), 26-Июн-22, 11:13 
> Тем не менее, от некорректного обращения к памяти эта технология не защищает. Она защищает от последствий некорректного обращения к памяти - то есть, вместо того, чтобы дать прочитать мусор или переписать адрес возврата, сгенерирует аппаратное исключение, а ОС, скорее всего, грохнет процесс. То есть, код по-прежнему может попытаться прочитать мусор или переполнить буфер, после чего упасть.

Там есть разные варианты в разных ситуациях:

1. Не убивать процессы, а только логировать ошибки.

2. Убивать процессы и логировать ошибки.

3. Убить ВСЕ процесы пользователя, запретить создание новых и логировать ошибки.

4. При угрозе изменения логов с ошибками, убивать все процесы и само ядро ОС, для сохранения лога.

> При статической же проверке некорректных обращений к памяти вовсе не будет.

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

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

Ответить | Правка | Наверх | Cообщить модератору

453. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 26-Июн-22, 13:17 
> А вот надежности работы программы не дает!

И правильно, кому она нужна? Главное - уязвимостей нет, а то что прога падает - так это проблемы пользователя, поэтому будем фанатично упираться и продолжать писать на C. Лучше пожертвуем пользователем, но на Rust принципиально писать не будем.

Ответить | Правка | К родителю #423 | Наверх | Cообщить модератору

477. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (477), 26-Июн-22, 19:52 
> уязвимостей нет,

Уязвимость есть они никуда не денутся. Криворукий сишник таки ошибку сделал. Благодаря проактивной защите реализованной в ОС и процессоре, бажную прогу убили и записали лог о ошибке.

> а то что прога падает - так это проблемы пользователя,

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

> на Rust принципиально писать не будем.

Я стал противником go и по инерции Rust когда увидел список зависимостей к ipfs, при компиляции мне с инета начало тянуть >1200 никем не подписаных пакетов. Также считаю Rust в ядре Linux неуместным, пусть оно остается на C и ASM.

Ответить | Правка | К родителю #453 | Наверх | Cообщить модератору

411. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 21:03 
Узри саму убогость и ущербность идеи Rust иметь частичную (ибо есть unsave) проверку во время сборки только для одной программы написанные на Rust, по сравнению с глобальной гарантией корректности и безопасности работы с памятью всех программ без любых исключений (включая даже блоки unsave) от ядра ОС и процессора. И без любых накладных расходов для x86_64.

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

Незыблимый принцип безопасности:

ГАРАНТИИ защиты и корректности работы с памятью дает ядро ОС с процессором. А не аккуратность програмиста, продвинутость компилятора (хотя это тоже очень важно) или какой-то очередной ЯП.

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

Ответить | Правка | К родителю #408 | Наверх | Cообщить модератору

414. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 22:06 
Прочитай мой комментарий ниже со ссылками на код Muen. Надеюсь, я там наглядно показал, чего стоят "гарантии надёжности и безопасности" SPARK, которые по принципу идентичны гарантиям Rust.

Даже на главной странице написано:

SPARK is a software development technology specifically designed for engineering high-reliability applications.

It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements.

> ultra-low defect software

Внимательно прочитал? Не defectless, а ultra-low defect. Не дают они "математическиие гарантии надёжности и безопасности", потому что это невозможно.

Ответить | Правка | Наверх | Cообщить модератору

422. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (423), 26-Июн-22, 10:49 
> Внимательно прочитал? Не defectless, а ultra-low defect. Не дают они "математическиие гарантии надёжности и безопасности", потому что это невозможно.

Имеется в ввиду ОБЩЕЕ решение "ultra-low defect".

SPARK это верификатор подмножества языка программирования ADA, дающий гарантии отсутствия ошибок и корректности работы с памятью на уровне исходных текстов. Проверяются ТОЛЬКО исходные тексты, а не запускаемые бинари.

Есть еще компилятор языка програмирования ADA, который тоже разрабатывался как высоконадежный и очень безопасный.

Незабываем о CPU с его асемблером в котором тоже иногда просачиваются ошибки.

Общие решение:

  исходный код на SPARK + компилятор языка программирования ADA + исполняющий бинарь процессор -- 100% гарантий не имеет,

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

Ответить | Правка | Наверх | Cообщить модератору

427. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +1 +/–
Сообщение от burjui (ok), 26-Июн-22, 12:28 
>100% гарантий не имеет,

Вот именно.

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

Согласен, с этим я не спорю.

Впервые за долгое время дискуссия на опеннете привела к чему-то кроме уничтожения нейронов головного мозга: кто-то признал, что 100% гарантий не даст ни один ЯП без серьёзных ограничений множества возможных программ, а я узнал о новом для себя ЯП, который имеет смысл изучить хотя бы для кругозора. Это повод принести в жертву компьютерным богам содержимое /tmp.

Ответить | Правка | К родителю #422 | Наверх | Cообщить модератору

476. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (477), 26-Июн-22, 19:34 
> кто-то признал, что 100% гарантий не даст ни один ЯП

Конечно не даст. В верификаторах SPARK наверняка есть ошибки, программист может "неаккуратно что написать" и бажный верификаторах пропустит дыру. Со временем вылежут и баги.

> я узнал о новом для себя ЯП, который имеет смысл изучить хотя бы для кругозора

Мне точно известно что версия SPARK-2021 у них получилась наконец рабочая. И компилятор GNU для ADA в 2021 году так-же наконец получился рабочим и пригодным для промышленного использования. Год прошел, а я так и не решилась что-то написать, другие задачи.

Меня интересуют ответы на вопросы:

1. Насколько готовый бинарь со SPARK медленнее бинаря скомпиленого с C.

2. Задачи жесткого реального времени. В ASM и C можно рассчитать количество тактов проца необходимых для работы проги. А в SPARK  можно дать гарантии исполнения бинаря за определенное количество тактов процессора?

3. Насколько долго писать на SPARK по сравнению с C или Python? Трудозатраты?

Ответить | Правка | К родителю #427 | Наверх | Cообщить модератору

479. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от warlock66613email (ok), 26-Июн-22, 20:14 
> В ASM и C можно рассчитать количество тактов проца необходимых для работы проги.

А вот объясните, как специалист, каким образом можно рассчитать количество тактов в асм, если оно зависит как минимум от того как удачно бранч предиктор справится со своей задачей?

Ответить | Правка | К родителю #476 | Наверх | Cообщить модератору

495. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (499), 27-Июн-22, 18:13 
Там считают не минимум (с "предсказаниями" проца) а максимум, чтобы сказать: "вот за такое количество тактов прога гарантировано отработает".
Ответить | Правка | К родителю #479 | Наверх | Cообщить модератору

496. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (499), 27-Июн-22, 18:31 
Если с предсказаниями рассчитывать, то считаем по худшему варианту.
Ответить | Правка | К родителю #479 | Наверх | Cообщить модератору

498. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (499), 27-Июн-22, 18:48 
Лучше без предсказателя считать и работать.
Ответить | Правка | К родителю #496 | Наверх | Cообщить модератору

421. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (358), 26-Июн-22, 10:36 
> ГАРАНТИИ защиты и корректности работы с памятью дает ядро ОС с процессором. А не аккуратность програмиста

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

Ответить | Правка | К родителю #411 | Наверх | Cообщить модератору

497. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (499), 27-Июн-22, 18:40 
> секты свидетелей прямых рук

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

К стати а на каком из уровней ИТ безопасности в США требуется чистка персонала?

C: DAC
B: MAC
A1: математическое доказательство корректности кода.

Ответить | Правка | Наверх | Cообщить модератору

400. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 18:28 
> Сами идите, пишите на обоих языках, а потом сравнивайте объём кода, трудозатраты и КПД своей работы.

Ты правильные вопросы задал:
  объем кода
  трудозатраты
  КПД
молодец.

Теперь в твою модель добавь следующие переменные:
  надежность (авиация, еретические производства, оборонка - сбой, падение программы неприемлемо)
  безопасность (требуется уровень не ниже A1 - математическое доказательство корректности, отсутствия ошибок и уязвимостей на уровне исходных текстов)
И перещетай заново свои критерии оценки языка:
  объем кода
  трудозатраты
  КПД
И где теперь Rust с C по сравнению со SPARK?

> А заодно подумайте, почему ни один из формально верифицируемых языков даже близко не пошёл в массы.

Это смотря кто заказчик. Массовому заказчику надо:
  быстро и дёшево
а не
  надежно, безопасно, верефицируемо.
По этому пишут на Python.

За SPARK стоит самый крутой заказчик, которому необхожим язык дающий сразу гарантии:
  надежности
  безопасности
  верефицируемости
всем написанным на нем програмам. Трудозатраты на мат верификацию исходного кода на отсутствие уязвимостей и збоев работы программы на SPARK равны 0.

Ответить | Правка | К родителю #369 | Наверх | Cообщить модератору

405. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 19:39 
Как я и писал выше, опеннетовский эксперт не умеет читать [1] и мыслить критически [2]. А в вашем случае ещё и минимально грамотно писать [3] - это при наличии спеллчекера в браузере. Зато всё на свете знает. И правильно - зачем думать, если можно просто знать?

[1] Выше я писал: "И тебе придётся каждую строчку кода обложить пачкой контрактов, далеко не всегда тривиальных, и тебе это очень быстро надоест, потому что успеешь постареть, пока напишешь хоть какой-то функционал. Для космических аппаратов и ядерных электростанций это приемлемо, а для менее критичного софта - нет. Никто не будет ждать 2 года, пока ты напишешь супернадёжный медиаплеер."

[2] "Трудозатраты на мат верификацию исходного кода на отсутствие уязвимостей и збоев работы программы на SPARK равны 0."
Ага, а про трудозатраты на написание нескольких контрактов на одну строчку кода мы, конечно же, забудем. Видимо, компилятор сам догадается, что ты имел ввиду и напишет контракты за тебя. Только непонятно тогда, зачем нужен программист, если компилятор такой умный.

[3] Не люблю докапываться до орфографии, но это же просто ужас какой-то - "перещетай", "збоев", "верефицируемо", "програмам".

Ответить | Правка | Наверх | Cообщить модератору

409. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Анлним (?), 25-Июн-22, 20:17 
Не хами. Писал грамотно, а вражеский спелчекер поменял слова.

Вот Ыксперту по безопасной работе с памятью еще:

https://www.opennet.ru/openforum/vsluhforumID3/127824.html#404
https://www.opennet.ru/openforum/vsluhforumID3/127824.html#406

Могу сравнить трудозатраты по разработке ПО на Python и C как 1 к 10. Соответственно считай КПД и цену ПО как 1 к 10.

Смотри код ядра ОС на СОВРЕМЕННОМ SPARK-2014: https://git.codelabs.ch/?p=muen.git;a=tree;f=kernel/src

Он легко читаем, понятен, удобен для поддержки.

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

Тебя обманули и ты вводишь в заблуждение других. Смотри спецификации языка SPARK-2014, лучше SPARK-2021. Им таки удалось написать АВТОМАТИЧЕСКИЙ ВЕРИФИКАТОР почти всего синтаксиса языка програмирования "ADA".

Сегодня GNU уже почти всевозможные вериыикаторы написала. В общем писать верифйикаторы не придется. Смотри пример кода ядра OS на SPARK-2014:
https://git.codelabs.ch/?p=muen.git;a=blob;f=kernel/src/sk-k...
https://git.codelabs.ch/?p=muen.git;a=blob;f=kernel/src/sk-k...

Ответить | Правка | Наверх | Cообщить модератору

412. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 25-Июн-22, 21:51 
Интересные ссылки ты приводишь. А я вот заглянул в другую часть сорцов, и что же я вижу?

https://git.codelabs.ch/?p=muen.git;a=blob;f=common/src/sk-c...
  27    procedure Cli
  28    with
  29       Global  => (In_Out => X86_64.State),
  30       Depends => (X86_64.State =>+ null),
  31       Inline_Always;

https://git.codelabs.ch/?p=muen.git;a=blob;f=common/src/sk-c...
  37    procedure Cli
  38    with
  39       SPARK_Mode => Off
  40    is
  41    begin
  42       System.Machine_Code.Asm
  43         (Template => "cli",
  44          Volatile => True);
  45    end Cli;

Итого 2 контракта на одну инструкцию "cli" и отключение режима SPARK. То есть, SPARK знать ничего не знает про инструкцию "cli" и никаких гарантий давать не может в принципе, поэтому компилируем функцию как обычную ADA. Ловко выкрутились 😁 Так это что получается, аналог unsafe? Вот тебе и хвалёная верификация. "Мамой клянусь, эта функция только X86_64.State меняет!". Ну что сказать, сильные гарантии. Прямо как в другом языке, где тоже можно из безопасного кода вызывать опасный. Но этот другой язык - плохой, потому что называется Rust, а вот SPARK намного лучше, хотя суть у него та же: разработчик в маленькой функции пообещал не хулиганить, а компилятор пожал плечами и разрешил её вызывать, полагаясь на честное слово.

Ответить | Правка | Наверх | Cообщить модератору

418. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (423), 26-Июн-22, 10:19 
1. Пока не весь код Mumen написан на SOARK-2014 и ASM, есть немного кода на неверифицируемой ADA+2012: https://git.codelabs.ch/?p=muen.git;a=blob;f=README

2. Ядро OS это очень низкоуровневое ПО работающие напрямую с железом, асемблерными инструкциями процессора. На данном этапе эволюции процессоров и языков программирования пока необходимо использовать асеблерный код для написание некоторых частей OS. Да, поддержку CPU без асеблера не напишешь. Асемблерный код неверифицируется SPARK, весь Асемблерный код необходимо проверять руками, но его немного: https://git.codelabs.ch/?p=muen.git;a=tree;f=kernel/src/asm В отношении асемблерного кода нет гарантий безопасности и надежности.

3. Использование неверифицируемой ADA, влияет только на математические доказательства отсутствия ошибок и корректности работы с памятью на уровне исходных текстов. По надежности и безопасности ПО на ADA на порядок выше чем C и Rust.

4. Прикладное ПО, это не ядро ОС, можно писать на чистом SPARK без ASM.

Ответить | Правка | Наверх | Cообщить модератору

419. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (423), 26-Июн-22, 10:33 
> поэтому компилируем функцию как обычную ADA.

Язык SPARK это верифицируемое подмножество языка программирования ADA.

SPARK своего компилятора не имеет, для компиляции программ на SPARK используется обычный компилятор ADA.

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

В автоматический верификации добавляются новые верификаторы добавляя синтаксис ADA в верифицируемое подмножество SPARK.

Ответить | Правка | К родителю #412 | Наверх | Cообщить модератору

420. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от n00by (ok), 26-Июн-22, 10:34 
Clear Interrupt Flag (cli)

Operation
0 → IF

Description
Clears the interrupt flag if the current privilege level is at least as privileged as IOPL;
affects no other flags. External interrupts disabled at the end of the cli instruction
or from that point on until the interrupt flag is set

Ответить | Правка | К родителю #412 | Наверх | Cообщить модератору

424. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 26-Июн-22, 12:05 
Я тоже умею копипастить и знаю, что делает инструкция cli. Что сказать-то хотел этим?
Ответить | Правка | Наверх | Cообщить модератору

450. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от n00by (ok), 26-Июн-22, 13:16 
> Я тоже умею копипастить и знаю, что делает инструкция cli.

Я это не заметил в "Мамой клянусь, эта функция только X86_64.State меняет!".


Ответить | Правка | Наверх | Cообщить модератору

458. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 26-Июн-22, 13:40 
Потому что у тебя опилки в голове.

Читаем https://sites.radford.edu/~nokie/classes/320/std_lib_html/sy...:

procedure Asm (
  Template : String;
  Outputs  : Asm_Output_Operand_List;
  Inputs   : Asm_Input_Operand_List;
  Clobber  : String  := "";
  Volatile : Boolean := False);

procedure Asm (
  Template : String;
  Outputs  : Asm_Output_Operand := No_Output_Operands;
  Inputs   : Asm_Input_Operand_List;
  Clobber  : String  := "";
  Volatile : Boolean := False);

procedure Asm (
  Template : String;
  Outputs  : Asm_Output_Operand_List;
  Inputs   : Asm_Input_Operand := No_Input_Operands;
  Clobber  : String  := "";
  Volatile : Boolean := False);

procedure Asm (
  Template : String;
  Outputs  : Asm_Output_Operand := No_Output_Operands;
  Inputs   : Asm_Input_Operand  := No_Input_Operands;
  Clobber  : String  := "";
  Volatile : Boolean := False);

function Asm (
  Template : String;
  Outputs  : Asm_Output_Operand_List;
  Inputs   : Asm_Input_Operand_List;
  Clobber  : String  := "";
  Volatile : Boolean := False)
  return     Asm_Insn;

function Asm (
  Template : String;
  Outputs  : Asm_Output_Operand := No_Output_Operands;
  Inputs   : Asm_Input_Operand_List;
  Clobber  : String  := "";
  Volatile : Boolean := False)
  return     Asm_Insn;

function Asm (
  Template : String;
  Outputs  : Asm_Output_Operand_List;
  Inputs   : Asm_Input_Operand := No_Input_Operands;
  Clobber  : String  := "";
  Volatile : Boolean := False)
  return     Asm_Insn;

function Asm (
  Template : String;
  Outputs  : Asm_Output_Operand := No_Output_Operands;
  Inputs   : Asm_Input_Operand  := No_Input_Operands;
  Clobber  : String  := "";
  Volatile : Boolean := False)
  return     Asm_Insn;

Ты здесь видишь какие-нибудь контракты? А здесь?

procedure Cli
  38    with
  39       SPARK_Mode => Off
  40    is
  41    begin
  42       System.Machine_Code.Asm
  43         (Template => "cli",
  44          Volatile => True);
  45    end Cli;

А здесь они откуда-то взялись, хотя функция System.Machine_Code.Asm контрактов не имеет:

  27    procedure Cli
  28    with
  29       Global  => (In_Out => X86_64.State),
  30       Depends => (X86_64.State =>+ null),
  31       Inline_Always;

Ну, и откуда они взялись? А их приписал разработчик. Но мог написать другие, некорректные, или вовсе не писать. Получается "мамой клянусь". А ведь верификация на контрактах держится, без них тебе компилятор ничего за пределами Ada 2012 не гарантирует.

Ответить | Правка | К родителю #450 | Наверх | Cообщить модератору

460. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от n00by (ok), 26-Июн-22, 14:13 
Я своими опилками не догоняю, как и что можно верифицировать в запрете прерываний. Посмотреть далее наличие Hlt и убедиться, что инициализируется Application Processor? У меня прям дымиться начинают опилки от этих мыслей.
Ответить | Правка | К родителю #458 | Наверх | Cообщить модератору

461. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от burjui (ok), 26-Июн-22, 14:31 
Такое ощущение, что ты притворяешься дурачком ради троллинга. Не могу поверить, что до сих пор непонятно. Какая разница, запрет прерываний это или что-то ещё? Нет контрактов - нет верификации. Контракты пишутся человеком, а не компилятором. Компилятор доверяет контрактам. Чем это принципиально отличается от unsafe в Rust?
Ответить | Правка | К родителю #460 | Наверх | Cообщить модератору

464. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от n00by (ok), 26-Июн-22, 16:05 
Возможно дело в том, что ты пытаешься везде разглядеть атаки на Rust. На само деле, мне интересна именно эта команда. Ты писал когда-нибудь команду cli? Если да, то зачем?
Ответить | Правка | К родителю #461 | Наверх | Cообщить модератору

474. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (-), 26-Июн-22, 18:30 
> procedure Asm (
>   Template : String;
>   Outputs  : Asm_Output_Operand_List;
>   Inputs   : Asm_Input_Operand_List;
>   Clobber  : String  := "";
>   Volatile : Boolean := False);

Что это за ужас? Это вроде не хруст? Они даже хрустиков по ужасному синтаксису сделали, с отрывом.

Ответить | Правка | К родителю #458 | Наверх | Cообщить модератору

475. "Линус Торвальдс не исключил возможность интеграции поддержки..."  +/–
Сообщение от Аноним (477), 26-Июн-22, 19:01 
> Мамой клянусь ...

Не клянись, никогда, ничем.

Тем более в вопросах языка на котором здесь никто не написал ни одной строчки кода. И никто не проверял что компилятор ADA эще с этим делает.

Клястся не хорошо.

Ответить | Правка | К родителю #412 | Наверх | Cообщить модератору

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

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




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

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