Войти
В информатике, Безопасность на основе языка (LBS ) - это набор методов, которые могут использоваться для усиления безопасности приложений на высоком уровне за счет использования свойств языков программирования. Считается, что LBS обеспечивает компьютерную безопасность на уровне приложений, позволяя предотвращать уязвимости, с которыми традиционная система безопасности операционной системы не справляется.
Программные приложения обычно задаются и реализуются на определенных языках программирования, и для защиты от атак, недостатков и ошибок исходный код приложения может быть уязвим для, существует потребность в безопасности на уровне приложений; безопасность, оценивающая поведение приложений по отношению к языку программирования. Эта область обычно известна как безопасность на основе языка.
Использование больших программные системы, такие как SCADA, используются во всем мире, а компьютерные системы составляют ядро многих инфраструктур. Общество в значительной степени полагается на инфраструктуру, такую как вода, энергия, связь и транспорт, которые, опять же, полагаются на полностью функционально работающие компьютерные системы. Существует несколько хорошо известных примеров, когда критические системы выходят из строя из-за ошибок или ошибок в программном обеспечении, например, когда нехватка компьютерной памяти вызвала сбой компьютеров LAX и задержку сотен рейсов (30 апреля 2014 г.).
Традиционно механизмы, используемые для контроля правильного поведения программного обеспечения, реализуются на уровне операционной системы. Операционная система обрабатывает несколько возможных нарушений безопасности, таких как нарушения доступа к памяти, нарушения переполнения стека, нарушения контроля доступа и многие другие. Это критически важная часть безопасности компьютерных систем, однако, защищая поведение программного обеспечения на более конкретном уровне, можно добиться еще большей безопасности. Поскольку многие свойства и поведение программного обеспечения теряются при компиляции, обнаруживать уязвимости в машинном коде значительно труднее. Оценивая исходный код перед компиляцией, можно также рассмотреть теорию и реализацию языка программирования, а также выявить больше уязвимостей.
«Так почему же разработчики продолжают совершать одни и те же ошибки? Вместо того, чтобы полагаться на воспоминания программистов, мы должны стремиться создавать инструменты, которые систематизируют то, что известно об общих уязвимостях безопасности, и интегрируют их непосредственно в процесс разработки».
- Д. Эванс и Д. Ларошель, 2002
Используя LBS, можно повысить безопасность программного обеспечения в нескольких областях, в зависимости от используемых методов. используемый. Распространенные ошибки программирования, такие как разрешение переполнения буфера и возникновение незаконных информационных потоков, могут быть обнаружены и запрещены в программном обеспечении, используемом потребителем. Также желательно предоставить потребителю некоторые доказательства свойств безопасности программного обеспечения, чтобы потребитель мог доверять программному обеспечению без необходимости получать исходный код и самостоятельно проверять его на наличие ошибок.
Компилятор, принимая исходный код в качестве входных данных, выполняет над кодом несколько операций, зависящих от языка, чтобы преобразовать его в машиночитаемый код. Лексический анализ, предварительная обработка, синтаксический анализ, семантический анализ, генерация кода и оптимизация кода - все это обычно используемые операции в компиляторах. Анализируя исходный код и используя теорию и реализацию языка, компилятор попытается правильно перевести код высокого уровня в код низкого уровня, сохранив поведение программы.
Иллюстрация сертифицирующего компилятора Во время компиляции программ, написанных на типобезопасном языке, таком как Java, исходный код должен пройти успешную проверку типов перед компиляцией. Если проверка типа завершится неудачно, компиляция не будет выполнена, и исходный код необходимо будет изменить. Это означает, что при правильном компиляторе любой код, скомпилированный из исходной программы с успешной проверкой типов, не должен содержать недопустимых ошибок присваивания. Это информация, которая может быть полезна для потребителя кода, поскольку она дает некоторую степень гарантии того, что программа не выйдет из строя из-за какой-либо конкретной ошибки.
Целью LBS является обеспечение наличия определенных свойств в исходном коде, соответствующих политике безопасности программного обеспечения. Информация, собранная во время компиляции, может быть использована для создания сертификата, который может быть предоставлен потребителю в качестве доказательства безопасности данной программы. Такое доказательство должно предполагать, что потребитель может доверять компилятору, используемому поставщиком, и что сертификат, информация об исходном коде, может быть проверена.
На рисунке показано, как сертификация и верификация низкоуровневого кода могут быть установлены с использованием сертифицирующего компилятора. Поставщик программного обеспечения получает преимущество в том, что ему не нужно раскрывать исходный код, а перед потребителем остается задача проверки сертификата, что является легкой задачей по сравнению с оценкой и компиляцией самого исходного кода. Для проверки сертификата требуется только ограниченная база доверенного кода, содержащая компилятор и верификатор.
Основными приложениями анализа программ являются оптимизация программ (время работы, требования к пространству, мощность потребление и т. д.) и корректность программы (ошибки, уязвимости и т. д.). Программный анализ может применяться к компиляции (статический анализ ), во время выполнения (динамический анализ ) или к обоим. В языковой безопасности анализ программы может предоставлять несколько полезных функций, таких как: проверка типов (статическая и динамическая), мониторинг, проверка зараженности и анализ потока управления.
Анализ потока информации можно описать как набор инструментов, используемых для анализа управления потоком информации в программе с целью сохранения конфиденциальность и целостность, где обычные механизмы управления доступом не работают.
«Разъединяя право на доступ к информации и право на ее распространение, потоковая модель выходит за рамки модели матрицы доступа в своей способности определять безопасный информационный поток. Практическая система нуждается как в управлении доступом, так и в управлении потоками для удовлетворения всех требований безопасности.. "
- Д. Деннинг, 1976
Контроль доступа принудительно проверяет доступ к информации, но не заботится о том, что происходит после этого. Пример: в системе два пользователя, Алиса и Боб. У Алисы есть файл secret.txt, который разрешено читать и редактировать только ей, и она предпочитает хранить эту информацию при себе. В системе также существует файл public.txt, который может свободно читать и редактировать все пользователи системы. Теперь предположим, что Алиса случайно загрузила вредоносную программу. Эта программа может получить доступ к системе как Алиса, минуя проверку контроля доступа на secret.txt. Затем вредоносная программа копирует содержимое secret.txt и помещает его в public.txt, позволяя Бобу и всем другим пользователям читать его. Это является нарушением предполагаемой политики конфиденциальности системы.
Невмешательство - это свойство программ, которое не пропускает и не раскрывает информацию о переменных с более высокой классификацией безопасности, в зависимости от ввода переменных с более низкой классификацией безопасности. Программа, удовлетворяющая требованиям невмешательства, должна выдавать один и тот же результат всякий раз, когда используются соответствующие входные данные для более низких переменных. Это должно выполняться для всех возможных значений на входе. Это означает, что даже если более высокие переменные в программе имеют разные значения от одного выполнения к другому, это не должно быть видно на более низких переменных.
Злоумышленник может попытаться выполнить программу, которая не удовлетворяет требованиям невмешательства, неоднократно и систематически, чтобы попытаться отобразить ее поведение. Несколько итераций могут привести к раскрытию более высоких переменных и позволить злоумышленнику узнать конфиденциальную информацию, например, о состоянии системы.
Может ли программа удовлетворять требованиям невмешательства или нет, может быть оценено во время компиляции, предполагая наличие систем типа безопасности.
A системы типов безопасности является разновидностью система типа, которая может использоваться разработчиками программного обеспечения для проверки свойств безопасности своего кода. В языке с типами безопасности типы переменных и выражений относятся к политике безопасности приложения, и программисты могут определять политику безопасности приложения через объявления типов. Типы могут использоваться для рассуждений о различных типах политик безопасности, включая политики авторизации (как контроль доступа или возможности) и безопасность информационных потоков. Системы типов безопасности могут быть формально связаны с лежащей в основе политикой безопасности, и система типов безопасности является надежной, если все программы, которые проверяют типы, удовлетворяют политике в семантическом смысле. Например, система типов безопасности для информационного потока может обеспечивать невмешательство, что означает, что проверка типов выявляет, есть ли какие-либо нарушения конфиденциальности или целостности в программе.
Уязвимости в низкоуровневом коде - это ошибки или изъяны, которые приводят программу в состояние, при котором дальнейшее поведение программы не определяется исходным языком программирования. Поведение низкоуровневой программы будет зависеть от деталей компилятора, исполняющей системы или операционной системы. Это позволяет злоумышленнику перевести программу в неопределенное состояние и использовать поведение системы.
Распространенные эксплойты небезопасного низкоуровневого кода позволяют злоумышленнику выполнять несанкционированное чтение или запись по адресам памяти. Адреса памяти могут быть случайными или выбранными злоумышленником.
Подход к достижению безопасного низкоуровневого кода заключается в использовании безопасных языков высокого уровня. Считается, что безопасный язык полностью определен в руководстве для программистов. Любая ошибка, которая может привести к зависящему от реализации поведению на безопасном языке, будет либо обнаружена во время компиляции, либо приведет к четко определенному ошибочному поведению во время выполнения. В Java при доступе к массиву за пределами границ будет выдано исключение. Примерами других безопасных языков являются C#, Haskell и Scala.
Во время компиляции небезопасного языка проверки времени выполнения добавляются к низкоуровневому коду для обнаружения неопределенного поведения на уровне источника. Примером может служить использование canaries, которое может завершить программу при обнаружении нарушений границ. Обратной стороной использования проверок времени выполнения, таких как проверка границ, является то, что они накладывают значительные накладные расходы на производительность.
Защита памяти, например использование неисполняемого стека и / или кучи, также может рассматриваться как дополнительные проверки во время выполнения. Это используется многими современными операционными системами.
Общая идея состоит в том, чтобы идентифицировать конфиденциальный код из данных приложения путем анализа исходного кода. Как только это будет сделано, разные данные разделяются и помещаются в разные модули. Предполагая, что каждый модуль имеет полный контроль над конфиденциальной информацией, которую он содержит, можно указать, когда и как следует покинуть модуль. Примером является криптографический модуль, который может предотвратить выход ключей из модуля незашифрованными.
Сертификационная компиляция - это идея создания сертификата во время компиляции исходного кода с использованием информации из семантики языка программирования высокого уровня. Этот сертификат должен быть приложен к скомпилированному коду, чтобы предоставить потребителю форму доказательства того, что исходный код был скомпилирован в соответствии с определенным набором правил. Сертификат может быть изготовлен разными способами, например: через Подтверждающий код (PCC) или Типизированный язык ассемблера (TAL).
Основные аспекты PCC можно резюмировать в следующих этапах:
Примером сертифицирующего компилятора является компилятор Touchstone, который предоставляет формальное доказательство PCC. безопасности типов и памяти для программ, реализованных на Java.
TAL применим к языкам программирования, которые используют систему типов . После компиляции объектный код будет содержать аннотацию типа, которую можно проверить с помощью обычного средства проверки типов. Созданные здесь аннотации во многом похожи на аннотации, предоставленные PCC, с некоторыми ограничениями. Однако TAL может обрабатывать любую политику безопасности, которая может быть выражена ограничениями системы типов, которая может включать, среди прочего, безопасность памяти и поток управления.
