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

image

Теги: ядро, защита

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

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

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

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

Следует заметить, что формальной проверкой программных систем занимаются множество научных коллективов в разных странах мира. Например, в Германии подобную задачу решает проект Verisoft. Новизна разработок NICTA заключается в отходе от традиционной методики формального подтверждения конкретных свойств системы на примере отдельных фрагментов ядра. В новой работе используется методика генерализованного, универсального доказательства корректной реализации всех заявленных в системе функций.

Благодаря новой методике проверки корректности новое ядро seL4 для встраиваемых систем устойчиво к большинству известных видов атак, в том числе к атакам на переполнение буфера, как утверждают разработчики. Работа над этим ядром и критериями формальной проверки заняла четыре года, а результаты переданы фирме Open Kernel Labs, специально созданной для дальнейшего развития этих результатов и создания защищенных ядер и микроядер для критически важных систем.

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


или введите имя

CAPTCHA
Страницы: 1  2  
Зладей
18-08-2009 12:51:22
Хммм... а интерфесы у него какие? К Линуксу прикрутить можно?
0 |
Серый кардинал BHC
20-08-2009 18:14:53
Интересно, что и как они доказали, с учетом: ... Простейшим примером алгоритмически неразрешимой массовой проблемы является так называемая проблема применимости алгоритма (называемая также проблемой остановки). Она состоит в следующем: требуется найти общий метод, который позволял бы для произвольной машины Тьюринга (заданной посредством своей программы) и произвольного начального состояния ленты этой машины определить, завершится ли работа машины за конечное число шагов, или же будет продолжаться неограниченно долго.
0 |
Kent
18-08-2009 12:58:05
7500 строк на языке CЧто-то как-то маловато. Это точно ядро? Они бы еще Hello world назвали ядром.
0 |
49792
18-08-2009 13:03:54
в minix 2500 строк, для ядра нормально __________________
0 |
rtfm
18-08-2009 13:24:16
в minix 2500 строк, для ядра нормально В MINIX 3 - 4500 строк, но тоже нормально
0 |
65109
18-08-2009 14:32:15
а что надо было ядро на 15 гигов и с GUI ? =
0 |
23541
18-08-2009 21:10:55
Windows 7 ?
0 |
SC
18-08-2009 13:02:34
мм ядро 7,5к строк кода и реальные чуток различаются в масштабах, порядка на 3. Будет ли к ним применим выбранный метод или нет нигде не написано.
0 |
green
18-08-2009 14:14:43
Для ПК маловато. А для ракеты, самолёта, автомобиля самое оно
0 |
s7s
18-08-2009 13:30:51
Если честно я не совсем понял принцип работы. Объясните кто нибудь.
0 |
alf
18-08-2009 13:40:06
А чего непонятного? Пишем 7500 строк на языке C, подводим под это формальные доказательства отсутствия ошибок, пиарим и за бабки внедряем везде где только можно.
0 |
98967
18-08-2009 14:33:47
вы прослушали лекцию умалишенного о построении микроядер. _
0 |
гик
18-08-2009 20:12:14
не придуривайся, что ты не понял иронию даже капча 09648 иронию поняла
0 |
18-08-2009 13:36:53
Кто думает, что 7000 для ядра мало - марш читать мануал по микроядерной архитектуре!
0 |
Страницы: 1  2