форумы  помощь  поиск  регистрация  майллист  вход/выход  слежка

Вариант для распечатки		Пред. тема | След. тема
Форум Разговоры, обсуждение новостей
Изначальное сообщение		[ Отслеживать ]

"На базе гипервизора seL4 создана платформа для создания высо..."	+/–
Сообщение от opennews (ok) on 28-Янв-11, 15:17
Австралийский исследовательский центр NICTA в сотрудничестве с организацией Open Kernel Labs после семи лет разработки представил основанную на микроядре seL4 платформу (http://ertos.nicta.com.au/software/) для обеспечения повышенного уровня безопасности критически важных систем. Принцип работы платформы сводится к полной изоляции работы групп приложений за счет использования низкоуровневого гипревизора, задачи которого выполняет микроядро seL4. В отличие от классических систем виртуализации микроядро seL4 является предельно минималистичным и его надежность доказана математически (http://www.opennet.dev/opennews/art.shtml?num=23011). Систему планируется использовать в таких областях, как авиационные, медицинские, финансовые и автомобильные программные комплексы, для изоляции критически важных приложений от дополнительных программных компонентов, уязвимость или сбой в которых не должны никаким образом влиять на первичные приложения. Например, можно обеспечить работу на смартфоне сист... URL: http://www.nicta.com.au/news/home_page_content_listing/nicta... Новость: http://www.opennet.dev/opennews/art.shtml?num=29414
Ответить | Правка | Cообщить модератору

Сообщения по теме

[Сортировка по времени | RSS]

1. "На базе гипервизора seL4 создана платформа для создания высо..."	–1 +/–
Сообщение от pavlinux (ok) on 28-Янв-11, 15:17
> его надежность доказана математически. По их мнению, надёжность это то: > что написанный код удовлетворяет всем тем спецификациям, > которые были заложены на этапе проектирования. Как мы видим, это не спасает это от ошибок проектирования.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	3. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от non anon on 28-Янв-11, 15:25
	>> его надежность доказана математически. >По их мнению, надёжность это то: Чтобы понять соль данной шутки, нужно иметь хотя бы общее представление о теоремах Гёделя ;-)
	Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

	4. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от pavlinux (ok) on 28-Янв-11, 15:46
	Так вроде решили этот гиммор, и кстати кто-то из наших.
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

	5. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от Анонимиус on 28-Янв-11, 16:02
	Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на базе Debian/Ubuntu. Не знаешь чего-нибудь подобного? Хочу простого - изолировать одни приложения от других на уровне запрета доступа к буферам обменов в различных зонах. Ну, и естественно, с разными корнями. Как это вообще устроено?
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	15. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от pavlinux (ok) on 28-Янв-11, 23:50
	> Павел, мне тут интересно стало попробовать что-то вроде Cubes OS, но на > базе Debian/Ubuntu. Qubes мож? То, что Рутковска в том году обещалась сделать супер-пупер изолированный Линух?! > Как это вообще устроено? Как, как, ... как и все виртуалки - гипервизор и разделение памяти.
	Ответить | Правка | ^ к родителю #5 | Наверх | Cообщить модератору

	21. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от Анонимиус on 29-Янв-11, 16:20
	Да, он самый. То, что виртуалки - это ясно. Мне другое не ясно: как регулировать, какому приложению можно получать доступ к буферу обмена, а какому нельзя?
	Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

	22. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от pavlinux (ok) on 29-Янв-11, 19:30
	> Да, он самый. > То, что виртуалки - это ясно. Мне другое не ясно: > как регулировать, какому приложению можно получать доступ к буферу обмена, а какому > нельзя? Ну, этой темы на семестр лекций хватит http://secure.wikimedia.org/wikipedia/en/wiki/Memory_barrier
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

	24. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от Анонимиус on 30-Янв-11, 04:10
	Ну, я не про такие низкоуровневые вещи спрашиваю. Мне интересно, чем можно сказать: это приложение не имеет права читать содержимое буфера обмена, если на нем стоит атрибут. А атрибут появился потому, что я номер кредитки выделил мышью в секурном окружении для того, чтобы вставить в секурный браузер банк-клиента. То есть, разделив на зоны безопасности, я хочу регулировать обмен данных между зонами.
	Ответить | Правка | ^ к родителю #22 | Наверх | Cообщить модератору

	25. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от pavlinux (ok) on 30-Янв-11, 05:54
	> ... чем можно сказать: Пока не придумали. Это надо всю ОСь переделывать (ну или хотя бы диспетчер памяти). Но ближе всего подобрались OpenVZ и Jail из FreeBSD > это приложение не имеет права читать содержимое буфера обмена, если на нем > стоит атрибут. А атрибут появился потому, что я номер кредитки выделил мышью > в секурном окружении для того, чтобы вставить в секурный браузер банк-клиента. > То есть, разделив на зоны безопасности, я хочу регулировать обмен данных между > зонами. Ну вот, сам почти и ответил - создаются зоны, разрешением занимается гипервизор.
	Ответить | Правка | ^ к родителю #24 | Наверх | Cообщить модератору

	11. "На базе гипервизора seL4 создана платформа для создания высо..."	+1 +/–
	Сообщение от анон on 28-Янв-11, 20:12
	Теоремы Геделя, внезапно, были доказаны Геделем. Великий тролль был. И поныне одно из важнейших применений его теорем о неполноте - троллинг математиками своих коллег и (особенно) нубов. Первая теорема используется для троллинга тех, кто собирается доказать что-то очень сложное и неочевидное (она гласит: в любой непротиворечивой аксиоматике можно построить такое истинное утверждение, что его нельзя будет ни доказать, ни опровергнуть в рамках этой аксиоматики). Т.е. в математике могут существовать вещи, которые в принципе нельзя доказать. Вторая теорема используется для троллинга тех, кто уже что-то доказал и теперь этим гордится (она гласит, что для непротиворечивой аксиоматики, ее непротиворечивость не может быть доказана ее собственными стредствами). Одно из интереснейших ее следствий - то, что корректность математики и всего, что на ней основано, не может быть доказана. В математику можно только верить. Или не верить. Но такая ситуация http://xkcd.ru/816/ в принципе не исключена. И поэтому любое утверждение, формально доказанное, но не проверенное эмпирически, может запросто оказаться и ложным.
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	18. "На базе гипервизора seL4 создана платформа для создания высо..."	+1 +/–
	Сообщение от fr0ster (ok) on 29-Янв-11, 10:10
	Использование принципа Гёделя для троллинга нарушает принцип Оккама :)
	Ответить | Правка | ^ к родителю #11 | Наверх | Cообщить модератору

2. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
Сообщение от non anon on 28-Янв-11, 15:23
>Принцип работы платформы сводится к полной изоляции работы групп приложений за счет использования низкоуровневого гипревизора, задачи которого выполняет микроядро seL4. Это типа os cubes на микроядре? Кстати, интересно, можно ли замутить такое на hurd (насколько я знаю, это наиболее живой из открытых микроядерных проектов). >В отличие от классических систем виртуализации микроядро seL4 является предельно минималистичным и его надежность доказана математически. Зачёт за тонкий юмор :-)
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

6. "На базе гипервизора seL4 создана платформа для создания высо..."	–1 +/–
Сообщение от User294 (ok) on 28-Янв-11, 16:12
> микроядро seL4 является предельно минималистичным и его надежность доказана математически. Молодцы, они осознали наконец что если ядро нихрена не умеет - то и глючить там будет нечему. Hello world, кстати, тоже вполне себе надежная программа. Проблема только в том что ни само по себе ядро L4, ни hello world никому не нужны. А вот за надежность готовой системы в целом эти исследователи явно отвечать не захотят, что собссно и является некоей проблемой :). В итоге будет возможно 2 варианта: "нифига не умеет и поэтому никому не нужно" и "за глюки чужого софта мы не отвечаем!" :)
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	9. "На базе гипервизора seL4 создана платформа для создания высо..."	+3 +/–
	Сообщение от Аноним (??) on 28-Янв-11, 18:20
	> Hello world, кстати, тоже вполне себе надежная программа Классический - ни разу. Надёжный hello, world занимает страницу кода где-то.
	Ответить | Правка | ^ к родителю #6 | Наверх | Cообщить модератору

	14. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от User294 (ok) on 28-Янв-11, 23:08
	> Классический - ни разу Да ладно вам. Там нет выделений памяти, а инициализацию и библиотеки можно подсунуть в духе тех которые используются в параиноидальной эмбеддовке, где обламываться тупо нечему. Ненадежность сторонних либ, системных вызовов, etc - не есть ненадежность программы, так что отмазка в духе аффтаров seL4 вполне прокатит имхо :)))
	Ответить | Правка | ^ к родителю #9 | Наверх | Cообщить модератору

	16. "На базе гипервизора seL4 создана платформа для создания высо..."	–1 +/–
	Сообщение от pavlinux (ok) on 28-Янв-11, 23:55
	>> Классический - ни разу > Там нет выделений памяти Не гони! 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)
	Ответить | Правка | ^ к родителю #14 | Наверх | Cообщить модератору

