LINUX.ORG.RU

А откуда инфа про 110 килобайт? Просмотрел бегло портянку по ссылке, не увидел там про это. Вообще, по инсайдерской инфе (правда мб она уже устарела), они собираются выпустить просто затюненный Linux под своим брендом, так что 110кб - как-то странно звучит.

DELIRIUM ☆☆☆☆☆
()
Ответ на: комментарий от RedPossum

так там линукс унутре?

«По мнению “Лаборатории Касперского”, максимально безопасная среда для контроля информационной инфраструктуры должна соответствовать следующим требованиям: ОС не может быть основана на каком-то уже существующем программном коде, поэтому должна быть написана с нуля. В целях гарантии безопасности она не должна содержать ошибок и уязвимостей в ядре, контролирующем остальные модули системы. Как следствие, ядро должно быть верифицировано средствами, не допускающими существования уязвимостей и кода двойного назначения. По той же причине ядро должно содержать критический минимум кода, а значит, максимально возможное количество кода, включая драйверы, должно контролироваться ядром и исполняться с низким уровнем привилегий. Наконец, в такой среде должна присутствовать мощная и надежная система защиты, поддерживающая различные модели безопасности.»

Manhunt ★★★★★
()
Ответ на: комментарий от DELIRIUM

А откуда инфа про 110 килобайт?

«На данный момент ядро ОС от “Лаборатории Касперского” занимает всего около 100 КБ. Рабочее название — 11.11. Это не клон Linux, QNX или прочих, это самостоятельный продукт. Разрабатывается он уже несколько лет, с нуля и полностью в России»

Karapuz ★★★★★
() автор топика
Ответ на: комментарий от DELIRIUM

А откуда инфа про 110 килобайт? Просмотрел бегло портянку по ссылке, не увидел там про это.

Там есть, грепни по слову «100 КБ»

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

В целях гарантии безопасности она не должна содержать ошибок и уязвимостей в ядре

Мне вот это особенно нравится. Он сделал открытие! Все, оказывается, были дураками, и не знали, что не надо делать ошибок, и делали их все специально!

XVilka ★★★★★
()
Ответ на: комментарий от Karapuz

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

XVilka ★★★★★
()

Туда еще просто драйверов не напихали

DNA_Seq ★★☆☆☆
()

Они изобрели Андроид-девайс с лоченым бутлоадером! Браааво!!!!

Jetty ★★★★★
()
Ответ на: комментарий от XVilka

Мне вот это особенно нравится. Он сделал открытие! Все, оказывается, были дураками, и не знали, что не надо делать ошибок, и делали их все специально!

Все, конечно, очень умные и всё знают, но программы в которых не сделано ошибок — это очень дорогое удовольствие.

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

Есть и другие подходы: несравнимо более дорогие, несравнимо более медленные, но за то дающие определенные гарантии. Для кода программ можно строить формальные математические доказательства, теоремы по сути, что программа обладает определенными качествами. Доказательства, правильность которых может механически проверить компьютер, и таким образом роль человеческого фактора сводится практически к нулю. Вот тебе пример из реальной жизни: http://www.ertos.nicta.com.au/research/l4.verified/

Manhunt ★★★★★
()
Ответ на: комментарий от XVilka

Ну, в презентации он упомянул о верификации ядра.

Ну и к чему тогда был твой сарказм про «все не знали»? Ты много верифицированного софта видел?

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

Мне вот интересно, что на самом деле имеется ввиду в том интервью под словом «верифицировано»? Действительно формальная верификация, или что-то другое?

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

Знаю я про формальную верификацию, SMT-солверы, z3 от Microsoft и т.д. Но! Формализация программы - это одно, верификация - другое. Саму программу на Си, почти невозможно формально верифицировать. Для этого пишут их на Ocaml, Haskell или других подобных языках. А потом надо будет переводить в Си/Си++. Вот на этапе перевода могут и вылезти ошибки, и никакая верификация не поможет.

Да, при работе с реальным железом никакой верификации быть не может. Достаточно небольшого бага в железе, например в том же USB или сетевом контроллере, и можно этим воспользоваться.

XVilka ★★★★★
()
Последнее исправление: XVilka (всего исправлений: 1)
Ответ на: комментарий от XVilka

Саму программу на Си, почти невозможно формально верифицировать.

В случае L4 верифицирован именно код на Си: «The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more». В том числе, верифицированы такие аспекты как «Buffer overflows», «Null pointer dereferences», «Pointer errors in general», «Memory leaks», «Arithmetic overflows and exceptions».

Manhunt ★★★★★
()
Ответ на: комментарий от XVilka

Да, при работе с реальным железом никакой верификации быть не может. Достаточно небольшого бага в железе

Используйте верифицированное железо ;)

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

Ну да, кроме ассемблерных вставок :) Да и подобная верификация - дорогая и долгая штука.

