Таки нет. В случае с той ракетой полное формальное доказательство не исключает глюки. Бо программа, если чо, отработала штатно. А вот реальность подкачала.

>Говорит же вам Шишкин про алгоритмы и про МГИМО. Не хотите слушать -

жрите, жрите это linux-way говно.

Manhunt (25.11.2010 19:56:05)

Ты действительно такой или прикидываешься - уязвимость то локальная.

Буть добр - разъясняйся на русском языке, если не в состоянии - подойдут листинги кода на любом ЯП, линуксовому народцу подойдет любой наряд, не привыкать.

Э, простите, если они не рассмотрели достаточно полную модель реальности (входа), то какое же оно полное доказательство?

>Э, простите, если они не рассмотрели достаточно полную модель реальности (входа), то какое же оно полное доказательство?

Вот таким образом спецефикации и разрастаются до нереализуемых over9000 страниц, и переходят в жанр «Войны и мира про калькулятор»

Нку что - сморщился ? прыщавый штангист-теоретик. иди подметай улицы, от тебя больше пользы.

Там же как дело было. Они использовали часть рабочего и оттестированного кода дла Ариан4, но, как выяснилось после аварии, были некие различия в параметрах выведения на орбиту, что и привело к могучему БАМС на сороковой секунде полёта. Таким образом код был правильным, но реальность ему не соответствовала. И если мы можем зафиксировать код в неизменном состоянии, то зафиксировать реальность не представляется возможным за исключением узкого класса случаев.

Всё просто. Чтобы избежать ошибок в спецификации нам нужно составить спецификацию на спецификацию.

> Они использовали часть рабочего и оттестированного кода дла Ариан4, но, как выяснилось после аварии, были некие различия в параметрах выведения на орбиту, что и привело к могучему БАМС на сороковой секунде полёта.

Там случилось банальное переполнение, потому что код Ариан-4 использовал 16-бит целые, которых для Ариан-5 оказалось мало. Как раз такие ошибки вполне поддаются отлову компиляторами.

Как раз такие ошибки вполне поддаются отлову компиляторами.

У вас есть компилятор, который знает какие значения может принимать сигнал с датчика на свежеспроектированной космической ракете?

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

Ну что там, патча нет ещё?
Я думал Линус вернётся с работы и напишет патч...

Помоему, после этого обвинения тайлганнер должен поделиться на ноль и, сколлапсировав, обрушить Лор вовнутрь себя.

Линус вернётся с работы

Боже! Боже!

> Латентный лиспотроль детекткед

Кто латентный ты латентный епт.

боготворящих говнопистон.

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

Там всё, кстати, было чуть иначе. Как я помню, параметры пивели к бамс только потому, что в продакшене остались ассерты на боле узкие диапазоны значения параметров >_<

Неужели ты до сих пор не понел что ты в говне ? Штангист, хуле тут - вопреки своей воле не понять что его говноязычок никуда не годен сегодня, и эти люди с серьезной рожей лица говорот что все нужно писать на КаЛе...

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


Ну же дурында, назови, почему не пользуешься ?

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

Ну же дурында, назови, почему не пользуешься ?

Ты наркоман штоле? Там написано «пользуюсь».

rtfm. не было там статической типизации. и много чего еще не было. погуглите на досуге

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

собрал http://lkml.org/lkml/2010/11/25/8 (ноут dell 1525, opensuse 11.3 32bit) - стало все медленно, но смог подать killall -9 a.out, но ни к чему полезному не привело (процесс не убивался)
зашел на ноут через ssh, подал «cat /dev/urandom >/dev/null» и через какоето время все стало нормально, процесс эксплоита сдох

повторил эксперимент: запустил a.out, вошел через ssh, подал «cat /dev/urandom >/dev/null» и через немного a.out сам сдох

на боле узкие диапазоны значения параметров

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

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

Проверяет, проверяет. И изнутри кода невозможно понять, что проверка неправильная.

1. Программа была написана на языке ада.

2. Язык ада использует строгую статическую типизацию.

3. ...

Какое из утверждений здесь не верно?

>Фееричный высер дурачка.

Да, Линукс та еще поделка ))

> нам будет нужна спецификация на реальность (в части диапазона параметров), с которой программа будет взаимодействовать. А это задача совершенно неподъёмная.

С чего бы? По-моему, это как раз тривиально.

> 1. Программа была написана на языке ада.

2. Язык ада использует строгую статическую типизацию.

3. ...

Какое из утверждений здесь не верно?

Полагаю, номер 3.

Может и тривиальная. Но вот у инженеров Ариана 5 не получилось.

