Языковая безопасность

В информатике ) — это набор методов , безопасность на основе языка ( LBS которые можно использовать для усиления безопасности приложений на высоком уровне за счет использования свойств языков программирования.Считается, что LBS обеспечивает безопасность компьютера на уровне приложений, позволяя предотвратить уязвимости, с которыми традиционная безопасность операционной системы не может справиться.

Программные приложения обычно определяются и реализуются на определенных языках программирования , и для защиты от атак, недостатков и ошибок, которым может быть уязвим исходный код приложения , необходима безопасность на уровне приложения; безопасность, оценивающая поведение приложений относительно языка программирования. Эта область обычно известна как языковая безопасность.

Мотивация

Использование крупных программных систем, таких как SCADA , происходит во всем мире. ^[1] компьютерные системы составляют ядро многих инфраструктур. Общество в значительной степени полагается на инфраструктуру, такую как водоснабжение, энергетика, связь и транспорт, которые, опять же, полагаются на полностью функционально работающие компьютерные системы. Есть несколько хорошо известных примеров, когда критически важные системы выходят из строя из-за ошибок или ошибок в программном обеспечении, например, когда нехватка компьютерной памяти привела к сбою компьютеров LAX и задержке сотен рейсов (30 апреля 2014 г.). ^[2]^[3]

Традиционно механизмы, используемые для контроля правильного поведения программного обеспечения, реализуются на уровне операционной системы. Операционная система обрабатывает несколько возможных нарушений безопасности, таких как нарушения доступа к памяти, нарушения переполнения стека, нарушения контроля доступа и многие другие. Это важнейшая часть безопасности компьютерных систем, однако, обеспечив безопасность поведения программного обеспечения на более конкретном уровне, можно достичь еще большей безопасности. Поскольку при компиляции теряется множество свойств и поведения программного обеспечения, обнаружить уязвимости в машинном коде значительно сложнее. Оценивая исходный код перед компиляцией, можно также рассмотреть теорию и реализацию языка программирования и обнаружить больше уязвимостей.

«Так почему же разработчики продолжают совершать одни и те же ошибки? Вместо того, чтобы полагаться на память программистов, мы должны стремиться создавать инструменты, которые систематизируют все, что известно об распространенных уязвимостях безопасности, и интегрируют их непосредственно в процесс разработки».
- Д. Эванс и Д. Ларошель, 2002 г.

Цель языковой безопасности

Используя LBS, безопасность программного обеспечения можно повысить в нескольких областях, в зависимости от используемых методов. Общие ошибки программирования, такие как переполнение буфера и незаконные потоки информации, могут быть обнаружены и запрещены в программном обеспечении, используемом потребителем. Также желательно предоставить потребителю некоторые доказательства свойств безопасности программного обеспечения, чтобы потребитель мог доверять программному обеспечению без необходимости получать исходный код и самостоятельно проверять его на наличие ошибок.

Компилятор, принимая исходный код в качестве входных данных, выполняет с кодом несколько операций, специфичных для языка, чтобы перевести его в машиночитаемый код. Лексический анализ , предварительная обработка , синтаксический анализ , семантический анализ , генерация кода и оптимизация кода — все это широко используемые операции в компиляторах. Анализируя исходный код и используя теорию и реализацию языка, компилятор попытается правильно перевести код высокого уровня в код низкого уровня, сохраняя поведение программы.

Во время компиляции программ, написанных на типобезопасном языке, таком как Java , исходный код должен успешно пройти проверку типов перед компиляцией. Если проверка типа не удалась, компиляция не будет выполнена, и исходный код необходимо будет изменить. Это означает, что при правильном компиляторе любой код, скомпилированный из успешно проверенной исходной программы, не должен содержать ошибок недопустимого присваивания. Это информация, которая может быть ценна для потребителя кода, поскольку она обеспечивает некоторую степень гарантии того, что программа не выйдет из строя из-за какой-либо конкретной ошибки.

Цель LBS — обеспечить наличие в исходном коде определенных свойств, соответствующих политике безопасности программного обеспечения. Информация, собранная в ходе компиляции, может быть использована для создания сертификата, который может быть предоставлен потребителю в качестве доказательства безопасности данной программы. Такое доказательство должно подразумевать, что потребитель может доверять компилятору, используемому поставщиком, и что сертификат, информация об исходном коде, может быть проверена.

На рисунке показано, как можно провести сертификацию и проверку низкоуровневого кода с помощью сертифицирующего компилятора. Поставщик программного обеспечения получает преимущество, заключающееся в том, что ему не нужно раскрывать исходный код, а потребителю остается задача проверки сертификата, что является простой задачей по сравнению с оценкой и компиляцией самого исходного кода. Для проверки сертификата требуется только ограниченная доверенная база кода, содержащая компилятор и верификатор.

Техники

Анализ программы

Основными применениями анализа программ являются оптимизация программ (время работы, требования к пространству, энергопотребление и т. д.) и корректность программы (ошибки, уязвимости безопасности и т. д.). Анализ программы может применяться к компиляции ( статический анализ ), во время выполнения ( динамический анализ ) или к тому и другому. В языковой безопасности анализ программы может предоставить несколько полезных функций, таких как: проверка типов (статическая и динамическая), мониторинг , проверка на наличие вредоносных данных и анализ потока управления .

Анализ информационных потоков

Анализ информационных потоков можно описать как набор инструментов, используемых для анализа управления информационными потоками в программе с целью сохранения конфиденциальности и целостности там, где обычные механизмы контроля доступа не работают.

«Отделяя право на доступ к информации от права на ее распространение, модель потока выходит за рамки модели матрицы доступа в своей способности определять безопасный поток информации. Практическая система нуждается как в доступе, так и в управлении потоком, чтобы удовлетворить всем требованиям безопасности».
- Д. Деннинг, 1976 г.

Контроль доступа обеспечивает проверку доступа к информации, но не заботится о том, что происходит после этого. Пример: в системе есть два пользователя: Алиса и Боб. У Алисы есть файл secret.txt , который разрешено читать и редактировать только ей, и она предпочитает хранить эту информацию при себе. В системе также существует файл public.txt , который могут свободно читать и редактировать все пользователи системы. Теперь предположим, что Алиса случайно скачала вредоносную программу. Эта программа может получить доступ к системе от имени Алисы, минуя проверку контроля доступа в secret.txt . Затем вредоносная программа копирует содержимое secret.txt и помещает его в public.txt , позволяя Бобу и всем другим пользователям прочитать его. Это представляет собой нарушение предусмотренной политики конфиденциальности системы.

Невмешательство

Невмешательство — это свойство программ, которые не утекают и не раскрывают информацию о переменных с более высокой классификацией безопасности в зависимости от ввода переменных с более низкой классификацией безопасности. Программа, которая обеспечивает невмешательство, должна выдавать один и тот же результат соответствующие одни и те же входные данные для младших всякий раз, когда используются переменных. Это должно выполняться для каждого возможного значения на входе. Это означает, что даже если переменные более высокого уровня в программе имеют разные значения от одного выполнения к другому, это не должно быть видно на переменных нижнего уровня .

Злоумышленник может попытаться выполнить программу, которая не обеспечивает невмешательство, неоднократно и систематически, чтобы попытаться отобразить ее поведение. Несколько итераций могут привести к раскрытию более высоких переменных и позволить злоумышленнику узнать конфиденциальную информацию, например, о состоянии системы.

Удовлетворяет ли программа невмешательству или нет, можно оценить во время компиляции, предполагая наличие систем типов безопасности .

Тип системы безопасности

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

Защита низкоуровневого кода

Уязвимости в низкоуровневом коде — это ошибки или недостатки, которые приводят программу в состояние, в котором дальнейшее поведение программы не определяется исходным языком программирования. Поведение низкоуровневой программы будет зависеть от особенностей компилятора, системы выполнения или операционной системы. Это позволяет злоумышленнику перевести программу в неопределенное состояние и использовать поведение системы.

Распространенные способы использования небезопасного низкоуровневого кода позволяют злоумышленнику выполнять несанкционированное чтение или запись по адресам памяти. Адреса памяти могут быть как случайными, так и выбранными злоумышленником.

Использование безопасных языков

Подход к обеспечению безопасного низкоуровневого кода заключается в использовании безопасных языков высокого уровня. Считается, что безопасный язык полностью определяется руководством для программиста. ^[4] Любая ошибка, которая может привести к зависимому от реализации поведению в безопасном языке, будет либо обнаружена во время компиляции, либо приведет к четко определенному поведению ошибки во время выполнения. В Java при доступе к массиву за пределами его границ будет выдано исключение. Примерами других безопасных языков являются C# , Haskell и Scala .

Защитное выполнение небезопасных языков

Во время компиляции небезопасного языка к низкоуровневому коду добавляются проверки времени выполнения для обнаружения неопределенного поведения на уровне исходного кода. Примером может служить использование canaries , которые могут завершить работу программы при обнаружении нарушений границ.Обратной стороной использования проверок во время выполнения, таких как проверка границ, является то, что они накладывают значительные затраты на производительность.

Защита памяти , такая как использование неисполняемого стека и/или кучи, также может рассматриваться как дополнительные проверки во время выполнения. Это используется многими современными операционными системами.

Изолированное исполнение модулей

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

Сертификация компиляции

Сертификация компиляции — это идея создания сертификата во время компиляции исходного кода с использованием информации из семантики языка программирования высокого уровня. Этот сертификат должен быть приложен к скомпилированному коду, чтобы предоставить потребителю форму доказательства того, что исходный код был скомпилирован в соответствии с определенным набором правил. Сертификат может быть изготовлен различными способами, например, с помощью кода подтверждения (PCC) или типизированного ассемблера (TAL).

Код подтверждения

Основные аспекты PCC можно свести к следующим этапам: ^[5]

Поставщик предоставляет исполняемую программу с различными аннотациями, созданными сертифицирующим компилятором .
Потребитель предоставляет условие проверки на основе политики безопасности . Оно отправляется поставщику.
Поставщик запускает условие проверки в средстве доказательства теорем, чтобы предоставить потребителю доказательство того, что программа действительно удовлетворяет политике безопасности.
Затем потребитель запускает доказательство в средстве проверки доказательств, чтобы проверить достоверность доказательства.

Примером сертифицирующего компилятора является компилятор Touchstone , который предоставляет формальное подтверждение PCC безопасности типов и памяти для программ, реализованных на Java.

Типизированный язык ассемблера

TAL применим к языкам программирования, использующим систему типов . После компиляции объектный код будет содержать аннотацию типа, которую можно проверить с помощью обычного средства проверки типов. Созданная здесь аннотация во многом аналогична аннотациям, предоставленным PCC, с некоторыми ограничениями. Однако TAL может обрабатывать любую политику безопасности, которая может быть выражена ограничениями системы типов, которые могут включать, среди прочего, безопасность памяти и поток управления.

Семинары

Семинар Дагстуль 03411 , Языковая безопасность, 5–10 октября 2003 г.

Ссылки

^ «Можем ли мы извлечь уроки из инцидентов безопасности SCADA?» (PDF) . www.oas.org . Эниса.
^ «Система управления воздушным движением дала сбой» . www.computerworld.com . Проверено 12 мая 2014 г.
^ «Программная ошибка, способствовавшая отключению электроэнергии» . www.securityfocus.com . Проверено 11 февраля 2004 г.
^ Пирс, Бенджамин К. (2002). Типы и языки программирования . Массачусетский технологический институт Пресс. ISBN 9780262162098 .
^ Козен, Декстер (1999). «Языковая безопасность» (PDF) . Корнелльский университет. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

Книги

Ж. Барт, Б. Грегуар, Т. Резк, Сборник сертификатов , 2008 г.
Брайан Чесс и Гэри МакГроу, Статический анализ безопасности , 2004 г.

Дальнейшее чтение

Декстер Козен, Языковая безопасность , Корнелльский университет, 1999 г.
Питер Агтен и др., «Последние разработки в области низкоуровневой безопасности программного обеспечения» , Левенский университет.
Андрей Сабельфельд и Эндрю Майерс, Языковая безопасность информационных потоков
Фред Б. Шнайдер и др., Языковой подход к безопасности , Университет Карнеги-Меллона, 2000 г.

[1] «Можем ли мы извлечь уроки из инцидентов безопасности SCADA?» (PDF) . www.oas.org . Эниса.

[2] «Система управления воздушным движением дала сбой» . www.computerworld.com . Проверено 12 мая 2014 г.

[3] «Программная ошибка, способствовавшая отключению электроэнергии» . www.securityfocus.com . Проверено 11 февраля 2004 г.

[4] Пирс, Бенджамин К. (2002). Типы и языки программирования . Массачусетский технологический институт Пресс. ISBN 9780262162098 .

[5] Козен, Декстер (1999). «Языковая безопасность» (PDF) . Корнелльский университет. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[1]

[2]

[3]

[4]

[5]