The OpenNET Project / Index page

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

Архитектура системы верификации кода драйверов Linux

14.11.2011 13:15

В статье "Архитектура Linux Driver Verification" (PDF, 700 Кб) представлено описание применимости метода статического анализа кода для проверки корректности драйверов устройств для платформы Linux. Представленный метод позволяет выявить ошибки на основании анализа исходных текстов, без непосредственного выполнения кода. В отличие от традиционных методов тестирования статический анализ кода позволяет проследить сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании.

Проект Linux Driver Verification является открытым и развивается при участии организации Linux Foundation, Института системного программирования Российской Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются в рамках лицензии Apache. Дополнительно подготовлен online-сервис для проверки драйверов. Список выявленных при помощи LDV проблем можно посмотреть на данной странице.

  1. Главная ссылка к новости (http://www.ispras.ru/ru/procee...)
  2. OpenNews: KEDR 0.2 - система для анализа работы модулей Linux-ядра
  3. OpenNews: Доступна предварительная версия стандарта LSB 4.0
  4. OpenNews: В России открылся Центр верификации ОС Linux
Лицензия: CC-BY
Тип: яз. русский / Практикум
Короткая ссылка: https://opennet.ru/32296-linux
Ключевые слова: linux, driver, analyze, debug
При перепечатке указание ссылки на opennet.ru обязательно
Обсуждение (29) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним (-), 15:50, 14/11/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    Неужели началось что-то вменяемое? Очень уж неплохие игроки в этом проекте...
     
     
  • 2.17, pavlinux (ok), 01:26, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Тут много чего полезного.
    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_18_2010_221.php

    Прозрачный механизм удаленного обслуживания системных вызовов.

    Аннотация

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


     

  • 1.2, Michael Shigorin (ok), 16:18, 14/11/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    К сожалению, Рубанов из ИСП ушёл.  Насколько знаю, некрасиво притом.
     
     
  • 2.3, ананим (?), 16:36, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    а проект то действительно нужный и правильный с соответствующим подходом.
    Зыж
    почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.
     
     
  • 3.4, Аноним (-), 18:19, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • –4 +/
    что не понятного то? ребята ценят свободу - а не становятся рабами Столмана.
     
     
  • 4.5, anonymous (??), 18:54, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    А еще не быть рабом Стольмана это выгодно, комфортно и удобно!
     
  • 4.7, Аноним (-), 20:13, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Ребята не ценят свободу всё же. Или не хотят защищать.
     
  • 4.11, arisu (ok), 22:12, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • +2 +/
    > ребята ценят свободу

    …проприетарщиков закрывать код.

     
  • 3.6, Аноним (-), 19:48, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > а проект то действительно нужный и правильный с соответствующим подходом.
    > Зыж
    > почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.

    Наверное потому, что русские любят лицензии *BSD, да и сами в душе - поклонники BSD :)
    (Остаётся только надеяться на то, что копирасты не зативоизируют всё опять)

     
     
  • 4.9, ram_scan (?), 20:46, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Все что чего-то стоит и можно прибрать к рукам копираст приберет. Это аксиома.

    Релизили бы под AGPL3 или накрайняк под GPL3 можно бы было быть увереным.

     
  • 3.15, zhenya_k (?), 23:09, 14/11/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > почему апач? в принципе понятно, но хотелось бы комментариев владеющих инфой.

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

     
     
  • 4.16, Anonym1 (?), 00:15, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Одинаково каждому гражданину данного государства, или ЛЮБОГО государства, даже и того, которое вовсе не платило за разработку? Нельзя ли уточнить эту деталь...
     
     
  • 5.29, Crazy Alex (??), 14:52, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Ну как вы себе в реальности представляете предоставление прав только гражданам какого-то одного государства? Поэтому по факту - получается всем.
     
  • 4.19, ананим (?), 04:39, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >Чего спрашивать, если понятно?

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

     
     
  • 5.21, Ваня (?), 11:17, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Просьба, а не приказ.

    Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было.

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

     
     
  • 6.22, ram_scan (?), 12:20, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть
    > открыты без ограничений на использование кем бы то ни было и
    > как бы то ни было.

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

    Хочет переть шлюх в куршавеле - пускай рабов себе нанимает и разрабатывает наново. Иначе сильно жирно получается.

     
     
  • 7.23, Ваня (?), 12:25, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами.

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

     
     
  • 8.24, Michael Shigorin (ok), 12:31, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Вы опять пытаетесь мух с котлетами в кучу свалить Вопрос в конечной цели Z, воз... текст свёрнут, показать
     
     
  • 9.26, Ваня (?), 12:52, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Начиная с Не стоит путать идёт моё мнение, которое сложилось в ходе общения с ... текст свёрнут, показать
     
     
  • 10.33, Michael Shigorin (ok), 15:59, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Именно поэтому и укорил Разумеется Просто другие вроде бы не замечены в попыт... текст свёрнут, показать
     
  • 8.36, ram_scan (?), 04:44, 16/11/2011 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Пускай пользуются, мне не жалко Я говорил, если вы не заметили, не о том, что м... текст свёрнут, показать
     
  • 6.25, ананим (?), 12:38, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >Я согласен с Женей К., разрабатываемые на государственные деньги проекты должны быть открыты без ограничений на использование кем бы то ни было и как бы то ни было.

    ванюша из пентагона.
    Оригинально. :D

     
  • 6.30, Crazy Alex (??), 14:56, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Не займёт. Просто потому что верификация - это, собственно, доказательство соответствия кода некоторой модели. Соответственно, нам нужно иметь гарантированно корректно работающий алгоритм верификации, корректно формализованную модель и корректные предположения, положенные в основу модели. Если с первым ещё можно как-то справиться (скажем, очень  большим и развесистым тестированием), то со вторым а особенно с третьим ничего не поделать. Причем описать модель частенько сложнее, чем написать сам код. Вот и думайте, где будет больше ошибок...

    Верификация - это просто ещё один инструмент, не более. Ничего она не заменит - может только дополнить.

     
     
  • 7.31, Ваня (?), 15:09, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Одна из задач столетия звучит как (моя трактовка): "что проще: решить задачу или доказать что задача имеет/не имеет решения?". Примеры: 2+2, трансдентность числа Пи. Важно не только решение, но и используемый мат.аппарат.
     
  • 2.18, новичок (??), 02:29, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Зато глядишь, и НПП нормальную выпилят, ведь для этого тоже спецы нужны
     

  • 1.27, q (??), 13:54, 15/11/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Верифицировать языки Си и С++ это не правильно, т.к. по сложности они не доступны для понимания. Верифицировать можно только код, написанный на нормальном языке типа pascal.
     
     
  • 2.28, Andrey Mitrofanov (?), 14:10, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >Верифицировать можно только код, написанный на нормальном
    > языке типа Ada.

    //obvious fix.

     
     
  • 3.37, anonymous vulgaris (?), 23:36, 16/11/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >Верифицировать можно только код, написанный на нормальном  языке типа Ada. //obvious fix.

    Причем в критичных задачах велено использовать толлько его подмножество.

     
  • 2.32, Аноним (-), 15:43, 15/11/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Верифицировать языки Си и С++ это не правильно, т.к. по сложности они
    > не доступны для понимания. Верифицировать можно только код, написанный на нормальном
    > языке типа pascal.

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

     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Спонсоры:
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

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