Здравствуйте, AlexRK, Вы писали:

ARK>Основная разница в том, что в случае аппаратной защиты рантайм-проверка выполняется автоматически самим процессором при каждом выполнении инструкции, а в случае с программной верификацией проверку инициирует программа, и не для каждой инструкции,

Для аппаратной — отнюдь не для каждой инструкции, а только для тех, которые обращаются к памяти. Остальное вообще не проверяется в этом плане.

>а только там, где надо. За счет этого достигается выигрыш в скорости.

Боюсь все же, что для того, чтобы определить места "там где надо", придется проанализировать тот код, который при аппаратной защите вообще никакой проверке не подвергается.



ARK>Я понимаю, что на интуитивном уровне принять такое сложно. Но, тем не менее, есть реальные примеры подобных реализаций — вышеприведенные Singularity, Verve, полагающиеся только на программные проверки.

Если бы еще была хоть какая-то статистика о том, насколько это надежно. Если бы была информация о том, кто и как пытался ее взломать, и что из этого вышло. А так они пока что Неуловимый Джо.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Для аппаратной — отнюдь не для каждой инструкции, а только для тех, которые обращаются к памяти. Остальное вообще не проверяется в этом плане.

Да, я говорю про такие инструкции.

>>а только там, где надо. За счет этого достигается выигрыш в скорости.
PD>Боюсь все же, что для того, чтобы определить места "там где надо", придется проанализировать тот код, который при аппаратной защите вообще никакой проверке не подвергается.

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

double Log10(double d)
    requires d > 0
{
    // вычисляем логарифм, никаких проверок нет - аргумент "d" гарантированно больше нуля
}

void Test1(double val)
{
    //double log1 = Log10(val);   // упс, не компилируется, нам неизвестен интервал "val"

    if (val > 0)   // единственная проверка, которая останется в машинном коде
    {
        double log2 = Log10(val);  // отлично, компилируется - мы проверили val и точно знаем, что он положителен
    }
}

void Test2(double val)
    requires val > 0      // предусловие гарантирует положительный "val"
{
    double log1 = Log10(val);   // а вот сейчас всё компилируется и без проверок - все проверки должен сделать тот, кто вызывает эту функцию
}

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

PD>Если бы еще была хоть какая-то статистика о том, насколько это надежно. Если бы была информация о том, кто и как пытался ее взломать, и что из этого вышло. А так они пока что Неуловимый Джо.

Пока что в промышленной эксплуатации такое применяется ограниченно (в основном аэрокосмическое ПО), так что да, тут пока непонятно.

Здравствуйте, AlexRK, Вы писали:


ARK> if (val > 0) // единственная проверка, которая останется в машинном коде

if(val > any_complex_function_whch_calls_a_tree_of_subfunctions())

double log2 = Log10(val); // компилируется ?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>if(val > any_complex_function_whch_calls_a_tree_of_subfunctions())

PD> double log2 = Log10(val); // компилируется ?

Если "any_complex_function_whch_calls_a_tree_of_subfunctions" объявлена так:

double any_complex_function_whch_calls_a_tree_of_subfunctions()
    ensures result > 0
{
    // ...
}

то компилируется. Если вот так:

double any_complex_function_whch_calls_a_tree_of_subfunctions()
{
    // ...
}

или, например, так:

double any_complex_function_whch_calls_a_tree_of_subfunctions()
    ensures (result > 0) || (abs(result) >= 2)
{
    // ...
}

то нет.

Конечно, возможности логики первого порядка тоже не бесконечны, поэтому какие-то особо сложные предусловия или постусловия писать не выйдет. Компьютер, конечно, не сможет доказать теорему Пуанкаре. Но оно в ядрах ОС и не нужно.

Здравствуйте, AlexRK, Вы писали:


ARK>то компилируется. Если вот так:

ARK>

ARK>double any_complex_function_whch_calls_a_tree_of_subfunctions()
ARK>{
ARK>    // ...
ARK>}
ARK>

ARK>то нет.

