The OpenNET Project / Index page

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



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

"Опасные уязвимости в GStreamer, CUPS, wolfSSL, OpenSSL, OpenClaw, Nix и ядре Linux"  +/
Сообщение от opennews (??), 10-Апр-26, 17:36 
Несколько выявленных за последние дни  опасных уязвимостей, большинство из которых можно эксплуатировать удалённо:...

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

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

Оглавление

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

1. Сообщение от Аноним (1), 10-Апр-26, 17:36   +3 +/
> 5 уязвимостей, выявленных в ходе экспериментов с инструментарием Claude Code

И это они ещё с мифосом не экспериментировали...

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

2. Сообщение от Аноним (2), 10-Апр-26, 17:39   +8 +/
> OpenClaw

https://days-since-openclaw-cve.com/

Days since last OpenClaw CVE - 0

A new CVE was published in the last 24 hours.
Because who needs security when you have vibes?

Best CVE-less streak - 12 days

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

3. Сообщение от Аноним (3), 10-Апр-26, 17:42   –5 +/
Ужас! Зачем нейронку для их выявления сделали?!
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #5

4. Сообщение от dannyD (?), 10-Апр-26, 17:55   +/
а представляете, когда-то это все будет работать без косяков и язв!
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #71, #84

5. Сообщение от Сладкая булочка (?), 10-Апр-26, 17:56   +/
Чтобы на раст не переписывать. Кстати, получается, что не выгодно. Если ошибок с памятью не будет, то кто будет менять деньги на токены. Думаю притормозят внедрение раста.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #3 Ответы: #11, #15, #68

7. Сообщение от Феникс123 (?), 10-Апр-26, 17:57   +/
Это все ИИ-шески понаходили?
Ответить | Правка | Наверх | Cообщить модератору

8. Сообщение от Сладкая булочка (?), 10-Апр-26, 17:58   +/
Интересно найдут ли ошибки в верифицированной библиотеке hacl*? Было бы инетересно.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #23, #45

9. Сообщение от 11009 (?), 10-Апр-26, 18:01   +1 +/
я так понимаю cups чинить уже некому? или нашли очередного беднягу за спасибо?
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #24

10. Сообщение от Аноним (11), 10-Апр-26, 18:05   –1 +/
> GStreamer - 11 уязвимостей: 3 переполнением буфера и 8 уязвимостей вызваны целочисленным переполнением или разыменованием нулевого указателя

Ну, Ж-стример всегда отличался какчственным кодом))

> CUPS - 8 уязвимостей, две могут использоваться для организации удалённого выполнения своего кода с правами root

Шикарно!
А ведь в нем уже находили подобную дырень.

> NixOS - Уязвимость даёт возможность перезаписать любой файл в системе ... с правами root. Проблема вызвана некорректным устранением уязвимости CVE-2024-27297 в 2024 году.

А как дышали, как дышали!

> В ядре Linux устранено 5 уязвимостей, выявленных в ходе экспериментов с инструментарием Claude Code

Даже дырявый опенклод находит уязвимости в ядре.

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

11. Сообщение от Аноним (11), 10-Апр-26, 18:08   –1 +/
Так во все эти проекты (особенно в ядро) каждый релиз добавляют 100500 строк нового кода.
И если бракоделы будут работать как диды, то такие проверки придется делать постоянно.

>Думаю притормозят внедрение раста.

Какой славный копиум)
Так уже в хроме больше чем 1.5 ляма строк раст кода, в андроиде больше 5 лямов.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #5 Ответы: #19

12. Сообщение от Аноним (12), 10-Апр-26, 18:09   +1 +/
А сколько уязвимостей может быть не опубликовано в массы а использовано "кем надо" и даже "кем не надо".
Ответить | Правка | Наверх | Cообщить модератору

13. Сообщение от Аноним (15), 10-Апр-26, 18:09   –1 +/
> помечена как неопасная так как она проявляется только на 32-разрядных платформах

Ха-ха-ха. Так их!

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

15. Сообщение от Аноним (15), 10-Апр-26, 18:12   +/
> Думаю притормозят внедрение раста.

И кто же, интересно, эти те кто притормозят?

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #5 Ответы: #17, #18

16. Сообщение от Аноним (16), 10-Апр-26, 18:12   +5 +/
> В ядре Linux устранено 5 уязвимостей,

