The OpenNET Project / Index page

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

форумы  помощь  поиск  регистрация  майллист  вход/выход  слежка  RSS
"Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"
Вариант для распечатки  
Пред. тема | След. тема 
Форум Разговоры, обсуждение новостей
Изначальное сообщение [ Отслеживать ]

"Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от opennews (??) on 23-Дек-10, 12:28 
Тэо де Раадт (Theo de Raadt), лидер проекта OpenBSD, обобщил (http://permalink.gmane.org/gmane.os.openbsd.tech/22727) информацию, связанную с высказанными (http://www.opennet.me/opennews/art.shtml?num=28998) на прошлой неделе опасениями по поводу возможности интеграции бэкдора в IPSEC-стек OpenBSD. По мнению Тэо, десять лет назад ФБД была особенно заинтересована в получении контроля над реализацией криптографических систем и компания NETSEC, выполнявшая правительственные контракты, вполне могла получить заказ на разработку и внедрение бэкдора. Но пока не обнаружено никаких фактов, указывающих на то, что бэкдор был внедрен в дерево исходных текстов OpenBSD. Наиболее вероятно, что бэкдор был интегрирован в выпускаемые NETSEC продукты на основе OpenBSD.


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


URL: http://permalink.gmane.org/gmane.os.openbsd.tech/22727
Новость: http://www.opennet.me/opennews/art.shtml?num=29098

Ответить | Правка | Cообщить модератору

Оглавление

Сообщения по теме [Сортировка по времени | RSS]


1. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  –3 +/
Сообщение от Andrew (??) on 23-Дек-10, 12:28 
Они хотят за неделю найти то что другие там "закапывали" несколько лет?!
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

3. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +7 +/
Сообщение от Амнезинус on 23-Дек-10, 12:42 
Трудно искать черную кошку в темной комнате, особенно если ее там нет.
Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

7. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  –1 +/
Сообщение от Andrew (??) on 23-Дек-10, 13:04 
Только после полного независимого анализа кода можно говорить что никаких бэкдоров нет.
Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

15. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +4 +/
Сообщение от Aleksey (??) on 23-Дек-10, 14:31 
Ну вот они его и проводят. Можете тоже поанализировать.
Ответить | Правка | ^ к родителю #7 | Наверх | Cообщить модератору

19. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от shpsn on 23-Дек-10, 15:50 
Еще труднее найти белую кошку в тёмной комнате, в которой помимо неё еще 50 чёрных.
Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

20. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 16:08 
белую в темной комнате? да запросто.
Ответить | Правка | ^ к родителю #19 | Наверх | Cообщить модератору

22. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  –2 +/
Сообщение от zazik (ok) on 23-Дек-10, 17:07 
> белую в темной комнате? да запросто.

Ну-ну. Задачу можно свести к поиску белого шара в тёмной комнате среди 50 чёрных шаров. По теории вероятности шансы есть.

Ответить | Правка | ^ к родителю #20 | Наверх | Cообщить модератору

33. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от Bolek email(ok) on 23-Дек-10, 21:50 
белую... в темной комнате... а как цвет различать будете без источника света... усилием мысли?
Ответить | Правка | ^ к родителю #20 | Наверх | Cообщить модератору

32. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от 8 on 23-Дек-10, 19:01 
Зато такой, надеюсь, в результате неудачный, поиск выявит изрядно таракашек (что, собственно, уже и началось).
Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

5. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от анонимиус on 23-Дек-10, 12:43 
Сколько там строк хоть?
Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

29. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от User294 (ok) on 23-Дек-10, 18:34 
Есть надежда что в открытой реализации теперь покопаются грамотные криптографы. Думаю что теперь после такого наброса немало специалистов по криптографии начнут искать бэкдор. Ведь если его найти - это однозначный EPIC WIN в профессиональном плане.

Проблема только в том что бзди позволяют еще и абузивное использование лицензионной свободы:
> что бэкдор был интегрирован в выпускаемые NETSEC продукты на основе OpenBSD.

Вероятно, NETSEC ни разу не собирается показывать всем исходники своих продуктов с бэкдорами, да? Ну как, кто-то еще хочет купить блобятину с черт знает чем, недоступным для аудита сторонними специалистами? :)

Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

41. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 24-Дек-10, 03:45 
> Есть надежда что в открытой реализации теперь покопаются грамотные криптографы.

Они копались там и до этого, вообще-то. Но свежий взгляд, конечно, не помешает.

> Думаю что теперь после такого наброса немало специалистов по криптографии начнут искать
> бэкдор. Ведь если его найти - это однозначный EPIC WIN в профессиональном
> плане.

Угу, на misc@openbsd.org и tech@openbsd.org уже поимела место быть куча дискуссий различной степени толковости, начатых новичками в криптографии. Правда, почему-то они в основном сваливаются в смежные темы.

> Проблема только в том что бзди позволяют еще и абузивное использование лицензионной
> свободы:
>> что бэкдор был интегрирован в выпускаемые NETSEC продукты на основе OpenBSD.
> Вероятно, NETSEC ни разу не собирается показывать всем исходники своих продуктов с
> бэкдорами, да? Ну как, кто-то еще хочет купить блобятину с черт
> знает чем, недоступным для аудита сторонними специалистами? :)

1. Если NETSEC и так разрабатывали этот код, то BSDL тут ни при чём.

2. Вам как будто неймётся, лишь бы связать BSDL и те или иные проблемы BSDL-продуктов. Сейчас это получилось уже слишком толсто.