А что мне делать, если я вообще не могу сказать, что она ensures ? Ничего она не гарантирует, не могу я гарантию дать. Вообще-то этот calls_a_tree_of_subfunctions , надеюсь, вернет >0, иначе что-то не в порядке с моим алгоритмом, ну а если все же иногда может <0 вернуть ? При обычном подходе, если есть подозрения — поставил try-catch, и все дела.

Например, некий приближенный алгоритм, исполняемый на ряде samples. Лучшего, увы, нет. А этот приближенный алгоритм, поскольку он приближенный, на некоторых sample может вообще ерунду выдать, на ноль поделить, INF устроить, логарифм от отрицательного числа брать. По условиям проекта мне разрешено этот sample просто отбросить — ну не смог .
Пример вполне реальный, был в такой ситуации, хоть и немного иначе.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>А что мне делать, если я вообще не могу сказать, что она ensures ? Ничего она не гарантирует, не могу я гарантию дать. Вообще-то этот calls_a_tree_of_subfunctions , надеюсь, вернет >0, иначе что-то не в порядке с моим алгоритмом, ну а если все же иногда может <0 вернуть ? При обычном подходе, если есть подозрения — поставил try-catch, и все дела.
PD>Например, некий приближенный алгоритм, исполняемый на ряде samples. Лучшего, увы, нет. А этот приближенный алгоритм, поскольку он приближенный, на некоторых sample может вообще ерунду выдать, на ноль поделить, INF устроить, логарифм от отрицательного числа брать. По условиям проекта мне разрешено этот sample просто отбросить — ну не смог .
PD>Пример вполне реальный, был в такой ситуации, хоть и немного иначе.

Тогда просто еще проверка:

double temp = any_complex_function_whch_calls_a_tree_of_subfunctions();

if ((temp > 0) && (val > temp))
{
    double log2 = Log10(val);
}

Везде, где мы не знаем, что со значением — компилятор заставляет вставить явную проверку. Если знаем — то нам проверка не нужна.

Здравствуйте, AlexRK, Вы писали:

ARK>Тогда просто еще проверка:

<skipped>

Ну и к чему мы пришли ?
В некоторых (относительно простых) случаях получается , верно, статический анализ. А в более сложных случаях — приходится вставлять условие, то есть проверять в рантайме, не статически. Фактически ты заставишь программиста писать все эти проверки в коде, вместо того, чтобы пустить все на нормальный самотек и ловить исключения, если он потек не туда.

Так я и с памятью могу в принципе обойтись без аппаратной проверки. Точнее, не обойтись, а сделать так, что она всегда будет успешной. Заведу у себя свой код, проверяющий при каждом обращении
к памяти указатель на валидность. Своя таблица допустимых адресов и размеров и проверка по ней. В общем, welcome to IndexOutOfBoundException в нативном варианте.
Вот только быстрее это не будет. Потому что 99.9% обращений обычно валидны, так что тут лишние проверки, и ничего больше.

А аппаратный контроль — это по сути тот же подход — пустить на самотек и ловить исключение в случае неприятности. В 99.9% их и не будет. Кстати, я не уверен даже в том, что там все проверки производятся. Если, скажем, *p обращение прошло, будет ли проверка по *(p+1), если это в пределах одной страницы ? Мне кажется, при этом TLB сработает, и проверки фактически не будет. Возможно, ошибаюсь.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>В некоторых (относительно простых) случаях получается , верно, статический анализ. А в более сложных случаях — приходится вставлять условие, то есть проверять в рантайме, не статически. Фактически ты заставишь программиста писать все эти проверки в коде, вместо того, чтобы пустить все на нормальный самотек и ловить исключения, если он потек не туда.

Да, всё верно.

PD>Вот только быстрее это не будет. Потому что 99.9% обращений обычно валидны, так что тут лишние проверки, и ничего больше.
PD>А аппаратный контроль — это по сути тот же подход — пустить на самотек и ловить исключение в случае неприятности. В 99.9% их и не будет. Кстати, я не уверен даже в том, что там все проверки производятся. Если, скажем, *p обращение прошло, будет ли проверка по *(p+1), если это в пределах одной страницы ? Мне кажется, при этом TLB сработает, и проверки фактически не будет. Возможно, ошибаюсь.