7. "На базе гипервизора seL4 создана платформа для создания высо..."	–3 +/–
Сообщение от Аноним122333 on 28-Янв-11, 17:22
> Все наработки проекта можно свободно использовать, при условии некоммерческого применения. надо было эту фразу первой написать... и после этого новость сразу можно не читать :-) ...технологии котореые можно использовать для только как "студентеские игрушки" -- не нужны. ибо любой студент рано или позно заканчивает быть студентом :-)
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	19. "На базе гипервизора seL4 создана платформа для создания высо..."	–3 +/–
	Сообщение от Аноним123321 (ok) on 29-Янв-11, 12:45
	минусов наставили, а никто причину не откомментировал.... видимо студенты-вендузятники зашли на сайт :-)
	Ответить | Правка | ^ к родителю #7 | Наверх | Cообщить модератору

	20. "На базе гипервизора seL4 создана платформа для создания высо..."	–1 +/–
	Сообщение от Andrey Mitrofanov on 29-Янв-11, 15:32
	Видимо, большая часть "посетителей сайта" считает несвободность для коммерческого использования... краеугольным камнем нашей демократии. Борется за неё и всячески поддерживает (=минусует). И нет, виндузятники тут не при чём. ЗЫЖ Минусуйте меня. Нежно!
	Ответить | Правка | ^ к родителю #19 | Наверх | Cообщить модератору

	23. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от non anon on 29-Янв-11, 21:05
	Смею предположить, что большая часть посетителей этого сайта являются пользователями/администраторами ПО, а не представителями коммерческих софтовых компаний. Поэтому их свободу данные ограничения никак не затрагивают. Жаловаться на несвободность данного ПО могут только коммерсанты.
	Ответить | Правка | ^ к родителю #20 | Наверх | Cообщить модератору

8. "На базе гипервизора seL4 создана платформа для создания высо..."	+1 +/–
Сообщение от vadiml (ok) on 28-Янв-11, 18:04
> его надежность доказана математически Это при условии что в программе, которая занимается проверками, тоже нет ошибок.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	12. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
	Сообщение от анон on 28-Янв-11, 20:17
	>> его надежность доказана математически > Это при условии что в программе, которая занимается проверками, тоже нет ошибок. Ну хоть кто-то, ну хотя бы поверхностно, оценил сей жестокий прикол ;)
	Ответить | Правка | ^ к родителю #8 | Наверх | Cообщить модератору

10. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
Сообщение от Аноним (??) on 28-Янв-11, 19:14
> Например, можно обеспечить работу на смартфоне системы для доступа к закрытой информации с обычными мобильными приложениями. Сейчас это делают, применяя специальные процессоры. Например, 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."
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

13. "На базе гипервизора seL4 создана платформа для создания высо..."	+/–
Сообщение от Аноним (??) on 28-Янв-11, 20:33
да, но математика это не наука в понимании Галлилея - наблюдение, опыт, заключение, очень характерен период развития теории множеств(огромное кол-во парадоксов- яркий пример парадокс Рассела, о том что множество не может быть элементов своего множества) математика это сила ума - созерцание, следовательно найдется такой человек который опровергнет данную систему в виде надежности - просто нужно время.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема