Comments 31
Буквально через месяц, когда я всерьез начал работу над проектом, где L4 было в качестве микроядра, я осознал, что это не сработает никогда.
Потому что можно формально верифицировать ядро. Но формально верифицировать хотелки заказчика…
я был в экстазе
Чорт, я прямо сейчас
P.S. Даже мимо ветки промахнулся под впечатлением. Или это таки глюк движка?
Но просто вспомните последний раз, когда вы видели формально оформленные требования от заказчика, и вернитесь в реальность.
А если этого недостаточно, то вспомните теорему о неполноте.
ИМХО верификация (по крайней мере, на текущем этапе) это больше о надежности, чем о безопасности. Начиная от хитрых физических эффектов типа Rowhammer, некоторые из которых обязательно забудут включить в модель; и заканчивая тем, что в самый первый раз верификатор запускается на неверифицированной системе, которая может быть за счет этого скомпрометирована и намеренно давать ложноположительные результаты (а париться с инкрементальной верификацией и начинать с человекопроверяемого уровня никто не станет). Плюс для верификации нужна сперва спецификация, которая, по сути, тоже код, потенциально содержащий ошибки. Плюс намеренные бэкдоры. Плюс зоопарк периферии и отсутствие контроля над ее производством. Так что это скорее актуально в случае какой-то узкоспециализированной системы, которую очень дорого или невозможно фиксить от багов, но на которую не проводится атак.
Верификация просто обычное дело для всякого летающего и мало отношения имеет к взлому.
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%? Тестов должно было бы быть бесконечное количество.
Товарищ Тюринг это математически доказал, кстати.
Конечно, товарищ Гедель в своей теореме о неполноте по большому счету доказал почти то же, но Тюринг все-таки как-то ближе к программистам… :-)
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Ха-Ха-ХА! Туше :-).
Но я даже могу сказать какая программа без багов существует — та, которая не написана. Нет программы — нет проблем.
Но я таки предполагал какую-то программу из реального мира, что предполагает, что она должна удовлетворять некоторому (хотя бы минимально очевидному) ТЗ.
И тут, конечно, возникают проблемы.
В реальности «волшебная программа без багов» невозможна.Он доказал, что существуют программы, у которых невозможно проверить корректность. Вот такие писать не надо.
Товарищ Тюринг это математически доказал, кстати.
habr.com/ru/post/342302
Пришел к выводу, что надо писать некий контейнер, в который помещаешь маленькие хотелки, которые выдают свои маленькие действия. Контейнер проверят, чтобы действия хотелок не противоречили друг другу.
Помоему самая главная мысль из этой статьи заложена здесь:
Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере
Что такое CAN? CAN — это CAN (англ. Controller Area Network — сеть контроллеров) — стандарт промышленной сети, ориентированный на передачу коротких, изначально заданных сообщений в реальном времени. Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать. Т.е. вы не сможете передать что-то, что не заложено в устройство на этапе проектирования сети — например файл, вирус, или изображение. Т.е. взломать Flight Computer через тот же CAN — физически невозможно. Возможно только повлиять на его работу давая ложные данные, но он их может перепроверить и не принять.
Т.е. изолируем критическую часть системы управления от некритической каким-то примитивным железным протоколом — и можно говорить, что уже половина дела в защите от кибератак сделана.
Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать.
Я бы сказал, что это слишком сильное заявление…
Которое отменяет все, что я сказал, чтобы ставить минусы?
Вы не можете взломать CAN в автомобиле, не получив физического доступа к проводам сети. Поэтому я не считаю это кибератакой. Кибератака, на мой взгляд, это взлом с использованием только программного обеспечения и через существующие коммуникации и их уязвимости.
Что изменится если заменить CAN на любые «внутренние провода»?
Переформулирую:
— невозможно «взломать CAN» также как нельзя взломать RS-232 или провода в розетке.
— но иногда можно взломать application уровень поверх CAN (или RS-232) и зависит это целиком от протоколов запущенного поверх CAN и их обработчиков.
Микроядро seL4. Формальная верификация программ в реальном мире