nfsd - не проверили размер буфера и получили out-of-bounds write
io_uring - чтение за пределами буфера
ksmbd - конвертили unsigned 32 в signed int (как же хорошо что язык это делает неявно) и получили heap buffer overflow
- race condition

и futex забыли (или забили?) на проверить могут ли флаги не совпадать

В общем все как обычно))

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

17. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:15   +1 +/
>> Думаю притормозят внедрение раста.
> И кто же, интересно, эти те кто притормозят?

Те же, кто дают команду на внедрение.

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

18. Сообщение от Аноним (-), 10-Апр-26, 18:17   +/
ОНИ!

Судя по всему мысля такова:
- подобные проверки требуют много токенов
- умственноотсталые будут делать одни и те же уязвимости, как они делают c 1972 года
- поэтому проверки надо будет делать постоянно, желательно после каждого коммита
- следовательно компании предоставляющие ЫЫ инфраструктуру смогут заработать много денег

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15 Ответы: #20, #83

19. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:17   +2 +/
> такие проверки придется делать постоянно.

В этом и цель: деньги за токены. В итоге все счастливы.

>>Думаю притормозят внедрение раста.
> Какой славный копиум)
> Так уже в хроме больше чем 1.5 ляма строк раст кода, в
> андроиде больше 5 лямов.

Продолжайте вести наблюдение.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #11 Ответы: #21

20. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:20   +/
> Идея в общем-то имеет какую-то логику, но вопрос "а нафига это корпам
> которые код пишут" остается открытым.
> Не проще ли выкинуть на мороз тех, кто не осиливает новые технологии?

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


Ответить | Правка | Наверх | Cообщить модератору
Родитель: #18 Ответы: #22, #48, #57

21. Сообщение от Аноним (-), 10-Апр-26, 18:21   +1 +/
> В этом и цель: деньги за токены.

Цель кого?

> В итоге все счастливы.

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

> Продолжайте вести наблюдение.

Продолжаю.
Дырявые ЯП будут вытеснены на обочину истории.
Спасти ИИшка тут не поможет, так как устряняет симптомы, а не причину.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #19 Ответы: #25, #79

22. Сообщение от Аноним (-), 10-Апр-26, 18:24   +/
> Уязвимости были, есть и будут.

Вопрос в количестве.

> Никто не осиливает.

Вопрос так же в количестве)
На плохом языке ты можешь получить рут просто нажав backspace 28 раз.

> Писать низкоуровневый код сложно.

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

> Да даже без этого уязвимости будут, только другие.

Т.е мы избавимся от части уязвимостей? Ну так это отлично.

> А корпам выгодно иметь дешевых разработчиков.

А еще они любят срезать косты на других направлениях.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #20 Ответы: #27

23. Сообщение от Аноним (-), 10-Апр-26, 18:25    Скрыто ботом-модератором+/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8

24. Сообщение от Аноним (-), 10-Апр-26, 18:27   +/
Он используется в куче дистрибутивов линукс и даже в бсд.
Конечно Сообщество™ не может скинуться по копейке, чтобы нанять человека.
Как говорится: узрите силу Сообщества™

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

25. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:28   +/
>> В итоге все счастливы.
> Если корпе сказать "вам не надо тратить деньги на токены, нужно просто
> внедрить..." то значительная часть задумается.

На чем твоя уверенность, что на переписывание + создание новых уязвимостей тратится меньше денен?

>> Продолжайте вести наблюдение.
> Продолжаю.
> Дырявые ЯП будут вытеснены на обочину истории.
> Спасти ИИшка тут не поможет, так как устряняет симптомы, а не причину.

А причина в самой теории вычислимости. Можно только уменьшить симптомы, но проблемы никуда не уйдет.


Ответить | Правка | Наверх | Cообщить модератору
Родитель: #21 Ответы: #29

26. Сообщение от Аноним (26), 10-Апр-26, 18:30   +/
> Ну, Ж-стример всегда отличался какчственным кодом))

Я так понимаю, Гном так и не засунул в сендбокс эту индексирующую утилиту и оно до сих пор выполняет все скачанные файлы просто так?

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

27. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:31   –1 +/
>> Уязвимости были, есть и будут.
> Вопрос в количестве.

Про что речь? Про "безопасные языки"? Ну вот жс безопасный же. А сколько уязвимостей в npm находят. Вот и думай.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22 Ответы: #34