XVilka ★★★★★
()

к тому времени как эту ос допилят, привид может окачуриться банально от старости

AGUtilities ★★★
()
Ответ на: комментарий от Manhunt

Верифицированное железо, верифицированный ассемблер, верифицированный компилятор, верифицированный язык программирования, верифицированная ОС. Миллиарды долларов, если не больше...

XVilka ★★★★★
()
Ответ на: комментарий от XVilka

Миллиарды долларов, если не больше...

Демократия на крыльях ракет, она такая.

Manhunt ★★★★★
()

Фактически речь идет об интеллектуальной системе противоаварийной защиты нового поколения, которая учитывает весь комплекс показателей предприятия сразу и не позволяет привести к аварии ни в результате неправильных действий оператора, ни в результате ошибок в ПО, ни в результате кибератак.

Скайнет в комплекте.

Прозреваю обычный попил бабла.

geekless ★★
()
Ответ на: комментарий от XVilka

Который, кстати, может вылезти через несколько лет после выхода девайса на рынок.

AiFiLTr0 ★★★★★
()
Ответ на: комментарий от AiFiLTr0

багет? багет уже обсуждали

Karapuz ★★★★★
() автор топика
Ответ на: комментарий от XVilka

Все, оказывается, были дураками, и не знали, что не надо делать ошибок, и делали их все специально!

Просто сейчас появились методы писать софт без ошибок. Смотри Spark, например.

Т.е. совсем без ошибок все равно не будет, но источник ошибок из кода переносится на более высокие уровни.

Deleted
()
Ответ на: комментарий от XVilka

Есть Spark. Пишешь как бы на Ada, пишешь аннотации, прогоняешь через процедуру проверки, профит.

Еще бы руки поскорее дошли это чудо-юдо попробовать...

Deleted
()
Ответ на: комментарий от Deleted

Ну, про это слышу в первый раз, хоть и интересуюсь системами формализации (в целях реверс-инжиниринга). Я так понял, он еще очень плохо распространен?

XVilka ★★★★★
()

Ждём релиз и пополнение в списке платиновых тредов.

GoNaX ★★★
()

Да пусть делают. Нам пофиг - она же платная будет, а мы - халявщини (ну, вернее, партнёры) в основной своей массе.

Pakostnik ★★★
()

Я так и не понял, что именно они делают? Если у ОС свое ядро, которое не линукс/виндовс/макос, то кому нужна эта ОС ? Готовый софт переписывать тоже будут в лаборатории? Или компании заставят своих разрабов это делать? А если я найду уязвимость в касперской ОС они откажутся от проекта? :)

gh0stwizard ★★★★★
()
Ответ на: комментарий от XVilka

Верифицированное железо, верифицированный ассемблер, ....

Главное в этом процессе не в коем случае не верифицировать миллиарды долларов потраченные на процесс верификации.

kernel ★★☆
()
Ответ на: комментарий от gh0stwizard

Если у ОС свое ядро, которое не линукс/виндовс/макос, то кому нужна эта ОС ? Готовый софт переписывать тоже будут в лаборатории?

О каком готовом софте идёт речь?

Kindly_Cat
()
Ответ на: комментарий от Kindly_Cat

Софт для АСУТП, он же для этого сектора рынка себя позиционирует.

XVilka ★★★★★
()
Ответ на: комментарий от Kindly_Cat

Тот, что крутится на «незащищенных» железках, аля софт, который управляет реакторами, лифтами и т.п. Или каспОС умеет rt компиляцию сишного кода как VxWorks (+ полная совместимость)?

gh0stwizard ★★★★★
()
Последнее исправление: gh0stwizard (всего исправлений: 2)
Ответ на: комментарий от XVilka

Ada вообще не особо популярна, как ни странно.

Deleted
()

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

hi_artem
()
Ответ на: комментарий от gh0stwizard

А если я найду уязвимость в касперской ОС они откажутся от проекта? :)

Для них было бы хорошей рекламой объявить награду за взлом. Если решатся публично выложить свои блобы, конечно.

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

Всё в userland'е.

Интересно, сколько Minix весит с минимумом драйверов и без юзерленда :D

Ядро MINIX3 это примерно 28 тысяч строк кода. Все (в смысле вообще все) драйверы вынесены из пространства ядра.

Camel ★★★★★
()
Ответ на: Всё в userland'е. от Camel

Ядро MINIX3 это примерно 28 тысяч строк кода. Все (в смысле вообще все) драйверы вынесены из пространства ядра.

Если верить ОП-овской ссылке, у касперского примерно так же.

Manhunt ★★★★★
()
Ответ на: комментарий от Manhunt

Для них было бы хорошей рекламой объявить награду за взлом.

Ага, яндекс уже так выпендрился, теперь всех клиентов теряют. Умники емнить :)

gh0stwizard ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.