форумы  помощь  поиск  регистрация  майллист  вход/выход  слежка

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

"Архитектура системы верификации кода драйверов Linux"	+/–
Сообщение от opennews (??) on 14-Ноя-11, 15:50
В статье "Архитектура Linux Driver Verification (http://www.ispras.ru/ru/proceedings/docs/2011/20/isp_20_2011...)" (PDF, 700 Кб) представлено описание применимости метода статического анализа кода для проверки корректности драйверов устройств для платформы Linux. Представленный метод позволяет выявить ошибки на основании анализа исходных текстов, без непосредственного выполнения кода. В отличие от традиционных методов тестирования статический анализ кода позволяет проследить сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании. Проект Linux Driver Verification (http://linuxtesting.ru/project/ldv) является открытым и развивается при участии организации Linux Foundation, Института системного программирования Российской Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются (http://forge.ispras.ru/projects/ldv) в рамках лицензии Apache. Дополнительно под... URL: http://www.ispras.ru/ru/proceedings/archives/isp_20_2011/isp... Новость: http://www.opennet.dev/opennews/art.shtml?num=32296
Ответить | Правка | Cообщить модератору

Сообщения по теме

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

1. "Архитектура системы верификации кода драйверов Linux"	+3 +/–
Сообщение от Аноним (??) on 14-Ноя-11, 15:50
Неужели началось что-то вменяемое? Очень уж неплохие игроки в этом проекте...
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	17. "Архитектура системы верификации кода драйверов Linux"	+1 +/–
	Сообщение от pavlinux (ok) on 15-Ноя-11, 01:26
	Тут много чего полезного. http://www.ispras.ru/ru/proceedings/archives Питерцы тоже рулят!!! http://se.math.spbu.ru/SE http://www.sysprog.info/issues_2010.html --- http://www.ispras.ru/ru/proceedings/archives/isp_18_2010/isp... Прозрачный механизм удаленного обслуживания системных вызовов. Аннотация В статье рассматривается подход к удаленному обслуживанию системных вызовов, не требующий модификации кода пользовательского приложения и операционной системы. Использование технологии аппаратной виртуализации для перехвата системных вызовов, чтения их параметров и записи результатов позволяет делегировать обслуживание перехваченных системных вызовов другой системе: виртуальной, выполняющейся на этом же физическом компьютере, или даже другой машине в сети. Возможность предоставлять отдельным процессам контролируемый доступ к ресурсам, к которым сама операционная система доступа не имеет, позволяет эффективно решать некоторые задачи компьютерной безопасности.
	Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

2. "Архитектура системы верификации кода драйверов Linux"	+1 +/–
Сообщение от Michael Shigorin (ok) on 14-Ноя-11, 16:18
К сожалению, Рубанов из ИСП ушёл.  Насколько знаю, некрасиво притом.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	3. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от ананим on 14-Ноя-11, 16:36
	а проект то действительно нужный и правильный с соответствующим подходом. Зыж почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

	4. "Архитектура системы верификации кода драйверов Linux"	–4 +/–
	Сообщение от Аноним (??) on 14-Ноя-11, 18:19
	что не понятного то? ребята ценят свободу - а не становятся рабами Столмана.
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

	5. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от anonymous (??) on 14-Ноя-11, 18:54
	А еще не быть рабом Стольмана это выгодно, комфортно и удобно!
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	7. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Аноним (??) on 14-Ноя-11, 20:13
	Ребята не ценят свободу всё же. Или не хотят защищать.
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	11. "Архитектура системы верификации кода драйверов Linux"	+2 +/–
	Сообщение от arisu (ok) on 14-Ноя-11, 22:12
	> ребята ценят свободу …проприетарщиков закрывать код.
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	6. "Архитектура системы верификации кода драйверов Linux"	–1 +/–
	Сообщение от Аноним (??) on 14-Ноя-11, 19:48
	> а проект то действительно нужный и правильный с соответствующим подходом. > Зыж > почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой. Наверное потому, что русские любят лицензии *BSD, да и сами в душе - поклонники BSD :) (Остаётся только надеяться на то, что копирасты не зативоизируют всё опять)
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

	9. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от ram_scan on 14-Ноя-11, 20:46
	Все что чего-то стоит и можно прибрать к рукам копираст приберет. Это аксиома. Релизили бы под AGPL3 или накрайняк под GPL3 можно бы было быть увереным.
	Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

	15. "Архитектура системы верификации кода драйверов Linux"	–1 +/–
	Сообщение от zhenya_k on 14-Ноя-11, 23:09
	> почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой. Чего спрашивать, если понятно? Если эта разработка ведётся на государственные деньги, то они не в праве вешать какие-то ограничения, которые есть в гпл, т.к. код принадлежит государству и лицензия без ограничений соответствует тому, что этот код принадлежит одинаково каждому. Если разработка спонсируется частным капиталом, то это решение владельца капитала.
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

	16. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Anonym1 on 15-Ноя-11, 00:15
	Одинаково каждому гражданину данного государства, или ЛЮБОГО государства, даже и того, которое вовсе не платило за разработку? Нельзя ли уточнить эту деталь...
	Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

	29. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Crazy Alex (??) on 15-Ноя-11, 14:52
	Ну как вы себе в реальности представляете предоставление прав только гражданам какого-то одного государства? Поэтому по факту - получается всем.
	Ответить | Правка | ^ к родителю #16 | Наверх | Cообщить модератору

	19. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от ананим on 15-Ноя-11, 04:39
	>Чего спрашивать, если понятно? была просьба - "хотелось бы комментариев владеющих инфой". и поскольку вы явно этой инфой не владеете, то просьба к вам - не беспокоится. как бы не хотелось проявить свою "эрудицию". или троллизм. Кому как нравится.
	Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

	21. "Архитектура системы верификации кода драйверов Linux"	–1 +/–
	Сообщение от Ваня on 15-Ноя-11, 11:17
	Просьба, а не приказ. Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было. Проект интересный, надеюсь в будущем место нынешних тестирований и отладок займёт математическая верификация и математическое доказательство безошибочности исходного кода.
	Ответить | Правка | ^ к родителю #19 | Наверх | Cообщить модератору

	22. "Архитектура системы верификации кода драйверов Linux"	+1 +/–
	Сообщение от ram_scan on 15-Ноя-11, 12:20
	> Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть > открыты без ограничений на использование кем бы то ни было и > как бы то ни было. А я вот не согласен, чтобы я как налогоплательщик разработку эту оплатил, а потом толстый дядя на майбахе это все себе единолично и копирастично отжал, и в куршавеле шлюх пер на второй раз слупленые с меня деньги. Хочет переть шлюх в куршавеле - пускай рабов себе нанимает и разрабатывает наново. Иначе сильно жирно получается.
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

	23. "Архитектура системы верификации кода драйверов Linux"	–1 +/–
	Сообщение от Ваня on 15-Ноя-11, 12:25
	Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами. Не стоит путать группу альтернативщиков, которые ненавидят деньги за то что у них их нет, и серьёзные компании или государство, ориентированные на доступность их наработок для тех, кто хочет продолжить их дело.
	Ответить | Правка | ^ к родителю #22 | Наверх | Cообщить модератору

	24. "Архитектура системы верификации кода драйверов Linux"	+1 +/–
	Сообщение от Michael Shigorin (ok) on 15-Ноя-11, 12:31
	> Не стоит путать группу альтернативщиков, которые ненавидят деньги Вы опять пытаетесь мух с котлетами в кучу свалить. Вопрос в конечной цели Z, возможных исходных точках An и осмысленности необходимых усилий для достижения Z из каждой An. Microsoft, конечно, очень бы приветствовало вариант а-ля DoD с бумажкой а-ля BSDL.  Но для России как для государства этот путь на сейчас существенно менее оправдан, и это понимает не только государство (а оно уже несколько лет как понимает), а и серьёзные компании. Насчёт налогов: Майкрософт Рус ещё за кидалово с поставками за госсредства вареза (upgrade в волгоградские и не только школы) не ответило, на их месте я бы сидел тихонько и не отсвечивал лишний раз.
	Ответить | Правка | ^ к родителю #23 | Наверх | Cообщить модератору

	26. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Ваня on 15-Ноя-11, 12:52
	Начиная с "Не стоит путать" идёт моё мнение, которое сложилось в ходе общения с представителями открытых сообществ и апологетами СПО, в т.ч. вами. И коммерческие компании это не только Майкрософт Рус.
	Ответить | Правка | ^ к родителю #24 | Наверх | Cообщить модератору

	33. "(offtopic) microsoft и 'не только'"	+2 +/–
	Сообщение от Michael Shigorin (ok) on 15-Ноя-11, 15:59
	> Начиная с "Не стоит путать" идёт моё мнение, которое сложилось в ходе > общения с представителями открытых сообществ и апологетами СПО, в т.ч. вами. Именно поэтому и укорил. > И коммерческие компании это не только Майкрософт Рус. Разумеется.  Просто другие вроде бы не замечены в попытках манипуляций общественным мнением здесь. Вообще не рекомендую пытаться бросать тень на плетень: на каждый подобный намёк может найтись гораздо более неприятный public disclosure.  Хотите обвинить в чём-либо -- скажите прямо и без попыток всунуть рекламу.  Если по существу, так почему ж нет. Пытаться выровнять несправедливое отношение к Microsoft Corp здесь обычно не стоит: люди по большей части достаточно взрослые и грамотные, чтобы либо не обращать внимания на мелочи, либо поправить вошедшего в раж собеседника.  Т.е. своими "защитными" действиями Вы только усугубляете неприязнь к фирме, которая системно применяет ложь как инструмент и затем пытается обелить себя любыми средствами.  Пусть исправляют в консерватории. PS: похоже, не доходит...
	Ответить | Правка | ^ к родителю #26 | Наверх | Cообщить модератору

	36. "Архитектура системы верификации кода драйверов Linux"	+2 +/–
	Сообщение от ram_scan on 16-Ноя-11, 04:44
	> Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами. Пускай пользуются, мне не жалко. Я говорил, если вы не заметили, не о том, что меня зажабило как дядя какой-то в куршавеле бургундское хлещет, а о том что код с "неправильной" лицензией дядя этот заберет у сообщества за спасибо, и не поделится, а все остальные, кто за него своими налогами заплатил лососнут тунца. Компрене ?
	Ответить | Правка | ^ к родителю #23 | Наверх | Cообщить модератору

	25. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от ананим on 15-Ноя-11, 12:38
	>Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было. ванюша из пентагона. Оригинально. :D
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

	30. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Crazy Alex (??) on 15-Ноя-11, 14:56
	Не займёт. Просто потому что верификация - это, собственно, доказательство соответствия кода некоторой модели. Соответственно, нам нужно иметь гарантированно корректно работающий алгоритм верификации, корректно формализованную модель и корректные предположения, положенные в основу модели. Если с первым ещё можно как-то справиться (скажем, очень  большим и развесистым тестированием), то со вторым а особенно с третьим ничего не поделать. Причем описать модель частенько сложнее, чем написать сам код. Вот и думайте, где будет больше ошибок... Верификация - это просто ещё один инструмент, не более. Ничего она не заменит - может только дополнить.
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

	31. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Ваня on 15-Ноя-11, 15:09
	Одна из задач столетия звучит как (моя трактовка): "что проще: решить задачу или доказать что задача имеет/не имеет решения?". Примеры: 2+2, трансдентность числа Пи. Важно не только решение, но и используемый мат.аппарат.
	Ответить | Правка | ^ к родителю #30 | Наверх | Cообщить модератору

	18. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от новичок (??) on 15-Ноя-11, 02:29
	Зато глядишь, и НПП нормальную выпилят, ведь для этого тоже спецы нужны
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