29. Сообщение от Аноним (29), 10-Апр-26, 18:45   +/
>>> Дырявые ЯП будут вытеснены на обочину истории.
>> Спасти ИИшка тут не поможет, так как устряняет симптомы, а не причину.
> А причина в самой теории вычислимости

Причина в теории? Ты сам-то хоть понял, что написал? 😂

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25 Ответы: #31, #33

30. Сообщение от Rev (ok), 10-Апр-26, 18:49   +1 +/
Вы всё врёти! Не может быть опенсорс таким дырявым! O_o
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #72, #73

31. Сообщение от Сладкая булочка (?), 10-Апр-26, 18:51   +/
>>>> Дырявые ЯП будут вытеснены на обочину истории.
>>> Спасти ИИшка тут не поможет, так как устряняет симптомы, а не причину.
>> А причина в самой теории вычислимости
> Причина в теории? Ты сам-то хоть понял, что написал? 😂

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #29 Ответы: #35, #37, #40, #44

32. Сообщение от Аноним (29), 10-Апр-26, 18:52   –1 +/
> В ядре Linux
> Уязвимость в драйвере NFS
> начиная с ядра 2.6.0 (2003 год).
> Claude Code

Ахаха! 23 года дырени, и нашлась она только благодаря ИИ.

Ну что, воины против ИИ, ваш выход! "Лже-ИИ бесполезен", говорили они. "Лже-ИИ ничего не пониает", говорили они. "Лже-ИИ разбирается только на том, на чем был натренирован", говорили они...

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

33. Сообщение от Аноним (40), 10-Апр-26, 18:53   +/
> Нет, причина дыр при работе с памятью - это именно дырявые языки.

дырява твоя модель памяти и архитектура Фон-как его там-Неймана!!!

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

34. Сообщение от Аноним (29), 10-Апр-26, 18:55   +/
> Ну вот жс безопасный же. А сколько уязвимостей в npm находят.

А сколько в npm находят уязвимостей типа buffer overflow и double free?

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #27 Ответы: #38

35. Сообщение от Аноним (35), 10-Апр-26, 18:55   +/
> Идеального алгоритма, гарантирующего поиск всех уязвимостей, не существует,

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

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

Ну, т.е раз современной пилой можно попасть по пальцу, то давайте махать каменным топором как диды?
Я правильно понял идею?


Ответить | Правка | Наверх | Cообщить модератору
Родитель: #31 Ответы: #42

37. Сообщение от Аноним (29), 10-Апр-26, 18:57   +/
> Идеального алгоритма, гарантирующего поиск всех уязвимостей, не существует

А никто и не говорит про все. Речь про проблемы работы с памятью.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #31 Ответы: #39

38. Сообщение от Аноним (35), 10-Апр-26, 18:59   +/
Ну шо ты начинаешь?! (с)

Тут тебя пытаются убедить что дырявый ЯП еще огого!
Надо не только обмазать овнокод санитайзарами, фаззерами, но и запускать регулярную ИИшку.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #34

39. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:02   +/
>> Идеального алгоритма, гарантирующего поиск всех уязвимостей, не существует
> А никто и не говорит про все. Речь про проблемы работы с
> памятью.

Про нее и речь. Ты можешь построить формальную модель, но в реальном мире (особенно низкоуровневом) придется из нее выходить, чтобы что-то сделать, поэтому есть unsafe в разных языках и прочие проблемы с асинхронным кодом.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #37 Ответы: #43, #51

40. Сообщение от Аноним (40), 10-Апр-26, 19:02   +/
> Попытка доказать правильность программы через верификацию часто сталкивается с алгоритмической неразрешимостью и решается различными допущениями.

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #31 Ответы: #47

41. Сообщение от Аноним (41), 10-Апр-26, 19:03   –1 +/
> В общем все как обычно))

Винда — зло?

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #16 Ответы: #62

42. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:04   +/
>> Попытка доказать правильность программы через верификацию часто сталкивается с алгоритмической неразрешимостью и решается различными допущениями.
> Ну, т.е раз современной пилой можно попасть по пальцу, то давайте махать
> каменным топором как диды?
> Я правильно понял идею?

Нет, ты сводишь все к волшебному инструменту, которого нет.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #35 Ответы: #80