Ответить | Правка | ^ к родителю #29 | Наверх | Cообщить модератору

44. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +2 +/
Сообщение от iZEN (ok) on 24-Дек-10, 07:43 
>Проблема только в том что бзди позволяют еще и абузивное использование лицензионной свободы:

Это не проблема бзди, а проблема пользователей — если они не способны для своей инфраструктуры решить все вопросы самостоятельно и им требуется "поводырь" в лице NETSEC/MS, Red Hat, Novell/, то они сами такие беспомощные и в некотором смысле безответственные, раз перекладывают существенную часть ответственности на "дядю".

>Вероятно, NETSEC ни разу не собирается показывать всем исходники своих продуктов с бэкдорами, да?

А что, должна? Лицензию-то прочёл?

Ответить | Правка | ^ к родителю #29 | Наверх | Cообщить модератору

6. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +8 +/
Сообщение от Аноним (??) on 23-Дек-10, 12:51 
> Проведенный за неделю беглый аудит выявил несколько несущественных проблем, но ничего значительного

О, и баги до кучи пофиксят. ^_^

Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

9. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  –3 +/
Сообщение от Аноним (??) on 23-Дек-10, 13:30 
Блин. И как же они до этого аудитили, что беглым аудитом сразу сразу нашли проблемы?
Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

14. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +8 +/
Сообщение от Vitaly_loki (ok) on 23-Дек-10, 14:13 
Премногоуважаемый анонимный Дон видимо пишет безошибочный код с первого раза. Куда уж там Тео до него
Ответить | Правка | ^ к родителю #9 | Наверх | Cообщить модератору

50. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от Аноним (??) on 24-Дек-10, 12:36 
>Премногоуважаемый анонимный Дон видимо пишет безошибочный код с первого раза. Куда уж там Тео до него

Да не в этом дело. OpenBSD славилась своим аудитом. ПО крайней мере, так говорили. Теперь же говорят, что беглый аудит выявил проблемы. Отксюда и вопрос: как же они аудитили (а не кодили, как Вы написали, уважаемый неаноним Дон), что беглый аудит (еще раз: "беглый аудит") сразу выявил проблемы, которые не нашлись во время предыдущего аудита. Почему все надо разжевывать?

Ответить | Правка | ^ к родителю #14 | Наверх | Cообщить модератору

52. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 24-Дек-10, 15:24 
>>Премногоуважаемый анонимный Дон видимо пишет безошибочный код с первого раза. Куда уж там Тео до него
> Да не в этом дело. OpenBSD славилась своим аудитом. ПО крайней мере,
> так говорили. Теперь же говорят, что беглый аудит выявил проблемы. Отксюда
> и вопрос: как же они аудитили (а не кодили, как Вы
> написали, уважаемый неаноним Дон), что беглый аудит (еще раз: "беглый аудит")
> сразу выявил проблемы, которые не нашлись во время предыдущего аудита. Почему
> все надо разжевывать?

Может, дело в том, что разработчики OpenBSD сами знают реальную цену кода, прежде всего - своего собственного?

http://www.openbsd.org/images/hackathons/c2k10.gif

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

Ответить | Правка | ^ к родителю #50 | Наверх | Cообщить модератору

18. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Aleksey (??) on 23-Дек-10, 15:36 
I've already found a small bug in a totally different side of the random subsystem, and am looking at cleaning up a truly ugly function.

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

Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

10. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 13:31 
Хм, но этот вброс про бэкдор был явно не спроста. Так зачем же?
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

11. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от Devider (ok) on 23-Дек-10, 13:37 
Месть Амазона? =)
Ответить | Правка | ^ к родителю #10 | Наверх | Cообщить модератору

13. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +4 +/
Сообщение от Аноним (??) on 23-Дек-10, 13:42 
Может быть девелоперы OpenBSD просто стали лениться аудиттить код, и Тэо де Раадт таким хитрым способом с помощью вброса решил их подстегнуть?

Как в анекдоте.
Жена во время Гражданской Войны пишет мужу на фронт, сажать картошку или нет. Он ей отвечает:
- Не вздумай! Я на нашем огороде припрятал кое-какое золотишко которое мы с мужиками поделили, когда раскулачивали нашего барина.
Жена снова пишет:
- Пришли из ВЧК, перекопали весь огород.
Муж:
- Вот теперь сажай картошку.

Ответить | Правка | ^ к родителю #10 | Наверх | Cообщить модератору

17. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от zazik (ok) on 23-Дек-10, 15:26 
> Может быть девелоперы OpenBSD просто стали лениться аудиттить код, и Тэо де
> Раадт таким хитрым способом с помощью вброса решил их подстегнуть?

Это очень глупый способ мотивации, аудит-то проведут, а осадок всё равно останется.

Ответить | Правка | ^ к родителю #13 | Наверх | Cообщить модератору

24. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 17:33 
> Это очень глупый способ мотивации, аудит-то проведут, а осадок всё равно останется.

Вы неверно рассуждаете.
Здесь получается выбор. Либо осадок останется у одних, что их "смотивировали" провести аудит. Либо осадок останется у других, что аудит должным образом не проводится.

Ответить | Правка | ^ к родителю #17 | Наверх | Cообщить модератору

60. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Анон on 25-Дек-10, 11:57 
О каком именно осадке идет речь?
кто то вбросил, провели аудит, ничего не нашли. Все довольны, да еще и баги исправили
Ответить | Правка | ^ к родителю #17 | Наверх | Cообщить модератору

61. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от zazik (ok) on 25-Дек-10, 14:49 
> О каком именно осадке идет речь?
> кто то вбросил, провели аудит, ничего не нашли. Все довольны, да еще
> и баги исправили

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

Ответить | Правка | ^ к родителю #60 | Наверх | Cообщить модератору

12. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от zazik (ok) on 23-Дек-10, 13:41 
Напоминает бородатый анекдот про ложечки и остаток.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

16. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pavlinux (ok) on 23-Дек-10, 14:55 
Надо по чаще такие подставы им подкидывать, чтоб чаще аудиты делали.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

21. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 23-Дек-10, 16:44 
Проще один раз публично засудить ФБР и им подобных. Надо жить и развиваться, а не ставить полицейский над полицейскими :)
Ответить | Правка | ^ к родителю #16 | Наверх | Cообщить модератору

26. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 17:41 
> Проще один раз публично засудить ФБР и им подобных. Надо жить и развиваться, а не ставить полицейский над полицейскими :)

По-вашему это сильно упрощает дело - поставить судью над полицейским, чем полицейского над полицейским.

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

Когда такие вот как вы "рационализаторы" обычно все и разваливают, поскольку дальше своего носа не видят.

Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

27. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 17:49 
И дело даже не в загруженности, а в том, что судебные и исполнительные функции по-вашему легко можно возложить на одни и те же структуры. Точнее возложить-то можно. У нас в 30-х годах прошлого века так и было. Только вы уверены, что вам это потом понравится?

Ответить | Правка | ^ к родителю #26 | Наверх | Cообщить модератору

28. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Aleksey (??) on 23-Дек-10, 18:05 
Видимо, человек из России и думает, что везде так: президент куда-нибудь звонит и бабушке проводят воду.
Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

35. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 23-Дек-10, 23:07 
> Видимо, человек из России и думает, что везде так: президент куда-нибудь звонит
> и бабушке проводят воду.

хахаха, видимо, вы не знаете, что в штатах некоторые только и живут, что судятся с кем угодно. На уровне бабушек, это вы правы - в РФ такая себе ситуёвина

Ответить | Правка | ^ к родителю #28 | Наверх | Cообщить модератору

38. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 23:24 
> хахаха, видимо, вы не знаете, что в штатах некоторые только и живут, что судятся с кем угодно. На уровне бабушек, это вы правы - в РФ такая себе ситуёвина

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

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

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

Ответить | Правка | ^ к родителю #35 | Наверх | Cообщить модератору

30. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +1 +/
Сообщение от pavlinux (ok) on 23-Дек-10, 18:34 
> И дело даже не в загруженности, а в том, что судебные и
> исполнительные функции по-вашему легко можно возложить на одни и те же
> структуры. Точнее возложить-то можно. У нас в 30-х годах прошлого века
> так и было. Только вы уверены, что вам это потом понравится?

А причем тут OpenBSD?

Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

34. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 23:02 
> А причем тут OpenBSD?

Наверное при том же, при чем и ФБР, и далее по тексту.
Или вы обо всем делаете выводы на основании последних прочитанных вами строк?

Ответить | Правка | ^ к родителю #30 | Наверх | Cообщить модератору

31. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от User294 (ok) on 23-Дек-10, 18:38 
> Проще один раз публично засудить ФБР.

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

Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

36. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 23-Дек-10, 23:08 
>> Проще один раз публично засудить ФБР.
> Оно, конечно, было бы хорошо и правильно, но как-то с трудом представляю
> себе такую картину.

Люди судятся и за меньшее. Неримское право, знаете ли :)

Ответить | Правка | ^ к родителю #31 | Наверх | Cообщить модератору

39. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 23:32 
> Люди судятся и за меньшее. Неримское право, знаете ли :)

То есть для вас правовые вопросы представляются исключительно на уровне "больше-меньше".

А с учетом ваших рассуждений о "полицейских" было бы интересно узнать, что именно вы имеете в виду под "неримским правом", кроме желания показать, что вы об этом что-то слышали.

Ответить | Правка | ^ к родителю #36 | Наверх | Cообщить модератору

46. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 24-Дек-10, 11:21 
Толстый, анонимы такие анонимы. А по существу?
Ответить | Правка | ^ к родителю #39 | Наверх | Cообщить модератору

47. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 24-Дек-10, 11:52 
> Толстый, анонимы такие анонимы. А по существу?

Вот вы и ответьте по существу, что вы имели в виду под "неримским правом".

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

Ответить | Правка | ^ к родителю #46 | Наверх | Cообщить модератору

54. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 24-Дек-10, 20:54 
> Вот вы и ответьте по существу, что вы имели в виду под
> "неримским правом".

С Луны или Альдебарана? Англо-американское право, включает прецеденты.

> И почему вы мечтаете засудить ФБР и "полицейских", но при этом вас
> раздражает, что юридически подкованные "бабушки" могут судиться по любому поводу, пользуясь своими на то правами.

Это ваши домыслы, непонятно почему вы их мне приписываете. Выйдите уже наконец из виртуала.


Ответить | Правка | ^ к родителю #47 | Наверх | Cообщить модератору

55. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 25-Дек-10, 00:11 
>> Вот вы и ответьте по существу, что вы имели в виду под "неримским правом".
>
> С Луны или Альдебарана? Англо-американское право, включает прецеденты.