27. "Архитектура системы верификации кода драйверов Linux"	–2 +/–
Сообщение от q (??) on 15-Ноя-11, 13:54
Верифицировать языки Си и С++ это не правильно, т.к. по сложности они не доступны для понимания. Верифицировать можно только код, написанный на нормальном языке типа pascal.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	28. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от Andrey Mitrofanov on 15-Ноя-11, 14:10
	>Верифицировать можно только код, написанный на нормальном > языке типа Ada. //obvious fix.
	Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

	37. "Архитектура системы верификации кода драйверов Linux"	+/–
	Сообщение от anonymous vulgaris on 16-Ноя-11, 23:36
	>Верифицировать можно только код, написанный на нормальном  языке типа Ada. //obvious fix. Причем в критичных задачах велено использовать толлько его подмножество.
	Ответить | Правка | ^ к родителю #28 | Наверх | Cообщить модератору

	32. "Архитектура системы верификации кода драйверов Linux"	+1 +/–
	Сообщение от Аноним (??) on 15-Ноя-11, 15:43
	> Верифицировать языки Си и С++ это не правильно, т.к. по сложности они > не доступны для понимания. Верифицировать можно только код, написанный на нормальном > языке типа pascal. Для того, чтобы быть нормальным, язык должен быть пригодным к использованию, а не верифицируемым. Несмотря на то, что эти качества не взаимоисключающие, первое качество к pascal явно не относится.
	Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

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

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