The OpenNET Project / Index page

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

Найден способ формального подтверждения 100% отсутствия ошибок в программе

14.08.2009 12:29

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

Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание было пройдено успешно и достигнуто 100% соответствие предъявляемым требованиям.

Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.

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

Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP). Также ожидается, что NICTA передаст все интеллектуальные права на результаты исследования opensource компании Open Kernel Labs.

  1. Главная ссылка к новости (http://tech.slashdot.org/story...)
  2. The L4.verified project
  3. Hypervisor technology claimed 100 percent bug-free
Автор новости: blkdog
Лицензия: CC-BY
Тип: К сведению
Короткая ссылка: https://opennet.ru/23011-code
Ключевые слова: code, verify
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (32) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним (-), 12:51, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    что-то они там упустили
     
  • 1.2, AlexanderYT (?), 12:56, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    Ну ты им расскажи об этом.
     
  • 1.3, Aleksey (??), 13:03, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    У нас сегодня определенно день надуманных новостей. В тексте новости явно рассказано, что исследователям удалось создать первое ядро системы для которого для которого было проведено доказательство 100% соответствия тех.заданию. (First Formally-Proven OS Kernel).

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

     
     
  • 2.4, Aleksey (??), 13:04, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +3 +/
    И как правильно заметили в комментарии к исходной новости:

    It only means it meets the spec, not that the spec is correct ...

    It does not mean that the faulty or erratic hardware cannot crash the system

    It does not mean that other programs cannot crash and lose your data ...

    It does not mean that buggy device drivers can make your system unusable

    It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...

     
     
  • 3.6, dq0s4y71 (?), 13:20, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Ну и нормально. И хорошо, что пока еще не изобрели методику, которая за меня определяет _что_ я хочу. :)
     
  • 3.43, Vkni (ok), 03:26, 11/06/2020 [^] [^^] [^^^] [ответить]  
  • +/
    > only that it will always do what it is supposed to

    Скорее, что она работает не выходя за рамки спецификации... Это не совсем "supposed to".

    Скажем, практически все спецификации на сортировку будут удовлетворены командами sort | uniq. А значительная часть спецификаций из всяких самоучителей вообще пропустит такую функцию сортировки:

    sort :: Ord a => [a] -> [a]
    sort _ = []

    Нельзя ведь сказать, что результат выполнения этой функции неотсортирован!

     
  • 2.26, anonymous (??), 15:42, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.

    Вот-вот. Поправьте новость уже, без слез смотреть нельзя.

     

  • 1.5, anonimous (?), 13:17, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    Риторический вопрос: как верифицировать верификатор?
     
     
  • 2.10, zazik (ok), 13:48, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    Первый вопрос, который пришёл в голову. Лем очень неплохо в Ананке над верификаторами постебался.
     
  • 2.23, nathoo (?), 15:21, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +2 +/
    примерно так же, как компилируют компиляторы: первым делом ;-)
     
  • 2.24, anonymous (??), 15:24, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    > Риторический вопрос: как верифицировать верификатор?

    Так ведь как обычно. Выбрать аксиоматику (ту же ZFC) и пожалуйста, в бой.

     
  • 2.29, Andrew Kolchoogin (?), 20:53, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    Никак. "Проблема обнаружения закладки в компиляторе" неразрешима.
     
     
  • 3.41, Аноним (-), 16:12, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Очередное ламерство от вас :(
     

  • 1.7, FractalizeR (ok), 13:21, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    И все равно непонятно, что именно доказано?
    >математически доказать, что определенное ПО не содержит ошибок

    Слишком общая формулировка. Никакой конкретики.

     
     
  • 2.8, Аноним (8), 13:28, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >И все равно непонятно, что именно доказано?

    Доказано соответствие спецификации.

     

  • 1.11, white_raven (?), 13:50, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    А кто будет отлавливать баги в Isabelle???
     
  • 1.12, psyhomo (?), 13:50, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    ого! (просто нет других слов)
     
  • 1.13, fooser (?), 13:52, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Пускай программу проверки проверят ею же. не исключено что программа не пройдет проверки корректности ;)
     
  • 1.14, uZver (??), 14:09, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    +1. Если они действительно смогут математически доказывать корректность программы, то это уменьшит количество проблем и багов на порядок.
     
     
  • 2.15, Имя (?), 14:26, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    Это смотря кем ещё программа написана. Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.
     
     
  • 3.20, psyhomo (?), 15:01, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    Угу. Вечный вопрос - "можно ли математически описать хаос?". Как-то тоже пришлось поглядеть на творчество и фантазию "программных гениев" изнутри.
     
  • 3.31, uZver (??), 21:53, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    > Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.

    дык в этом случае пофигу - прописать в ТЗ что код должен проходить анализ. Потому сдыхание анализатора это несоответствие ТЗ, а сам програмер идет переучиваться.

     
  • 2.22, Aleksey (??), 15:15, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Выдержка из с их страницы (statistic):
    =======
    Сколько строк было проверено?
    > 7500 строк на C. Пока не проверен эсемблерный код и код, ответственный за загрузку (1200 строк)

    Насколько большое получилось доказательство?

    Около 200000 строк кода на языке доказательств Isabelle. Весь код доказательства был написан вручную с последующей машинной проверкой. В сумме это приблизительно 3500 страниц формата A4, если его распечатать (высота распечатки будет около полуметра высотой).

    Это одно из самых больших формальных доказательств из когда-либо сделаных. Для примера, известная теорема о четырех красках (которая тоже была доказана машиной) состояла из 60000 строк в доказательстве теоремы. Единственное известное доказательство, которое больше этого принадлежит проекту Verisoft (они сообщают о 245000 строк доказательства). И конечно, в математике, чем меньше доказательство, тем оно понятнее :)
    =======

    Так что ни о каком прорыве в программировании речи не идет.

     
     
  • 3.32, uZver (??), 21:55, 14/08/2009 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Так что ни о каком прорыве в программировании речи не идет.

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

     

  • 1.30, Slava_K (?), 21:32, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    >> Итоговый анализ выполняется с помощью интерактивной программы Isabelle

    А кто проверит Isabelle? Вдруг там ошибка?

     
  • 1.33, аноним (?), 23:36, 14/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая проблема в общем случае
     
     
  • 2.42, Vkni (ok), 03:20, 11/06/2020 [^] [^^] [^^^] [ответить]  
  • +/
    +1

    Новость в стиле "учёный изнасиловал журналиста". Проверка спецификации, кстати, отдельная задача. ;-)

     

  • 1.35, Качатель (?), 19:37, 15/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы для её проверки на соответствие с КОДОМ.
     
  • 1.36, FrBrGeorge (ok), 08:16, 16/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, с помощью которого доказывается непротиворечивость этой теории.
     
     
  • 2.38, nuclight (??), 15:00, 18/08/2009 [^] [^^] [^^^] [ответить]  
  • +/
    >Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий,
    >с помощью которого доказывается непротиворечивость этой теории.

    Это напрямую запрещено теоремой Гёделя.

     
     
  • 3.40, Аноним (-), 15:31, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Достаточно богата еще не значит полна. С Геделем все ОК )
     

  • 1.37, Онаним (?), 16:17, 17/08/2009 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    А если наша Гостехкомиссия (или кто там щас вместо неё) будет юзать эту штуку - время выдачи сертификата уменьшится или увеличится?

     

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



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

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