43. Сообщение от Аноним (43), 10-Апр-26, 19:05   –1 +/
Есть большая разница "у тебя unsafe только в низкоуровневом коде" и "у тебя весь код unsafe и CVEшка может случиться даже при парсинге строки в UI".

Более того если у тебя каким-то образом помечены "стремные" места, то ИИшке будет гораздо легче.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #39 Ответы: #49

44. Сообщение от Аноним (29), 10-Апр-26, 19:06   –1 +/
> Попытка доказать правильность программы через верификацию часто сталкивается с алгоритмической неразрешимостью и решается различными допущениями.

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

Ты бы хоть посмотрел, как это работает в том же Ada/Spark, прежде чем умными словами бросаться. Допущениями решается, блждад...

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #31 Ответы: #52

45. Сообщение от Аноним (40), 10-Апр-26, 19:07   +/
тут уже спеку на анализ давать надо, а не код (имплементацию)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #8 Ответы: #78

46. Сообщение от Oe (?), 10-Апр-26, 19:08   +/
> обработке данных в форматах WAV

Прикалываются что ли? Метаданные WAV даже ардуина восьми битная читает

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

47. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:10   +/
>> Попытка доказать правильность программы через верификацию часто сталкивается с алгоритмической неразрешимостью и решается различными допущениями.
> зависит от области определения той или иной функции, "типы" как раз и
> есть те "ограничители" допустимых значений аргументов функций.

Посмотри формальную верификацию чего-либо околосистемного.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #40 Ответы: #53

48. Сообщение от Аноним (40), 10-Апр-26, 19:13   +/
> Писать низкоуровневый код сложно

нет, его писали на листе бумаги, это ваши современные зоопарки ISA привели к тому, что обычному студенту в лом читать 4000 страниц референс мануала по архитектуре ЦПУ, который через полгода будет выкинут на свалку, потому-что и ЦПУ проектирует такие же "дятлы" в угоду прибыли. Архитектура Фон-Неймана - кал!!!

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

49. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:14   +/
> Есть большая разница "у тебя unsafe только в низкоуровневом коде" и "у
> тебя весь код unsafe и CVEшка может случиться даже при парсинге
> строки в UI".
> Более того если у тебя каким-то образом помечены "стремные" места, то ИИшке
> будет гораздо легче.

Не будет, т.к. отустуствие ub в unsafe блоке - это допущение, которое не проверяется. Эти проверки уже идут в райнтайме (смотри miri и сколько багов он нашел в safe коде). Это как раз аналогично тому, что в формализме мы говорим "забей, тут все будет выполняться", а по факту оно не выполняется, например, из-за аппаратной ошибки, чем и пользуются экплуатации уязвимостей.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #43 Ответы: #56

50. Сообщение от Аноним (50), 10-Апр-26, 19:16   +/
Там, эээ, как следствие, формат проприетарный и в нём часто через обруч прыгать надо. Как видим, это умеют не только лишь все. Лично мне приходилось патчить туеву хучу софта, чтобы WAVE_FORMAT с fffe поддерживался, иначе файлы тупо не определялись. Показательно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #46

51. Сообщение от Аноним (29), 10-Апр-26, 19:18   +/
>>> поиск всех уязвимостей
>> Речь про проблемы работы с памятью.
> Про нее и речь.

Нет, ты только что пел буквально про "все уязвимости", а не только те, что вызваны работой с памятью. Ты прямо на лету переобуваешься, я смотрю.

> Ты можешь построить формальную модель, но в реальном мире (особенно низкоуровневом) придется из нее выходить, чтобы что-то сделать, поэтому есть unsafe

Главное, что за пределами unsafe в 95% остального кода этих проблем не будет.

> прочие проблемы с асинхронным кодом.

Давай поподробнее, что это за "проблемы с асинхронностью". Вот с учетом того, что одна из основных целей создания borrow checker была как раз решение всех проблем с асинхронным/многопоточным кодом, а не просто "память не ронять".

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #39 Ответы: #54

52. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:19   +/
>> Попытка доказать правильность программы через верификацию часто сталкивается с алгоритмической неразрешимостью и решается различными допущениями.
> Ты не понимаешь, что несешь. При формальной верификации кода для каждой функции,
> ее аргументов и их типов жестко задаются пред/пост-условия и инварианты, и
> если они отсутствуют или не полны, то верификатор просто откажется дать
> тебе ответ.