Римское право тоже включает прецеденты. Ну и?
И что же все-таки означала ваша фраза:
> Люди судятся и за меньшее. Неримское право, знаете ли :)

Вы хотели сказать, что по-вашему в соответствии с Римским правом за меньшее чем над ФБР судиться было нельзя, и только по "неримскому праву" по-вашему значит можно. Так что ли?

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

> Это ваши домыслы, непонятно почему вы их мне приписываете. Выйдите уже наконец из виртуала.

На этот раз было бы интересно узнать, что именно вы считате "виртуалом", общаясь при этом на форумах.

М-да, с вашими "про100 мастерскими" способностями не удивительно, что вы побаиваетесь юридически подкованных "бабушек", вам видимо даже до них далеко. С вашими мечтами "один раз публично засудить ФБР" и развиваться в мире, где нет "полицейских над полицейскими" (видимо вы считаете это самой главной помехой в развитии).

И это конечно по-вашему никак не "виртуал".

Ответить | Правка | ^ к родителю #54 | Наверх | Cообщить модератору

37. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 23-Дек-10, 23:12 
>> Проще один раз публично засудить ФБР.
> Оно, конечно, было бы хорошо и правильно, но как-то с трудом представляю себе такую картину.

Вам ведь уже намекнули выше на некоторую почву для развития воображения.
Годике где-то в 17-м в России таки удалось "публично засудить" "полицейских" и прочие местные спецслужбы, "хорошо и правильно".

"Мне не нравится вот эта деталь в системе, было бы хорошо и правильно ее удалить, но как-то с трудом представляю себе такую картину".

Вы уж сначала представьте, прежде чем делать выводы, что хорошо, и что правильно.

Ответить | Правка | ^ к родителю #31 | Наверх | Cообщить модератору

53. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от pro100master (ok) on 24-Дек-10, 20:53 
В 17-м? А может раньше? У вас странные, если не сказать - глупые, аналогии. Да - в штатах - англо-американское право и, в отличии от, оно работает. И, в отличии от, это создаст прецедент. Вплоть до курьёзов http://www.google.com/search?q=%D0%B0%D0%...

Впрочем все вышеответившие мне лично (непонятно, почему такой ажиотаж) частично правы. Штаты, таки да - стали полицейским государством (страной уже язык не поворачивается назвать).

Ответить | Правка | ^ к родителю #37 | Наверх | Cообщить модератору

56. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 25-Дек-10, 00:58 
> В 17-м? А может раньше?

Может даже и раньше. И что?

> У вас странные, если не сказать - глупые, аналогии. Да - в штатах - англо-американское право и, в отличии от, оно работает. И, в отличии от, это создаст прецедент.

Создаст? Т.е. по-вашему еще не создало? Целый один прецедент?
И по-вашему именно само право "создает прецеденты"?

> Вплоть до курьёзов http://www.google.com/search?q=американское+забавные+законы

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

> Впрочем все вышеответившие мне лично (непонятно, почему такой ажиотаж) частично правы.
> Штаты, таки да - стали полицейским государством (страной уже язык не поворачивается назвать).

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

И притом, что у вас Штаты "страной уже язык не поворачивается назвать", вы одновременно признаете, что там "англо-американское право и, в отличии от, оно работает".

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

Ответить | Правка | ^ к родителю #53 | Наверх | Cообщить модератору

40. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Buy email(??) on 24-Дек-10, 00:31 
Команде OpenBSD будет практически невозможно сделать безоговорочное заявление, что бэкдора не было. Доказать отсутствие - нелегкое дело.

"Это будет практически невозможно доказать или опровергнуть", - сказал Нейт Лосон из Root Labs, криптограф и эксперт в сфере безопасности, который выполнил много работ по встроенным устройствам и аппаратной безопасности. "Эти заявления почти точно неправильны, по крайней мере в широком понимании (скрытые каналы, встроенные в основный исходники OpenBSD). Возможно, что кто-то добавил бэкдор в индивидуальные (возможно, созданные частным образом) OpenBSD-исходники или бинарный дистрибутив. Существует множество способов, как это могло бы быть сделано, от простых и очевидных до еле уловимых и изощренных. Возможно создать что-то, что выглядит как простая ошибка в коде и назначение которой будет невозможно доказать".

http://www.xakep.ru/post/54412/

Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

42. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 24-Дек-10, 03:50 
> Команде OpenBSD будет практически невозможно сделать безоговорочное заявление, что бэкдора
> не было. Доказать отсутствие - нелегкое дело.

Вы очень-очень-очень большой оптимист. Доказать корректность кода в таком сложном проекте, как стек IPsec, встроенный в достаточно сложное ядро, реально, по сути, только теоретически. По крайней мере, на данном этапе развития средств анализа.

Ответить | Правка | ^ к родителю #40 | Наверх | Cообщить модератору

43. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 24-Дек-10, 07:09 
> Вы очень-очень-очень большой оптимист. Доказать корректность кода в таком сложном проекте, как стек IPsec, встроенный в достаточно сложное ядро, реально, по сути, только теоретически. По крайней мере, на данном этапе развития средств анализа.

Можно только представить, что творится во FreeBSD. И уж тем более в Linux.

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

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

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

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

Ответить | Правка | ^ к родителю #42 | Наверх | Cообщить модератору

45. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 24-Дек-10, 11:21 
>> Вы очень-очень-очень большой оптимист. Доказать корректность кода в таком сложном проекте, как стек IPsec, встроенный в достаточно сложное ядро, реально, по сути, только теоретически. По крайней мере, на данном этапе развития средств анализа.
> Можно только представить, что творится во FreeBSD. И уж тем более в
> Linux.
> Хотя на самом деле "на данном этапе развития средств анализа", и даже
> еще гораздо раньше, существуют уже достаточно методов организации кода таким образом,
> чтобы было возможно доказывать его правильность с помощью автоматизированных средств доказательств
> и анализа.
> Если код можно автоматически оптимизировать, то вообще-то можно и доказывать правильность,
> если изначально в система генрации кода интегрирована с системой доказательства. Ну
> и желательно, чтобы синтаксические средства этому способствовали.

Оптимизация кода делается, во-первых, без учёта семантики. Это у автора в голове уже есть какая-то картинка «как надо», и корректность программы однозначно определяется соответствием этой картинке. Но верификатор-то этой картинки не имеет! Её ему надо как-то ввести. Выстроить модель и связать с терминами, используемыми в программе. Это едва ли не больший объём работы по сравнению с собственно программой. И там тоже будут ошибки...

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

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

Ответить | Правка | ^ к родителю #43 | Наверх | Cообщить модератору

48. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 24-Дек-10, 12:05 
> Оптимизация кода делается, во-первых, без учёта семантики. Это у автора в голове уже есть какая-то картинка «как надо», и корректность программы однозначно определяется соответствием этой картинке. Но верификатор-то этой картинки не имеет! Её ему надо как-то ввести. Выстроить модель и связать с терминами, используемыми в программе. Это едва ли не больший объём работы по сравнению с собственно программой. И там тоже будут ошибки...

Оптимизатор работает на уровне семантики потока исполнения и прочих семантик, необходимых для оптимизации. Да, не на уровне целевой семантики. Ну и?
Поменяйте семантику, по которой работает оптимизатор на целевую семантику, и вы получите примерно те же срества в другой области приложения.

Мыслите проще.

> Во-вторых, оптимизация делается на базе считанных объектов одновременно, редко когда выходя за пределы одной функции. Верификатору надо обрабатывать громадные объёмы данных (по сути, для каждого оператора — проверять все связанные, которые могут быть разбросаны по всей программе... но тут я могу ошибаться), и насколько я могу догадываться, он столкнётся как минимум с одной NP-полной задачей при этом, которая будет поддаваться лишь частичной оптимизации.
> Существующие верификаторы действуют по тому же принципам, что и оптимизаторы: они выискивают несложные паттерны, которые более или менее уверенно могут свидетельствовать об ошибках кодинга. Но доказать корректность они не могут.

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

А вы продолжаете описывать техники верификации произвольного кода на произвольном языке.

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

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

Ответить | Правка | ^ к родителю #45 | Наверх | Cообщить модератору

57. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 25-Дек-10, 01:51 
>> Оптимизация кода делается, во-первых, без учёта семантики. Это у автора в голове уже есть какая-то картинка «как надо», и корректность программы однозначно определяется соответствием этой картинке. Но верификатор-то этой картинки не имеет! Её ему надо как-то ввести. Выстроить модель и связать с терминами, используемыми в программе. Это едва ли не больший объём работы по сравнению с собственно программой. И там тоже будут ошибки...
> Оптимизатор работает на уровне семантики потока исполнения и прочих семантик, необходимых
> для оптимизации. Да, не на уровне целевой семантики. Ну и?
> Поменяйте семантику, по которой работает оптимизатор на целевую семантику, и вы получите
> примерно те же срества в другой области приложения.
> Мыслите проще.

Проще? То есть, по-вашему, описание целевой семантики — это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как — поделитесь секретом?

>> Во-вторых, оптимизация делается на базе считанных объектов одновременно, редко когда выходя за пределы одной функции. Верификатору надо обрабатывать громадные объёмы данных (по сути, для каждого оператора — проверять все связанные, которые могут быть разбросаны по всей программе... но тут я могу ошибаться), и насколько я могу догадываться, он столкнётся как минимум с одной NP-полной задачей при этом, которая будет поддаваться лишь частичной оптимизации.
>> Существующие верификаторы действуют по тому же принципам, что и оптимизаторы: они выискивают несложные паттерны, которые более или менее уверенно могут свидетельствовать об ошибках кодинга. Но доказать корректность они не могут.
> Вам же уже было сказано, что для этого используются специальным образом организованный
> код, специальные библиотеки. И возможно даже специальные синтаксические средства.

Гениально! (кстати, я говорил об этом тоже, не знаю, почему вы мне мои же мысли тыкаете) Вот только если бы вы ещё и думали... Во-первых, строить такой верификатор (писать синтаксические средства, библиотеки, организовывать нужным образом код и т.д.) вы на чём будете? На обычных синтаксических средствах? Во-вторых, таким верификатором будет сложно заинтересовать людей, если надо будет переписывать программы на новом языке. Такой верификатор будет бесполезен, ибо прежде всего актуальна задача проверки _уже_имеющегося_ кода. На куче разных языков.

А то, о чём вы говорите, это сферический верификатор в вакууме.

> А вы продолжаете описывать техники верификации произвольного кода на произвольном языке.

Да, потому что они востребованы.

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

> Другой вопрос, что даже для того чтобы пользоваться такими верификаторами, недостаточно
> знать только алгоритмику и даже ширпотребное ООП. Тут надо разбираться в
> современных системах логического вывода, ИИ и т.п. Иначе просто не получится
> писать код, пригодный для автоматизированной верификации.

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

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

