The OpenNET Project / Index page

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

На базе гипервизора seL4 создана платформа для создания высокозащищённых систем

28.01.2011 14:59

Австралийский исследовательский центр NICTA в сотрудничестве с организацией Open Kernel Labs после семи лет разработки представил основанную на микроядре seL4 платформу для обеспечения повышенного уровня безопасности критически важных систем. Принцип работы платформы сводится к полной изоляции работы групп приложений за счёт использования низкоуровневого гипервизора, задачи которого выполняет микроядро seL4. В отличие от классических систем виртуализации, микроядро seL4 является предельно минималистичным и его надёжность доказана математически.

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

Для загрузки доступен пакет, включающий основанное на открытом проекте OKL4 микроядро seL4 в сборке для архитектур ARM11 и x86, документацию, библиотеки для создания приложений, примеры кода и специальный пара-виртуализированный вариант Linux. Все наработки проекта можно использовать свободно, но при условии некоммерческого применения.

  1. Главная ссылка к новости (http://www.nicta.com.au/news/h...)
  2. OpenNews: Релиз открытой микроядерной ОС Genode 10.08
  3. OpenNews: Виртуальный десктоп для смартфонов
  4. OpenNews: Гипервизор для запуска Android на телефонах и симулятор Android в Moblin
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/29414-virtual
Ключевые слова: virtual, secrutiy, limit
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (24) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, pavlinux (ok), 15:17, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    > его надежность доказана математически.

    По их мнению, надёжность это то:
    > что написанный код удовлетворяет всем тем спецификациям,
    > которые были заложены на этапе проектирования.

    Как мы видим, это не спасает это от ошибок проектирования.

     
     
  • 2.3, non anon (?), 15:25, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >> его надежность доказана математически.
    >По их мнению, надёжность это то:

    Чтобы понять соль данной шутки, нужно иметь хотя бы общее представление о теоремах Гёделя ;-)

     
     
  • 3.4, pavlinux (ok), 15:46, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Так вроде решили этот гиммор, и кстати кто-то из наших.


     
     
  • 4.5, Анонимиус (?), 16:02, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на базе Debian/Ubuntu.
    Не знаешь чего-нибудь подобного?

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

    Как это вообще устроено?

     
     
  • 5.15, pavlinux (ok), 23:50, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    > Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на
    > базе Debian/Ubuntu.

    Qubes мож? То, что Рутковска в том году обещалась сделать супер-пупер изолированный Линух?!

    > Как это вообще устроено?

    Как, как, ... как и все виртуалки - гипервизор и разделение памяти.

     
     
  • 6.21, Анонимиус (?), 16:20, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Да, он самый.
    То, что виртуалки - это ясно. Мне другое не ясно:
    как регулировать, какому приложению можно получать доступ к буферу обмена, а какому нельзя?
     
     
  • 7.22, pavlinux (ok), 19:30, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    > Да, он самый.
    > То, что виртуалки - это ясно. Мне другое не ясно:
    > как регулировать, какому приложению можно получать доступ к буферу обмена, а какому
    > нельзя?

    Ну, этой темы на семестр лекций хватит

    http://secure.wikimedia.org/wikipedia/en/wiki/Memory_barrier

     
     
  • 8.24, Анонимиус (?), 04:10, 30/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Ну, я не про такие низкоуровневые вещи спрашиваю Мне интересно, чем можно сказа... текст свёрнут, показать
     
     
  • 9.25, pavlinux (ok), 05:54, 30/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Пока не придумали Это надо всю ОСь переделывать ну или хотя бы диспетчер памят... текст свёрнут, показать
     
  • 4.11, анон (?), 20:12, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Теоремы Геделя, внезапно, были доказаны Геделем. Великий тролль был.

    И поныне одно из важнейших применений его теорем о неполноте - троллинг математиками своих коллег и (особенно) нубов.

    Первая теорема используется для троллинга тех, кто собирается доказать что-то очень сложное и неочевидное (она гласит: в любой непротиворечивой аксиоматике можно построить такое истинное утверждение, что его нельзя будет ни доказать, ни опровергнуть в рамках этой аксиоматики). Т.е. в математике могут существовать вещи, которые в принципе нельзя доказать.

    Вторая теорема используется для троллинга тех, кто уже что-то доказал и теперь этим гордится (она гласит, что для непротиворечивой аксиоматики, ее непротиворечивость не может быть доказана ее собственными стредствами). Одно из интереснейших ее следствий - то, что корректность математики и всего, что на ней основано, не может быть доказана. В математику можно только верить. Или не верить. Но такая ситуация http://xkcd.ru/816/ в принципе не исключена. И поэтому любое утверждение, формально доказанное, но не проверенное эмпирически, может запросто оказаться и ложным.

     
     
  • 5.18, fr0ster (ok), 10:10, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Использование принципа Гёделя для троллинга нарушает принцип Оккама :)
     

  • 1.2, non anon (?), 15:23, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    >Принцип работы платформы сводится к полной изоляции работы групп приложений за счет использования низкоуровневого гипревизора, задачи которого выполняет микроядро seL4.

    Это типа os cubes на микроядре?

    Кстати, интересно, можно ли замутить такое на hurd (насколько я знаю, это наиболее живой из открытых микроядерных проектов).

    >В отличие от классических систем виртуализации микроядро seL4 является предельно минималистичным и его надежность доказана математически.

    Зачёт за тонкий юмор :-)

     
  • 1.6, User294 (ok), 16:12, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    > микроядро seL4 является предельно минималистичным и его надежность доказана математически.

    Молодцы, они осознали наконец что если ядро нихрена не умеет - то и глючить там будет нечему. Hello world, кстати, тоже вполне себе надежная программа. Проблема только в том что ни само по себе ядро L4, ни hello world никому не нужны. А вот за надежность готовой системы в целом эти исследователи явно отвечать не захотят, что собссно и является некоей проблемой :). В итоге будет возможно 2 варианта: "нифига не умеет и поэтому никому не нужно" и "за глюки чужого софта мы не отвечаем!" :)

     
     
  • 2.9, Аноним (-), 18:20, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +3 +/
    > Hello world, кстати, тоже вполне себе надежная программа

    Классический - ни разу. Надёжный hello, world занимает страницу кода где-то.

     
     
  • 3.14, User294 (ok), 23:08, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    > Классический - ни разу

    Да ладно вам. Там нет выделений памяти, а инициализацию и библиотеки можно подсунуть в духе тех которые используются в параиноидальной эмбеддовке, где обламываться тупо нечему. Ненадежность сторонних либ, системных вызовов, etc - не есть ненадежность программы, так что отмазка в духе аффтаров seL4 вполне прокатит имхо :)))

     
     
  • 4.16, pavlinux (ok), 23:55, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Не гони mmap видишь code execve a out , a out , 90 vars 0... большой текст свёрнут, показать
     

  • 1.7, Аноним122333 (?), 17:22, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • –3 +/
    > Все наработки проекта можно свободно использовать, при условии некоммерческого применения.

    надо было эту фразу первой написать... и после этого новость сразу можно не читать :-)

    ...технологии котореые можно использовать для только как "студентеские игрушки" -- не нужны. ибо любой студент рано или позно заканчивает быть студентом :-)

     
     
  • 2.19, Аноним123321 (ok), 12:45, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • –3 +/
    минусов наставили, а никто причину не откомментировал.... видимо студенты-вендузятники зашли на сайт :-)
     
     
  • 3.20, Andrey Mitrofanov (?), 15:32, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Видимо, большая часть "посетителей сайта" считает несвободность для коммерческого использования... краеугольным камнем нашей демократии. Борется за неё и всячески поддерживает (=минусует). И нет, виндузятники тут не при чём.

    ЗЫЖ Минусуйте меня. Нежно!

     
     
  • 4.23, non anon (?), 21:05, 29/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    Смею предположить, что большая часть посетителей этого сайта являются пользователями/администраторами ПО, а не представителями коммерческих софтовых компаний.
    Поэтому их свободу данные ограничения никак не затрагивают. Жаловаться на несвободность данного ПО могут только коммерсанты.
     

  • 1.8, vadiml (ok), 18:04, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    > его надежность доказана математически

    Это при условии что в программе, которая занимается проверками, тоже нет ошибок.

     
     
  • 2.12, анон (?), 20:17, 28/01/2011 [^] [^^] [^^^] [ответить]  
  • +/
    >> его надежность доказана математически
    > Это при условии что в программе, которая занимается проверками, тоже нет ошибок.

    Ну хоть кто-то, ну хотя бы поверхностно, оценил сей жестокий прикол ;)

     

  • 1.10, Аноним (-), 19:14, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > Например, можно обеспечить работу на смартфоне системы для доступа к закрытой информации с обычными мобильными приложениями.

    Сейчас это делают, применяя специальные процессоры. Например, Broadcom 5892:

    http://www.broadcom.com/products/Security/Point-of-Sale/BCM5892

    "The BCM5892/BCM5893 has advanced security features, including Secure Processing Architecture (SPA) that enforces a security boundary between secure and open applications within the device. The secure mode provides an environment where only trusted application code can be executed. The BCM5892/BCM5893 can simultaneously operate in both secure and open mode without compromising the integrity of the secure application."

     
  • 1.13, Аноним (-), 20:33, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    да, но математика это не наука в понимании Галлилея - наблюдение, опыт, заключение, очень характерен период развития теории множеств(огромное кол-во парадоксов- яркий пример парадокс Рассела, о том что множество не может быть элементов своего множества)
    математика это сила ума - созерцание, следовательно найдется такой человек который опровергнет данную систему в виде надежности - просто нужно время.
     

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



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

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