The OpenNET Project / Index page

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



Индекс форумов
Составление сообщения

Исходное сообщение
"Rust включён в число основных языков для разработки платформ..."
Отправлено Ordu, 11-Апр-21 13:14 
>> Продолжай накладывать заплатку поверх заплатки
> Никто бездумно заплатки на дыры не накладывал. Или поведение ядра приводилось в
> соответствии стандарту POSIX или уязвимости групировались в классы и разрабатывалась одна
> техника защиты от целого класа уязвимостей.

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

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

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

Ты не слышал про wuffs[1]? Язык, который видя a[i], пытается доказать, что i не выйдет за границы массива, и если ему это не удаётся, выкидывает ошибку компиляции. Мне очень понравилась идея. То есть ты пишешь a[i], и если компилятор не смог доказать, то надо добавить if(i < 0 || i > a.len()) { return Error } перед индексацией, после этого компилятор сможет доказать. Это, кстати, в некотором смысле подход противоположный rust'у: в расте стандартная библиотека принудительно втыкает проверки, и если компилятор потом может доказать, что они не нужны, он их удаляет. Не может, не удаляет. wuffs даёт больше контроля программисту, при этом заставляя его доказывать, что проверка не нужна, если тот хочет от неё избавиться.

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

[1] https://github.com/google/wuffs

 

Ваше сообщение
Имя*:
EMail:
Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email).
Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
  Введите код, изображенный на картинке: КОД
 
При общении не допускается: неуважительное отношение к собеседнику, хамство, унизительное обращение, ненормативная лексика, переход на личности, агрессивное поведение, обесценивание собеседника, провоцирование флейма голословными и заведомо ложными заявлениями. Не отвечайте на сообщения, явно нарушающие правила - удаляются не только сами нарушения, но и все ответы на них. Лог модерирования.



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

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