Показано с 1 по 1 из 1.

Австралийские ученые создали микроядро с формально подтвержденным уровнем защиты

  1. #1
    Global Moderator Репутация Репутация Репутация Репутация Репутация Репутация Репутация Репутация Репутация Репутация Репутация Аватар для ALEX(XX)
    Регистрация
    31.03.2005
    Адрес
    Чернигов
    Сообщений
    10,777
    Вес репутации
    3704

    Австралийские ученые создали микроядро с формально подтвержденным уровнем защиты

    Австралийские ученые нашли способ формального доказательства отсутствия ошибок в ядре операционной системы. Согласно их заявлению, это первый случай, когда удалось математически строго показать корректность ядра для операционных систем общего назначения – ранее подобные проверки осуществлялись только для небольших ядер, пригодных только для теоретических исследований.
    Ядро seL4 (secure embedded L4), которое первым прошло формальную проверку защищенности, создано в австралийской частной исследовательской организации NICTA. В разработке ядра, состоящего из 7500 строк на языке C, и методов доказательства его корректности также приняли участие сотрудники университета Нового Южного Уэльса (Австралия). Вдобавок к этому, сама методика проверки корректной работы ядра основана на технологии Isabelle, которую Лоуренс Полсон (Lawrence Paulson), профессор вычислительной логики из Кембриджского университета (Великобритания), разработал для проверки корректности программ общего назначения.
    Найденное математически строгое доказательство корректной работы ядра может получить самые широкие последствия для всей индустрии разработки программного обеспечения. Благодаря появлению формального критерия корректности разработчики смогут создавать действительно надежные прикладные алгоритмы и системные программы. Так, ядро seL4, созданное в центре NICTA, с большой вероятностью может получить применение в критически важных системах, включая авиацию и автомобили.
    Следует заметить, что формальной проверкой программных систем занимаются множество научных коллективов в разных странах мира. Например, в Германии подобную задачу решает проект Verisoft. Новизна разработок NICTA заключается в отходе от традиционной методики формального подтверждения конкретных свойств системы на примере отдельных фрагментов ядра. В новой работе используется методика генерализованного, универсального доказательства корректной реализации всех заявленных в системе функций.
    Благодаря новой методике проверки корректности новое ядро seL4 для встраиваемых систем устойчиво к большинству известных видов атак, в том числе к атакам на переполнение буфера, как утверждают разработчики. Работа над этим ядром и критериями формальной проверки заняла четыре года, а результаты переданы фирме Open Kernel Labs, специально созданной для дальнейшего развития этих результатов и создания защищенных ядер и микроядер для критически важных систем.
    Подробнее о ядре seL4 для встраиваемых систем общего назначения и революционных результатах исследователей NICTA в области проверки системных и прикладных алгоритмов можно прочитать на официальном сайте

    securitylab.ru
    Left home for a few days and look what happens...

  2. Реклама
     

Похожие темы

  1. Ответов: 0
    Последнее сообщение: 29.09.2010, 13:23
  2. Японские ученые создали осязаемые голограммы
    От kps в разделе Высокие технологии
    Ответов: 0
    Последнее сообщение: 12.08.2009, 12:16
  3. Ученые создали DVD-диск на 42 Гб
    От kps в разделе Высокие технологии
    Ответов: 0
    Последнее сообщение: 05.07.2008, 23:13
  4. Ученые создали шину для квантового компьютера
    От ALEX(XX) в разделе Высокие технологии
    Ответов: 0
    Последнее сообщение: 01.10.2007, 09:10
  5. Американские ученые создали нано-память
    От ALEX(XX) в разделе Высокие технологии
    Ответов: 1
    Последнее сообщение: 27.09.2007, 14:59

Метки для этой темы

Свернуть/Развернуть Ваши права в разделе

  • Вы не можете создавать новые темы
  • Вы не можете отвечать в темах
  • Вы не можете прикреплять вложения
  • Вы не можете редактировать свои сообщения
  •  
Page generated in 0.01187 seconds with 18 queries