Sécurité de la mémoire basée sur le type sans gestion manuelle de la mémoire ni récupération de place lors de l'exécution?

Supposons que nous voulions un langage de programmation pur et fonctionnel, comme Haskell ou Idris, qui vise la programmation de systèmes sans collecte de déchets et n'a pas d'exécution (ou du moins pas plus que les «exécutions» C et Rust). Quelque chose qui peut plus ou moins fonctionner sur du métal nu.

Quelles sont certaines des options de sécurité de la mémoire statique qui ne nécessitent pas de gestion manuelle de la mémoire ou de récupération de place lors de l'exécution, et comment le problème peut-il être résolu en utilisant le système de type d'une fonctionnalité pure similaire à Haskell ou Idris?

En gros, il existe deux stratégies principales pour une gestion manuelle de la mémoire en toute sécurité.

1. La première approche consiste à utiliser une logique sous-structurelle comme la logique linéaire pour contrôler l'utilisation des ressources. Cette idée a flotté essentiellement depuis le début de la logique linéaire, et fonctionne essentiellement sur l'observation qu'en interdisant la règle structurelle de contraction, chaque variable est utilisée au plus une fois, et donc il n'y a pas d'alias. Par conséquent, la différence entre la mise à jour sur place et la réallocation est invisible pour le programme, et vous pouvez donc implémenter votre langue avec une gestion manuelle de la mémoire.

   C'est ce que fait Rust (il utilise un système de type affine). Si vous êtes intéressé par la théorie des langages de style rouille, l'un des meilleurs articles à lire est le L3 d' Ahmed et al : un langage linéaire avec des emplacements . Soit dit en passant, le calcul LFPL mentionné par Damiano Mazza est également linéaire, a un langage complet qui en dérive dans le langage RAML .

   Si vous êtes intéressé par la vérification de style Idris, vous devriez regarder le langage ATS de Xi et al , qui est un langage de style Rust / L3 avec prise en charge de la vérification basée sur des types indexés de style Haskell, uniquement rendu non pertinent et linéaire pour donner plus contrôle des performances.

   Une approche dépendante encore plus agressive est le langage F-star développé par Microsoft Research, qui est une théorie de type totalement dépendante. Ce langage a une interface monadique avec des conditions préalables et postérieures dans l'esprit de la théorie des types de Hoare de Nanevski et al (ou même ma propre intégration de types linéaires et dépendants ), et a un sous-ensemble défini qui peut être compilé en code C de bas niveau - en fait, ils envoient déjà du code crypté vérifié dans Firefox!

   Pour être clair, ni F-star ni HTT ne sont des langages de type linéaire, mais le langage d'index de leurs monades est généralement basé sur la logique de séparation de Reynold et O'Hearn , qui est une logique sous-structurelle liée à la logique linéaire qui a connu un grand succès comme le langage d'assertion pour les logiques Hoare pour les programmes de pointeurs.

2. La deuxième approche consiste à simplement spécifier quel assemblage (ou quel IR de bas niveau vous voulez), puis à utiliser une forme de logique linéaire ou de séparation pour raisonner directement sur son comportement dans un assistant de preuve. Essentiellement, vous pouvez utiliser l'assistant de preuve ou un langage de type dépendant comme un assembleur de macros très sophistiqué qui ne génère que des programmes corrects.

   La logique de séparation de haut niveau de Jensen et al pour le code de bas niveau en est un exemple particulièrement pur - elle construit une logique de séparation pour l'assemblage x86! Cependant, il existe de nombreux projets dans cette veine, comme le Vérifié Software Toolchain à Princeton et le projet CertiKOS à Yale.

Toutes ces approches "se sentiront" un peu comme Rust, car le suivi de la propriété en restreignant l'utilisation des variables est la clé de toutes.

Les types linéaires et la logique de séparation sont tous deux excellents, mais peuvent nécessiter beaucoup d'efforts de programmation. L'écriture d'une liste de liens sécurisés dans Rust peut être assez difficile, par exemple.

Mais il existe une alternative qui nécessite beaucoup moins d'efforts de programmation, bien qu'avec des garanties moins strictes. Un flux de travail (assez ancien) consiste à garantir la sécurité de la mémoire en utilisant (généralement une pile de) régions. En utilisant l'inférence de région, un compilateur peut statiquement décider dans quelle région un élément de données allouées doit entrer et désallouer la région lorsqu'elle sort de la portée.

L'inférence de région est prouvée en toute sécurité (ne peut pas désallouer la mémoire accessible) et nécessite une interférence minimale du programmeur, mais elle n'est pas "totale" (c'est-à-dire qu'elle peut toujours fuir la mémoire, bien que nettement meilleure que "ne rien faire"), donc elle est généralement combinée avec GC en pratique. leMLtonLe compilateur ML Kit utilise des régions pour éliminer la plupart des appels GC, mais il a toujours un GC car il y aurait toujours une fuite de mémoire sinon. Selon certains des premiers pionniers sur les régions, l'inférence de région n'a pas été réellement inventée à cette fin (c'était pour la parallélisation automatique, je pense); mais il s'est avéré qu'il pouvait également être utilisé pour la gestion de la mémoire.

Pour un point de départ, je dirais optez pour le document "Implémentation du λ-calcul typé Call-by-Value utilisant une pile de régions" par Mads Tofte et Jean-Pierre Talpin. Pour plus d'articles sur l'inférence régionale, recherchez d'autres articles de M. Tofte et J.-P. Talpin, une partie du travail de Pierre Jouvelot, ainsi que la série d'articles de Greg Morrisett, Mike Hicks et Dan Grossman sur le cyclone.

Un schéma trivial pour les systèmes "bare metal" consiste à simplement interdire toutes les allocations de mémoire d'exécution. N'oubliez pas que même la malloc/freepaire C nécessite une bibliothèque d'exécution. Mais même lorsque tous les objets sont définis au moment de la compilation, ils peuvent être définis de manière sécurisée.

Le problème principal ici est la fiction des valeurs immuables dans les langages fonctionnels purs, qui sont créés pendant l'exécution du programme. Le vrai matériel (et certainement les systèmes de métal nu) repose sur une RAM mutable, qui est en quantité limitée. Le runtime d'une implémentation de langage fonctionnel dans la pratique alloue dynamiquement de la RAM à mesure que de nouvelles valeurs "immuables" sont créées, et les ordures les récupèrent lorsque la valeur "immuable" n'est plus nécessaire.

Et pour les problèmes les plus intéressants, la durée de vie d'au moins certaines valeurs dépend de l'entrée d'exécution (utilisateur), de sorte que les durées de vie ne peuvent pas être statiquement déterminées. Mais même si la durée de vie ne dépend pas de l'entrée, elle peut être très simple. Prenez le programme simple à plusieurs reprises pour trouver des nombres premiers simplement en vérifiant chaque nombre dans l'ordre, en comparant tous les nombres premiers jusqu'à sqrt(N). De toute évidence, ce besoin conserve les nombres premiers et peut recycler la mémoire utilisée pour les non-nombres premiers.