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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Соответствие программы этому свойству может быть проверено на этапе компиляции при наличии систем типов безопасности.

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

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

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

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

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

Защита памяти, в частности запрет на исполнение кода из областей стека/кучи, также является примером подобных проверок и применяется в большинстве современных ОС.

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

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

Основные этапы PCC:^[5]

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

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

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