Полностью согласен. Правда, смысла в этой пафосной фразе в данном случае нет никакого. :))

Ответить | Правка | ^ к родителю #48 | Наверх | Cообщить модератору

59. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 25-Дек-10, 11:03 
> Проще? То есть, по-вашему, описание целевой семантики — это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как — поделитесь секретом?

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

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

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

> Гениально! (кстати, я говорил об этом тоже, не знаю, почему вы мне мои же мысли тыкаете) Вот только если бы вы ещё и думали... Во-первых, строить такой верификатор (писать синтаксические средства, библиотеки, организовывать нужным образом код и т.д.) вы на чём будете? На обычных синтаксических средствах?

Вы не знаете, что такое self-hosting? (Вполне достаточно, чтобы на "другом" языке [C, asm и т.п.] было сделано емкое ядро, остальное - селфхостинг).

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

Вы просто плохо знаете предмет. И вам сильно мешают стереотипы.

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

Странно слышать такое от человека, который интересуется OpenBSD.
Вы считаете, что либо всем, либо никому?

Большинством людей вообще информационные технологии не востребованы, если тупо по головам считать.

> А то, о чём вы говорите, это сферический верификатор в вакууме.

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

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

Вы явно путаете факт востребованности и факт существования.

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

Уже давным-давно научились. По крайней мере, все что охватывается первопорядковой логикой (а это вся "классическая" математика, за исключением самой логики или точнее, разных логик, где собственно и начинаются проблемы "селфхостинга"). Другое дело, что математика, которая раньше доказывалась "на бумаге", вообще говоря не была строго формальной. Сама математика используется _другая_ для строгих доказательств. См. интуиционизм и конструктивизм. Что уже говорить о языках программирования.

У вас опять стереотипы и неверная информация.
Есть огромное число людей, которые таким же образом, например, убеждены, что в UNIX-системах отсутствует графика. По крайней мере до широкого раскрута ширпотребных Linux-дистрибутивов так думало большинство, которое об этом что-то слышали. И опять же даже сейчас большинство даже о Линуксе ничего не знают.

А вы все "заинтересованность", "востребованость". Кому надо, те и заинтересованы. И этого вполне достаточно для общего прогресса.

> Вот-вот. Верификация для верификатора получается. А должно быть наоборот. С ваших слов, автомобиль едет для того, чтобы сжигать бензин, а не нефть перерабатывается в бензин для того, чтобы, сжигая его, ехал автомобиль.

Еще раз, это называется self-hosting.

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

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

> Полностью согласен. Правда, смысла в этой пафосной фразе в данном случае нет никакого. :))

Смысл в этой "пафосной фразе" такой, что вы далеко не первый, кому кажется, что он "все-все-все об этом знает".

Ответить | Правка | ^ к родителю #57 | Наверх | Cообщить модератору

62. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от PereresusNeVlezaetBuggy email(ok) on 25-Дек-10, 22:14 
>> Проще? То есть, по-вашему, описание целевой семантики — это просто? Почему же тогда никто ещё не изобрёл такой верификатор, м-м-м? Или это вы только что решили эту задачу, но ещё никто не знает, как — поделитесь секретом?
> Простой в данном случае является не описание семантики, а взаимосвязь отдельных систем.
> Где модуль (система), отвечающий за конкретную семантику, рассматривается как отдельный
> компонент.

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

> Вы пока что к сожалению демонстрируете отсутствие системного мышления, когда у вас
> все детали перемешаны в кучу на одном уровне.

Вы хотите сказать, что мы говорим о разных вещах? Охотно верю. Правда, я понимаю, о чём вы говорите. А вы закопались на своих микрооптимизациях-микроверификациях. Которые НЕ выполнят поставленную изначально задачу (доказательство корректности программы).

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

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

>> Гениально! (кстати, я говорил об этом тоже, не знаю, почему вы мне мои же мысли тыкаете) Вот только если бы вы ещё и думали... Во-первых, строить такой верификатор (писать синтаксические средства, библиотеки, организовывать нужным образом код и т.д.) вы на чём будете? На обычных синтаксических средствах?
> Вы не знаете, что такое self-hosting? (Вполне достаточно, чтобы на "другом" языке
> [C, asm и т.п.] было сделано емкое ядро, остальное - селфхостинг).

Во-первых, то, что вы называете, это не self-hosting. Self-hosting — это, например, у FreePascal, который полностью сам себя собирает.

Во-вторых, как видите, я знаю, о чём вы (хоть и путаясь в терминах) говорите. А вот вы, изначально считая себя умнее собеседника, даже не попытались понять, что же до вас пытаются донести. А донести пытаются то, что это, опять-таки, получается среда "сама в себе". Да, _сравнительно_ легко можно построить специальную среду, в которой доказательство корректности будет производится автоматически. Но если это будет единственное её достоинство, то с тем же успехом её могло бы не быть.

Возможно, при разработке такой среды будут сделаны какие-то ценные наработки, согласен. Но в целом это напоминает Plan9: звучит красиво, а использовать неудобно.

> Многие компиляторы являются таковыми. И здесь мы плавно возращаемся к тому, что
> технологии, используемые для оптимизации во многом идентичны таковым, используемым для
> верификации. Только целевая семантика разная (см выше). Просто большиству нужна только
> скорость и ничего более (см. ниже о большинстве).