Вы забываете про переключения контекста, которые очень сильно снижают производительность и выполняются в стстемах с аппаратной защитой _постоянно_. Статическая верификация позволяет выполнять весь код в одном «кольце» (да, собственно, кольца вообще не нужны).

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Далее. Представь себе, что это программа линейной алгебры. Там этих a[i][j] в каждой строке может быть по нескольку штук. Если заставлять каждое такое описание верифицировать по твоему механизму — код за этими верификациями видно уже не будет, а отладка превратится в ад.
http://halide-lang.org/ рвёт С++ как тузик грелку.
При этом он делает все эти проверки.
Но делает их умно. Не на каждое a[i][j], а один раз на всю цепочку операций.

PD>А не запретишь. И управляемые языки не помогут.
То что ты не знаешь как не значит что это сделать нельзя.
Твоя проблема в том, что ты за пределами С++ ничего даже не пытаешься изучать.

Вот тебе ещё пример: Dafny доказательство сортировки выбором.

Автор: WolfHound
Дата: 29.04.16

Там математически доказано что код:
1)Не выходит за пределы массива.
2)Результирующий массив является перестановкой исходного массива.
3)Результирующий массив отсортирован.
4)Код завершается.
Всё что находится внутри requires, ensures и invariant работает исключительно на этапе компиляции и на результирующий код не влияет.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Но все же давай договорим это до конца. Да, все ПО исчезло. Но демиург должен его воссоздать, тоже по условиям топика. Он не обязан воссоздать C/C++, но либо он обязан

PD>1. Либо создать новый нативный язык
PD>2. Либо запретить нативный язык как минимум для пользовательских программ. В ОС не запретишь — кто этим управляемым кодом управлять-то будет ?
PD>3. Либо придумать что-то такое, в котором нет понятия нативного и управляемого кода (например, аппаратная Java машина)

PD>Третье невозможно, так как демиургу не дано менять аппаратуру опять же по условиям топика. При существующей аппаратуре нативный код существует по определению.

PD>Что из первых двух выбираешь ?
Но это ведь не взаимоисключающие вещи.

PD>Если первое — те же проблемы, не на С++, так на ином языке. Потому что проблема не в языке, а в доступе к памяти по адресу.
PD>Если второе — это значит, что ты ставишь всех авторов ПО для пользователя в условия, когда они не могут использовать всю мощь процессора.

А разве статическая верификация программы на нативном языке как-то ограничивает мощь процессора?

Вот чисто что бы ради поржать, предлагаю специальный режим многозадачности: программы с недоказанной корректностью обращений к памяти не могут выполняться одновременно с программами, которым нужна гарантия недоступности их памяти.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD> А что мне делать, если я вообще не могу сказать, что она ensures ? Ничего она не гарантирует, не могу я гарантию дать. Вообще-то этот calls_a_tree_of_subfunctions , надеюсь, вернет >0, иначе что-то не в порядке с моим алгоритмом, ну а если все же иногда может <0 вернуть ?
А вот для этого есть branch prediction. Он позволяет исполнять код быстро при наличии runtime-проверки когда всё в порядке и по сути аналог try-catch когда что-то пошло не так.

Здравствуйте, WolfHound, Вы писали:

WH> Вот тебе ещё пример: Dafny доказательство сортировки выбором.

Автор: WolfHound
Дата: 29.04.16

Поясни, плиз, немного. Как доказать, что в этом доказательстве нет ошибки?

Здравствуйте, MTD, Вы писали:

MTD>2. HTML, CSS, гуевые фреймворки на помоечку, вместо всего этого универсальный язык разметки с размерами в миллиметрах (отобразить правильно задача драйвера железки) для всего от принтеров, до экрана телефона. Все иконки строго векторные

А задача армии дизайнеров и верстальщиков, сверстать дизайн в миллиметрах для каждого экрана.

