Австралийский исследовательский центр NICTA в сотрудничестве с организацией Open Kernel Labs после семи лет разработки представил основанную на микроядре seL4 платформу (http://ertos.nicta.com.au/software/) для обеспечения повышенного уровня безопасности критически важных систем. Принцип работы платформы сводится к полной изоляции работы групп приложений за счет использования низкоуровневого гипревизора, задачи которого выполняет микроядро seL4. В отличие от классических систем виртуализации микроядро seL4 является предельно минималистичным и его надежность доказана математически (http://www.opennet.me/opennews/art.shtml?num=23011).
Систему планируется использовать в таких областях, как авиационные, медицинские, финансовые и автомобильные программные комплексы, для изоляции критически важных приложений от дополнительных программных компонентов, уязвимость или сбой в которых не должны никаким образом влиять на первичные приложения. Например, можно обеспечить работу на смартфоне сист...URL: http://www.nicta.com.au/news/home_page_content_listing/nicta...
Новость: http://www.opennet.me/opennews/art.shtml?num=29414
> его надежность доказана математически.По их мнению, надёжность это то:
> что написанный код удовлетворяет всем тем спецификациям,
> которые были заложены на этапе проектирования.Как мы видим, это не спасает это от ошибок проектирования.
>> его надежность доказана математически.
>По их мнению, надёжность это то:Чтобы понять соль данной шутки, нужно иметь хотя бы общее представление о теоремах Гёделя ;-)
Так вроде решили этот гиммор, и кстати кто-то из наших.
Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на базе Debian/Ubuntu.
Не знаешь чего-нибудь подобного?Хочу простого - изолировать одни приложения от других на уровне запрета доступа к буферам обменов в различных зонах. Ну, и естественно, с разными корнями.
Как это вообще устроено?
> Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на
> базе Debian/Ubuntu.Qubes мож? То, что Рутковска в том году обещалась сделать супер-пупер изолированный Линух?!
> Как это вообще устроено?
Как, как, ... как и все виртуалки - гипервизор и разделение памяти.
Да, он самый.
То, что виртуалки - это ясно. Мне другое не ясно:
как регулировать, какому приложению можно получать доступ к буферу обмена, а какому нельзя?
> Да, он самый.
> То, что виртуалки - это ясно. Мне другое не ясно:
> как регулировать, какому приложению можно получать доступ к буферу обмена, а какому
> нельзя?Ну, этой темы на семестр лекций хватит
http://secure.wikimedia.org/wikipedia/en/wiki/Memory_barrier
Ну, я не про такие низкоуровневые вещи спрашиваю. Мне интересно, чем можно сказать:
это приложение не имеет права читать содержимое буфера обмена, если на нем стоит атрибут.
А атрибут появился потому, что я номер кредитки выделил мышью в секурном окружении для того, чтобы вставить в секурный браузер банк-клиента.То есть, разделив на зоны безопасности, я хочу регулировать обмен данных между зонами.
> ... чем можно сказать:Пока не придумали. Это надо всю ОСь переделывать (ну или хотя бы диспетчер памяти).
Но ближе всего подобрались OpenVZ и Jail из FreeBSD> это приложение не имеет права читать содержимое буфера обмена, если на нем
> стоит атрибут. А атрибут появился потому, что я номер кредитки выделил мышью
> в секурном окружении для того, чтобы вставить в секурный браузер банк-клиента.
> То есть, разделив на зоны безопасности, я хочу регулировать обмен данных между
> зонами.Ну вот, сам почти и ответил - создаются зоны, разрешением занимается гипервизор.
Теоремы Геделя, внезапно, были доказаны Геделем. Великий тролль был.И поныне одно из важнейших применений его теорем о неполноте - троллинг математиками своих коллег и (особенно) нубов.
Первая теорема используется для троллинга тех, кто собирается доказать что-то очень сложное и неочевидное (она гласит: в любой непротиворечивой аксиоматике можно построить такое истинное утверждение, что его нельзя будет ни доказать, ни опровергнуть в рамках этой аксиоматики). Т.е. в математике могут существовать вещи, которые в принципе нельзя доказать.
Вторая теорема используется для троллинга тех, кто уже что-то доказал и теперь этим гордится (она гласит, что для непротиворечивой аксиоматики, ее непротиворечивость не может быть доказана ее собственными стредствами). Одно из интереснейших ее следствий - то, что корректность математики и всего, что на ней основано, не может быть доказана. В математику можно только верить. Или не верить. Но такая ситуация http://xkcd.ru/816/ в принципе не исключена. И поэтому любое утверждение, формально доказанное, но не проверенное эмпирически, может запросто оказаться и ложным.
Использование принципа Гёделя для троллинга нарушает принцип Оккама :)
>Принцип работы платформы сводится к полной изоляции работы групп приложений за счет использования низкоуровневого гипревизора, задачи которого выполняет микроядро seL4.Это типа os cubes на микроядре?
Кстати, интересно, можно ли замутить такое на hurd (насколько я знаю, это наиболее живой из открытых микроядерных проектов).
>В отличие от классических систем виртуализации микроядро seL4 является предельно минималистичным и его надежность доказана математически.
Зачёт за тонкий юмор :-)
> микроядро seL4 является предельно минималистичным и его надежность доказана математически.Молодцы, они осознали наконец что если ядро нихрена не умеет - то и глючить там будет нечему. Hello world, кстати, тоже вполне себе надежная программа. Проблема только в том что ни само по себе ядро L4, ни hello world никому не нужны. А вот за надежность готовой системы в целом эти исследователи явно отвечать не захотят, что собссно и является некоей проблемой :). В итоге будет возможно 2 варианта: "нифига не умеет и поэтому никому не нужно" и "за глюки чужого софта мы не отвечаем!" :)
> Hello world, кстати, тоже вполне себе надежная программаКлассический - ни разу. Надёжный hello, world занимает страницу кода где-то.
> Классический - ни разуДа ладно вам. Там нет выделений памяти, а инициализацию и библиотеки можно подсунуть в духе тех которые используются в параиноидальной эмбеддовке, где обламываться тупо нечему. Ненадежность сторонних либ, системных вызовов, etc - не есть ненадежность программы, так что отмазка в духе аффтаров seL4 вполне прокатит имхо :)))
>> Классический - ни разу
> Там нет выделений памятиНе гони! mmap видишь?
execve("./a.out", ["./a.out"], [/* 90 vars */]) = 0
brk(0) = 0x602000
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f87ac4f9000
access("/etc/ld.so.preload", R_OK) = 0
open("/etc/ld.so.preload", O_RDONLY) = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=0, ...}) = 0
close(3) = 0
open("/etc/ld.so.cache", O_RDONLY) = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=124158, ...}) = 0
mmap(NULL, 124158, PROT_READ, MAP_PRIVATE, 3, 0) = 0x7f87ac4da000
close(3) = 0
open("/lib64/libc.so.6", O_RDONLY) = 3
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0\320\354\1\0\0\0\0\0"..., 832) = 832
fstat(3, {st_mode=S_IFREG|0755, st_size=1482288, ...}) = 0
mmap(NULL, 3591112, PROT_READ|PROT_EXEC, MAP_PRIVATE|MAP_DENYWRITE, 3, 0) = 0x7f87abf70000
fadvise64(3, 0, 3591112, POSIX_FADV_WILLNEED) = 0
mprotect(0x7f87ac0d3000, 2097152, PROT_NONE) = 0
mmap(0x7f87ac2d3000, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x163000) = 0x7f87ac2d3000
mmap(0x7f87ac2d8000, 19400, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_ANONYMOUS, -1, 0) = 0x7f87ac2d8000
close(3) = 0
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f87ac4d9000
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f87ac4d8000
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f87ac4d7000
arch_prctl(ARCH_SET_FS, 0x7f87ac4d8700) = 0
mprotect(0x7f87ac2d3000, 16384, PROT_READ) = 0
mprotect(0x600000, 4096, PROT_READ) = 0
mprotect(0x7f87ac4fa000, 4096, PROT_READ) = 0
munmap(0x7f87ac4da000, 124158) = 0
fstat(1, {st_mode=S_IFCHR|0620, st_rdev=makedev(136, 0), ...}) = 0
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f87ac4f8000
write(1, "Hello World!\n", 13Hello World!
) = 13
exit_group(13)
> Все наработки проекта можно свободно использовать, при условии некоммерческого применения.надо было эту фразу первой написать... и после этого новость сразу можно не читать :-)
...технологии котореые можно использовать для только как "студентеские игрушки" -- не нужны. ибо любой студент рано или позно заканчивает быть студентом :-)
минусов наставили, а никто причину не откомментировал.... видимо студенты-вендузятники зашли на сайт :-)
Видимо, большая часть "посетителей сайта" считает несвободность для коммерческого использования... краеугольным камнем нашей демократии. Борется за неё и всячески поддерживает (=минусует). И нет, виндузятники тут не при чём.ЗЫЖ Минусуйте меня. Нежно!
Смею предположить, что большая часть посетителей этого сайта являются пользователями/администраторами ПО, а не представителями коммерческих софтовых компаний.
Поэтому их свободу данные ограничения никак не затрагивают. Жаловаться на несвободность данного ПО могут только коммерсанты.
> его надежность доказана математическиЭто при условии что в программе, которая занимается проверками, тоже нет ошибок.
>> его надежность доказана математически
> Это при условии что в программе, которая занимается проверками, тоже нет ошибок.Ну хоть кто-то, ну хотя бы поверхностно, оценил сей жестокий прикол ;)
> Например, можно обеспечить работу на смартфоне системы для доступа к закрытой информации с обычными мобильными приложениями.Сейчас это делают, применяя специальные процессоры. Например, 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."
да, но математика это не наука в понимании Галлилея - наблюдение, опыт, заключение, очень характерен период развития теории множеств(огромное кол-во парадоксов- яркий пример парадокс Рассела, о том что множество не может быть элементов своего множества)
математика это сила ума - созерцание, следовательно найдется такой человек который опровергнет данную систему в виде надежности - просто нужно время.