Вы путаете верификацию сравнительно простых, компактных конструкций, и верификацию целых моделей. На уровне моделей возникают новые требования, новые спецификации, которые нельзя проверить на уровне модулей. Грубый пример: вот у вас есть два автомобильных колеса и ось. Сами по себе все они могут быть прекрасными. И колёса могут прекрасно стыковаться с осью (верификация на уровне модулей). Но если колёса окажутся разного диаметра, то автомобиль получится косым. Вот только теми способами верификации, про которые вы говорите, это проверить нельзя.

А проверить можно только заранее выстроив модель автомобиля, на каком-то понятном верификатору языке. И это — весьма трудоёмкая работа. Не факт, что вообще полностью решаемая.

> Вы просто плохо знаете предмет. И вам сильно мешают стереотипы.

Что порекомендуете?

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

Почему???

> Вы считаете, что либо всем, либо никому?

Не обязательно. Но давайте я напомню, с чего начался наш с вами разговор?

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

Так вот, хотя методы организации кода существуют, но речь-то изначально шла о конкретике: стек IPSec в ядре OpenBSD. Вы как будто не заметили этого. Потому что из ваших слов, чтобы как-то связать их с исходной темой, я могу сделать только вывод, что опёнковский стек IPSec надо переписать, используя другие "методы организации кода", которые, помимо прочего, по вашему (вроде бы — различать анонимов у меня пока экстрасенсорных способностей не хватает) собственному признанию, включают "специальным образом организованный код, специальные библиотеки. И возможно даже специальные синтаксические средства". То есть фактически вы предлагаете переписать стек IPSec заново. Но какое отношение это будет иметь к верификации текущего стека?! То, что вы предлагаете, это НЕ обеспечение верификации имеющегося кода. Это требование написания НОВОГО кода. По новым правилам.

> Большинством людей вообще информационные технологии не востребованы, если тупо по головам
> считать.

Смотря что понимать под востребованностью... но это уже совсем оффтопик.

>> А то, о чём вы говорите, это сферический верификатор в вакууме.
> Разберитесь в вопросе и попрактикуйтесь, и он перестанет быть для вас сферическим,
> только и всего.

В чём мне следует, по-вашему, попрактиковаться?

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

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

>> Компьютеры, между прочим, до сих пор толком не научились математические теоремы доказывать.
>> Хотя в этом направлении работы ведутся намного дольше, чем над верификацией программ на обычных ЯП.
> Уже давным-давно научились. По крайней мере, все что охватывается первопорядковой логикой
> (а это вся "классическая" математика, за исключением самой логики или точнее,
> разных логик, где собственно и начинаются проблемы "селфхостинга"). Другое дело, что
> математика, которая раньше доказывалась "на бумаге", вообще говоря не была строго
> формальной. Сама математика используется _другая_ для строгих доказательств. См. интуиционизм
> и конструктивизм. Что уже говорить о языках программирования.

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

> У вас опять стереотипы и неверная информация.
> Есть огромное число людей, которые таким же образом, например, убеждены, что в
> UNIX-системах отсутствует графика. По крайней мере до широкого раскрута ширпотребных Linux-дистрибутивов
> так думало большинство, которое об этом что-то слышали. И опять же
> даже сейчас большинство даже о Линуксе ничего не знают.

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

> А вы все "заинтересованность", "востребованость". Кому надо, те и заинтересованы. И этого
> вполне достаточно для общего прогресса.

Повторюсь, вы сами изначально перепутали решение одной конкретной задачи (верификация кода IPSec-стека OpenBSD) с другой (создание системы для написания кода, позволяющей писать автоматически или хотя бы автоматизированно доказываемые программы).

>> Вот-вот. Верификация для верификатора получается. А должно быть наоборот. С ваших слов, автомобиль едет для того, чтобы сжигать бензин, а не нефть перерабатывается в бензин для того, чтобы, сжигая его, ехал автомобиль.
> Еще раз, это называется self-hosting.

Нет, это называется "лошадь с телегой местами перепутали".

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

Видимо, вы не поняли аналогию. Кто из нас после этого узко мыслит? :)

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

Да что вы говорите...

>> Полностью согласен. Правда, смысла в этой пафосной фразе в данном случае нет никакого. :))
> Смысл в этой "пафосной фразе" такой, что вы далеко не первый, кому
> кажется, что он "все-все-все об этом знает".

Мне так не кажется. В отличие от вас.

Попробую резюмировать:

1. Изначальную задачу предлагаемые вами средства НЕ решают.

2. Тем не менее, они работоспособны.

3. Но насколько они подходят для решения реальных задач? Если такая автоматическая верификация будет требовать в 100 раз большие по размерам накладные расходы (как-то: вычислительные мощности, трудозатраты на описание модели, уменьшение производительности труда каждого отдельно взятого кодера и т.д.), то вопрос о практической ценности такого решения будет стоять весьма остро.

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

А ненужное отмирает. Закон жизни.

Ответить | Правка | ^ к родителю #59 | Наверх | Cообщить модератору

63. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 26-Дек-10, 20:45 
> <...> Но давайте я напомню, с чего начался наш с вами разговор?
>
> "Хотя на самом деле "на данном этапе развития средств анализа", и даже еще гораздо раньше, существуют уже достаточно методов организации кода таким образом, чтобы было возможно доказывать его правильность с помощью автоматизированных средств доказательств и анализа."
>
> Так вот, хотя методы организации кода существуют, но речь-то изначально шла о конкретике: стек IPSec в ядре OpenBSD. Вы как будто не заметили этого.
>
>То есть фактически вы предлагаете переписать стек IPSec заново. Но какое отношение это будет иметь к верификации текущего стека?! То, что вы предлагаете, это НЕ обеспечение верификации имеющегося кода. Это требование написания НОВОГО кода. По новым правилам.
>
> Повторюсь, вы сами изначально перепутали решение одной конкретной задачи (верификация кода IPSec-стека OpenBSD) с другой (создание системы для написания кода, позволяющей писать автоматически или хотя бы автоматизированно доказываемые программы).

Нет, я ничего не перепутал, я именно об этом и говорил. И вы только что подтвердили, что вы прекрасно поняли, о чем я говорил. Ну разве что не обязательно переписывать, можно произвести рефакторинг. Для этого тоже есть автоматизированные средства. Какой ужас! По новым правилам! Да, для некоторых это страшный сон.

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

(Хотя конечно, если для вас "темой" является верификация стека - флаг вам в руки и успешного долбления головой "апстену".)

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

> Вы путаете верификацию сравнительно простых, компактных конструкций, и верификацию целых моделей. На уровне моделей возникают новые требования, новые спецификации, которые нельзя проверить на уровне модулей. Грубый пример: вот у вас есть два автомобильных колеса и ось. .........

Почему нельзя? Может можно, да вы не знаете как.
Колеса и ось - это никакие не модули! Это физические объекты! Вы вообще не представляете себе что такое модули, раз такие аналогии приводите! (См. ниже)

Модель сложная? Ну так упростите! Анализ для чего нужен? Абстрагирование (как способность) зачем человеку дана?

> Вот вы и смешиваете разные уровни в один. Доказать корректность одного модуля ещё как-то можно (хотя уже тут зачастую приходится использовать либо специальные языки — про это я уже говорил, — либо NP-полные решения — тупой перебор всех возможных комбинаций входных параметров).

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

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

И кто вам говорил про необходимость NP-полных решений? Вы вообще представляете себе весь диапазон применения дедуктивных систем и прочего "ИИ"? Кроме "полных доказательств".

> А проверить можно только заранее выстроив модель автомобиля, на каком-то понятном верификатору языке. И это — весьма трудоёмкая работа. Не факт, что вообще полностью решаемая.

Трудоемко? Ай ай ай! Специальные языки, говорите, придется учить? А как вы хотели? Все на С? Ну нетривиально это точно. А вот степень трудоемкости зависит от умения проектировать и моделировать. По краней мере не так безнадежно, как верификация "традиционного" кода. Просто вы об этом ничего не знаете.

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

> Компьютеры, между прочим, до сих пор толком не научились математические теоремы доказывать.
>
>> Уже давным-давно научились. По крайней мере, все что охватывается первопорядковой логикой (а это вся "классическая" математика, за исключением самой логики или точнее, разных логик, где собственно и начинаются проблемы "селфхостинга"). ...............
>>
> О, прогресс. Печально, что если не спровоцировать (каюсь, фраза про "толком не научились" была провокацией), вы ничего толком сказать не можете, отделываясь безосновательными утверждениями.

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

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

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

>> Во-первых, то, что вы называете, это не self-hosting. Self-hosting — это, например, у FreePascal, который полностью сам себя собирает.

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

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

> Вот-вот. Верификация для верификатора получается. А должно быть наоборот. С ваших слов, автомобиль едет для того, чтобы сжигать бензин, а не нефть перерабатывается в бензин для того, чтобы, сжигая его, ехал автомобиль.
>
>> Еще раз, это называется self-hosting.
>
> Нет, это называется "лошадь с телегой местами перепутали".

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

>> А в аналогии с автомобилем вы путаете энергоноситель с механизмом. Тогда по-вашему получается, что компилятор, собирающий себя - это тоже автомобиль ради бензина?
>
> Видимо, вы не поняли аналогию. Кто из нас после этого узко мыслит? :)

Ну да, конечно. Стоит вам лажануться, как оказывается, что либо у вас это была "провокация", либо вас не поняли.

> Во-вторых, как видите, я знаю, о чём вы (хоть и путаясь в терминах) говорите.

Да уж, оно видно, как вы "знаете".

Ответить | Правка | ^ к родителю #62 | Наверх | Cообщить модератору

49. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от Аноним (??) on 24-Дек-10, 12:29 
>Можно только представить, что творится во FreeBSD. И уж тем более в Linux.

Это очень важная проблема всех больших проектов: полностью то, что в них творится, реально понимает от силы 1-2 человека.

Ответить | Правка | ^ к родителю #43 | Наверх | Cообщить модератору

58. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от anonymous vulgaris on 25-Дек-10, 08:15 
>Существует множество способов, как это могло бы быть сделано, от простых и очевидных  до еле уловимых и изощренных. Возможно создать что-то, что выглядит как простая ошибка в коде и назначение которой будет невозможно доказать.

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

Ответить | Правка | ^ к родителю #40 | Наверх | Cообщить модератору

51. "Поверхностный аудит OpenBSD пока не выявил наличие бэкдора"  +/
Сообщение от upyx (ok) on 24-Дек-10, 13:15 
Есть у меня подозрение, что этот вброс неспроста. Бэкдора может никогда и не было... Мозила и Гугель не мало денег выплачивают за поиск дырок, а тут... ;)
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема




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

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