Sécurité basée sur la langue - Language-based security

En informatique , la sécurité basée sur le langage ( LBS ) est un ensemble de techniques qui peuvent être utilisées pour renforcer la sécurité des applications à un niveau élevé en utilisant les propriétés des langages de programmation. LBS est censé appliquer la sécurité informatique au niveau de l'application, ce qui permet d'éviter les vulnérabilités que la sécurité du système d'exploitation traditionnel est incapable de gérer.

Les applications logicielles sont généralement spécifiées et implémentées dans certains langages de programmation , et afin de se protéger contre les attaques, les failles et les bogues auxquels le code source d' une application peut être vulnérable, une sécurité au niveau de l'application est nécessaire ; sécurité évaluant le comportement des applications par rapport au langage de programmation. Cette zone est généralement connue sous le nom de sécurité basée sur le langage.

Motivation

L'utilisation de grands systèmes logiciels, tels que SCADA , se fait partout dans le monde et les systèmes informatiques constituent le cœur de nombreuses infrastructures. La société dépend grandement d'infrastructures telles que l'eau, l'énergie, les communications et les transports, qui, encore une fois, reposent toutes sur des systèmes informatiques pleinement fonctionnels. Il existe plusieurs exemples bien connus de défaillances de systèmes critiques en raison de bogues ou d'erreurs logicielles, par exemple lorsque le manque de mémoire informatique a provoqué le crash des ordinateurs LAX et le retard de centaines de vols (30 avril 2014).

Traditionnellement, les mécanismes utilisés pour contrôler le bon comportement des logiciels sont implémentés au niveau du système d'exploitation. Le système d'exploitation gère plusieurs violations de sécurité possibles, telles que les violations d'accès à la mémoire, les violations de débordement de pile, les violations de contrôle d'accès et bien d'autres. Il s'agit d'un élément crucial de la sécurité des systèmes informatiques, mais en sécurisant le comportement des logiciels à un niveau plus spécifique, une sécurité encore plus forte peut être obtenue. Étant donné que de nombreuses propriétés et comportements du logiciel sont perdus lors de la compilation, il est nettement plus difficile de détecter les vulnérabilités dans le code machine. En évaluant le code source, avant la compilation, la théorie et la mise en œuvre du langage de programmation peuvent également être prises en compte, et davantage de vulnérabilités peuvent être découvertes.

"Alors pourquoi les développeurs continuent-ils à faire les mêmes erreurs ? Au lieu de s'appuyer sur la mémoire des programmeurs, nous devrions nous efforcer de produire des outils qui codifient ce que l'on sait des vulnérabilités de sécurité courantes et l'intègrent directement dans le processus de développement."

— D. Evans et D. Larochelle, 2002

Objectif de la sécurité basée sur le langage

En utilisant LBS, la sécurité des logiciels peut être augmentée dans plusieurs domaines, selon les techniques utilisées. Les erreurs de programmation courantes, telles que les débordements de mémoire tampon et les flux d'informations illégaux, peuvent être détectées et interdites dans le logiciel utilisé par le consommateur. Il est également souhaitable de fournir au consommateur des preuves des propriétés de sécurité du logiciel, ce qui permet au consommateur de faire confiance au logiciel sans avoir à recevoir le code source et à vérifier lui-même les erreurs.

Un compilateur, prenant le code source en entrée, effectue plusieurs opérations spécifiques au langage sur le code afin de le traduire en code lisible par la machine. L'analyse lexicale , le prétraitement , l' analyse syntaxique , l'analyse sémantique , la génération de code et l' optimisation de code sont toutes des opérations couramment utilisées dans les compilateurs. En analysant le code source et en utilisant la théorie et la mise en œuvre du langage, le compilateur tentera de traduire correctement le code de haut niveau en code de bas niveau, en préservant le comportement du programme.

Lors de la compilation de programmes écrits dans un langage de type sécurisé , tel que Java , le code source doit être vérifié avec succès avant la compilation. Si la vérification de type échoue, la compilation ne sera pas effectuée et le code source doit être modifié. Cela signifie que, avec un compilateur correct, tout code compilé à partir d'un programme source dont le type a été vérifié avec succès doit être exempt d'erreurs d'affectation invalide. Il s'agit d'informations qui peuvent être utiles au consommateur de code, car elles offrent un certain degré de garantie que le programme ne plantera pas en raison d'une erreur spécifique.

Un objectif de LBS est de s'assurer de la présence de certaines propriétés dans le code source correspondant à la politique de sécurité du logiciel. Les informations recueillies lors de la compilation peuvent être utilisées pour créer un certificat qui peut être fourni au consommateur comme preuve de sécurité dans le programme donné. Une telle preuve doit impliquer que le consommateur peut faire confiance au compilateur utilisé par le fournisseur et que le certificat, les informations sur le code source, peuvent être vérifiés.

