https://www.opennet.ru/openforum/vsluhforumID3/73545.html Тэо де Раадт (Theo de Raadt), лидер проекта OpenBSD, обобщил (http://permalink.gmane.org/gmane.os.openbsd.tech/22727) информацию, связанную с высказанными (http://www.opennet.ru/opennews/art.shtml?num=28998) на прошлой неделе опасениями по поводу возможности интеграции бэкдора в IPSEC-стек OpenBSD. По мнению Тэо, десять лет назад ФБД была особенно заинтересована в получении контроля над реализацией криптографических систем и компания NETSEC, выполнявшая правительственные контракты, вполне могла получить заказ на разработку и внедрение бэкдора. Но пока не обнаружено никаких фактов, указывающих на то, что бэкдор был внедрен в дерево исходных текстов OpenBSD. Наиболее вероятно, что бэкдор был интегрирован в выпускаемые NETSEC продукты на основе OpenBSD. <br><br><br>В данном вопросе пока остается слишком много пробелов и неточностей, окончательно об отсутствии закладок в коде OpenBSD может будет говорить только после проведения полного аудита. Проведенный за неделю беглый аудит выявил несколько несущественных проблем, н https://www.opennet.ru/openforum/vsluhforumID3/73545.html#63 Sun, 26 Dec 2010 17:45:41 GMT &gt; &lt;...&gt; Но давайте я напомню, с чего начался наш с вами разговор?<br>&gt;<br>&gt; "Хотя на самом деле "на данном этапе развития средств анализа", и даже еще гораздо раньше, существуют уже достаточно методов организации кода таким образом, чтобы было возможно доказывать его правильность с помощью автоматизированных средств доказательств и анализа."<br>&gt;<br>&gt; Так вот, хотя методы организации кода существуют, но речь-то изначально шла о конкретике: стек IPSec в ядре OpenBSD. Вы как будто не заметили этого.<br>&gt;<br>&gt;То есть фактически вы предлагаете переписать стек IPSec заново. Но какое отношение это будет иметь к верификации текущего стека?! То, что вы предлагаете, это НЕ обеспечение верификации имеющегося кода. Это требование написания НОВОГО кода. По новым правилам.<br>&gt;<br>&gt; Повторюсь, вы сами изначально перепутали решение одной конкретной задачи (верификация кода IPSec-стека OpenBSD) с другой (создание системы для написания кода, позволяющей писать автоматически или хотя бы автоматизированно доказываемые программы).<br><br>Нет, я нич https://www.opennet.ru/openforum/vsluhforumID3/73545.html#62 Sat, 25 Dec 2010 19:14:57 GMT &gt;&gt; Проще? То есть, по-вашему, описание целевой семантики &#8212; это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как &#8212; поделитесь секретом?<br>&gt; Простой в данном случае является не описание семантики, а взаимосвязь отдельных систем. <br>&gt; Где модуль (система), отвечающий за конкретную семантику, рассматривается как отдельный <br>&gt; компонент.<br><br>В том-то и дело, что когда мы начинаем говорить о корректности работы программы, то в полный рост встаёт проблема проверки связей между модулями. Полная корректность &#8212; это далеко не только &#171;этот параметр не должен быть меньше десяти&#187;. Такие проблемы действительно ловятся на том же уровне анализа, что работают современные оптимизаторы кода. Но это ни разу не доказательство корректности программы. Возьмите молоко, солёные огурцы и селёдку &#8212; все высочайшего качества &#8212; и совместите их в своём желудке. Каждый отдельный продукт (модуль) сам по себе в порядке https://www.opennet.ru/openforum/vsluhforumID3/73545.html#61 Sat, 25 Dec 2010 11:49:01 GMT &gt; О каком именно осадке идет речь?<br>&gt; кто то вбросил, провели аудит, ничего не нашли. Все довольны, да еще <br>&gt; и баги исправили <br><br>О таком, что в любом случае многие теперь будут думать, что не закладок нет, а аудит плохо проведён. А можно пойти ещё дальше - найдены только специально оставленные на виду закладки, а настоящие не найдут.<br> https://www.opennet.ru/openforum/vsluhforumID3/73545.html#60 Sat, 25 Dec 2010 08:57:59 GMT О каком именно осадке идет речь?<br>кто то вбросил, провели аудит, ничего не нашли. Все довольны, да еще и баги исправили <br> https://www.opennet.ru/openforum/vsluhforumID3/73545.html#59 Sat, 25 Dec 2010 08:03:19 GMT &gt; Проще? То есть, по-вашему, описание целевой семантики &#8212; это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как &#8212; поделитесь секретом?<br><br>Простой в данном случае является не описание семантики, а взаимосвязь отдельных систем. Где модуль (система), отвечающий за конкретную семантику, рассматривается как отдельный компонент.<br><br>Вы пока что к сожалению демонстрируете отсутствие системного мышления, когда у вас все детали перемешаны в кучу на одном уровне.<br><br>Хотя если говорить в общем, все сложные вещи состоят из простых. И если не удается сложное разложить на простое, то вообще о каком анализе может идти речь?<br><br>&gt; Гениально! (кстати, я говорил об этом тоже, не знаю, почему вы мне мои же мысли тыкаете) Вот только если бы вы ещё и думали... Во-первых, строить такой верификатор (писать синтаксические средства, библиотеки, организовывать нужным образом код и т.д.) вы на чём будете? На обычных синтаксических средства https://www.opennet.ru/openforum/vsluhforumID3/73545.html#58 Sat, 25 Dec 2010 05:15:24 GMT &gt;Существует множество способов, как это могло бы быть сделано, от простых и очевидных до еле уловимых и изощренных. Возможно создать что-то, что выглядит как простая ошибка в коде и назначение которой будет невозможно доказать.<br><br>Приятно послушать умного человека. Вообще то и правда интересно сколько постоянно обнаруживаемых уязвимостей в софте случайных, а сколько умышлено сделано.<br> https://www.opennet.ru/openforum/vsluhforumID3/73545.html#57 Fri, 24 Dec 2010 22:51:59 GMT &gt;&gt; Оптимизация кода делается, во-первых, без учёта семантики. Это у автора в голове уже есть какая-то картинка &#171;как надо&#187;, и корректность программы однозначно определяется соответствием этой картинке. Но верификатор-то этой картинки не имеет! Её ему надо как-то ввести. Выстроить модель и связать с терминами, используемыми в программе. Это едва ли не больший объём работы по сравнению с собственно программой. И там тоже будут ошибки...<br>&gt; Оптимизатор работает на уровне семантики потока исполнения и прочих семантик, необходимых <br>&gt; для оптимизации. Да, не на уровне целевой семантики. Ну и?<br>&gt; Поменяйте семантику, по которой работает оптимизатор на целевую семантику, и вы получите <br>&gt; примерно те же срества в другой области приложения.<br>&gt; Мыслите проще.<br><br>Проще? То есть, по-вашему, описание целевой семантики &#8212; это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как &#8212; поделитесь секретом?<br><br>&gt;&gt; Во-вторых, о https://www.opennet.ru/openforum/vsluhforumID3/73545.html#56 Fri, 24 Dec 2010 21:58:40 GMT &gt; В 17-м? А может раньше?<br><br>Может даже и раньше. И что?<br><br>&gt; У вас странные, если не сказать - глупые, аналогии. Да - в штатах - англо-американское право и, в отличии от, оно работает. И, в отличии от, это создаст прецедент.<br><br>Создаст? Т.е. по-вашему еще не создало? Целый один прецедент?<br>И по-вашему именно само право "создает прецеденты"?<br><br>&gt; Вплоть до курьёзов http://www.google.com/search?q=американское+забавные+законы<br><br>Я уже понял давно, что вы знания о праве получили, немного погуглив по теме. А теперь вы это еще и подтвердили. Только надо ведь еще понимать то, что вы читаете. А то так и не продвинетесь дальше "забавных законов".<br><br>&gt; Впрочем все вышеответившие мне лично (непонятно, почему такой ажиотаж) частично правы.<br>&gt; Штаты, таки да - стали полицейским государством (страной уже язык не поворачивается назвать).<br><br>На этот раз интересно, чем в вашем понимании государство отличается от страны?<br>И что по-вашему мешает Штатам считаться страной, пусть даже полицейской?<br><br>И притом, что у вас Штаты "страно https://www.opennet.ru/openforum/vsluhforumID3/73545.html#55 Fri, 24 Dec 2010 21:11:37 GMT &gt;&gt; Вот вы и ответьте по существу, что вы имели в виду под "неримским правом".<br>&gt;<br>&gt; С Луны или Альдебарана? Англо-американское право, включает прецеденты.<br><br>Римское право тоже включает прецеденты. Ну и?<br>И что же все-таки означала ваша фраза:<br>&gt; Люди судятся и за меньшее. Неримское право, знаете ли :)<br><br>Вы хотели сказать, что по-вашему в соответствии с Римским правом за меньшее чем над ФБР судиться было нельзя, и только по "неримскому праву" по-вашему значит можно. Так что ли?<br><br>У вас явное стремление казаться компетентным в областях, в которых вы не разбираетесь, при помощи поверхностного гугления и туманных намеков с использованием где-то прочитанных вами словечек. В надежде что вам задним числом можно будет истолковать ваши намеки как угодно с помощью дополнительного гуления.<br><br>&gt; Это ваши домыслы, непонятно почему вы их мне приписываете. Выйдите уже наконец из виртуала.<br><br>На этот раз было бы интересно узнать, что именно вы считате "виртуалом", общаясь при этом на форумах.<br><br>М-да, с вашими "про100 мастер