Уже было в толксах.

Это?

Да.

Молодцы, чё.

чё молодцы. у меня андроид циан занимает 150Мб в зипе. а тут всего 110Кб. подозреваю н@ёп

Просто там нет окошек со спецэффектами.

Аааа

толксы не нужны.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

А блин, я по «110» грепал.

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

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

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

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

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

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

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

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

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

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

В случае 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».

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

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

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

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

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

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

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

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

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

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

С нуля? Это что еще за БАГЕТ ОСРВ 3000?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

bullshit

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

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

Всё в userland'е.

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

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

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

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

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

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