Репликация "Taint mode" из "Fortify static check tool" в Haskell

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

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

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

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

Есть ли лучшие способы сделать это? Любая существующая работа по теме?

Ответы

Ответ 1

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

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

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

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

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

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

Ответ 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. Кроме того, вы можете использовать функцию "pseudo- Applicative" apply (<+>) для объединения taints. Мы могли бы легко создать аналогичный комбинатор для интерфейса "псевдо-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)