Выявлена дыра, позволяющая «уронить» компьютер с Linux под любым пользователем

> запусти while(true) {} и убедись, насколько автомат конечный.

Хм, странно, а mclaudt так хорошо о тебе отзывался.. Прежде чем отправить тебя изучать матчасть, дам подсказку: «конечный» в названии «конечный автомат» означает, что он имеет ограниченное число возможных состояний. А вовсе не то, что он обязан рано или поздно «завершиться» (придти в какой-нибудь final state). Более того, у конкретного FSM никакого final state может в принципе не существовать.

> Давай-ка я перескажу тебе историю про америку.

Начали за здравие, закончили за упокой. Сначала речь шла о posix, а сейчас внезапно вылез человеческий фактор. Предлагаю убить всех человеков, да.

Там ковбои, долбанутые на всю голову.

Всё, я понял ваше видение: все дебилы.

> Тогда причем тут Гедель?

Я выше ссылку приводил. Доказательство Тьюринга - всего лишь частный случай неполноты такой формальной арифметики, как теория алгоритмов.

Что-то неладное творится вокруг линукс.

Напомнило "...МОЛЧИТ НАРУШАЕТ ГОМОЕОПАТИЧЕСКОЕ МИРОЗДАНИЕ...".

Ааа. Нечего делать, придется ставить Windows 7!

>В линуксе даже дыры нормально сделать не могут.

Да, не говори! Вирусы с комплектом зависимостей и толстым мануалом идут, запускаются самим пользователем, да ещё и спрашивают: «вы действительно хотите запустить». Эксплойты компилировать надо. И то не работают. Был один дырявый php4. И то его сменили на php5.

Надо на венду переходить. Им даже письма с темой «I love you» как-то приходили.

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

Бггг, верно. Давай даже считать, что у нас настоящая машина Тюринга, а не жалкий FSM. Объясни, как это делало бы невозможным написание программ, удовлетворяющих спецификациям? Берешь, и руками доказываешь теорему о том, что твой код в самом деле ведет себя так, как того требует спецификация. Компьтер же может автоматически убедиться в верности твоего доказательства. Всё, дело в шляпе.

> А может добавить и про FreeBSD в новость, чтобы не было нежелательных пиар-атак товарищейBSDшников)

Поподробнее, пожалуйста)

Я выше ссылку приводил.

Как-то скучно и не в тему вовсе.

Этот баг работает, если на машине один пользователь? А то я волнуюсь.

// это lester_dev, просто лень перелогиниваться

Нет, там только «разработать улиточными темпами» присутствует.

Ну так реализуй мне конечным автоматом рекурсию.

man Buchi Automaton Число состояний --- конечно.

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

> Ну так реализуй мне конечным автоматом рекурсию.

Рекурсию ограниченной глубины (скажем, стек не больше 2 мегабайт) - запросто.

Ну и что? Для этого надо скачать код, скомпилить его и запустить. Кому попало я доступа на свои машины не даю, а сам левые программы не запускаю. Вспомнился анекдот: «Нашел вирус под линукс. Решил поставить, попробовать. Два дня компелял, но так и не смог запустить.»

> Ну так реализуй мне конечным автоматом рекурсию.

Если память конечна --- нет проблем.

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

ну не знаю, руки при постановке винды как бы не очень важны.

я думаю тут аура плюс гоепатогенные зоны сказались. :-)

P.S.

эфект проявлялся на 2х компах - отличие в видеокартах. расстояние между ними метра 2.

В NT 3.5 - 4.0 вроде как

> При чем тут лента?

При том, что число состояний реальной вычислительной машины --- конечное.

Заботайте поскорее что-то типа: http://mstu.sevik.ru/docs/Model_Checking.pdf

Понял.

> Рекурсию ограниченной глубины (скажем, стек не больше 2 мегабайт) - запросто.

О, уже юлить начал

Запустил, система тут же ушла в даун, даже на другой десктоп не смог переключиться (там был запущен top), минуты через три нажал reset, но комп не смог загрузиться - сработала система защиты на материнке (у меня такое когда-то случалось когда баловался с разгоном проца), потом ящик всёже загрузился с третьей попытки. Прикольно :)

http://www.opennet.ru/openforum/vsluhforumID3/72817.html#27 http://www.opennet.ru/openforum/vsluhforumID3/72817.html#30

фикс не сильно лучше, но хотя бы имеет меньше пост эффектов. если заменить get_max_files на NR_FILES (ограничивая очередь до 8к сообщений) то вобще для машины проблем не возникает.

мисье забывает о статической линковке с ucLibc ? ее вполне хватает для распространения виря.. как он и поступал при распространении через дыру в апаче.. Молодежь забывает как в ~2002 гулял червяк и положил пол европы, а гулял через дырку в апачах :)

> Имелась ввиду верификация кода относительно спецификаций.

Это просто переваливание отвественности.

да, действительно напомнило.
//отписываюсь в эпический тред

>> Рекурсию ограниченной глубины (скажем, стек не больше 2 мегабайт) - запросто.

О, уже юлить начал

На реальных машинах (которые, по сути, конечные автоматы) рекурсия ограничена _всегда_.

Вот на SLOR-е праздник-то будет...

Интересно, соурсфордж ляжет? )

> Боюсь показаться занудой, но вторая теорема Геделя утверждает, что если формальная арифметика непротиворечива, то в ней невыводима некоторая формула, содержательно утверждающая непротиворечивость этой теории.

