Комментарии 31
Как только много лет назад я узнал о L4, и о том, что L4 формально верифицируют, я был в экстазе.
Буквально через месяц, когда я всерьез начал работу над проектом, где L4 было в качестве микроядра, я осознал, что это не сработает никогда.
Потому что можно формально верифицировать ядро. Но формально верифицировать хотелки заказчика…
Буквально через месяц, когда я всерьез начал работу над проектом, где L4 было в качестве микроядра, я осознал, что это не сработает никогда.
Потому что можно формально верифицировать ядро. Но формально верифицировать хотелки заказчика…
я был в экстазе
Чорт, я прямо сейчас
P.S. Даже мимо ветки промахнулся под впечатлением. Или это таки глюк движка?
Злоумышленник в потоке камеры сделает вот так и будет глубоко пофигу, что микроядро формально корректно работает, и компилятор формально верифицирован…
А все от того, что есть доверие к процессору. И к памяти доверие тоже есть… А если тяжелая заряженная частица пролетит через ту память?!
А все от того, что есть доверие к процессору. И к памяти доверие тоже есть… А если тяжелая заряженная частица пролетит через ту память?!
Зачем тяжёлая заряженная частица? Можно аккуратно лазером посветить в нужный бит памяти)
>Злоумышленник
ИМХО верификация (по крайней мере, на текущем этапе) это больше о надежности, чем о безопасности. Начиная от хитрых физических эффектов типа Rowhammer, некоторые из которых обязательно забудут включить в модель; и заканчивая тем, что в самый первый раз верификатор запускается на неверифицированной системе, которая может быть за счет этого скомпрометирована и намеренно давать ложноположительные результаты (а париться с инкрементальной верификацией и начинать с человекопроверяемого уровня никто не станет). Плюс для верификации нужна сперва спецификация, которая, по сути, тоже код, потенциально содержащий ошибки. Плюс намеренные бэкдоры. Плюс зоопарк периферии и отсутствие контроля над ее производством. Так что это скорее актуально в случае какой-то узкоспециализированной системы, которую очень дорого или невозможно фиксить от багов, но на которую не проводится атак.
ИМХО верификация (по крайней мере, на текущем этапе) это больше о надежности, чем о безопасности. Начиная от хитрых физических эффектов типа Rowhammer, некоторые из которых обязательно забудут включить в модель; и заканчивая тем, что в самый первый раз верификатор запускается на неверифицированной системе, которая может быть за счет этого скомпрометирована и намеренно давать ложноположительные результаты (а париться с инкрементальной верификацией и начинать с человекопроверяемого уровня никто не станет). Плюс для верификации нужна сперва спецификация, которая, по сути, тоже код, потенциально содержащий ошибки. Плюс намеренные бэкдоры. Плюс зоопарк периферии и отсутствие контроля над ее производством. Так что это скорее актуально в случае какой-то узкоспециализированной системы, которую очень дорого или невозможно фиксить от багов, но на которую не проводится атак.
Они тут конкретную модель угроз заявили. И хакеров притянули за уши к процессу. И суть защиты в изолировании памяти. Так вот в этой модели — и с защитой памяти птичку можно уложить при неких исследованиях «поглубже»…
Верификация просто обычное дело для всякого летающего и мало отношения имеет к взлому.
Верификация просто обычное дело для всякого летающего и мало отношения имеет к взлому.
А чем формальная спецификация ОС отличается от формального исходного кода ОС? И там и там могут быть баги. Если мы предполагаем, что формальная спецификация не содержит ошибок, то мы можем так же предположить, что исходный код не содержит ошибок. Если же мы допускаем возможность ошибок в формальной спецификации, то это получаются, обычные тесты на необычном языке. Часть багов ловят, но не идеальны.
Тесты не покрывают все возможные пути выполнения обычно, а верификация покрывает. Это скорее можно сравнить с параллельным написанием программы на двух языках. Но в плане багов да.
Если представить себе тесты с 100% cyclomatic coverage, то это же оно и будет? То есть люди говорят про «формальное доказательство программы», и все себе представляют волшебную программу без багов. А в реальности — это всего лишь tdd-от-математиков.
unsigned char unsafe_images_vault [100500];
unsigned char kernel_security_settings [256];
//какой-то код
void verySecureFunction (size_t l)
{
memcpy(kitty_image_with_shellcode_ptr, unsafe_images_vault, l);
}
Тестовое покрытие не учитывает состояние, разве нет? Если тесты покрывают эту функцию, это ничего в общем случае не говорит о состоянии в момент прохода, а в низкоуровневых языках (да и не только) фактический смысл кода может полностью изменяться при изменении состояния, как в примере выше. Если доступ к памяти никак не ограничивается, то вариантов будет околобесконечное количество для каждой функции, и все не протестируешь.
НЛО прилетело и опубликовало эту надпись здесь
Нет, это не то же самое. Тестами невозможно покрыть 100%. Даже если покрыты все ветки, остаются ещё все комбинации всех значений переменных. Если в программе есть рекурсивные структуры данных типа списков или деревьев, то количество возможных значений бесконечно.
Там в принципе совершенно другой подход. Например, как выглядят олимпиады по программированию. Дают задание на написание программы, которая что-то делает, дают примеры входных тестовых данных и примеры ожидаемых выходных. Человек пишет программу, запускает её на этих тестовых данных. Добавляет для верности какие-то свои тесты. Затем если программа нормально работает на тестовых данных на сервере, то всё норм.
А, вот, как выглядит это с формальными доказательствами. Дается задание написать функцию, которая после тройного применения к списку возвращает исходный список. Задание написано на формальном языке, его невозможно как-то неправильно интерпретировать. И нет ни одного теста! Ни в задании, ни на сервере, ни самому разработчику их тоже писать не нужно. Если программа соответствует спецификации, то она на 100% корректна.
Как вы эту простую задачку покрыли бы тестами на 100%? Тестов должно было бы быть бесконечное количество.
Там в принципе совершенно другой подход. Например, как выглядят олимпиады по программированию. Дают задание на написание программы, которая что-то делает, дают примеры входных тестовых данных и примеры ожидаемых выходных. Человек пишет программу, запускает её на этих тестовых данных. Добавляет для верности какие-то свои тесты. Затем если программа нормально работает на тестовых данных на сервере, то всё норм.
А, вот, как выглядит это с формальными доказательствами. Дается задание написать функцию, которая после тройного применения к списку возвращает исходный список. Задание написано на формальном языке, его невозможно как-то неправильно интерпретировать. И нет ни одного теста! Ни в задании, ни на сервере, ни самому разработчику их тоже писать не нужно. Если программа соответствует спецификации, то она на 100% корректна.
Как вы эту простую задачку покрыли бы тестами на 100%? Тестов должно было бы быть бесконечное количество.
Так оно и будет для однопоточных, детерминированных, нераспределенных (т.е. тривиальных) программ.
В реальности «волшебная программа без багов» невозможна.
Товарищ Тюринг это математически доказал, кстати.
Конечно, товарищ Гедель в своей теореме о неполноте по большому счету доказал почти то же, но Тюринг все-таки как-то ближе к программистам… :-)
Товарищ Тюринг это математически доказал, кстати.
Конечно, товарищ Гедель в своей теореме о неполноте по большому счету доказал почти то же, но Тюринг все-таки как-то ближе к программистам… :-)
Вы путаете существование программы без багов и возможность доказать, что данная программа без багов.
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Ха-Ха-ХА! Туше :-).
Но я даже могу сказать какая программа без багов существует — та, которая не написана. Нет программы — нет проблем.
Но я таки предполагал какую-то программу из реального мира, что предполагает, что она должна удовлетворять некоторому (хотя бы минимально очевидному) ТЗ.
И тут, конечно, возникают проблемы.
В реальности «волшебная программа без багов» невозможна.Он доказал, что существуют программы, у которых невозможно проверить корректность. Вот такие писать не надо.
Товарищ Тюринг это математически доказал, кстати.
Тоже занимался темой самодиагностики программ
habr.com/ru/post/342302
Пришел к выводу, что надо писать некий контейнер, в который помещаешь маленькие хотелки, которые выдают свои маленькие действия. Контейнер проверят, чтобы действия хотелок не противоречили друг другу.
habr.com/ru/post/342302
Пришел к выводу, что надо писать некий контейнер, в который помещаешь маленькие хотелки, которые выдают свои маленькие действия. Контейнер проверят, чтобы действия хотелок не противоречили друг другу.
Помоему самая главная мысль из этой статьи заложена здесь:
Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере
Что такое CAN? CAN — это CAN (англ. Controller Area Network — сеть контроллеров) — стандарт промышленной сети, ориентированный на передачу коротких, изначально заданных сообщений в реальном времени. Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать. Т.е. вы не сможете передать что-то, что не заложено в устройство на этапе проектирования сети — например файл, вирус, или изображение. Т.е. взломать Flight Computer через тот же CAN — физически невозможно. Возможно только повлиять на его работу давая ложные данные, но он их может перепроверить и не принять.
Т.е. изолируем критическую часть системы управления от некритической каким-то примитивным железным протоколом — и можно говорить, что уже половина дела в защите от кибератак сделана.
Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать.
Я бы сказал, что это слишком сильное заявление…
Которое отменяет все, что я сказал, чтобы ставить минусы?
В целом да. Вот рассказ про взлом CAN в автомобиле, первая же ссылка из гугла.
Вы не можете взломать CAN в автомобиле, не получив физического доступа к проводам сети. Поэтому я не считаю это кибератакой. Кибератака, на мой взгляд, это взлом с использованием только программного обеспечения и через существующие коммуникации и их уязвимости.
Окей, вот пример чисто программного вскрытия коммуникаций через девайс, подключенный к остальному оборудованию автомобиля через CAN.
Ну так и причем тут CAN?
Что изменится если заменить CAN на любые «внутренние провода»?
Переформулирую:
— невозможно «взломать CAN» также как нельзя взломать RS-232 или провода в розетке.
— но иногда можно взломать application уровень поверх CAN (или RS-232) и зависит это целиком от протоколов запущенного поверх CAN и их обработчиков.
Что изменится если заменить CAN на любые «внутренние провода»?
Переформулирую:
— невозможно «взломать CAN» также как нельзя взломать RS-232 или провода в розетке.
— но иногда можно взломать application уровень поверх CAN (или RS-232) и зависит это целиком от протоколов запущенного поверх CAN и их обработчиков.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Микроядро seL4. Формальная верификация программ в реальном мире