DEF CON 30 - Адам Заброцки и Алекс Терешкин - Эксплуатация в эпоху формальной верификации

DEF CON 30 - запись доклада: Адам Заброцки, Алекс Терешкин - Эксплуатация в эпоху формальной верификации На протяжении десятилетий уязвимости программного обеспечения оставались неразрешимой проблемой безопасности, несмотря на многолетние инвестиции в различные стратегии смягчения, усиления защиты и фаззинга. В последние годы в качестве пути к повышению безопасности были применены формальные методы. Верификация и формальные методы могут привести убедительные аргументы в пользу отсутствия целых классов ошибок безопасности и являются мощным инструментом для создания высокозащищенного программного обеспечения. AdaCore/SPARK - это формально определенный язык программирования, предназначенный для разработки программного обеспечения высокой степени целостности, используемого в системах, где предсказуемая и высоконадежная работа имеет решающее значение. Формальное, недвусмысленное определение SPARK позволяет применять различные методы статического анализа, включая анализ информационных потоков, подтверждение отсутствия исключений во время выполнения, подтверждение завершения, подтверждение функциональной корректности и доказательство надежности и защищенных свойств. В этом докладе мы углубимся в AdaCore/SPARK, рассмотрим слабые места и ограничения, а также покажем реальные уязвимости, с которыми мы столкнулись во время моей работы и которые все еще возможны в официально проверенном программном обеспечении. Мы также покажем эксплойт, нацеленный на одну из ранее описанных...