Прекрасно, не будем доказывать непротиворечивость арифметики.

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

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

Уже написано. В других ОС. Функциональности там на порядок меньше, но за то она без говна.

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

> Это просто переваливание отвественности.

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

OpenBSD 4.8, socketpair (PF_UNIX, SOCK_DGRAM, 0, ff) завершается с ENFILE

Ну как тут не вспомнить о Minix Таннебаума? Он Линуса предупреждал, что написание ядра ОС в виде гигантской монолитной конструкции до добра не доведёт. Главные возражения Линуса: 1. Микроядро медленней работает. 2. Его намного тяжелей писать.

Что касается производительности, то это правда. Микроядро медленней, хотя бы потому, что использует сложный механизм посылки сообщений между модулями. Написание микроядра на начальном этапе разработки в разы более трудоёмкое, чем монолитного ядра.

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

А в микроядре вы можете тщательно проверить само это ядро(в силу его небольшой сложности и объёмов), затем проверить каждый модуль, и в результате получить надёжную ОС. Мало того, если модуль вдруг начнёт сбоить, микроядро может его перезапустить.А если не поможет, отключить. В монолитных и гибридных ядрах намного больше проблем. Не зря в США, да и в России, многие важные военные проекты работают на микроядерных ОСРВ.

Но хаить Linux, не ругнув уродливых гибридов(Windows и MacOS X), и не вспомнив о не менее архаичных BSD будет нечестно. Хотя BSD, субъективно конечно, надёжней некоторых систем из данного списка.

> На реальных машинах (которые, по сути, конечные автоматы) рекурсия ограничена _всегда_.

Да! Но! Представим на минуту, что ты получил доказательство своего алгоритма, используя представление о компьютере как конечном автомате, в том числе и с лимитом стека, например в 1 Гб. Теперь берем твой компьютер, вынимаем из него 512 Мб... и что имеем с доказательством?

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

> Представим на минуту, что ты получил доказательство своего алгоритма, используя представление о компьютере как конечном автомате, в том числе и с лимитом стека, например в 1 Гб. Теперь берем твой компьютер, вынимаем из него 512 Мб... и что имеем с доказательством?

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

Странно, весь этот buzz я читаю уже второй десяток лет, а вменяемой ОС так и не написали. Да-да, я в курсе про QNX, L4, Mach... Где они?

>> На реальных машинах (которые, по сути, конечные автоматы) рекурсия ограничена _всегда_.

Да! Но! Представим на минуту, что ты получил доказательство своего алгоритма, используя представление о компьютере как конечном автомате, в том числе и с лимитом стека, например в 1 Гб. Теперь берем твой компьютер, вынимаем из него 512 Мб... и что имеем с доказательством?

Смотря что доказывалось. Если конечность алгоритма - доказательство останется валидным :)

Лично я сильно сомневаюсь в возможности фанатично пропагандируемой Manhunt программы по формальной верификации кода

Я не силен в теории, но полагаю, что гарантированно безотказных систем она не даст. Хотя по сравнению с текущим положением, это будет прорыв.

> Неужели, что компьютер не удовлетворяет требованиям данной программы?

А если управление событийное? 512 потребуется отдать real-time программе, и все, привет, здравствую глюки? Или работать по схеме «одна задача — один компьютер». Здравствую DOS?

> 512 потребуется отдать real-time программе, и все, привет, здравствую глюки?

В линуксе это называется OOM Killer.

Конечный, одно состояние

> Смотря что доказывалось. Если конечность алгоритма - доказательство останется валидным :)

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

Я не силен в теории, но полагаю, что гарантированно безотказных систем она не даст. Хотя по сравнению с текущим положением, это будет прорыв.

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

>> Неужели, что компьютер не удовлетворяет требованиям данной программы?

А если управление событийное? 512 потребуется отдать real-time программе

Это вообще не возражение - виртуальную память придумали 45 лет назад. Поэтому для целей доказательства можно считать, что у нас есть полное 32 (или 64-бит) пространство :)

> В линуксе это называется OOM Killer.

Поогоди, нечего на линукс пенять, мы его хороним. Где обещанная тобой при доказательстве («мамой клянусь!») вычислимость?

> Поэтому для целей доказательства можно считать, что у нас есть полное 32 (или 64-бит) пространство :)

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

Читаю на их странице:

Stay tuned for the first commercially available, fully formally verified microkernel.

А как же ядро QNX? Оно вроде бы тоже fully formally verified, причем давно уже.

Действительно работает. Пишу на лор, а эта дрянь висит в фоне, полностью загрузив процессор. Причем съедает исключительно время ядра. Последний раз такое на своем компе видел 4 года назад под вендой. Прямо венду напомнило по отзывчивости на действия пользователя. Но работает и не падает. В графике правда обновление происходит где-то 1 раз в секунду, мышью пользоваться не комфортно, но клавиатура работает, события не съедаются. Убивать пробовал по разному kill -STOP не помог, kill -KILL тоже, renice -n 20 тоже не уменьшил тормозов. Сама эта дрянь, как у некоторых не желает дохнуть. Система - дефолтная убунта. Счас проверю, будет ли запыкаться музыка (пульсаудио бы-гы-гы), поставлю обновления и перезагружу.

> Ааа. Нечего делать, придется ставить Windows 7!

ставь, там ремотные нюки не закрываются годами