Prouver l'absence de corruption en Haskell

Question

Je travaille dans un secteur où la sécurité est essentielle, et nos projets de logiciels sont généralement soumis à des exigences de sécurité, c'est-à-dire des choses dont nous devons démontrer que le logiciel les réalise avec un degré élevé de certitude. Il s'agit souvent d'exigences négatives, telles que " ne doit pas se corrompre plus fréquemment qu'une fois sur " (j'ajouterai que ces exigences proviennent d'exigences de sécurité de systèmes statistiques).

Une source de corruption est clairement les erreurs de codage, et j'aimerais utiliser le système de types Haskell pour exclure au moins certaines classes de ces erreurs. Quelque chose comme ça :

Tout d'abord, voici notre donnée critique qui ne doit pas être corrompue.

newtype Critical = Critical String

Maintenant, je veux stocker cet élément dans d'autres structures.

data Foo = Foo Integer Critical
data Bar = Bar String Critical

Je veux maintenant écrire une fonction de conversion de Foo en Bar qui soit garantie de ne pas toucher aux données critiques.

goodConvert, badConvert :: Foo -> Bar

goodConvert (Foo n c) = Bar (show n) c

badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)

Je veux que "goodConvert" vérifie le type, mais que "badConvert" échoue la vérification du type.

Évidemment, je ne peux pas importer le constructeur de Critical dans le module qui effectue la conversion. Mais ce serait bien mieux si je pouvais exprimer cette propriété dans le type, car alors je peux composer des fonctions qui sont garanties de préserver cette propriété.

J'ai essayé d'ajouter des types fantômes et des "forall" à divers endroits, mais cela n'aide pas.

Une chose qui pourrait fonctionner serait de ne pas exporter le constructeur Critical, et d'avoir alors

mkCritical :: String -> IO Critical

Comme le seul endroit où ces éléments de données critiques sont créés est dans les fonctions d'entrée, cela a un certain sens. Mais je préférerais une solution plus élégante et plus générale.

Modifier

Dans les commentaires, FUZxxl a suggéré de jeter un œil à Haskell sûr . Cela semble être la meilleure solution. Plutôt que d'ajouter un modificateur "pas de corruption" au niveau du type comme je le voulais à l'origine, il semble que vous puissiez le faire au niveau du module, comme ceci :

1 : Créez un module "Critical" qui exporte toutes les caractéristiques du type de données Critical, y compris son constructeur. Marquez ce module comme "unsafe" en mettant "{-# LANGUAGE Unsafe #-}" dans l'en-tête.

2 : Créer un module "SafeCritical" qui réexporte tout sauf le constructeur et toutes les autres fonctions qui pourraient être utilisées pour corrompre une valeur critique. Marquez ce module comme "digne de confiance".

3 : Marquez comme "sûrs" tous les modules qui doivent manipuler des valeurs critiques sans corruption. Ensuite, utilisez ceci pour démontrer que toute fonction importée comme "sûre" ne peut pas causer la corruption d'une valeur critique.

Il restera une petite minorité de code, comme le code d'entrée qui analyse les valeurs critiques, nécessitant une vérification supplémentaire. Nous ne pouvons pas éliminer ce code, mais la réduction du nombre de codes nécessitant une vérification détaillée est une victoire importante.

La méthode est basée sur le fait qu'une fonction ne peut inventer une nouvelle valeur que si une autre fonction la renvoie. Si une fonction ne reçoit qu'une seule valeur critique (comme dans la fonction "convert" ci-dessus), c'est la seule qu'elle peut retourner.

Une variante plus difficile du problème se présente lorsqu'une fonction possède deux ou plusieurs valeurs critiques du même type ; elle doit garantir de ne pas les mélanger. Par exemple,

swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)

Cependant, cela peut être géré en donnant le même traitement aux structures de données qui les contiennent.

Answer 1

Vous pouvez utiliser la paramétrie pour y parvenir.

data Foo c = Foo Integer c
data Bar c = Bar String c

goodConvert :: Foo c -> Bar c
goodConvert (Foo n c) = Bar (show n) c

Depuis c est une variable de type non contraint, vous savez que la fonction goodConvert ne peut rien savoir de c et ne peut donc pas construire une autre valeur de ce type. Il doit utiliser celle qui est fournie en entrée.

Enfin, presque. Les valeurs de fond vous permettent de briser cette garantie. Cependant, vous savez au moins que si vous essayez d'utiliser une valeur "corrompue", cela entraînera une exception (ou une non-terminaison).

badConvert :: Foo c -> Bar c
badConvert (Foo n c) = Bar (show n) undefined

Answer 2

Bien que la solution de hammar soit excellente et que je suggérerais normalement des constructeurs intelligents / de ne pas exporter le constructeur, j'ai décidé aujourd'hui d'essayer de résoudre ce problème dans le cadre du Coq Assistant de preuve et extraction vers Haskell.

