Действительно открытые веб-фреймворки настолько небезопасны?

Причем, начни уже с самого начала: http://marc.info/?l=openbsd-misc&m=118296441702631

Этот минимум — теоретически недостижимый предел. В случае решения недопоставленной задачи при помощи неавтоматизируемых средств (программистов) нет никаких аргументированно уменьшающих число ошибок средств.

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

Вот только стоимость такой поделки будет астрономическая, и сроки разработки - тоже.

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

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

Конечно нет. Недоказанные практики, которые помогали трём с половиной анонимусам, слова которых в последний раз пытались проверять статистическим анализом эдак в 85 году (ну ладно, в 95 если считать проверку на которую я дал ссылку в прошлом сообщении — корректной), как-то не внушают мне достаточно уверенности.

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

Требования типа «работать без переполнения буферов» формализуются достаточно просто, чтобы надеяться на корректность в этой части; вплоть до готовности отвечать яйцами после того, как будет проведено тщательное тестирование. Нетривиальные бизнес-сценарии могут быть формализованы не вполне верно, да - согласен, тут проблема.

математическое доказательство не содержало ошибок интерпретации (вы ведь доказываете про модель, а не реальный код на реальном железе?)

Про машинный код.

а системы верификации никогда не ошибаются

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

вы ведь доказываете про модель

Да, про модель ЭВМ. Доказать, что ЭВМ соответствует модели - отдельное, презабавнейшее занятие для разработчиков аппаратуры :D

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

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

Требования типа «работать без переполнения буферов» формализуются достаточно просто, чтобы надеяться на корректность в этой части

Ты, конечно, про динамические проверки, а не статические. Для надежных статических проверок надо иметь статическую систему проверки зависимых типов (а такие системы упираются в проблему останова). С динамическими проверками всё проще, но они значат только то, что при вызове «five_elements_array[6] = 12» в программе вызовется исключение/завершение программы с ошибкой, вместо того, чтобы засрать чужую память.

В системах автоматического доказательства теорем периодически тоже находят ошибки

Между поиском доказательства и проверкой доказательства - огромная пропасть. Первое несравнимо сложнее.

а доказательства великих теорем проверяются топовыми математиками по два года

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

Ты, конечно, про динамические проверки, а не статические.

Это уже от требований зависит. Можно и про статические.

Для надежных статических проверок надо иметь статическую систему проверки зависимых типов (а такие системы упираются в проблему останова).

В общем случае - упираются. А в частном случае - пиши свою программу так, чтобы не уперлось.

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

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

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

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

И сколько лет мне придётся потратить на изобретение структуризации математического знания

Изобретено уже. http://www.reflexion.ru/club/16-04-09Beklemishev.pdf

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

Как вариант. Лишь бы формально удовлетворить формальным требованиям.

Изобретено уже. http://www.reflexion.ru/club/16-04-09Beklemishev.pdf

Сам ты, как я понимаю, не открывал презенташку?

Формализм ZFC и PA … плохо приспособлен к нуждам реальной формализации математики.
развёрнутая запись числа 1 в формальной теории множеств содержит 4 523 659 424 929 символов

Замечательно. Это получается 4 терабайта на одно число. А ведь ими ещё и ворочать надо. И ведь при этом:

Абсолютной надёжности не гарантирует ни один прувер.

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

Лишь бы формально удовлетворить формальным требованиям

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

а причем здесь потребление проца и 12309? Если нет замираний мышки, зависаний, невозможности нормального ввода данных с устройств ввода - это НЕ 12309. Высокая нагрузка проца при fsck ни о чем не говорит

Сам ты, как я понимаю, не открывал презенташку?

Открывал.

развёрнутая запись числа 1 в формальной теории множеств содержит 4 523 659 424 929 символов

Пфф. Во-первых, вовсе не обязательно всегда манипулировать развернутой записью. Во-вторых, вот тебе работа, на которую дается ссылка: http://personnel.univ-reunion.fr/ardm/inefff.pdf

If one seeks an ad hoc definition of the number 1 in Bourbaki's dialect of set theory, a shorter one — perhaps the shortest ? — would be. τZ (∃x(x ∈ Z et ∀y(y ∈ Z =⇒ y = x))), which runs to 176 symbols

Абсолютной надёжности не гарантирует ни один прувер.

Нам не прувер нужен, а верификатор.

Только вот не все формальные задачи можно уложить в такие формальные решения.

Думаю, это вопрос трудозатрат. Совершенно невменяемых, к сожалению.

Большинство библиотек на безопасность не влияют. Те, которые влияют, обычно вполне вылизаны. Проблема высосана из пальца.

Высокая нагрузка на проц при IOWAIT (я уже в который раз обращаю внимание: _WAIT_, акула тебе в печень! Не _RUN_!) это 12309. Просто на первых порах а) два ядра были редкостью, б) шедулеры были в еще более плачевном состоянии, чем сейчас. В итоге: простаивающие в основном на десктопах со второе по последнее ядра позволяют нормально рендерить графические отклики на действия пользователя, а в шедулеры напихали костылей, дабы не лечить этот говнокод. Однако, нагрузку во время простоя системы так и не вылечили. И, самое печальное, никто даже не может толком объяснить, какого хрена происходит. Однако, на серверах, а данный розовый чатик просто кишит лжецами и девственниками, с соплями на губах кричащими, что сабжевая ось - тех бест фор сёваз, ситуация совсем другая. Там каждый такт на счету. Просранное на «форматирование дискетки» зеоновское вычислительное ядро (даже одно из 32-64х) - это лютейший звиздец, какого может ожидать хайлоад.

> или использовать ПО вендоров несущих какую либо ответственность за свои ошибки (никаких AS IS, NO WARRANTY?).

Пример такого продукта в студию.

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

Эти все баги есть недосмотр разработчиков.

А ссылки на баги это такое хитрое подтверждение вашей правоты?

нагрузка на проц может быть ЛЮБОЙ при 12309. У меня top на проблемной машине говорит 80% idle, а тем не менее всё становится в позу речного омара когда идет копирование с флешки. Проблема гораздо более глубока, нежели думаешь ты или я. Не, возможно я ошибаюсь и ты знаешь больше(возможно даже являешься разработчиком ядра), тогда я умываю руки... В противном случае наш с тобой спор - как пердение в лужу, причем с обоих сторон...