Здравствуйте, Pavel Dvorkin, Вы писали:
PD>А перенести jvm и т.д. в режим ядра — это просто будет означать перенос всей работы в ядро. После этого о безопасности ядра говорить будет сложно.
Хотя по условию про софт тут все забыли, железо осталось таким, как было. А про железо, в частности, защиту памяти, тут говорили в далеком 2005 году. Нужна ли Оберон-ОС защита памяти?
Здравствуйте, AlexRK, Вы писали:
ARK>Да, речь именно о переносе всего в режим ядра (собственно, никаких "колец" уже и не будет).
Так, давай по порядку.
Колец не будет.
Приложения могут использовать только управляемый код.
Тогда вопрос — а кто имеет право разрабатывать нативный код ? Его все же добавлять может некий сторонний производитель, или же только изготовитель процессора и те,кому он это доверит ?
>Безопасность обеспечивается статической верификацией (как в Singularity или Rust).
Я понимаю, к чему ты клонишь. Но Singularity не пошла.
Кроме того, я что-то не уверен в том, что статическая верификация совершенно надежна.
Здравствуйте, Privalov, Вы писали:
P>Хотя по условию про софт тут все забыли, железо осталось таким, как было. А про железо, в частности, защиту памяти, тут говорили в далеком 2005 году.
О нем не только говорили, его и сделали (Итаниум), да только архитектура x86/x64 за себя постоять сумела.
Просто если начать это обсуждать — тред превратится в обсуждение того, каким должен быть процессор (потому что архитектуру x86/x64 никто защищать не будет).
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Приложения могут использовать только управляемый код. PD>Тогда вопрос — а кто имеет право разрабатывать нативный код ? Его все же добавлять может некий сторонний производитель, или же только изготовитель процессора и те,кому он это доверит ?
Не обязательно в приложениях должен быть управляемый код. Вполне может быть и статически верифицируемый нативный код.
Verve — статически верифицируемая ОС, снизу доверху, абсолютно целиком и полностью — включая самые-самые низкоуровневые части на ассемблере (это, конечно, не простой ассемблер, а TAL — ассемблер, подходящий для статической верификации).
То есть это всё нативный код, но при этом верифицируемый на этапе компиляции. Думаю, в будущем все к тому и придет. Хотя для обычных приложений писать на управляемых языках просто дешевле, поэтому, думаю, управляемый код тоже останется.
PD>Я понимаю, к чему ты клонишь. Но Singularity не пошла.
Не пошла, верно. Но показала, что подобная реализация при желании вполне возможна. (Будет такое желание у кого-то или нет, и если будет, то когда — это все открытые вопросы.)
PD>Кроме того, я что-то не уверен в том, что статическая верификация совершенно надежна.
На 100%, конечно, нет. Равно как и процессоры не надежны на 100% (см. недавние дыры).
Здравствуйте, AlexRK, Вы писали:
ARK>На 100%, конечно, нет. Равно как и процессоры не надежны на 100% (см. недавние дыры).
OK.
Создана эта самая ОС с верификацией. В ней можно писать программы на нативном коде, но его верифицируют.
Но верификация не на 100% надежна. Более того, предполагаю, что она гораздо меньше надежна, чем защита в процессоре. Там все же из 0 кольца к ядру добраться нельзя. И не надо мне про Meltdown и Spectre — они все же доступа по записи не дают.
Кто-то находит способ обойти эту верификацию. Обойти не потому, что ее алгоритм содержит ошибки, а потому что он нашел ситуацию, когда верификация не работает. Какими-то хитрыми упражнениями , сводящими с ума статический верификатор.
Такое может быть ? Все же программа исполняется в динамике — ты уверен, что статическими средствами можно все случаи предусмотреть ?
В итоге он хозяин машины. Другой-то защиты больше нет. У него полный доступ к ядру ОС.
А если он — автор вируса, то есть делает это сознательно — и что теперь делать ?
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Но верификация не на 100% надежна. Более того, предполагаю, что она гораздо меньше надежна, чем защита в процессоре.
Трудно сказать. Вряд ли можно это измерить.
PD>Там все же из 0 кольца к ядру добраться нельзя.
В теории нельзя, но кто сказал, что в процессоре нет дырок? Современные процы — штука очень сложная.
PD>Кто-то находит способ обойти эту верификацию. Обойти не потому, что ее алгоритм содержит ошибки, а потому что он нашел ситуацию, когда верификация не работает. Какими-то хитрыми упражнениями , сводящими с ума статический верификатор. PD>Такое может быть ?
Вполне может, думаю. На практике, ИМХО, вероятность не слишком велика. Но, конечно, что-то в этом плане утверждать я не могу.
PD>Все же программа исполняется в динамике — ты уверен, что статическими средствами можно все случаи предусмотреть ?
Теоретически можно предусмотреть всё, на практике можно какую-то дырку и пропустить.
PD>В итоге он хозяин машины. Другой-то защиты больше нет. У него полный доступ к ядру ОС. PD>А если он — автор вируса, то есть делает это сознательно — и что теперь делать ?
Так и сейчас примерно то же самое. Баги в процессоре, баги в ядре, эскалация привилегий — и у тебя полный доступ к ядру ОС, ты хозяин машины.
Сейчас, конечно, можно сказать, что "эшелонированная оборона" состоит из двух бастионов — сперва дыры в софте, а потом дыры в железе. Но что мешает сделать несколько эшелонов в софте? Не вижу принципиальной разницы.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>О нем не только говорили, его и сделали (Итаниум), да только архитектура x86/x64 за себя постоять сумела.
Я, признаться, по Итаниум ничего не знаю. Попробовал читать, но что-то не пошло. Правда, у меня по графику трудовые свершения. Оказывается, они нехило влияют на способность быстро переваривать прочитанное.
Вкратце, у него есть защита памяти или нет?
И если есть, то можно придумывать C++, а если нет, то Оберон? Правда, с последним не все так просто. Короче, Фортран рулит, как ни крути.
Здравствуйте, Privalov, Вы писали:
P>Я, признаться, по Итаниум ничего не знаю. Попробовал читать, но что-то не пошло. Правда, у меня по графику трудовые свершения. Оказывается, они нехило влияют на способность быстро переваривать прочитанное. P>Вкратце, у него есть защита памяти или нет?
Хм, не понял. Как может быть процессор 21 века без защиты памяти ?
P>И если есть, то можно придумывать C++, а если нет, то Оберон? Правда, с последним не все так просто. Короче, Фортран рулит, как ни крути.
Здравствуйте, AlexRK, Вы писали:
PD>>Но верификация не на 100% надежна. Более того, предполагаю, что она гораздо меньше надежна, чем защита в процессоре.
ARK>Трудно сказать. Вряд ли можно это измерить.
Может, я что-то не понимаю, но
int n,m;
read(m,n); // ввод откуда-то
int a[m]; // выделяем память и создаем массив
a[n] = 1;
Как можно этот фрагмент статически проверить ? При корректных m и n все будет замечательно. При большом n мы свободно сейчас можем уехать в адреса ядра, за что и получим AV
Здравствуйте, lpd, Вы писали:
lpd>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Что бы Вы из существующего сделали в практически том же виде, в каком оно существует сейчас и что сделали бы по-другому ?
lpd>Я бы заменил С++, Java и C# на один язык без VM со сборкой мусора(отключемой). Но насчет этого разных мнений много.
было такое в Objective-C. Не прижилось. Кстати, не знаю, почему. Есть инсайдеры, пролить свет?
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Может, я что-то не понимаю, но
PD>int n,m; PD>read(m,n); // ввод откуда-то PD>int a[m]; // выделяем память и создаем массив PD>a[n] = 1;
PD>Как можно этот фрагмент статически проверить ? При корректных m и n все будет замечательно. При большом n мы свободно сейчас можем уехать в адреса ядра, за что и получим AV PD>А статически — как ?
В принципе, идея простая. Можем ли мы сказать, глядя на этот код, что он 100% корректен? Нет. Мы этого не можем утверждать. И верификатор, естественно, тоже не может. Результат? Ошибка компиляции.
Как сделать, чтобы код скомпилировался? Убедить верификатор в том, что код безопасен.
int n,m;
read(m,n); // ввод откуда-тоif (stack_available(m)) // stack_available - специальная функция, известная верификатору
{
int a[m]; // выделяем память и создаем массивif (is_valid_index(a, n)) // is_valid_index - специальная функция, известная верификатору
{
a[n] = 1;
}
else
{
// тут мы хотели обратиться по некорректному адресу, но рантайм-проверка нам не дала
// что делать? наверное вернуть ошибку или выдать какое-то сообщение
}
}
else
{
// тут рантайм-проверка показала, что места на стеке нет, создать массив мы не можем
// и что же нам делать? ну, что угодно, можно вернуть ошибку или терминировать процесс
}
Так что сама идея довольно простая. Там, где верификатор не знает, корректная операция или нет — он заставляет программиста вставить рантайм-проверку.
Конечно, эти явные проверки замусоривают код, но потенциальный выигрыш в том, что их может быть не так уж много. Это как типы данных. Если мы хотим принять в функцию int, то компилятор не даст нам туда сунуть string. Аналогичным образом мы можем потребовать предусловие наподобие "is_valid_index" и тогда внутри функции этой проверки уже не будет — она будет где-то выше по стеку вызовов.
Да, такой код писать сложнее. Но это возможно. Примерно так пишут софт для марсоходов и самолетов. Я думаю, что такой вариант возможен для самых низкоуровневых частей ОС, а что-то более высокоуровневое можно писать уже на управляемых языках, более тормозных, но и более простых.
Здравствуйте, AlexRK, Вы писали:
ARK>В принципе, идея простая. Можем ли мы сказать, глядя на этот код, что он 100% корректен? Нет. Мы этого не можем утверждать. И верификатор, естественно, тоже не может. Результат? Ошибка компиляции.
<skipped>
Понятно, но выглядит пугающе. Для меня, по крайней мере.
Одним махом уничтожается весь существующий нативный код. Он практически со 100% вероятностью не пройдет эту проверку, а значит, придется переписывать в нем очень многое.
Далее. Представь себе, что это программа линейной алгебры. Там этих a[i][j] в каждой строке может быть по нескольку штук. Если заставлять каждое такое описание верифицировать по твоему механизму — код за этими верификациями видно уже не будет, а отладка превратится в ад.
А не запретишь. И управляемые языки не помогут. Ты же ОС собрался делать, и что, ты мне скажешь, что в этой ОС писать "тяжелый" код можно только на управляемых языках ? Он и без того тяжелый, там O(N^3), например, а мне, выходит, его оптимально написать нельзя ?
Кроме того, почему ты решил, что массив отведен в стеке ? Для него относительно просто написать stack_available. А если в куче ? Да еще двумерный и при этом jagged ? И при этом еще и не прямоугольный, а хорошо если только треугольный ? Тебе не кажется, что такая "статическая" проверка просто не получится ? А еще realloc (в С) есть. А еще union в нем же есть.
Что-то у меня такое ощущение, что это лекарство хуже болезни. Сейчас мне как программисту по крайней мере все ясно — я могу делать (в нативе) что хочу, за свои безобразия в юзермодной части АП я отвечаю сам (кстати, и тут мне помогают, доступ к невыделенным адресам блокируется), а за попытку безобразия в системной части АП будут бить со 100% гарантией. И код я при этом пишу, как его всегда писали. А тут предлагается писать его совсем по-другому, с массой накладных расходов, а успех не гарантирован.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Хм, не понял. Как может быть процессор 21 века без защиты памяти ?
Я ж говорил, период трудовых свершений даром не проходит. Что защита памяти нужна, я писал в Философии еще в 2005 году в оберонных войнах. А про Итаниум, повторю, я ничего не знаю. И чтение в голову не лезет по причине, которую я только что отметил. Попозже я к этому вернусь.
P>>И если есть, то можно придумывать C++, а если нет, то Оберон? Правда, с последним не все так просто. Короче, Фортран рулит, как ни крути.
PD>Фортран наша молодость
И ведь до сих пор работает. И кросплатформенность такая, что C++ и не снилась.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Одним махом уничтожается весь существующий нативный код. Он практически со 100% вероятностью не пройдет эту проверку, а значит, придется переписывать в нем очень многое.
Безусловно. Существующий код переиспользовать в безопасном контексте малореально.
PD>Далее. Представь себе, что это программа линейной алгебры. Там этих a[i][j] в каждой строке может быть по нескольку штук. Если заставлять каждое такое описание верифицировать по твоему механизму — код за этими верификациями видно уже не будет, а отладка превратится в ад.
Верно. Но речь не о математическом ПО. Его вообще писать удобнее с помощью совершенно других средств и языков.
PD>А не запретишь. И управляемые языки не помогут. Ты же ОС собрался делать, и что, ты мне скажешь, что в этой ОС писать "тяжелый" код можно только на управляемых языках ? Он и без того тяжелый, там O(N^3), например, а мне, выходит, его оптимально написать нельзя ?
Для верифицируемого нативного кода внутри ОС не так уж много применений, ИМХО — ядро, менеджер памяти, диспетчер процессов, ну может еще файловая система. Можно и поднапрячься немного.
А остальной код — просто не использует сырые указатели, как я писал вначале (при этом он может быть и не обязательно управляемым, может быть что-то типа Rust).
PD>Кроме того, почему ты решил, что массив отведен в стеке ? Для него относительно просто написать stack_available. А если в куче ? Да еще двумерный и при этом jagged ? И при этом еще и не прямоугольный, а хорошо если только треугольный ? Тебе не кажется, что такая "статическая" проверка просто не получится ?
Может я чего не понимаю, но в чем принципиальное отличие? Ну будет еще функция "heap_available". Треугольный-прямоугольный — сводится к дополнительным проверкам тех же функций. Если я неправ, покажите псевдокод, что вы имеете в виду.
PD>А еще realloc (в С) есть.
Заменяется на типизированную аллокацию (не просто сырой блок памяти).
PD>А еще union в нем же есть.
Дополняется «тегом», описывающим текущее содержимое.
PD>Что-то у меня такое ощущение, что это лекарство хуже болезни.
В некритичных к безопасности местах — да.
PD>А тут предлагается писать его совсем по-другому, с массой накладных расходов, а успех не гарантирован.
Ну, успех никогда не гарантирован. Насчет накладных расходов — они в общем случае будут больше при написании и сопровождении кода, но — опять же, в общем случае — меньше при работе программы (особенно если учесть то, что можно отказаться от аппаратной защиты в процессоре).
PD>Нет, не верю, что это пойдет.
В массы не пойдет. В ядра ОС — вполне может быть, ИМХО.
Здравствуйте, AlexRK, Вы писали:
ARK>Верно. Но речь не о математическом ПО. Его вообще писать удобнее с помощью совершенно других средств и языков. ARK>Для верифицируемого нативного кода внутри ОС не так уж много применений, ИМХО — ядро, менеджер памяти, диспетчер процессов, ну может еще файловая система. Можно и поднапрячься немного. ARK>В массы не пойдет. В ядра ОС — вполне может быть, ИМХО.
Нет, извини, давай уточним. Если бы речь шла о том, что при существующей архитектуре процессора и ОС предлагается добавить эту статическую верификацию — это одно. Ты же предлагаешь существующую архитектуру заменить такой, в которой не будет аппаратной защиты вообще. А значит, все приложения смогут делать что им вздумается, если только не помешает статическая верификация.
И тогда одно из двух. Либо ты запретишь писать на нативном коде любое несистемное ПО (а на это никто не пойдет), либо остается молиться статической верификации в надежде на то, что она безошибочна. Оба хуже.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Одним махом уничтожается весь существующий нативный код. Он практически со 100% вероятностью не пройдет эту проверку, а значит, придется переписывать в нем очень многое.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Ты же предлагаешь существующую архитектуру заменить такой, в которой не будет аппаратной защиты вообще. А значит, все приложения смогут делать что им вздумается, если только не помешает статическая верификация.
Да, все верно.
PD>либо остается молиться статической верификации в надежде на то, что она безошибочна. Оба хуже.
Да, вот этот вариант. Но я не вижу, почему этот вариант менее надежен, чем аппаратная защита в процессоре. В чем принципиальная разница?
Здравствуйте, AlexRK, Вы писали:
ARK>Да, вот этот вариант. Но я не вижу, почему этот вариант менее надежен, чем аппаратная защита в процессоре. В чем принципиальная разница?
В количестве вариантов.
Аппаратная защита в процессоре, грубо говоря устроена так. Делайте там в своей программе что хотите. Процессору на все это наплевать. Как вы там адреса вычисляете, что при этом делаете — его не касается.
И только тогда, когда Вы попытаетесь получить доступ к памяти, процессор Вас проверит. Независимо от того, что Вы там до этого делали.
В сущности, у процессора лишь один вариант. Либо пропуск валиден, тогда иди, либо невалиден — тогда иди обратно.
А исполнение программы — это , вообще говоря, NP вариантов, и доказать с помощью статического анализа, что все NP этих путей не приведут к ошибке защиты — сомневаюсь.
Здравствуйте, samius, Вы писали:
PD>>Одним махом уничтожается весь существующий нативный код. Он практически со 100% вероятностью не пройдет эту проверку, а значит, придется переписывать в нем очень многое.
S>По условию топика
S>
S>Представим себе вольную фантазию.
S>Все существующее ПО одномоментно исчезло. Все.
Да. Поймал
Но все же давай договорим это до конца. Да, все ПО исчезло. Но демиург должен его воссоздать, тоже по условиям топика. Он не обязан воссоздать C/C++, но либо он обязан
1. Либо создать новый нативный язык
2. Либо запретить нативный язык как минимум для пользовательских программ. В ОС не запретишь — кто этим управляемым кодом управлять-то будет ?
3. Либо придумать что-то такое, в котором нет понятия нативного и управляемого кода (например, аппаратная Java машина)
Третье невозможно, так как демиургу не дано менять аппаратуру опять же по условиям топика. При существующей аппаратуре нативный код существует по определению.
Что из первых двух выбираешь ?
Если первое — те же проблемы, не на С++, так на ином языке. Потому что проблема не в языке, а в доступе к памяти по адресу.
Если второе — это значит, что ты ставишь всех авторов ПО для пользователя в условия, когда они не могут использовать всю мощь процессора.
Здравствуйте, Pavel Dvorkin, Вы писали:
ARK>>Да, вот этот вариант. Но я не вижу, почему этот вариант менее надежен, чем аппаратная защита в процессоре. В чем принципиальная разница? PD>В количестве вариантов.
Ну, количество вариантов в обоих случаях примерно одинаковое.
PD>В сущности, у процессора лишь один вариант. Либо пропуск валиден, тогда иди, либо невалиден — тогда иди обратно.
У валидатора так же. Либо данный кусок кода валиден, либо нет. Ему не надо смотреть всю программу — максимум только текущую функцию.
PD>А исполнение программы — это , вообще говоря, NP вариантов, и доказать с помощью статического анализа, что все NP этих путей не приведут к ошибке защиты — сомневаюсь.
А все пути исполнения проверять не нужно. Верификатор имеет дело только с входом и выходом функции. Тут нет всего возможного множества путей исполнения, мы анализируем только предусловия функции (ну, опционально еще работу с глобальными переменными, хотя лучше, конечно, без них).
Основная разница в том, что в случае аппаратной защиты рантайм-проверка выполняется автоматически самим процессором при каждом выполнении инструкции, а в случае с программной верификацией проверку инициирует программа, и не для каждой инструкции, а только там, где надо. За счет этого достигается выигрыш в скорости.
Слабое место программной верификации — это возможность аппаратных сбоев, приводящих к искажениям значений в памяти. Ну, тут ничего не поделаешь — для критичных вещей проверок надо как можно больше, а для пользовательских это не столь важно, ИМХО (потому что эксплуатировать такие сбои весьма затруднительно).
Я понимаю, что на интуитивном уровне принять такое сложно. Но, тем не менее, есть реальные примеры подобных реализаций — вышеприведенные Singularity, Verve, полагающиеся только на программные проверки.
