Репликация "Режим порчи" из "инструмента статической проверки Fortify" в Haskell

Question

Я прочитал некоторую документацию инструмента статической проверки Fortify. Одна из концепций, используемых этим инструментом, называется порчей. Некоторые источники, такие как веб-запросы, предоставляют данные, которые могут быть испорчены одним или несколькими способами, а некоторые приемники, такие как веб-ответы, требуют, чтобы данные были незапятнанными.

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

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

В Haskell я мог бы делать такие типы, как Tainted [BadRandom,Unbounded] Int но вычисление с ними кажется довольно сложным, так как этот новый тип ограничивает также операции, которые не ограничивают вред.

Есть ли более приятные способы сделать это? Есть какие-нибудь работы по теме?

Answer 1

Не полное решение (= хороший существующий способ сделать это), но некоторые подсказки:

Мне известны две статьи о безопасном информационном потоке в Haskell: Li and Zdanevic, 2006 (один из авторов также участвует в Jif) и Russo et al., 2008. И те, и другие подходят к "порче" с противоположной стороны, а именно, помечая значения по степени их безопасности, и используют решетчатую структуру для упорядочения разных уровней безопасности, но решаемая проблема должна быть такой же, как вы описали.

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

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

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

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

Answer 2

Простая модель этого может быть следующей:

{-# LANGUAGE EmptyDataDecls             #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators              #-}

module Taint ( (:+), srand, BadRandom, Unbounded, Tainted (), (<+>)) where

import           Control.Applicative
import           Control.Monad.Identity

data a :+ b

data BadRandom
data Unbounded

newtype Tainted taint a = Tainted { clean :: Identity a }
  deriving ( Functor, Applicative, Monad )

(<+>) :: Tainted t1 (a -> b) -> Tainted t2 a -> Tainted (t1 :+ t2) b
Tainted (Identity f) <+> Tainted (Identity x) = Tainted (Identity (f x))

srand :: IO (Tainted BadRandom Int)
srand = undefined

поскольку clean не экспортируется, это невозможно для пользователей srand удалить Tainted тег. Кроме того, вы можете использовать "псевдоApplicative"применить функцию (<+>) слить портит. Мы могли бы легко получить аналогичный комбинатор для "псевдо-MonadИнтерфейс также:

(>>-) :: Tainted t1 a -> (a -> Tainted t2 b) -> Tainted (t1 :+ t2) b
Tainted (Identity a) >>- f = let Tainted (Identity b) = f a in Tainted (Identity b)