скомпилил, запустил. что-то у меня ничего не упало, а так хотелось посмотреть. минут 10 ждал-- не падает. просто все стало жутко тормозить. на ^с не среагировало. закрыл мышкой терминальное окно. минуты две закрывалось, но нечего не изменилось. на комбинацию из 3 пальцев гном нехотя отреагировал. перезагрузилось щелчком мышки. debian squeeze 2.6.32

> Таки нет. В случае с той ракетой полное формальное доказательство не исключает глюки. Бо программа, если чо, отработала штатно. А вот реальность подкачала.

Прочитал много постов, но так и не понял, откуда взято про формальную верификацию программы для компьютера Ariane-5

Кстати, даже VMS вроде бы UNIX-сертификат имеет.

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

>А микроядро навсегда останется учебным примером в академических исследованиях.

Ему есть применение в ОС реального времени. Но не потому, что так проще, надёжнее и производительнее, а потому, что можно чётко поделить задачи по приоритетам.

откуда взято про формальную верификацию программы для компьютера Ariane-5

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

и что с того что он был написан на АДА? почитайте что такое подтипы в аде, для чего они предназначены. а потом прочтите что сделали тамошние программеры. а они решили что «таких значений быть не может никогда» и для части переменных использовали базовые (без ограничений на дипазон значений и значит и без проверок и без контроля) типы. соптимизировали «ненужные» проверки отключив таким образом типизацию. если у нас есть парметр «температура воды» (скажем в котле для подогрева воды) то тип у него (в строгом языке) не int и не флоат. а дипазон -4..+120. а если у нас вдруг -200 или +400 то значит работаем мы в какойто другой неземной рельности и надо не выпедриваться а прекращать работу. PS я уж молчу что тот «оттестированный код» был плохо документирован. что вызывает вопросы - а как же его всетаки тестировали?

а им не нужно было «спецификация на реальность». им всего то надо было написать спецификацию на тот кусок реальности в которой будет работать ракета. это много но это обозримая задача. а они 1) это не доделали 2) контркат с проверками на допустимость а также подтип данных выкинули в угоду «оптимизации».

>Эти же проблемы с ДНК и у Сышкина, если бы кроме пафоса от диплома МГУ он что-то хотел то пошел бы по пути ntfs-3g чтобы реализация ФС не зависела от ОС.

фееричный бред школьника-двоечника

практическая реализация дырки в коде какая? на торренты не влияет? :-)))

а они решили что «таких значений быть не может никогда»

нормальный, инженерный подход к задаче. И на момент принятия решения (т.е. на Ариан 4) это было абсолютно верное решение.

спецификацию на тот кусок реальности в которой будет работать ракета.

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

>для вас может быть и Facebook OS, если RedHat для вас неизвестен...

Red Hat - пишется _раздельно_.

1. Все те кто во фразе про «МГУ vs МГИМО» не прочли смысла «я технарь, а не политик», и кинулись искать какой-то пафос - кретины с заниженой самооценкой. И в ход пускается их любимый убойный аргумент «сам дурак». Сочувствую, но общаться с ними смысла нет ни малейшего.

2. Все беды современного «промышленного программирования» проистекают из одного - лицензионного соглашения, где программеры «ничего не гарантируют и ни за что не отвечают». В какой ещё отрасли промышленности есть такая халява - брать деньги не отвечая за результат?

3. Насчет платы программистов за ошибки - двумя руками за!!! Ибо постоянно сталкиваюсь с подходом «да, это работает неправильно, но починить это мы не можем т.к. нам было удобно сделать именно так»...

P.S. А тред получился настолько эпичным, что пришлось таки купить книжку Вирта и поинтересоваться как там Оберон :)

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

Классное допущение. «Если бы у бабушки...» (с)

А значит и пользоа от той верефикации завышена.

Cпециально для троллей с женской^Wнечеткой логикой: ПО Ариан-5 не было формально верифицировано - только собрано компилятором Ады.

> пришлось таки купить книжку Вирта и поинтересоваться как там Оберон :)

Устарел давно и сильно.

Устарел для чего и по сравнению с чем?

Или вы всё ещё собираетесь на ФП писать ОС ?

Устарел для чего и по сравнению с чем?

Или вы всё ещё собираетесь на ФП писать ОС ?

ПО Ариан-5 не было формально верифицировано

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

> Для особо одарённых и внимательных слушателей: при авариях такого рода от формальной проверки кода нет никакого толка.

Как раз при такой аварии, формальная проверка выявила бы это ещё на этапе проектирования.

Зато я трезвым за компом сижу, и дерьмовый виски не бухаю, и само рабочее место хоть старое хоть новое на пивнуху с дешевым антуражем не похоже...