Prenez note ! Je ne suis pas très versé dans le domaine du Coq / de l'extraction. Certaines personnes ont fait bon travail de prouver et d'extraire du code Haskell, alors tournez-vous vers eux pour obtenir des exemples de qualité - je ne fais que m'amuser !

Tout d'abord, nous voulons définir vos types de données. Dans Coq, cela ressemble beaucoup aux GADTs de Haskell :

Require Import String.
Require Import ZArith.

Inductive Critical :=
  Crit : string -> Critical.

Inductive FooT :=
  Foo : Z -> Critical -> FooT.

Inductive BarT :=
  Bar : string -> Critical -> BarT.

Pensez à ceux Inductive les lignes, telles que Inductive FooT := Foo : ... . comme des déclarations de type de données : data FooT = Foo Integer Critical

Pour faciliter l'utilisation, nous allons utiliser des accesseurs de champ :

Definition critF f := match f with Foo _ c => c end.
Definition critB b := match b with Bar _ c => c end.

Puisque Coq ne définit pas beaucoup de fonctions de style "show", je vais utiliser un substitut pour afficher les entiers.

Definition ascii_of_Z (z : Z) : string := EmptyString. (* FIXME *)

Maintenant que nous avons les bases, nous allons définir l'élément goodConvert fonction !

Definition goodConvert (foo : FooT) : BarT :=
  match foo with
    Foo n c => Bar (ascii_of_Z n) c
  end.

Tout cela est assez évident - il s'agit de votre fonction de conversion mais dans Coq et en utilisant une fonction case à la place du filtrage de haut niveau. Mais comment savoir si cette fonction va réellement maintenir l'invariant ? Nous le prouvons !

Lemma convertIsGood : forall (f : FooT) (b : BarT),
  goodConvert f = b -> critF f = critB b.
Proof.
  intros. 
  destruct f. destruct b.
  unfold goodConvert in H. simpl.
  inversion H. reflexivity.
Qed.

Cela signifie que si la conversion f résulte en b alors le champ critique de f doit être le même que le champ critique de b (en supposant qu'il y ait quelques détails mineurs, comme le fait que vous ne gâchiez pas les implémentations des accesseurs de champs).

Maintenant, extrayons cela en Haskell !

Extraction Language Haskell.
Extract Constant ascii_of_Z => "Prelude.show".  (* obviously, all sorts of unsafe and incorrect behavior can be introduced by your extraction *)
Extract Inductive string => "Prelude.String" ["[]" ":"]. Print positive.
Extract Inductive positive => "Prelude.Integer" ["`Data.Bits.shiftL` 1 + 1" "`Data.Bits.shiftL` 1" "1"].
Extract Inductive Z => "Prelude.Integer" ["0" "" ""].

Extraction "so.hs" goodConvert critF critB.

Producteur :

module So where

import qualified Prelude

data Bool =
   True
 | False

data Ascii0 =
   Ascii Bool Bool Bool Bool Bool Bool Bool Bool

type Critical =
  Prelude.String
  -- singleton inductive, whose constructor was crit

data FooT =
   Foo Prelude.Integer Critical

data BarT =
   Bar Prelude.String Critical

critF :: FooT -> Critical
critF f =
  case f of {
   Foo z c -> c}

critB :: BarT -> Critical
critB b =
  case b of {
   Bar s c -> c}

ascii_of_Z :: Prelude.Integer -> Prelude.String
ascii_of_Z z =
  []

goodConvert :: FooT -> BarT
goodConvert foo =
  case foo of {
   Foo n c -> Bar (ascii_of_Z n) c}

On peut l'exécuter ? Est-ce qu'il fonctionne ?

> critB $ goodConvert (Foo 32 "hi")
"hi"

Super ! Si quelqu'un a des suggestions à me faire, même si c'est une "réponse", je suis tout ouïe. Je ne suis pas sûr de savoir comment abandonner le code mort de choses comme Ascii0 ou Bool sans parler de faire de bons exemples de spectacles. Si quelqu'un est curieux, je pense que les noms des champs peuvent être faits automatiquement si j'utilisais une balise Record au lieu d'un Inductive mais cela pourrait rendre ce post syntaxiquement plus laid.

Answer 3

Je pense que la solution consistant à cacher les constructeurs est idiomatique. Vous pouvez exporter deux fonctions :

mkCritical :: String -> D Critical
extract :: Critical -> String

où D est le monade triviale ou tout autre. Toute fonction qui crée des objets de type Critical à un moment donné est marqué par D . Une fonction sans que D peut extraire des données de Critical mais pas de créer de nouveaux objets.

Alternativement :

data C a = C a Critical
modify :: (a -> String -> b) -> C a -> C b
modify f (C x (Critical y)) = C (f x y) (Critical y)

Si vous n'exportez pas le constructeur C seulement modify vous pouvez écrire :

goodConvert :: C Int -> C String
goodConvert = modify (\(a, _) -> show a)

mais badConvert est impossible à écrire.