Введение

Метод компьютерной безопасности

Доказуемая безопасность относится к любому типу или уровню компьютерной безопасности, который можно доказать. Она используется различными способами в разных областях. Как правило, это относится к математическим доказательствам, которые широко распространены в криптографии. В таком доказательстве возможности злоумышленника определяются моделью противника (также называемой моделью атакующего): цель доказательства – показать, что злоумышленнику необходимо решить сложную базовую задачу, чтобы скомпрометировать безопасность моделируемой системы. Подобное доказательство обычно не рассматривает атаки по сторонним каналам или другие атаки, специфичные для реализации, поскольку их, как правило, невозможно смоделировать без реализации самой системы (и, следовательно, доказательство применимо только к данной реализации). За пределами криптографии этот термин часто используется в контексте безопасного кодирования и безопасности через проектирование, оба из которых могут опираться на доказательства для демонстрации безопасности конкретного подхода. Как и в криптографическом контексте, это предполагает наличие модели противника и модели системы. Например, код может быть верифицирован на соответствие предполагаемой функциональности, описанной моделью: это можно сделать с помощью статической проверки. Эти методы иногда используются для оценки продуктов (см. Common Criteria – Общие критерии): в этом случае безопасность зависит не только от корректности модели противника, но и от модели кода. Наконец, термин "доказуемая безопасность" иногда используют продавцы программного обеспечения безопасности, стремящиеся продать продукты безопасности, такие как межсетевые экраны, антивирусное программное обеспечение и системы обнаружения вторжений. Поскольку эти продукты обычно не подвергаются тщательной проверке, многие исследователи в области безопасности считают подобные заявления шарлатанством.

В криптографии

В криптографии система обладает доказуемой безопасностью, если её требования к безопасности могут быть формально определены в рамках модели противника, а не эвристически, с чёткими предположениями о том, что противник имеет доступ к системе, а также располагает достаточными вычислительными ресурсами. Доказательством безопасности (называемым «сведением») является то, что эти требования к безопасности выполняются при условии, что предположения о доступе противника к системе соблюдены и выполняются чётко сформулированные предположения о сложности решения определённых вычислительных задач. Ранний пример таких требований и доказательства был предложен Голдвассером и Микали для семантической безопасности и конструкции, основанной на задаче об остатках квадратов. Некоторые доказательства безопасности строятся в заданных теоретических моделях, таких как модель случайного оракула, где реальные криптографические хеш-функции заменяются идеализацией. Существует несколько направлений исследований в области доказуемой безопасности. Одно из них – установление «корректного» определения безопасности для конкретной, интуитивно понятной задачи. Другое – разработка конструкций и доказательств, основанных на максимально общих предположениях, например, на существовании односторонней функции. Важной нерешённой проблемой является построение таких доказательств на основе P ≠ NP, поскольку существование односторонних функций не известно как следствие гипотезы P ≠ NP.

Противоречия

Несколько исследователей обнаружили математические ошибки в доказательствах, которые использовались для обоснования безопасности важных протоколов. В следующем частичном списке таких исследователей их имена сопровождаются сначала ссылкой на оригинальную статью с предполагаемым доказательством, а затем ссылкой на статью, в которой исследователи сообщили об обнаруженных недостатках: В. Шоуп; А. Дж. Менезес; А. Джха и М. Нанди; Д. Галиндо; Т. Ивата, К. Охаши и К. Минематсу; М. Нанди; Дж. С. Корона и Д. Наккаше; Д. Чакраборти, В. Эрнандес Хименес и П. Саркар; П. Гажи и У. Маурер; С. А. Какви и Э. Кильц; и Т. Холенштейн, Р. Кюнцлер и С. Тессаро. Коблиц и Менезес утверждали, что результаты, подтверждающие безопасность важных криптографических протоколов, часто содержат ошибки в доказательствах; нередко интерпретируются вводящим в заблуждение образом, создавая ложное чувство уверенности; как правило, опираются на сильные предположения, которые могут оказаться неверными; основаны на нереалистичных моделях безопасности и отвлекают внимание исследователей от необходимости "традиционного" (нематематического) тестирования и анализа. Их серия статей, подтверждающих эти утверждения, вызвала широкую дискуссию в сообществе. Среди исследователей, не согласных с точкой зрения Коблица и Менезеса, – Одед Голдрайх, ведущий теоретик и автор книги "Основы криптографии". Он написал опровержение их первой статьи "Еще один взгляд на 'доказуемую безопасность'", назвав его "О постмодернистской криптографии". Голдрайх писал: "Мы указываем на некоторые фундаментальные философские недостатки, лежащие в основе упомянутой статьи, и некоторые заблуждения относительно теоретических исследований в криптографии за последние четверть века". В своем эссе Голдрайх утверждал, что строгая методология анализа доказуемой безопасности – единственная, совместимая с научным подходом, и что Коблиц и Менезес являются "реакционерами (то есть поддерживают противников прогресса)". Статья содержала ряд спорных утверждений о доказуемой безопасности и других темах. Исследователи Одед Голдрайх, Боаз Барак, Джонатан Кац, Хьюго Краучик и Ави Вигдерсон написали письма в ответ на статью Коблица, которые были опубликованы в номерах журнала за ноябрь 2007 и январь 2008 года. Кац, соавтор высоко оцененного учебника по криптографии, назвал статью Коблица "вычурным снобизмом"; а Скотт Ааронсон рекомендовал ее как глубокий и всесторонний анализ. Брайан Сноу, бывший технический директор Управления информационной безопасности Агентства национальной безопасности США, рекомендовал статью Коблица и Менезеса "Храбрый новый мир смелых предположений в криптографии" аудитории на панельных обсуждениях криптографов на конференции RSA 2010 года.

Практически ориентированная доказуемая безопасность

Классическая доказуемая безопасность в основном была направлена на изучение взаимосвязей между асимптотически определенными объектами. В отличие от этого, практико-ориентированная доказуемая безопасность рассматривает конкретные объекты криптографической практики, такие как хеш-функции, блочные шифры и протоколы, в том виде, в котором они развертываются и используются. Практико-ориентированная доказуемая безопасность использует понятие конкретной безопасности для анализа практических конструкций с фиксированными размерами ключей. "Точная безопасность" или "конкретная безопасность" – это термин, используемый для обозначения доказуемых сведений о безопасности, в которых уровень безопасности количественно оценивается путем вычисления точных оценок вычислительных затрат, а не асимптотической границы, гарантированно выполняющейся для "достаточно больших" значений параметра безопасности.