Ну дак это искусственные условия. На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать.

> Ты бы хоть посмотрел, как это работает в том же Ada/Spark, прежде
> чем умными словами бросаться. Допущениями решается, блждад...

Покажи мне на ada/spark формально верифицированный аллокатор, например.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #44 Ответы: #64, #65

53. Сообщение от Аноним (40), 10-Апр-26, 19:23   +/
> Посмотри формальную верификацию чего-либо околосистемного.

Допустим шедуллер процессов, ввода-вывода, и т.д. и что? Сложно это верифицировать? Думаю даже на оборот, у таких систем строго должна быть описана спека, и всякая имплементация должна быть верифицирована. Не вижу проблемы. Перед тем как писать код какого-либо шедуллера, необходимо написать теоретическую (научную) статью описывающий алгоритм, доказать его корректность и т.д., написать строгую спецификацию с приложениями по имплементации, и только после всего этого писать имплементацию (кодировать), которую собственно потом необходимо верифицировать. А в реальности что? - "я у мамы погромист" или "бабушка, я не нах*р"! :)

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #47 Ответы: #55

54. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:24   –1 +/
>>>> поиск всех уязвимостей
>>> Речь про проблемы работы с памятью.
>> Про нее и речь.
> Нет, ты только что пел буквально про "все уязвимости", а не только
> те, что вызваны работой с памятью. Ты прямо на лету переобуваешься,
> я смотрю.

Очередной дешевый тролинг с обвинениями? Продолжать не буду.

>> Ты можешь построить формальную модель, но в реальном мире (особенно низкоуровневом) придется из нее выходить, чтобы что-то сделать, поэтому есть unsafe
> Главное, что за пределами unsafe в 95% остального кода этих проблем не
> будет.

Главное не забывать это повторять перед сном.

>> прочие проблемы с асинхронным кодом.
> Давай поподробнее, что это за "проблемы с асинхронностью". Вот с учетом того,
> что одна из основных целей создания borrow checker была как раз
> решение всех проблем с асинхронным/многопоточным кодом, а не просто "память не
> ронять".

Видно, что дальше рекламных буклетов раста ты не смортел. Штош, это было сразу понятно.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #51 Ответы: #58

55. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:25   +/
>> Посмотри формальную верификацию чего-либо околосистемного.
> Допустим шедуллер процессов, ввода-вывода, и т.д. и что? Сложно это верифицировать? Думаю даже на оборот

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


Ответить | Правка | Наверх | Cообщить модератору
Родитель: #53 Ответы: #60, #67

56. Сообщение от Аноним (29), 10-Апр-26, 19:25   +/
>> Более того если у тебя каким-то образом помечены "стремные" места, то ИИшке будет гораздо легче.
> Не будет, т.к. отустуствие ub в unsafe блоке - это допущение, которое не проверяется

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

> например, из-за аппаратной ошибки

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #49 Ответы: #59

57. Сообщение от Аноним (57), 10-Апр-26, 19:27   +/
> уязвимости будут, только другие

Да и слава богу, может те другие будет проще выловить. А если и нет, то всяко интереснее, чем по одним и тем же граблям 50 лет.

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

58. Сообщение от Аноним (29), 10-Апр-26, 19:30   +/
>> Нет, ты только что пел буквально про "все уязвимости", а не только те, что вызваны работой с памятью. Ты прямо на лету переобуваешься, я смотрю.
> Очередной дешевый тролинг с обвинениями?

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

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

Какая ирония...

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #54 Ответы: #61

59. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:31   +/
>>> Более того если у тебя каким-то образом помечены "стремные" места, то ИИшке будет гораздо легче.
>> Не будет, т.к. отустуствие ub в unsafe блоке - это допущение, которое не проверяется
> Конечно будет, потому что количество небезопасного кода сокращается в десятки раз по
> сравнению с изначальными 100% сишочной лапши. Не говоря уж о том,
> что вся хитроумная логика и асинхронщина находятся за пределами unsafe.

У тебя любой примитив синхронизации будет с unsafe внутри.  

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

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

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #56 Ответы: #66

60. Сообщение от Аноним (29), 10-Апр-26, 19:32    Скрыто ботом-модератором+/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #55 Ответы: #63

61. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:34   +/
>>> Нет, ты только что пел буквально про "все уязвимости", а не только те, что вызваны работой с памятью. Ты прямо на лету переобуваешься, я смотрю.
>> Очередной дешевый тролинг с обвинениями?
> Нет, просто констатация того факта, что ты переобуваешься на лету и (как
> теперь очевидно) не в состоянии отвечать за свои собственные слова.

У тебя всегда тролинг строится по одной схеме? Мой тебе совет: пора что-то менять, палишься.

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

62. Сообщение от Аноним (62), 10-Апр-26, 19:34   +/
Да
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #41

63. Сообщение от Сладкая булочка (?), 10-Апр-26, 19:37    Скрыто ботом-модератором–1 +/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #60

64. Сообщение от Аноним (29), 10-Апр-26, 19:38   –2 +/
> Ну дак это искусственные условия. На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать.

Это как раз не исукственные условия - это условия, которые ты контролируешь на уровне алгоритма. Все поведение за пределами алгоритма (например, сломанное железо) к самому алгоритму и его реализации в коде отношения не имеет, и, соответсвенно, чисто физически не сожет быть математически верифицируемым.

Это как бы очевидно, не?

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #52 Ответы: #77

65. Сообщение от Аноним (40), 10-Апр-26, 19:46   –1 +/
> Ну дак это искусственные условия. На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать.

Так и есть, но это ведь не самообман, вы говорите за формальную верификацию как за самообман, тоже самое можно сказать про всю математику, где есть допущения, аксиомы и другие "неловкие" моменты, и все сведется к тому, а что есть собственно понятие - "доказать" (формально доказать). Брауэр вообще не признавал доказательства от противного :)

Вот seL4 описали эти моменты:

//sel4.systems/Verification/proofs.html

//sel4.systems/Verification/implications.html

//sel4.systems/Verification/assumptions.html

А вот тут про ironclad-os:

//ironclad-os.org/formalverification.html

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #52 Ответы: #75

66. Сообщение от Аноним (29), 10-Апр-26, 19:47   –2 +/
>>  что вся хитроумная логика и асинхронщина находятся за пределами unsafe.
> У тебя любой примитив синхронизации будет с unsafe внутри.

А вся логика снаружи - нет. Об этом как бы и речь.

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

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

Заканчивай чушь нести.

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

67. Сообщение от Аноним (40), 10-Апр-26, 19:48    Скрыто ботом-модератором–1 +/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #55 Ответы: #74

68. Сообщение от Аноним (29), 10-Апр-26, 19:51   +/
> Если ошибок с памятью не будет, то кто будет менять деньги на токены.
> Думаю притормозят внедрение раста.

Не притормозят, а наоборот: закупятся токенами и с помощью ИИ перепишут на Раст еще быстрее.

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

69. Сообщение от Аноним (69), 10-Апр-26, 19:52   +/
Ахаха... Что-то пилят, всё допилить не могут!
Ответить | Правка | Наверх | Cообщить модератору

70. Сообщение от Аноним (70), 10-Апр-26, 20:16   +/
Это ещё даже Алису не попробовали
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

71. Сообщение от Аноним (71), 10-Апр-26, 20:37   +/
Никогда не будет. Появятся новые типы уязвимостей, и новые способы защиты от них. Война щита и меча. С ростом мощи искусственного интеллекта люди перестанут в своей массе понимать его выводы, но будут всё больше и больше слепо на него полагаться. Это уже происходит, но это лишь начало. Постепенно даже те, кто будут пытаться его понять, смогут иметь лишь набор возможных интерпретаций относительного того, что он мог бы иметь в виду. В новой форме воскреснут такие средневековые дисциплины, как герменевтика, экзегетика и схоластика, но уже применительно к его отровениям.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #4 Ответы: #76

72. Сообщение от 1 (??), 10-Апр-26, 20:42   +/
все в этом мире гораздо дырявее чем мы думаем!!!

весь мир -- дыра!!!)))

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

73. Сообщение от Аноним (73), 10-Апр-26, 20:47   +/
На Си только илита пишет, они не ошибаются! 12yoexpert не даст соврать!
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #30

74. Сообщение от Сладкая булочка (?), 10-Апр-26, 20:52   +/
>> Найди и покажи такую верификацию
> Вот
> //sel4.systems/Verification/proofs.html
> //sel4.systems/Verification/implications.html
> //sel4.systems/Verification/assumptions.html

А внутрь ты смотрел?