La figure illustre comment la certification et la vérification du code de bas niveau pourraient être établies à l'aide d'un compilateur de certification. Le fournisseur du logiciel a l'avantage de ne pas avoir à révéler le code source, et le consommateur se retrouve avec la tâche de vérifier le certificat, ce qui est une tâche facile par rapport à l'évaluation et à la compilation du code source lui-même. La vérification du certificat ne nécessite qu'une base de code de confiance limitée contenant le compilateur et le vérificateur.

Technique

Analyse du programme

Les principales applications de l'analyse de programme sont l'optimisation du programme (temps d'exécution, espace requis, consommation électrique, etc.) et l'exactitude du programme (bogues, failles de sécurité, etc.). L'analyse de programme peut être appliquée à la compilation ( analyse statique ), à l'exécution ( analyse dynamique ) ou aux deux. Dans la sécurité basée sur le langage, l'analyse de programme peut fournir plusieurs fonctionnalités utiles, telles que : la vérification de type (statique et dynamique), la surveillance , la vérification de souillure et l' analyse de flux de contrôle .

Analyse des flux d'informations

L'analyse des flux d'informations peut être décrite comme un ensemble d'outils utilisés pour analyser le contrôle des flux d'informations dans un programme, afin de préserver la confidentialité et l' intégrité lorsque les mécanismes de contrôle d'accès réguliers font défaut .

« En découplant le droit d'accéder aux informations du droit de les diffuser, le modèle de flux va au-delà du modèle de matrice d'accès dans sa capacité à spécifier un flux d'informations sécurisé. Un système pratique a besoin à la fois d'un contrôle d'accès et de flux pour satisfaire toutes les exigences de sécurité.

— D. Denning, 1976

Le contrôle d'accès applique des contrôles sur l' accès à l'information, mais ne se préoccupe pas de ce qui se passe après cela. Un exemple : un système a deux utilisateurs, Alice et Bob. Alice a un fichier secret.txt , qui ne peut être lu et modifié que par elle, et elle préfère garder cette information pour elle. Dans le système, il existe également un fichier public.txt , qui est libre de lire et de modifier pour tous les utilisateurs du système. Supposons maintenant qu'Alice ait accidentellement téléchargé un programme malveillant. Ce programme peut accéder au système en tant qu'Alice, en contournant le contrôle d'accès sur secret.txt . Le programme malveillant copie ensuite le contenu de secret.txt et le place dans public.txt , permettant à Bob et à tous les autres utilisateurs de le lire. Cela constitue une violation de la politique de confidentialité prévue du système.

Non-interférence

La non-interférence est une propriété des programmes qui ne divulgue pas ou ne révèle pas d'informations sur les variables avec une classification de sécurité plus élevée , en fonction de l'entrée de variables avec une classification de sécurité inférieure . Un programme qui satisfait à la non-interférence devrait produire la même sortie chaque fois que la même entrée correspondante sur les variables inférieures est utilisée. Cela doit être valable pour chaque valeur possible sur l'entrée. Cela implique que même si les variables supérieures du programme ont des valeurs différentes d'une exécution à l'autre, cela ne devrait pas être visible sur les variables inférieures .

Un attaquant pourrait tenter d'exécuter un programme qui ne satisfait pas à la non-interférence de manière répétée et systématique pour tenter de cartographier son comportement. Plusieurs itérations pourraient conduire à la divulgation de variables plus élevées et permettre à l'attaquant d'apprendre des informations sensibles sur, par exemple, l'état du système.

Le fait qu'un programme satisfait ou non à la non-interférence peut être évalué lors de la compilation en supposant la présence de systèmes de type sécurité .

Système de type sécurité

Un système de types de sécurité est une sorte de système de types qui peut être utilisé par les développeurs de logiciels afin de vérifier les propriétés de sécurité de leur code. Dans un langage avec des types de sécurité, les types de variables et d'expressions se rapportent à la politique de sécurité de l'application, et les programmeurs peuvent être en mesure de spécifier la politique de sécurité de l'application via des déclarations de type. Les types peuvent être utilisés pour raisonner sur divers types de politiques de sécurité, y compris les politiques d'autorisation (comme le contrôle d'accès ou les capacités) et la sécurité des flux d'informations. Les systèmes de types de sécurité peuvent être formellement liés à la politique de sécurité sous-jacente, et un système de types de sécurité est valable si tous les programmes qui vérifient les types satisfont la politique au sens sémantique. Par exemple, un système de type de sécurité pour le flux d'informations peut imposer la non-interférence, ce qui signifie que la vérification de type révèle s'il y a une violation de la confidentialité ou de l'intégrité dans le programme.

Sécurisation du code de bas niveau

Les vulnérabilités dans le code de bas niveau sont des bogues ou des failles qui conduiront le programme dans un état où le comportement ultérieur du programme n'est pas défini par le langage de programmation source. Le comportement du programme de bas niveau dépendra des détails du compilateur, du système d'exécution ou du système d'exploitation. Cela permet à un attaquant de conduire le programme vers un état indéfini et d'exploiter le comportement du système.

Les exploits courants de code de bas niveau non sécurisé permettent à un attaquant d'effectuer des lectures ou des écritures non autorisées sur des adresses mémoire. Les adresses mémoire peuvent être soit aléatoires, soit choisies par l'attaquant.

Utiliser des langues sûres

Une approche pour obtenir un code de bas niveau sécurisé consiste à utiliser des langages de haut niveau sécurisés. Un langage sûr est considéré comme complètement défini par son manuel du programmeur. Tout bogue qui pourrait conduire à un comportement dépendant de l'implémentation dans un langage sûr sera soit détecté au moment de la compilation, soit entraînera un comportement d'erreur bien défini au moment de l'exécution. En Java , si vous accédez à un tableau hors limites, une exception sera levée. Des exemples d'autres langages sûrs sont C# , Haskell et Scala .

Exécution défensive de langages dangereux

Lors de la compilation d'un langage non sécurisé, des contrôles d'exécution sont ajoutés au code de bas niveau pour détecter un comportement non défini au niveau de la source. Un exemple est l'utilisation de canaries , qui peuvent terminer un programme lors de la découverte de violations de limites. Un inconvénient de l'utilisation de vérifications à l'exécution telles que la vérification des limites est qu'elles imposent une surcharge de performances considérable.

La protection de la mémoire , telle que l'utilisation d'une pile et/ou d'un tas non exécutables, peut également être considérée comme des vérifications d'exécution supplémentaires. Ceci est utilisé par de nombreux systèmes d'exploitation modernes.

Exécution isolée des modules

L'idée générale est d'identifier le code sensible à partir des données d'application en analysant le code source. Une fois cela fait, les différentes données sont séparées et placées dans différents modules. En supposant que chaque module a un contrôle total sur les informations sensibles qu'il contient, il est possible de spécifier quand et comment quitter le module. Un exemple est un module cryptographique qui peut empêcher les clés de quitter le module non cryptées.

Compilation certifiante

La compilation certifiante est l'idée de produire un certificat lors de la compilation du code source, en utilisant les informations de la sémantique du langage de programmation de haut niveau. Ce certificat doit être joint au code compilé afin de fournir une forme de preuve au consommateur que le code source a été compilé selon un certain ensemble de règles. Le certificat peut être produit de différentes manières, par exemple à l'aide d'un code de support de preuve (PCC) ou d'un langage d'assemblage typé (TAL).

Code justificatif

Les principaux aspects du PCC peuvent être résumés dans les étapes suivantes :

1. Le fournisseur fournit un programme exécutable avec diverses annotations produites par un compilateur certificateur .
2. Le consommateur fournit une condition de vérification, basée sur une politique de sécurité . Celui-ci est envoyé au fournisseur.
3. Le fournisseur exécute la condition de vérification dans un prouveur de théorème pour produire une preuve au consommateur que le programme satisfait en fait la politique de sécurité.
4. Le consommateur exécute ensuite la preuve dans un vérificateur de preuve pour vérifier la validité de la preuve.

Un exemple de compilateur de certification est le compilateur Touchstone , qui fournit une preuve formelle PCC de sécurité de type et de mémoire pour les programmes implémentés en Java.

Langage d'assemblage typé

TAL est applicable aux langages de programmation qui utilisent un système de types . Après la compilation, le code objet portera une annotation de type qui peut être vérifiée par un vérificateur de type ordinaire. L'annotation produite ici est à bien des égards similaire aux annotations fournies par PCC, avec quelques limitations. Cependant, TAL peut gérer toute politique de sécurité qui peut être exprimée par les restrictions du système de type, qui peuvent inclure la sécurité de la mémoire et le flux de contrôle, entre autres.

Séminaires

• Séminaire Dagstuhl 03411 , Language-Based Security, 5 – 10 octobre 2003.

Les références

Livres

• G. Barthe, B. Grégoire, T. Rezk, Recueil de certificats , 2008
• Brian Chess et Gary McGraw, Analyse statique pour la sécurité , 2004.

Lectures complémentaires

• Dexter Kozen, Sécurité basée sur le langage , Université Cornell, 1999
• Pieter Agten et al., Développements récents dans la sécurité logicielle de bas niveau , Universiteit Leuven
• Andrei Sabelfeld et Andrew C. Myers, Sécurité des flux d'informations basés sur la langue
• Fred B. Schneider et al., A Language-Based Approach to Security , Carnegie Mellon University, 2000