Здравствуйте, Pavel Dvorkin, Вы писали:
PD>А защита ? Ты предлагаешь ее на чисто софтверном уровне делать ? Но тогда и проверять каждый раз придется с использованием ПО, это вряд ли будет быстро
Нет. Современные среды работают не так.
PD>char * p = чему-то
PD>*p = 0;
PD>И как здесь на софтверном уровне проверять, имею ли я право доступа туда ? Встраивать на каждый mov команды проверки ?
Как в C# или Java — происходит статическая верификация кода. "Случайных" указателей в коде не бывает. Нельзя просто взять квадратный корень из Pi и использовать в качестве указателя.
PD>Вопрос не в ограничениях, а в архитектуре. Тебе не кажется, что тот же интерфейс GET с параметрами можно бы на что-то более элегантное заменить ? И заодно Header переделать.
У GET нет никаких параметров. Там же только URI. Куда элегантнее-то? Расширить набор поддерживаемых символов? Зачем?...
С заголовками тоже всё хорошо.

Здравствуйте, Sharov, Вы писали:
S>Зачем? Чем диалекты типа t-sql не устраивают?
Возможностями по декомпозиции и по диагностике ошибок.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Что из того, что заложено в существующее ПО, сделано так, как и надо было бы "по уму" сделать, и что надо было бы сделать иначе, да только , увы, невозможно — мешают проклятая compatibility и огромные наработки ?

поскольку всё получилось так из-за гравитации, а её трогать нельзя...
то тогда надо бы только отказаться от статической типизации и разрешить жалкоскриптерам работать только в водолазном костюме.

Здравствуйте, Ziaw, Вы писали:

Z>А задача армии дизайнеров и верстальщиков, сверстать дизайн в миллиметрах для каждого экрана.

Вот смотри. Палец среднестатистического человека, допустим имеет пятно контакта 5 на 5 мм, из этого следует, что надо кнопочку сделать 10 на 10 мм, условно. Потом, есть текст, известно, что он хорошо читается размером 7 мм, тоже условно. Если задавать размеры в мм, то и выглядеть везде будет одинаково и взаимодействовать будет возможно одинаково. Еще раз — 1 раз задать, получить одно и тоже везде. Теперь переходим к условным попугаям в пикселах — в зависимости от плотности пикселов размер меняется в разы, так что твой комментарий актуален сейчас, если перейти на миллиметры жизнь серьезно упроститься.

Здравствуйте, ·, Вы писали:

·>Поясни, плиз, немного. Как доказать, что в этом доказательстве нет ошибки?

Никак.
Расчет на то, что "если ошибка есть, где-нибудь что-нибудь не сойдется" (и это часто так и есть).
Но доказать это невозможно. Надо писать еще одно доказательство более высокого порядка.

Здравствуйте, AlexRK, Вы писали:


ARK>Вы забываете про переключения контекста, которые очень сильно снижают производительность и выполняются в стстемах с аппаратной защитой _постоянно_. Статическая верификация позволяет выполнять весь код в одном «кольце» (да, собственно, кольца вообще не нужны).

Почему они выполняются постоянно ? Они выполняются при переключении процессов, при системных вызовах и еще в некоторых случаях. Если я просто обращаюсь к юзермодным страницам памяти — никаких переключений контекста не будет.

Здравствуйте, samius, Вы писали:

PD>>Что из первых двух выбираешь ?
S>Но это ведь не взаимоисключающие вещи.

Хорошо, давай свой гибрид.

S>А разве статическая верификация программы на нативном языке как-то ограничивает мощь процессора?

Нет, конечно, но я не уверен, что она гарантирует то, что требуется.

S>Вот чисто что бы ради поржать, предлагаю специальный режим многозадачности: программы с недоказанной корректностью обращений к памяти не могут выполняться одновременно с программами, которым нужна гарантия недоступности их памяти.

И на каждую программу ставится клеймо, а в ОС вводим 2 режима и переключаемся между ними для того, чтобы запустить какую-то программу, которая текущему режиму не соответствует