Здравствуйте, AlexRK, Вы писали:
PD>>Одна дыра — и мало не покажется, не заштопаешь. Программы уже на компьютере пользователя, этап статической верификации позади, иной защиты нет, не поправишь, как Meltdown.
ARK>Ну так а в чем разница с дырой в процессоре?
Разница в том, что Meltdown заштопали вроде как. С накладными расходами, но заштопали.
Потому что это все же дыра на уровне процессора, а у процессора есть kernel mode и user mode, и в kernel mode пользовательские программы не пускают ни под каким видом, а у kernel mode есть хозяин (ОС) , в которую только и нужно внести изменения, что и было сделано.
А вот что будут делать, если в алгоритме статической верификации обнаружилась ошибка, а программы уже прошли этап этой верификации, разошлись в миллионах копий и теперь рушат ОС или получают доступ к чужой памяти — объясни. Срочно патчить все выпущенные программы ? Как ? Фирма, выпустившая эту программу, давно закрылась, авторы разбрелись кто куда.
Я уж не говорю о том, что заставить пользователей быстро поменять программу, даже если есть на что менять — задача почти безнадежная.
Здравствуйте, MTD, Вы писали:
MTD>1. Никаких кодировок кроме utf-8
Почему не UTF-16 или UTF-32?
MTD>2. HTML, CSS, гуевые фреймворки на помоечку, вместо всего этого универсальный язык разметки с размерами в миллиметрах (отобразить правильно задача драйвера железки) для всего от принтеров, до экрана телефона. Все иконки строго векторные
Идея с универсальным языком для отображения на всех устройствах — хорошая. Каким он должен быть? Похожим на PostScript или попроще?
Здравствуйте, Pavel Dvorkin, Вы писали:
ARK>>Ну так а в чем разница с дырой в процессоре?
PD>Разница в том, что Meltdown заштопали вроде как. С накладными расходами, но заштопали. PD>Потому что это все же дыра на уровне процессора, а у процессора есть kernel mode и user mode, и в kernel mode пользовательские программы не пускают ни под каким видом, а у kernel mode есть хозяин (ОС) , в которую только и нужно внести изменения, что и было сделано.
Я говорю не о Meltdown, а о такой дыре, которую заштопать невозможно (и которая, вполне возможно, присутствует в современных процессорах).
PD>А вот что будут делать, если в алгоритме статической верификации обнаружилась ошибка, а программы уже прошли этап этой верификации, разошлись в миллионах копий и теперь рушат ОС или получают доступ к чужой памяти — объясни. Срочно патчить все выпущенные программы ? Как ? Фирма, выпустившая эту программу, давно закрылась, авторы разбрелись кто куда.
А что вы будете делать, если в процессоре найдут дыру, которую невозможно заштопать удаленными средствами? Процессоры разошлись в миллионах копий и теперь рушат ОС. Срочно менять все компьютеры?
Или вы считаете, что такой дыры в процессоре быть не может в принципе?
Если такой дыры в процессоре даже теоретически быть не может, то почему тогда вы считаете, что такая дыра может быть в верификаторе?
Если такая дыра в процессоре теоретически возможна, то чем подход с защитой в процессоре лучше подхода с защитой путем верификации?
Здравствуйте, AlexRK, Вы писали:
ARK>Угу, конечно. Ошибок в доказательстве быть не может.
Конечно не может. Его машина проверяет.
Единственный шанс ошибки проскочить это если верификатор сломается.
А он очень простой. И его не трудно доказать.
ARK>Запросто может быть что угодно, причем доказать доказательство будет на порядки сложнее, чем обычный код.
Ну попробуй написать код, который выходит за приделы массива.
Править предусловия массива то ты не можешь.
ARK>Все корректно проверяется, только вот программа будет выдавать совершеннейший мусор.
То, что ты сделал можно сделать проще. Достаточно просто выкинуть предикаты SortedRange и PremutateRange и всё.
В реальной жизни предикаты SortedRange и PremutateRange будут лежать в стандартной библиотеке. И эта баблиотека будет изучена и протестирована до дыр.
И изменить их ты не сможешь.
И маразм дафны с old(a[..]) тоже можно устранить.
А вот теперь попробуй, используя оригинальные предикаты и их правильное использование написать что-то кроме сортировки.
Ну и главное не забудь обратиться за приделы массива.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Я же не против верификатора, но речь-то идет об ОС, где нужна 100% надежность, хотя бы в принципе. Одна дыра — и мало не покажется, не заштопаешь. Программы уже на компьютере пользователя, этап статической верификации позади, иной защиты нет, не поправишь, как Meltdown.
Это просто курам на смех. Обновить ОС куда проще. После чего ОС перепроверит весь установленный софт.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
WH>Ну попробуй написать код, который выходит за приделы массива. WH>Править предусловия массива то ты не можешь.
Понятно, что я не смогу выйти за пределы массива. Речь о том, что само по себе доказательство может содержать логические ошибки и доказывать совсем не то, что имел в виду автор. Или вообще не доказывать (хотя автор уверен, что доказательство работает). Вот об этом речь. И такие вещи поймать будет ой как сложно.
WH>А вот теперь попробуй, используя оригинальные предикаты и их правильное использование написать что-то кроме сортировки. WH>Ну и главное не забудь обратиться за приделы массива.
Да и и в C# не могу выйти за пределы массива, без всяких предикатов.
Конечно, ошибка компиляции всегда лучше рантайм-ошибки, но в массы такие доказательства точно не пойдут.
Здравствуйте, AlexRK, Вы писали:
ARK>Понятно, что я не смогу выйти за пределы массива.
Теперь смотрим на что я отвечал:
Ну в смысле если в паре мест перепутать "<" и "<=" или "a" и "b" — компилятор гарантированно обнаружит ошибку? Или просто получится какое-то другое доказательсто — логически верное с т.з. компилятора, но иногда допускающее выход за границы массива, например?
ARK>Речь о том, что само по себе доказательство может содержать логические ошибки и доказывать совсем не то, что имел в виду автор. Или вообще не доказывать (хотя автор уверен, что доказательство работает). Вот об этом речь. И такие вещи поймать будет ой как сложно.
Доказательствами будет заниматься очень небольшой процент высококвалифицированных программистов.
ARK>Конечно, ошибка компиляции всегда лучше рантайм-ошибки, но в массы такие доказательства точно не пойдут.
И не надо.
Перечитай вторую половину вот этого сообщения
Здравствуйте, AlexRK, Вы писали:
ARK>Я говорю не о Meltdown, а о такой дыре, которую заштопать невозможно (и которая, вполне возможно, присутствует в современных процессорах). ARK>Или вы считаете, что такой дыры в процессоре быть не может в принципе? ARK>Если такой дыры в процессоре даже теоретически быть не может, то почему тогда вы считаете, что такая дыра может быть в верификаторе? ARK>Если такая дыра в процессоре теоретически возможна, то чем подход с защитой в процессоре лучше подхода с защитой путем верификации?
Мы тут уже в область абстракций переходим. Пока что дыры такой нет, и жизнь вполне себе идет. Если найдется — не знаю, что будет. Но пока что за 40 лет такого не оказалось.
Если будет реально сделана ОС с этой самой статической верификацией, если ее не взломают через полгода, если она пойдет по другим критерием — тогда видно будет.
В реальность этого я плохо верю.
Что-то мне интуиция подсказывает, что такое предложить рынку всерьез ни одна фирма не решится. Эксперименты — да, пожалуйста.
На этом предлагаю дискуссию и закончить, тем более, что через день я уезжаю, а там, где буду, Интернет крайне плохой, и не уверен, что я хоть что-то напишу. Да и не любитель я писать с телефона.
Здравствуйте, WolfHound, Вы писали:
WH>Не пойму ты со мной споришь или соглашаешься.
Спорю с тем, что натив не нужен.
WH>Компилятор дело техники. Если нет нативного кода, то его нужно написать один раз. И интел в конце концов написал. WH>А вот то что он тормозил в 10 раз на исполнении x86'ого кода его и убило.
Переписывая по сути с нуля ОС, субд и вот это вот все. Разумеется не взлетит.
Здравствуйте, WolfHound, Вы писали:
PD>>Я же не против верификатора, но речь-то идет об ОС, где нужна 100% надежность, хотя бы в принципе. Одна дыра — и мало не покажется, не заштопаешь. Программы уже на компьютере пользователя, этап статической верификации позади, иной защиты нет, не поправишь, как Meltdown. WH> WH>Это просто курам на смех. Обновить ОС куда проще. После чего ОС перепроверит весь установленный софт.
И сообщит пользователю, что его любимая программа, которая сейчас вылетает по access violaltion один раз в полгода, будет удалена с компьютера, так как она эту новую верификацию не прошла.
Куры плачут уже, а не смеются.
Пользователи говорят <censored> и сносят эту ОС.
Здравствуйте, MTD, Вы писали:
Z>>А задача армии дизайнеров и верстальщиков, сверстать дизайн в миллиметрах для каждого экрана. MTD>Вот смотри. Палец среднестатистического человека, допустим имеет пятно контакта 5 на 5 мм, из этого следует, что надо кнопочку сделать 10 на 10 мм, условно. Потом, есть текст, известно, что он хорошо читается размером 7 мм, тоже условно. Если задавать размеры в мм, то и выглядеть везде будет одинаково и взаимодействовать будет возможно одинаково. Еще раз — 1 раз задать, получить одно и тоже везде. Теперь переходим к условным попугаям в пикселах — в зависимости от плотности пикселов размер меняется в разы, так что твой комментарий актуален сейчас, если перейти на миллиметры жизнь серьезно упроститься.
В миллиметрах — это тоже не верно, потому что для человеческого взгляда важен угловой размер, а не линейный. Т.е. 7мм на смартфоне и на телевизоре — это очень разные вещи, из-за того, что их рассматривают с разного расстояния. Более того, есть ещё и различные особенности зрения (близорукость там и т.п.), из-за которых пользователи предпочитают менять под себя стандартный размер шрифтов. Так что жёсткое зашивание размеров элементов GUI в миллиметрах — это опять же пример плохой реализации GUI.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>И сообщит пользователю, что его любимая программа, которая сейчас вылетает по access violaltion один раз в полгода, будет удалена с компьютера, так как она эту новую верификацию не прошла.
Есть и другой вариант.
ОС находит те места, которые не может верифицировать и добавляет туда проверку.
Сделать это можно полностью автоматически. Примерно так же как это делает ява и компания.
Приложение немного замедлится, но будет работать.
Пользователь скорее всего ничего даже не заметит.
PD>Куры плачут уже, а не смеются. PD>Пользователи говорят <censored> и сносят эту ОС.
Либо в клиническом случае пользователи качают патч на эту программу и всё.
Ты кстати в курсе что винда молча при запуске исправляет некоторые популярные программы чтобы они работали.
Так что тут опять нет ничего нерешаемого.
Ну и не забывай о том, что мы говорим о крайне гипотетической ситуации.
Ибо верификатор на несколько порядков проще чем процессор.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Sharov, Вы писали:
WH>>Компилятор дело техники. Если нет нативного кода, то его нужно написать один раз. И интел в конце концов написал. WH>>А вот то что он тормозил в 10 раз на исполнении x86'ого кода его и убило. S>Переписывая по сути с нуля ОС, субд и вот это вот все. Разумеется не взлетит.
Это нужно исключительно из-за того код нативный.
Если бы код был под ВМ, то никакого переписывания было бы не нужно.
Всё просто бы заработало.
Объём переделок в случае с ВМ только бэкенд и очень маленькая часть ядра ОС.
Объём работы сопоставимый с адаптацией одного компилятора под новый процессор.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Что из того, что заложено в существующее ПО, сделано так, как и надо было бы "по уму" сделать, и что надо было бы сделать иначе, да только , увы, невозможно — мешают проклятая compatibility и огромные наработки ?
— Другие сетевые протоколы в сети Internet. Помимо личного адреса каждой кофеварке, должны обеспечивать идентификацию, аутентификацию и шифрование для каждого каждого узла в сети. сетевой адрес должен быть прибит гвоздями к конкретной железке и провайдеру
— Стандартный байткод. Все языки высокого уровня, как со сборкой мусора, так и без неё, компилируются только в него. Компиляторы в нативный код стоят на машинах конечных пользователей и понимают только стандартный байткод. У стандартного байткода есть "безопасное" подмножество, программы на котором можно использовать в песочницах типа браузера.
— Полная aппаратная и программная поддержка изоляции процессов в ОС.
— Единый стандарт взаимодействия программ с ОС. POSIX был хорош, но недостаточен.
— Единый стандарт платформ для дистрибьюции софта, включая платный софт. Включая платные библиотеки, входящие в платный софт
— Компании, которые специализируются на разработке платных библиотек и рантаймов с монетизацией "0.1% с каждой проданной программы, которая использует нашу либу"
Здравствуйте, WolfHound, Вы писали:
WH>1)Запретить языки с динамической типизацией.
Даже для 3-ёх строчных скриптов? ) Вот буквально вчера у меня тут обнаружилось, что fb2 файлы скаченные с одного известного сайта имеют некорректную структуру (содержат html entities, хотя fb2 — это обычный xml) и из-за этого не читаются некоторым ПО. Проблема была решена (причём для целой папки таких fb2 файлов за раз) за минуту в три строчки на Питоне. На популярных статических языках я бы к этому времени успел бы разве что оборудовать инфраструктуру (настроить проект или скрипты сборки) и перешёл бы к написанию обязательного каркаса приложения...
WH>2)Запретить нативный код. WH>Проблема нативного кода в том, что он не даёт заменять систему команд процессоров. WH>Через пару лет после того как не станет нативного кода x86 сдохнет. WH>Исключение можно сделать только для совсем дохлых микропроцессоров где даже ОС нет.
Согласен (и кстати для МК не обязательно делать исключение). И думаю что идеальной заменой нативного кода должно быть что-то вроде LLVM IR. Согласен? )
Кстати индустрия постепенно движется в этом направление: если webassembly (которые внутри по сути и есть LLVM IR, с мелкими правками для облегчения организации песочницы) реально взлетит, то...
WH>3)За основу ОС берем мидори. http://joeduffyblog.com/2015/11/03/blogging-about-midori/
WH>mutable, readonly и immutable становятся атрибутами кластеров.
Ну про это я тебе уже говорил, что самая идея любопытная, но требуется хотя бы один реально работающий прототип, чтобы оценить эффективность на реальных тестах. А то из подобной теории совершенно не очевидны итоговые параметры производительности.
WH>в)Добавляем http://halide-lang.org/ для параллельного программирования.
Ну "параллельное программирование" — это громко сказано. Всё же в общем случае оно делится (на современном железе) на 3 совместно работающих уровня: SIMD, многоядерность (решения типа OpenMP), кластеры (решения типа MPI). И данный язык, насколько я помню, занимался решением только нижнего уровня параллельности (SIMD).
WH>г)Заменяем контракты на это: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/
Любопытная игрушка, но до реального применения ей ещё очень далеко. Но будем следить...
Здравствуйте, WolfHound, Вы писали:
PD>>Я же не против верификатора, но речь-то идет об ОС, где нужна 100% надежность, хотя бы в принципе. Одна дыра — и мало не покажется, не заштопаешь. Программы уже на компьютере пользователя, этап статической верификации позади, иной защиты нет, не поправишь, как Meltdown. WH> WH>Это просто курам на смех. Обновить ОС куда проще. После чего ОС перепроверит весь установленный софт.
Так ты хочешь верификатор, который работает не с исходным, а с исполняемым кодом? Хм хм хм...
Здравствуйте, WolfHound, Вы писали:
WH>ОС находит те места, которые не может верифицировать и добавляет туда проверку.
М-да... В общем, без проверок в рантайме ничего не выходит ни у тебя, ни у AlexRK. Если ОС или верификатор не может верифицировать, надо вставлять проверку в рантайме,
Кстати, не совсем понял, как ОС верифицировать-то будет ? Вроде в дискуссии с AlexRK мы исходили из того, что проверяет статический анализатор на этапе компиляции.
Компиляция прошла давно, на машине пользователя бинарник. Машинные коды верифицировать будем ?
WH>Либо в клиническом случае пользователи качают патч на эту программу и всё.
Фирма, выпустившая программу, давно не существует, программисты разбрелись. Ты в курсе, что программы иногда живут очень долго ?
WH>Ты кстати в курсе что винда молча при запуске исправляет некоторые популярные программы чтобы они работали.
WH>Ну и не забывай о том, что мы говорим о крайне гипотетической ситуации. WH>Ибо верификатор на несколько порядков проще чем процессор.
Вот только бы знать, насколько менее надежен.
По большому счету, за 35 лет существования защищенного режима (считая с 80286, 1982 год) критических (неисправляемых) ошибок в нем не оказалось. Вынесли эти процессоры все версии Windows, Unix-Linux, а потом и MacOS — ничего, все нормально.
Ладно. Появится эта самая верфицируемая ОС в реальном мире (не экспериментальная Singularuty, приказавшая долго жить, а то, что продается сотнями миллионов копий), подождем 35 лет — посмотрим.
Вот только скорее всего ее появление и есть крайне гипотетическая ситуация.
Здравствуйте, alex_public, Вы писали:
_>Так ты хочешь верификатор, который работает не с исходным, а с исполняемым кодом? Хм хм хм...
Не с исполняемым, а с промежуточным. Что-то типа MSIL только сделанный по-умному, а не как у МС.
И работать на этом уровне намного проще чем с исходным кодом.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
PD>А вот что будут делать, если в алгоритме статической верификации обнаружилась ошибка, а программы уже прошли этап этой верификации, разошлись в миллионах копий и теперь рушат ОС или получают доступ к чужой памяти — объясни. Срочно патчить все выпущенные программы ? Как ? Фирма, выпустившая эту программу, давно закрылась, авторы разбрелись кто куда.
(небольшая придирка) Фирмы, работающие в таких объемами так быстро не исчезают. Как минимум сотрудники на тех поддержку и саппорт отстаться должны.