Доказывают они, на самом деле, свойства урезанной статичной версии ядра https://github.com/seL4/l4v/blob/59b2d2f630119be823f3f444651...

> This specification is a cut-down version of the seL4 abstract specification
> that removes all system calls apart from notifications. The resulting kernel
> is a classic static separation kernel without any dynamism.
>
> A proof that seL4 is equivalent to this cut-down version if configured
> appropriately can be found in the `proof` directory under
> [`bisim`](../../proof/bisim/).

Переходим https://github.com/seL4/l4v/tree/59b2d2f630119be823f3f444651... и читаем

> This proof establishes that seL4, if configured fully statically with 1-level CSpaces and notification caps only, is bi-similar to a static separation kernel that has no other system calls than signalling notifications.

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

При этом надежность микроядерной архитектуры надежная, никто не спорит.

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

75. Сообщение от Сладкая булочка (?), 10-Апр-26, 20:53   +/
>[оверквотинг удален]
> верификацию как за самообман, тоже самое можно сказать про всю математику,
> где есть допущения, аксиомы и другие "неловкие" моменты, и все сведется
> к тому, а что есть собственно понятие - "доказать" (формально доказать).
> Брауэр вообще не признавал доказательства от противного :)
> Вот seL4 описали эти моменты:
> //sel4.systems/Verification/proofs.html
> //sel4.systems/Verification/implications.html
> //sel4.systems/Verification/assumptions.html
> А вот тут про ironclad-os:
> //ironclad-os.org/formalverification.html

Ответил здесь https://www.opennet.me/openforum/vsluhforumID3/139772.html#74

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

76. Сообщение от dannyD (?), 10-Апр-26, 20:56   +/
1. все это описанно в книжке Пети Ж.-П. "О чем размышляют роботы?" советское издание 1987 год, оригинал 1982 год.

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

2. Проблематика "современной" математики, широкой публике непонятна уже более тысячи лет.
и что?

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

77. Сообщение от Сладкая булочка (?), 10-Апр-26, 20:56   +/
>> Ну дак это искусственные условия. На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать.
> Это как раз не исукственные условия - это условия, которые ты контролируешь
> на уровне алгоритма. Все поведение за пределами алгоритма (например, сломанное железо)
> к самому алгоритму и его реализации в коде отношения не имеет,
> и, соответсвенно, чисто физически не сожет быть математически верифицируемым.
> Это как бы очевидно, не?

Нет. Это выставление условий модели удобных для доказательства. В sel4 доказывают не про исходник, а про модель на haskell, доказывают не полные свойства, а некоторые урезанные варианты, в урезанных конфигурациях.

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

78. Сообщение от Сладкая булочка (?), 10-Апр-26, 21:04   +/
> тут уже спеку на анализ давать надо, а не код (имплементацию)

ЕМНИП они заверяли, что там верифицирована работа с памятью. Почему бы не попробовать найти вулны в генерированном си коде?

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

79. Сообщение от Аноним83 (?), 10-Апр-26, 21:15   +/
Да да, "The RUST crowd" :)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #21 Ответы: #82

80. Сообщение от Аноним (80), 10-Апр-26, 21:15   +/
> Нет, ты сводишь все

Что "все"?

> к волшебному инструменту, которого нет.

Ты кажется невнимательно читала.
Волшебного инструмента не существует.
Есть развитие инструмента - то что мы наблюдаем всю историю человечества.

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

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

81. Сообщение от Аноним (81), 10-Апр-26, 21:17   +/
Язык Rust не защищает от утечек памяти. Язык Argentum защищает.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #85

82. Сообщение от Аноним (80), 10-Апр-26, 21:18    Скрыто ботом-модератором+/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #79

83. Сообщение от Аноним83 (?), 10-Апр-26, 21:18   +/
Не надо свои заскоки на других переносить.

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

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

84. Сообщение от Аноним83 (?), 10-Апр-26, 21:21   +/
Оно уже работает лет 5-10 без косяков.
Падения на цельных данных пролечили, сейчас на всяких специально повреждённых только иногда падает - что вообще никак не мешается в каждодневной работе.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #4

85. Сообщение от Аноним (50), 10-Апр-26, 21:23   +/
Ada получше будет. А потом формально верифицированный код транслируешь в си и всё норм. Нвидия не даст соврать.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #81


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

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




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

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