Comments 30
Тема защиты каналов данных нифига не раскрыта. Скажем, если мы поддерживаем обычный протокол типа SSL, и в нем найдены какие-то уязвимости by design — у нас в ОС они тоже есть? А если нет — то как верифицированное микроядро от них защитит?
Кроме того, слабое место всех без исключения подобных проектов — это периферия вообще. Т.е. грубо говоря, как только у вас появились устройства — у вас появились драйвера. Драйвера в пользовательском пространстве ограничены, потому что переключение контекста — иногда слишком дорогая штука, чтобы часто позволять ее себе.
А драйвера в пространстве ядра, с привилегиями ядра — это дырища, и это так во всех системах. Исключениями являются разве что системы типа IOS — у которых фактически не бывает сторонней периферии. Кроме того, нынешние железяки сами по себе содержат кучу закрытого софта.
Т.е., можно сделать сверхнадежную ОС — но она будет ограничена поддержкой узкого набора периферии, и плохой совместимостью с внешними системами. Как-то так.
Ну, в сверхнадежных ОС нуждаются организации, которые вероятнее всего заказывают переферию. И это лишь вопрос времени, когда появится необходимое количество переферии для комфортабельного персонального использования.
Так это не вопрос. Вопрос в том, что это (т.е. верификацию кода ядра) нельзя рассматривать как технологию, которая позволить достичь безопасности массово.
Периферия — вопрос времени? А ничего, что производителей некоторых видов периферии считанное число в мире вообще? Т.е. например, типовой HDD или SSD, или видеокарта содержат внутри гигабайты кода, который никем не верифицирован, который вообще никто не видел, и при этом он имеет доступ ко всему железу (например к памяти, потому что архитектура-то компьютера у нас все равно может быть обычная, например x86). А ОС для дронов — почему нет, можно наверное.
Драйвера в пользовательском пространстве ограничены, потому что переключение контекста — иногда слишком дорогая штука, чтобы часто позволять ее себе
У L4 нет драйверов в ядре. У нее даже диспетчера памяти в ядре нет. Ядро в L4 сверхмаленькое, такие ядра даже называются наноядрами (чтобы отличать от микроядер, подобных Mach, которые по сравнению с L4 просто гиганты).
И переключение контекста в L4 на порядок или на два порядка дешевле мейнстримных ОС. Пересылка данных между процессами может быть в режиме «взял страницу памяти, убрал из памяти 1 процесса, заммэппил другому».
От вас несёт уринотерапией и прочим ГМО. Математика никогда не отказывается рассматривать все возникающие случаи. Просто она рассматривает специальные случаи отдельно. Вы ещё скажите, что математика не умеет оперировать полем характеристики 2. Ещё как умеет, просто этот случай описан отдельно, а для множества других теорем внесён как исключение. И так везде.
Это не так, все математические операции определены на некоторых множествах. Если вы видите «деление на ноль» как специальный случай, то вы определяете деление так, что второй операнд должен принадлежать множеству, включающему в себя ноль.
Отсутствие определения деления на ноль в ряде случаев — это явление того же порядка, как отсутствие определения деления, к примеру, на поле. Вот у нас есть поле ℚ (в котором, кстати, деление на ноль не определяется) и с ним мы можем написать a/b и что‐то с этим делать дальше. К вам пришёл студент и написал a/ℚ. Значит ли это, что вам внезапно нужно начать рассматривать «специальный случай» «деление числа на поле», добавив его во все теоремы, где вы что‐то на что‐то делите или нужно послать такого человека куда подальше, потому что поле ℚ не входит в множество рациональных чисел, на котором у вас определено деление (кроме деления на ноль, которое не определено вполне себе официально)?
Но пока студент не дал «валидное описание для объектов a/ℚ» эта ситуация именно что «просто не рассматривается». И с делением на ноль то же самое: оно может быть не определено и, соответственно, не рассматриваться. Возможно, это приведёт к возникновению специального случая в другом месте (пример: решение a * x = b, когда a = 0: мы не будем рассматривать неопределённое b / a, мы скажем, что если a = 0, то x — любое число, если b = 0 и укажем на отсутствие решения, когда b ≠ 0), возможно мы доопределим операцию деления, но случай за границами области определения рассматриваться не будет.
Кстати, они ещё и подстраиваются под разные применения. Если ожидается постоянное деление на ноль, то они готовы ввести теорию, которая будет разделять разные типы возникающих в задаче нулей, задействуют более сильные абстракции вроде актуальных бесконечно малых и неархимедовы поля.
Математический подход в корне отличается от того, что вы написали — давайте сделаем какую-нибудь запись алгоритма, и проигнорируем все возможные ошибки выполнения. В математике записи и формулы ничего не стоят, если за ними не стоит какой-то теории, доказательств существования и корректности объектов, упомянутых в этих записях. Написать (назвать) можно всё что угодно, хоть треугольник с четырьмя углами. Объектом рассмотрения математики эта бессмыслица не станет.
Скорее всего кодом или частью когда кто то уже располагает, иначе они б не офишировали то что пробуют создать самую крутую для дронов ОС или исправить уязвимости коих нет, как выходит из статьи тем более что услуги данных компаний стоят как ВВП некоторых стран!
Если ее действительно тестили то ошибки точно были найдены и убраны, так как никто не будет писать что в дронах специального(военного) назначение нашли уязвимости… кто их купит после того ?)
2.Теперь тупая идея с ПЗУ от third112:
(ПЗУ) предназначены для постоянного хранения информации, которая записывается туда при изготовлении и не подлежит изменению. Следовательно, прочитать эту информацию можно, а изменить нельзя. Даже при выключении питания информация в ПЗУ остается, в этом состоит отличие ПЗУ от ОЗУ. — Отличный повод сбить дрон, снять ПЗУ считать все ПО и дизесимблировать или изменить под себя! Поверте самый тугой способ защиты!
Для разницы и контраста:
(ОЗУ) предназначены для записи, хранения и считывания информации при запуске и работе системы;
При выключении питания вся информация из ОЗУ разрушается. — следовательно противник может похвастаться что у него есть чистый ОЗУ отжатый у дрона на котором нифига нет :)
Вопрос в том, является ли дрон тем случаем, когда надо закрыть ПО. Ну, наверно, закрыть его от произвольного доступа — надо: доступ д.б. только у тех, кто разрабатывает дрон. Осталось понять, сколько людей будут иметь доступ к ПО, и какова вероятность того, что ПО утечёт через одного из людей, имеющих доступ.
Если ПО дрона в ОЗУ, то как оно там окажется? Заливать его туда перед запуском?
Кстати, интересная идея. Ведь задачу (координаты цели) всё равно надо будет заливать.
2.ПО для военных разработок — сугубо закрытое, глупо спорить почему оно не должно быть ОПЕН СОРС)))
3.Есть смысл заливать через каналы, так как он будет заточен именно под конкретные задачи и например набор программ для операторов дрона будет сугубо для выполнения миссии! Не нужно знать операторам всевозможные программы и интерфейсы дрона (я в том смысле на заданиях, что бы не отвликать внимание и не иметь возможность превышать полномочия)
Если ПО дрона в ОЗУ, то как оно там окажется? Заливать его туда перед запуском?Такой метод очень уязвим. Если в дроне стоит носитель информации, нпр., HDD или ПЗУ, то бортовой компьютер можно сделать в виде единого невскрываемого блока залитого эпоксидкой, с устройством саморазрушения. В этом случае у технического персонала, обслуживающего дрон, не будет возможности скопировать систему. А если заливать систему с компа перед запуском, нпр., через USB, то оператор-шпион может легко записать ее на флешку с минимальным риском для себя.
Отличный повод сбить дрон, снять ПЗУ считать все ПО и дизесимблировать или изменить под себя!Чтобы секретная информация не попала в руки противника борт снабжают системой саморазрушения. Если не весь дрон, то ПЗУ разрушить не так уж сложно. Зачем читать ПЗУ? Чтобы сделать копию дрона? У противника для этого должен быть неслабый индустриальный уровень. Но учитывая нарастающую скорость прогресса подобное копирование становится все более и более сомнительным — пока противник делает копию, появятся более совершенные дроны и копия окажется устаревшей. Если я правильно понял статью, речь идет о другой защите — о защите от перехвата управления дроном в полете, когда противник по каналам связи внедряет в систему свои компоненты. В ПЗУ такое внедрение невозможно. ОЗУ уязвимо не только внедрением осмысленного кода, но, что гораздо проще сделать, внедрением случайного кода, который просто нарушит работу системы и дрон упадет. Если дрон сбит и попал в руки противника источник питания (а значит и информация в ОЗУ) может уцелеть. Если противнику так нужна система дрона, то он будет сбивать так, чтобы ОЗУ и питание уцелели, нпр., стрелять по винтам и двигателям, но не по корпусу. ИМХО над этими вопросами не могли не думать разработчики и если они не использовали столь простое и очевидное решение, как ПЗУ, значит на это есть веские основания. К сожалению, статья их не приводит.
(ПЗУ) предназначены для постоянного хранения информации, которая записывается туда при изготовлении и не подлежит изменению.Само ПЗУ (микросхему) обычно делают на заводе пустой. А зашить туда инфу можно где угодно (хоть в полевых условиях) для этого нужен ПК с картой программатора. Столь же просто, как DVD-R прожечь.
Кстати, я совершенно не понимаю, зачем тут приведено три «типа атак». Все они сводятся к «уязвимостям в ПО».
Т.о. ИМХО можно говорить только о частичной и очень ограниченной верификации.
Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP).Год сообщения 2009. Работу признали?
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода.При таких объемах возникают большие сомнения.
Обычно под формальной верификацией понимают скорее проверку соответствия формальной модели (не конкретной конечной реализации) некоторым требованиям (например, нет гонок, нет бесконечных циклов, нет выходов за границы массивов и так далее). То есть, например, я пишу некий алгоритм, и хочу формально доказать, что он ни при каких условиях — любые комбинации собственного состояния, входных данных, переключений контекста потоков — не сможет писать/читать не свою память, не зависнет, всегда выполнится за ограниченное количество шагов… вот такого плана задачи. Хотя, судя по их публикациям, корректность реализации они тоже проверяли.
реакция совсем другая: «это непрактично», «всего не предусмотришь»
А ведь так и есть, собственно, из идеи «всего не предусмотришь» и выросла философия аджайл. Другое дело, когда программисты просто ленятся или не могут(в силу неразвитости абстрактного мышления) качественно продумать концепцию во всех аспектах перед реализацией. То есть им, грубо говоря, проще сначала вырыть траншею, а потом уже посмотреть, ровная ли она и подровнять(или подг***ять), если не очень. Работаю в среднестатистической веб-конторе, таких большинство.
Что еще более интересно теперь нам, спустя 5 лет — то что этот L4 MSM похоже взломали:
research.checkpoint.com/2021/security-probe-of-qualcomm-msm
Позволит ли формальная верификация кода микроядра создавать сверхнадежные ОС