The OpenNET Project / Index page

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



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

Оглавление

Проблемы из-за подготовленных AI-инструментами отчётов об уязвимостях, opennews (??), 05-Янв-24, (0) [смотреть все]

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


40. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +1 +/
Сообщение от Витюшка (?), 06-Янв-24, 00:18 
Для формальной верификации кода микроядра L4 в 5000 строк кода на С (или как-то так) было написано 200 000 строк кода верификации.

Уж не знаю, все ли они были написаны вручную или там что-то генерируется.

Но в общем удачи тебе)

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

45. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от Аноним (103), 06-Янв-24, 00:39 
> Но в общем удачи тебе)

Он и так удачлив. Это не ему формально верифицировать чей-то код.
Его долг — лежать на диване и объяснять другим, как правильно делать.

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

127. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +1 +/
Сообщение от _ (??), 06-Янв-24, 21:54 
>лежать на диване и объяснять другим, как правильно делать.

Да он лошара! Для этого AI-ботов и придумали! Теперь уже моно просто лежать на диване и _ничего_ не делать! Светлое будущее наступило! :)

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

59. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от Витюшка (?), 06-Янв-24, 02:36 
Добавляю. Написана верификация на языке Isabelle/HOL.

https://github.com/seL4/l4v

Files 2436
Lines 1336767
Blanks 114572
Comments 36636
Lines of Code 1185559

Те 1.2 млн сгенерированного кода доказательств.

Кода доказательств (руками людьми) там 15000 на 8700 строк кода С.

Те на каждую строчку кода 2 строчки кода формальной верификации.

Трудозатраты - 20 человеко-лет на верификацию (суммарно, включая автоматизацию доказательств, фреймворки, библиотеки и т.п.), 11 человеко-лет чисто на доказательство.

Итого, 5 строчек кода в день на С (полный рабочий день) можно верифицировать.

Или в 50-100 раз меньше (медленнее) чем пишет программист кода на С.

Срочно всем верифицировать!


            

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

62. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от Аноньимъ (ok), 06-Янв-24, 03:18 
А могли бы сразу на АДЕ писать и не мучиться.
Ответить | Правка | Наверх | Cообщить модератору

128. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  –1 +/
Сообщение от _ (??), 06-Янв-24, 21:58 
Ariane 5, Ariane 5, Ariane 5 ! Это комарик такой :-)))

Но таки да - еЯ угробила полностью верифицированная Ada :) а это вам не дыряшковый Си какой нить! :)

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

135. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от Аноньимъ (ok), 07-Янв-24, 02:57 
Все ошибки сертифицированы и верифицированы.

Но два раза писать одну программу ненужно.

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

95. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +1 +/
Сообщение от Аноним (-), 06-Янв-24, 10:41 
> Те 1.2 млн сгенерированного кода доказательств.

А это счастье кто-то верифицировал? И не окажется так что в верификаторе - баги были? :)

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

129. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от _ (??), 06-Янв-24, 22:00 
Quis custodiet ipsos custodes?!
Классико :)
Ответить | Правка | Наверх | Cообщить модератору

131. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +1 +/
Сообщение от Витюшка (?), 06-Янв-24, 22:09 
Это хороший вопрос. Они верифицировали и саму корректность соответствия программы С кодом и их формальной моделью, и ещё что-то там с компилятором.

Те, в целом да. Понятия не имею как. Я посмотрел код - это такая жесть. Как там что-то можно понять и верифицировать и не наделать багов? Хуже ассемблера.

У них есть кое какие предложения. Скорее всего что сам Isabelle работает корректно. Но я думаю он сам был проверен раньше.

И что железо тоже работает корректно (не знаю что это значит).

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

142. "Проблемы из-за подготовленных AI-инструментами отчётов об уя..."  +/
Сообщение от Прохожий (??), 08-Янв-24, 02:48 
Похоже, ты - не читатель. А человек же специально оговорку сделал "критический для безопасности софт".
Ответить | Правка | К родителю #59 | Наверх | Cообщить модератору

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

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




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

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