Здравствуйте, Sinclair, Вы писали:
S>Здравствуйте, thesz, Вы писали:
T>>Теория это одно, практика — с кратковременными сбоями аппаратуры, — это другое. S>Не очень понял про кратковременные сбои.
Сбои, не связанные с постоянно присутствующим дефектом в аппаратуре. Например, скачок напряжения. Или выброс радиации.
T>>Чтобы не повторяться: http://rsdn.ru/forum/philosophy/3440056.1.aspx
Здравствуйте, WolfHound, Вы писали: WH>В паскале просто нет константности.
И много чего еще. К примеру, нет типа "ссылка". Нет типа "указатель на член".
WH>Те это легко выражается на любом языке где есть интерфейсы. Хоть на C# хоть на Java.
Ну, я бы не сказал, что это "легко" выражается. Тебя не затруднит показать мне, каким образом ты автоматически сгенерируешь этот "интерфейс, содержащий не меняющие состояния методы"?
Вручную-то всё возможно. WH>Нет.
Откуда же тогда берутся типы? По-моему, они всё таки конструируются.
S>>Увы, Павел не может понять даже такие, статически зависимые типы. Несмотря на то, что в его любимом языке они есть. WH>Он вообще ничего что выходит за рамки WinAPI понять не может.
... << RSDN@Home 1.2.0 alpha rev. 677>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, Sinclair, Вы писали:
S>Ну, я бы не сказал, что это "легко" выражается. Тебя не затруднит показать мне, каким образом ты автоматически сгенерируешь этот "интерфейс, содержащий не меняющие состояния методы"? S>Вручную-то всё возможно.
Сразу после того как ты на С++ реализуешь статическую проверку
mult : ∀i , j , k : Nat ⇒ Matrix i j → Matrix j k → Matrix i k
при условии что i, j и k не известны на этапе компиляции.
Всякие там агды и эпиграмы справляются с этим на раз.
И вообще это твое утверждение что в С++ есть зависимые типы вот ты его и доказывай.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, thesz, Вы писали: T>Сбои, не связанные с постоянно присутствующим дефектом в аппаратуре. Например, скачок напряжения. Или выброс радиации.
Это я понимаю. Я не понимаю, чем бит RO в таблице страниц спасает от скачков радиации, по сравнению с софтной верификацией корректности.
T>Там оценка расходов на аппаратную изоляцию, на кэширование и на защиту от сбоев с помощью TAL.
А защиты от сглаза там случайно не встроено? T>В переводе на русский язык, аппаратная изоляция не столь дорога, как кажется. Я имею в виду код, выполняющийся внутри одной области защиты. T>Она дорога для переключения между областями защиты. Копать надо в этом направлении, по-моему.
Ну, так в эту сторону и копают.
... << RSDN@Home 1.2.0 alpha rev. 677>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, WolfHound, Вы писали: S>>Вручную-то всё возможно. WH>Сразу после того как ты на С++ реализуешь статическую проверку
Еще раз: я не говорю, что эта задача разрешима на С++. Можно решить только её подзадачу — когда i, j и k известны на этапе компиляции.
А вот на Паскале невозможно решить и эту, значительно более простую подзадачу.
На дотнете невозможно решить задачу, которую я привёл.
Поэтому не надо видеть мир исключительно в чёрно-белом свете.
... << RSDN@Home 1.2.0 alpha rev. 677>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Все skipped ибо схоластика. Кроме одного.
PD>>Вот и расскажи, как ты это можешь до запуска определить. А еще скажи, как ты это сможешь до запуска определить, если этот несчастный флаг окажется параметром командной строки или будет вводиться с консоли во время исполнения
Вот на этот вопрос когда ответишь, тогда и будем говорить насчет возможности верификации правильности программ до исполнения. Хоть на С++, хоть на C#, хоть на чем ином.
Здравствуйте, Pavel Dvorkin, Вы писали: PD>Вот на этот вопрос когда ответишь, тогда и будем говорить насчет возможности верификации правильности программ до исполнения. Хоть на С++, хоть на C#, хоть на чем ином.
Этот вопрос и есть схоластика. Ты не в состоянии привести пример задачи, где это нужно. Слив засчитан.
Заодно засчитаем и слив про пример применения твоей новоизобретённой техники.
Которая сначала "от языка не зависит, так как реализована на чисто Win API", а потом сразу же "речь идет о необходимости добавить кое-что для этой цели в язык".
Вот показал бы предлагаемые дополнения в язык — сам бы увидел, что с ними никакая аппаратная защита не нужна.
... << RSDN@Home 1.2.0 alpha rev. 677>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, Sinclair, Вы писали:
S>Которая сначала "от языка не зависит, так как реализована на чисто Win API", а потом сразу же "речь идет о необходимости добавить кое-что для этой цели в язык".
Здравствуйте, Sinclair, Вы писали:
S>Здравствуйте, thesz, Вы писали: T>>Сбои, не связанные с постоянно присутствующим дефектом в аппаратуре. Например, скачок напряжения. Или выброс радиации. S>Это я понимаю. Я не понимаю, чем бит RO в таблице страниц спасает от скачков радиации, по сравнению с софтной верификацией корректности.
Итак, ты точно знаешь, что a[i]=10 корректно.
Это дело разворачивается в
ldi r1,a
shl r2,r10,2 # r10 - i, int a[...]
ldi r3, 10
add r4,r1,r2
st (r4),r3
Пять команд.
При выполнении любой из них может возникнуть сбой, который может привести к ошибке (либо прямо здесь, в st, либо позже).
Что ты предлагаешь делать, чтобы код a[i]=10 остался корректным с большой вероятностью для существенной вероятности сбоя в одной команде?
Что произойдёт, если у нас ошибка в случае с аппаратной защитой памяти современного типа.
Во-первых, мы не сможем порушить данные других процессов. Во-вторых, велика вероятность, что появление кратковременного сбоя приведёт к ошибке обращения к памяти, что будет отловлена её защитой.
Только прошедшая через всё это ошибка, оказавшаяся только в потоке вычислений, имеет шанс попасть в данные, доступные другим процессам.
T>>Там оценка расходов на аппаратную изоляцию, на кэширование и на защиту от сбоев с помощью TAL. S>А защиты от сглаза там случайно не встроено?
Я, что, провоцирую ёрничанье?
T>>В переводе на русский язык, аппаратная изоляция не столь дорога, как кажется. Я имею в виду код, выполняющийся внутри одной области защиты. T>>Она дорога для переключения между областями защиты. Копать надо в этом направлении, по-моему. S>Ну, так в эту сторону и копают.
По-моему, вариант с защитой памяти и тут будет полезен.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Если в существующем софте есть ошибка, то все возможно. Но по постингу WolfHound можно понять так, что достаточно переполнить буфер , и мы попадем в страницы, находящиеся под контролем системы. А причина банальная — он не вполне понимает отличие виртуальной памяти от физической, он считает, что если выйти за пределы страницы, то мы попадем на соседнюю страницу физической памяти, которая может принадлежать системе WH>Опять фантазируешь на тему того что я что-то не понимаю. WH>Просвещайся http://en.wikipedia.org/wiki/Buffer_overrun
PD>Тебе же тут уже объяснили — не работайте под админом. Кстати, как ты собираешься устроить эту самую эскалацию для процесса броузера, если он (под Вистой) запущен хоть и от админа, но без админских прав ? (т.е с юзеровскими правами) Это тоже очень интересно бы знать WH>Через переполнение буфера например.Что думаешь в WinAPI ни одного нет?
Сорри, отослал, не дописав.
PD>Здравствуйте, WolfHound, Вы писали:
WH>>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>>Если в существующем софте есть ошибка, то все возможно. Но по постингу WolfHound можно понять так, что достаточно переполнить буфер , и мы попадем в страницы, находящиеся под контролем системы. А причина банальная — он не вполне понимает отличие виртуальной памяти от физической, он считает, что если выйти за пределы страницы, то мы попадем на соседнюю страницу физической памяти, которая может принадлежать системе WH>>Опять фантазируешь на тему того что я что-то не понимаю. WH>>Просвещайся http://en.wikipedia.org/wiki/Buffer_overrun
PD>>Тебе же тут уже объяснили — не работайте под админом. Кстати, как ты собираешься устроить эту самую эскалацию для процесса броузера, если он (под Вистой) запущен хоть и от админа, но без админских прав ? (т.е с юзеровскими правами) Это тоже очень интересно бы знать WH>>Через переполнение буфера например.Что думаешь в WinAPI ни одного нет?
Пожалуйста, подробности того, как это может произойти. То есть ты переполнишь буфер, а результат — эскалация привилегий для процесса броузера. Win API для запущенных процессов изменить токен в плане добавления прав не дает. Вызовов для замены токена у процесса нет. Так что Win API попросту это не умеет делать. А вот если, переполнив буфер, мы попадем на другую страницу, а она окажется системной, да нам удастся на нее записать, тогда да, можно и данные ядра изменить, в том числе и объект токен.
Но не сможем мы на эту страницу записать. Ибо переполнив буфер мы попадем на соседнюю страницу виртуальной памяти , но отнюдь не физической. И натворить дел мы можем таким образом только у себя в виртуальном адресном пространстве.
то мэппинг будет именованный, а значит, может быть доступен другим процессам. При этом разные процессы могут делать его view по-разному, один — R/O, другой — R/W. Таким образом один процесс, например, может рассматривать некие данные как константы, в то время как другой — как переменные. Или оба как константы. Или еще как. Разумеется, если реализовать такое, то эту кучу надо сделать отдельной , специально для этих разделяемых переменных/констант. Передавать их из процесса в процесс не надо — они уже переданы, то есть автоматом присутствуют в обоих процессах. Естественно, для доступа к ним теперь нужна синхронизация, впрочем, это уже банальности.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>>Тебе же тут уже объяснили — не работайте под админом. Кстати, как ты собираешься устроить эту самую эскалацию для процесса броузера, если он (под Вистой) запущен хоть и от админа, но без админских прав ? (т.е с юзеровскими правами) Это тоже очень интересно бы знать WH>>>Через переполнение буфера например.Что думаешь в WinAPI ни одного нет?
PD>Пожалуйста, подробности того, как это может произойти. То есть ты переполнишь буфер, а результат — эскалация привилегий для процесса броузера. Win API для запущенных процессов изменить токен в плане добавления прав не дает.
Всё не так. Эскалация привелегий происходит с помощью атаки на процесс, работающий с нужными привелегиями. Например:
[Атака на службы]
Есть много сервисов, исполняющихся с повышенными привелегиями. Эти сервисы обрабатывают запросы менее привелегированных процессов. (Собственно они и существуют для этих целей, чтобы не вынуждать конечное приложение иметь слишком много полномочий.) Через LPC/RPC, ага. Если в таком сервисе есть уязвимость — теоретически можно сформировать запрос, который приведёт к исполнению кода злоумышленника. Причём необязательно код должен содержаться в самом запросе. Это актуально при атаке на внешние системы. Для локальных атак вполне достаточно, скажем, заставить процесс загрузить специально подготовленную DLL и привет. И даже не обязательно переполнять буфера. Достаточно криво написанной службы, которую можно "обмануть". Очень многие программисты пишут код откровенно халатно, не обращая внимание на безопасность. Им бы надо руки отрубать, а не придумывать очередные памперсы (а теперь новые! с выводом типов и запахом банана! тьфу!)
[Атака на драйвера]
Соответственно драйвера тоже умеют обрабатывать запросы от юзермодного кода. Вкратце: драйвер создаёт устройство и символическую ссылку на него. После этого юзермодный код может попытаться открыть устройство (через CreateFile). Из открытого устройтсва можно читать/писать (если драйвер сообщил что он это умеет) и отправлять I/O команды (через DeviceIoControl). На объект устройства ставятся (при создании) нужный набор ACL-ей, и система сама проверит права доступа при открытии устройства. Надо ли говорить, что доморощенные драйверописатели на это кладут с пробором ? Ну а дальше начинаются старые знакомые атаки, эквивалентные акакам на службы. Только кроме парочки LPC/RPC + конфигурационные параметры, добавляется вектор ReadFile/WriteFile/DeviceIOControl.
Здравствуйте, WolfHound, Вы писали:
V>>Блин, тебе хочется хлеба и зрелищ? Ну давай покажи как можно в ОбЩЕМ случае. Заодно список языков с примерами. WH>Сначала пойми что такое зависимые типы. После чего вопросы у тебя отпадут сами собой. WH>А заниматься твоим образованием у меня нет никакого желания.
Если ты считаешь, что в С++ не реализована система зависимых типов, то ты не знаешь, о чем речь. Так что возвращаю твой "лозунг" относительно образования.
В любом случае, если быть ближе к делу, просто покажи хоть на каком-нибудь ЯП вот это ограничение рекурсии на зависимых типах (пусть даже в твоем понимании зависимых типов). А я тебе на С++ аналог покажу.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Последний раз ИМХО исправляли одну из первых версий 386, в которой был какой-то баг в чем-то, связанном с плавающей точкой.
Скорее, это был первый Pentium. Современные процессоры по-видимому слишком сложны для верификации, поскольку содержат не только массу документированных errata, но и некоторые проблемы с дизайном начинают всплывать только в последнее время (см например эксплуатацию TLB вshadow walker)
.
People who are more than casually interested in computers should have at least some idea of what the underlying hardware is like. Otherwise the programs they write will be pretty weird (c) D.Knuth
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Да ну ? А можно поподробнее, как это можно переполнить буфер и проникнуть таким образом в нулевое кольцо ?
Очевидно, нужно переполнить кучу или стек в ядре, послав драйверу запрос, который он не сможет правильно обработать.
При этом аппаратная защита не затрагивается
PD> Можно примерчик кода 3 кольца ? Или это только вирусописатели умеют так буфер переполнять ?
здесь DoS. Запуск кода в свободном доступе найти сложно, но описаний много здесь
.
People who are more than casually interested in computers should have at least some idea of what the underlying hardware is like. Otherwise the programs they write will be pretty weird (c) D.Knuth
Здравствуйте, Chrome, Вы писали:
C>Или его со временем полностью вытеснит верифицируемый промежуточный код? C>Уйдет ли в прошлое "работа потока в режиме ядра и в пользовательском режиме" и связанные с этим накладные расходы? C>Утратит ли смысл изоляция приложений с помощью отдельного виртуального адресного пространства?
LLVM can replace most of the "lower levels" of the GCC toolchain, offering more aggressive optimization of GCCs three address code intermediate form (IF). LLVM supports a language-independent instruction set and type system. Each instruction is in static single assignment form (SSA), meaning that each variable (called a typed register) is assigned once and is frozen. This helps simplify the analysis of dependencies among variables. LLVM allows code to be compiled statically, as it is under the traditional GCC system, or left for late-compiling from the IF to machine code in a just-in-time compiler (JIT) in a fashion similar to Java.
Здравствуйте, IID, Вы писали:
IID>Обновление микрокода в процессоре решает!
И отсюда следует, что такой процессор интерпретирует "нативный код" Осталось только залить туда другую ВМ с верификатором...
.
People who are more than casually interested in computers should have at least some idea of what the underlying hardware is like. Otherwise the programs they write will be pretty weird (c) D.Knuth
Здравствуйте, gear nuke, Вы писали:
GN>Здравствуйте, IID, Вы писали:
IID>>Обновление микрокода в процессоре решает!
GN>И отсюда следует, что такой процессор интерпретирует "нативный код" Осталось только залить туда другую ВМ с верификатором...
В общем случае не следует. Например — ПЛИС нифига не интерпретирует. Но перезалить прошивку в неё можно.
Осталось только залить туда другую ВМ с верификатором...