| 1.1, pavlinux (ok), 15:17, 28/01/2011 [ответить] [﹢﹢﹢] [ · · · ]
| –1 +/– |
 > его надежность доказана математически.
По их мнению, надёжность это то:
> что написанный код удовлетворяет всем тем спецификациям,
> которые были заложены на этапе проектирования.
Как мы видим, это не спасает это от ошибок проектирования.
| | |
| |
| 2.3, non anon (?), 15:25, 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 [^] [^^] [^^^] [ответить]
| +/– |
Да, он самый.
То, что виртуалки - это ясно. Мне другое не ясно:
как регулировать, какому приложению можно получать доступ к буферу обмена, а какому нельзя?
| | |
|
|
| 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 вполне прокатит имхо :)))
| | |
|
|
| 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 [ответить] [﹢﹢﹢] [ · · · ]
| +/– |
да, но математика это не наука в понимании Галлилея - наблюдение, опыт, заключение, очень характерен период развития теории множеств(огромное кол-во парадоксов- яркий пример парадокс Рассела, о том что множество не может быть элементов своего множества)
математика это сила ума - созерцание, следовательно найдется такой человек который опровергнет данную систему в виде надежности - просто нужно время.
| | |
|
