В статье "Архитектура 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.me/opennews/art.shtml?num=32296
Неужели началось что-то вменяемое? Очень уж неплохие игроки в этом проекте...
Тут много чего полезного.
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...Прозрачный механизм удаленного обслуживания системных вызовов.
Аннотация
В статье рассматривается подход к удаленному обслуживанию системных вызовов, не требующий
модификации кода пользовательского приложения и операционной системы. Использование
технологии аппаратной виртуализации для перехвата системных вызовов, чтения их параметров
и записи результатов позволяет делегировать обслуживание перехваченных системных вызовов
другой системе: виртуальной, выполняющейся на этом же физическом компьютере, или даже
другой машине в сети. Возможность предоставлять отдельным процессам контролируемый доступ
к ресурсам, к которым сама операционная система доступа не имеет, позволяет эффективно
решать некоторые задачи компьютерной безопасности.
К сожалению, Рубанов из ИСП ушёл. Насколько знаю, некрасиво притом.
а проект то действительно нужный и правильный с соответствующим подходом.
Зыж
почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.
что не понятного то? ребята ценят свободу - а не становятся рабами Столмана.
А еще не быть рабом Стольмана это выгодно, комфортно и удобно!
Ребята не ценят свободу всё же. Или не хотят защищать.
> ребята ценят свободу…проприетарщиков закрывать код.
> а проект то действительно нужный и правильный с соответствующим подходом.
> Зыж
> почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.Наверное потому, что русские любят лицензии *BSD, да и сами в душе - поклонники BSD :)
(Остаётся только надеяться на то, что копирасты не зативоизируют всё опять)
Все что чего-то стоит и можно прибрать к рукам копираст приберет. Это аксиома.Релизили бы под AGPL3 или накрайняк под GPL3 можно бы было быть увереным.
> почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.Чего спрашивать, если понятно?
Если эта разработка ведётся на государственные деньги, то они не в праве вешать какие-то ограничения, которые есть в гпл, т.к. код принадлежит государству и лицензия без ограничений соответствует тому, что этот код принадлежит одинаково каждому. Если разработка спонсируется частным капиталом, то это решение владельца капитала.
Одинаково каждому гражданину данного государства, или ЛЮБОГО государства, даже и того, которое вовсе не платило за разработку? Нельзя ли уточнить эту деталь...
Ну как вы себе в реальности представляете предоставление прав только гражданам какого-то одного государства? Поэтому по факту - получается всем.
>Чего спрашивать, если понятно?была просьба - "хотелось бы комментариев владеющих инфой".
и поскольку вы явно этой инфой не владеете, то просьба к вам - не беспокоится. как бы не хотелось проявить свою "эрудицию". или троллизм. Кому как нравится.
Просьба, а не приказ.Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было.
Проект интересный, надеюсь в будущем место нынешних тестирований и отладок займёт математическая верификация и математическое доказательство безошибочности исходного кода.
> Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть
> открыты без ограничений на использование кем бы то ни было и
> как бы то ни было.А я вот не согласен, чтобы я как налогоплательщик разработку эту оплатил, а потом толстый дядя на майбахе это все себе единолично и копирастично отжал, и в куршавеле шлюх пер на второй раз слупленые с меня деньги.
Хочет переть шлюх в куршавеле - пускай рабов себе нанимает и разрабатывает наново. Иначе сильно жирно получается.
Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами.Не стоит путать группу альтернативщиков, которые ненавидят деньги за то что у них их нет, и серьёзные компании или государство, ориентированные на доступность их наработок для тех, кто хочет продолжить их дело.
> Не стоит путать группу альтернативщиков, которые ненавидят деньгиВы опять пытаетесь мух с котлетами в кучу свалить.
Вопрос в конечной цели Z, возможных исходных точках An и осмысленности необходимых усилий для достижения Z из каждой An.
Microsoft, конечно, очень бы приветствовало вариант а-ля DoD с бумажкой а-ля BSDL. Но для России как для государства этот путь на сейчас существенно менее оправдан, и это понимает не только государство (а оно уже несколько лет как понимает), а и серьёзные компании.
Насчёт налогов: Майкрософт Рус ещё за кидалово с поставками за госсредства вареза (upgrade в волгоградские и не только школы) не ответило, на их месте я бы сидел тихонько и не отсвечивал лишний раз.
Начиная с "Не стоит путать" идёт моё мнение, которое сложилось в ходе общения с представителями открытых сообществ и апологетами СПО, в т.ч. вами. И коммерческие компании это не только Майкрософт Рус.
> Начиная с "Не стоит путать" идёт моё мнение, которое сложилось в ходе
> общения с представителями открытых сообществ и апологетами СПО, в т.ч. вами.Именно поэтому и укорил.
> И коммерческие компании это не только Майкрософт Рус.
Разумеется. Просто другие вроде бы не замечены в попытках манипуляций общественным мнением здесь.
Вообще не рекомендую пытаться бросать тень на плетень: на каждый подобный намёк может найтись гораздо более неприятный public disclosure. Хотите обвинить в чём-либо -- скажите прямо и без попыток всунуть рекламу. Если по существу, так почему ж нет.
Пытаться выровнять несправедливое отношение к Microsoft Corp здесь обычно не стоит: люди по большей части достаточно взрослые и грамотные, чтобы либо не обращать внимания на мелочи, либо поправить вошедшего в раж собеседника. Т.е. своими "защитными" действиями Вы только усугубляете неприязнь к фирме, которая системно применяет ложь как инструмент и затем пытается обелить себя любыми средствами. Пусть исправляют в консерватории.
PS: похоже, не доходит...
> Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами.Пускай пользуются, мне не жалко. Я говорил, если вы не заметили, не о том, что меня зажабило как дядя какой-то в куршавеле бургундское хлещет, а о том что код с "неправильной" лицензией дядя этот заберет у сообщества за спасибо, и не поделится, а все остальные, кто за него своими налогами заплатил лососнут тунца. Компрене ?
>Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было.ванюша из пентагона.
Оригинально. :D
Не займёт. Просто потому что верификация - это, собственно, доказательство соответствия кода некоторой модели. Соответственно, нам нужно иметь гарантированно корректно работающий алгоритм верификации, корректно формализованную модель и корректные предположения, положенные в основу модели. Если с первым ещё можно как-то справиться (скажем, очень большим и развесистым тестированием), то со вторым а особенно с третьим ничего не поделать. Причем описать модель частенько сложнее, чем написать сам код. Вот и думайте, где будет больше ошибок...Верификация - это просто ещё один инструмент, не более. Ничего она не заменит - может только дополнить.
Одна из задач столетия звучит как (моя трактовка): "что проще: решить задачу или доказать что задача имеет/не имеет решения?". Примеры: 2+2, трансдентность числа Пи. Важно не только решение, но и используемый мат.аппарат.
Зато глядишь, и НПП нормальную выпилят, ведь для этого тоже спецы нужны
Верифицировать языки Си и С++ это не правильно, т.к. по сложности они не доступны для понимания. Верифицировать можно только код, написанный на нормальном языке типа pascal.
>Верифицировать можно только код, написанный на нормальном
> языке типа Ada.//obvious fix.
>Верифицировать можно только код, написанный на нормальном языке типа Ada. //obvious fix.Причем в критичных задачах велено использовать толлько его подмножество.
> Верифицировать языки Си и С++ это не правильно, т.к. по сложности они
> не доступны для понимания. Верифицировать можно только код, написанный на нормальном
> языке типа pascal.Для того, чтобы быть нормальным, язык должен быть пригодным к использованию, а не верифицируемым. Несмотря на то, что эти качества не взаимоисключающие, первое качество к pascal явно не относится.