- Institut de la Francophonie pour l Informatique. - 2.1 Exigences de sécurité. - A.2 Vue d ensemble de la JVM et de vérification de code d octet. - Le problème de la sécurité des téléphones portables connaît un regain d intérêt depuis l année 2003 avec la généralisation des plates-formes Symbian OS et Windows CE : leur richesse et leurs failles dans le modèle de sécurité permettent aux attaquants de réaliser des opérations malveillantes comme le ver Cabir et récemment Skulls pour Symbian OS et le ver Dust pour Windows CE.. - Nous nous concentrons sur les raisons pour lesquelles la sécurité des téléphones portables n'est pas actuellement garantie à fin de proposer une approche globale de la sécurité. - En plus de la fonctionnalité standard de PDAs, le smartphone ajoute un téléphone portable intégré. - Le sujet de la sécurité des dispositifs mobiles, en général, ou des téléphones portables, spécifiquement, n'est pas nouveau, en 2000, le virus VBS/Timofonica [52] avait pour charge d'envoyer des SMS 1 aux abonnés du service Movistar. - Depuis l'année 2003, le problème de la sécurité connaît un regain d'intérêt avec la généralisation des plates-formes Symbian OS [46] et Windows CE [35], qui sont beaucoup plus performantes en termes de programmation que les anciens téléphones propriétaires. - 9 sécurité et les solutions existantes) pour lesquelles la sécurité des téléphones portables n'est pas actuellement garantie à fin de proposer une approche globale de la sécurité.. - Le chapitre 5 décrit les aspects pour le renforcement de la sécurité des téléphones portables. - Plusieurs primitives fonctionnelles de sécurité ont été proposées dans le contexte de la sécurité du système informatique. - Les exemples des attaques invasives incluent micro-probing et rétro-ingénierie (reverse engineering) de la conception. - Le problème peut avoir lieu à cause de la vérification réduite des limites des tampons. - Les effets de débordement de mémoire peuvent réécrire (overwriting) la mémoire de la pile, les tas, et les pointeurs de fonction. - En particulier, dans le contexte d'un commerce électronique, l'opérateur garantit à l'utilisateur la confidentialité, l'authenticité et la validité de la transaction.. - La SIM intègre également de la mémoire sous forme de ROM qui accueille essentiellement l'OS, d'EEPROM 12 qui sert à stocker les applications et les données persistantes, et de RAM. - Une caractéristique fondamentale de la SIM est que son ensemble d'informations et d'applications contenues appartient à l'opérateur, non à l'utilisateur. - L'Institut européen des normes de télécommunication (ETSI) définit dans la spécification GSM 11.11 [15] les caractéristiques physiques (connecteurs), électroniques (protocole de transmission) et logique (commandes) de l'interconnexion du téléphone portable et de la SIM. - définit une plate-forme pour le développement de fonctionnalités implémentées dans la majorité des téléphones portables, une partie du code s'exécutant dans le téléphone, l'autre au sein de la SIM. - Ces applications SIM réalisent au besoin des services de sécurité en s'appuyant sur des clés et algorithmes de la SIM.. - La spécification WIM 14 [53] du OMA forum [38], anciennement WAP forum, définit, pour sa part, une application au sein de la SIM avec une API dédiée à la sécurité dans les protocoles WAP. - La SIM peut ainsi être utilisée pour stocker des certificats et des clés de type RSA, réaliser les opérations de signature et d'authentification pour les services de sécurité de la couche transport (protocoles WTLS et TLS). - Au niveau des JavaCard, nous retrouvons un mécanisme équivalent (JCRMI 16 ) pour accéder à une Appliquette de la carte par simple appel de méthode, simplifiant encore l'interconnexion des applications du téléphone avec celles de la SIM.. - La spécification JSR 17 177 [27] étend cette approche aux fonctions de sécurité de la SIM.. - Au niveau de l'accès au réseau, l'authentification est basée sur la SIM et est réalisée de la manière suivante.. - 22 Chaque SIM contient une clé secrète K f , le « réseau » retrouvant K f à l'aide d'une clé mère K m et des données d'identification de la SIM (ex.: numéro de série, etc.) Le « réseau » envoie un challenge RAND (un nombre aléatoire de 128 bits). - l'authentification de la SIM est valide si tel est le cas, sinon l'authentification a échoué.. - Nous voyons que la sécurité de l'authentification et de la génération de la clé de session repose exclusivement sur le secret de la clé K f . - La sécurité des communications revient à protéger le secret de la clé K s . - Toute communication est alors imputée à l'utilisateur porteur de la SIM authentifiée, ce dernier étant supposé s'être identifié via le code PIN. - L'OS Symbian souligne l'importance de la gestion sophistiquée de mémoire sur des dispositifs avec des ressources restreintes. - 28 la récupération de la pile : une méthode pour récupérer la mémoire si l'allocation de mémoire pour une fonction échoue.. - Il s'agit de la méthode de « recherche de signature. - Il existe des erreurs d'implémentation dans le modèle de sécurité de Java (risque accru compte tenu des compromis imposés par la faible mémoire et la faible puissance de calcul des téléphones portables), par exemple, l'attaque sur le Siemens S55 [41] permettant d'envoyer un SMS avant l'affichage de la fenêtre de confirmation. - De plus, lors de la récente conférence Hack in the Box en Malaisie [23], des failles de sécurité dans J2ME ont été mises à jour, failles qu'un attaquant peut exploiter pour installer un programme malveillant.. - Comme nous l'avons vu dans la section Chapitre 3:, la sécurité des applications de la SIM est depuis longtemps prise en compte. - Les améliorations de la programmation système de contrôle d'accès n'améliore pas le niveau de la sécurité : il y a un besoin de changer la technologie. - Le chiffrement peut être considéré comme le niveau ultime de la protection de données.. - Ce que nous devons protéger avec le niveau ultime de la sécurité sont les clés utilisées pour le chiffrement et le déchiffrement. - A partir de la SIM, en basant sur le principe de l informatique de confiance, nous proposons une approche pour améliorer la sécurité des téléphones portables. - De notre point de vue, le renforcement de la sécurité des téléphones portables passe par la prise en compte des trois aspects qui sont expliqués dans les trois sous-sections ci-dessous. - les composants du téléphone portable pour les opérations de cryptographie nécessitant de la performance (chiffrement symétrique par cryptoprocesseurs), pour le stockage des données sensibles et volumineuse, ainsi que pour la protection du code natif (en particulier, le chargeur de démarrage (boot loader) doit être sécurisé par utilisation de mémoire morte).. - A l image de la performance (brèches de traitement), l expérience a montré que si les fonctions de la génération de nombre aléatoire, de la cryptographie et du chargeur de démarrage sont programmées dans le matériel, la sécurité est améliorée avec le prix très petit. - D'autres améliorations d'OS pour la sécurité incluent des modifications de la commutation de contexte, de la manipulation d'exception, de la communication d'interprocessus, et de la gestion de mémoire. - Le problème principal pour lequel la sécurité des téléphones portables n'est pas actuellement garantie est un manque d'approche globale de la sécurité. - Une approche globale à la sécurité des téléphones portables revient à construire une informatique de confiance (Trusted Computing Base) à partir de la SIM. - Depuis sa sortie en 1995, les concepteurs de la technologie de Java ont eu une emphase explicite sur la sécurité. - La première section donne une vue d'ensemble de la JVM et du but de la vérification de code d octet. - De plus, un ensemble de registres (également appelés les variables locales) est fourni, ils peuvent être accédés via des instructions load et store qui empile la valeur d'un registre donné sur la pile ou stocke le sommet de la pile dans le registre donné, respectivement. - La plupart de compilateurs de Java utilisent les registres pour stocker des variables locales et des paramètres de méthode au niveau de la source, et la pile pour tenir des résultats temporaires pendant l'évaluation des expressions. - 47 registres et de blocs de pile utilisés par la méthode, ainsi permettant à un rapport d'activation de la bonne taille d'être alloué sur l'entrée de méthode.. - Une caractéristique importante de la JVM est que la plupart des instructions sont typées.. - L'opération correcte de la JVM n'est pas garantie à moins que le code vérifie les conditions suivantes. - La taille de la pile : une instruction ne dépile jamais un argument d'une pile vide, ni pousse un résultat sur une pile pleine (dont la taille est égale à la taille maximale de pile déclarée pour la méthode).. - La position du compteur de programme : le compteur de programme (CP par la suite) doit toujours pointer dans le code pour la méthode, au commencement d'une instruction valide (aucun ne doit tomber de la fin du code de méthode. - L approche défensive de la JVM [A4] peut garantir ces conditions dynamiquement, en exécutant le code. - Le but de la vérification de code d octet est de vérifier ces conditions une fois pour toutes, par l'analyse statique du code d octet au chargement. - Le but de la vérification de code d octet est de déplacer les vérifications énumérées ci-dessus du temps d'exécution au temps de chargement.. - Il peut être décrit comme l'analyse de flux de données appliquée à une interprétation abstraite au niveau des types de la machine virtuelle. - Le coeur de la plupart des algorithmes de la vérification de code d octet est un interprète abstrait pour l'ensemble d'instructions de la JVM qui exécute ces instructions comme une JVM défensive (y compris des tests de type, des tests de pile, etc. - Les types initiaux de la pile et du registre reflètent l'état de la JVM sur l'entrée de méthode : le type de pile est vide. - les types de registres 0...n-1 correspondent aux n paramètres de méthode sont mis au type des paramètres correspondants dans la signature de la méthode. - Les branches et les traiteurs d'exception introduisent des fourches et des joints dans le flux de contrôle de la méthode. - La vérificateur de code d octet de Sun traite cette situation de la façon usuelle pour l'analyse de flux de données : l état (type de pile et type de registre. - un point de programme p est pris à partir de la liste de travail et son état « après » out(p) est déterminé par son état. - La différence est que la complétion de la hiérarchie de classes/interfaces est exécutée une fois pour toutes, et la vérification manipule seulement les types simples plutôt que les ensembles de types. - d'abord, l'instruction new C crée un nouvel objet, une instance de la classe C, avec tous les champs d'instance remplis de valeurs par défaut (0 pour les champs et null pour les champs de référence). - Par conséquent, le code produit par des compilateurs de Java pour x = new C(arg) est généralement de la forme suivante:. - Quand cet initialiseur retourne, la deuxième référence est maintenant au sommet de la pile et pointe sur un objet correctement initialisé, qui est alors stocké dans le registre assigné au x. - Bertot [A1] prouve l'exactitude de p cette approche en utilisant le prouveur de théorème de Coq, et extrait un algorithme de vérification à partir de la preuve.. - D'abord, on a besoin de préciser ce qu'un corps de sous-programme est : puisque le code d octet de la JVM est non structuré, des sous-programmes ne sont pas syntaxiquement délimités dans le code. - Bien qu'elle est efficace dans la pratique, l'approche de Sun à la vérification de sous- programme soulève un problème difficile : la détermination de la structure de sous- programme. - Beaucoup d'alternatives à la vérification de sous-programme de Sun ont été proposées dans la littérature, souvent dans le contexte de petit sous ensembles de la JVM, menant aux algorithmes qui sont plus simples et plus élégants, mais en général ne sont pas complets pour la JVM entière.. - Le travail postérieur par Hagiya et de Tozawa [A9] se repose également sur la détermination antérieure de la structure de sous-programme, mais exprime le flux des types par des sous-programmes d'une manière différente, en utilisant le type spécial last(n) pour se référer au type de registre n dans l'appeleur de la sous-programme. - Bien que ces travaux soient considérables au niveau des sous-programmes, ils sont portés dans le contexte de petits sous-ensembles de la JVM qui excluent les exceptions et l'initialisation d'objet en particulier. - Quant aux exceptions, la manipulation d'exception complique de manière significative la détermination de la structure de sous-programme. - ou, un traiteur d'exception couvre des instructions appartenant d'un sous-programme et des instructions non-sous-programme, dans ce cas le code du traiteur est considéré comme en dehors de la sous-programme. - Ainsi, c'est désirable de développer des stratégies pour la vérification de sous-programme, qui ne se fondent pas sur la détermination antérieure de la structure de sous-programme, mais plutôt « découvrir » cette structure pendant la vérification. - Comme on montre dans cette section, la vérification polyvariante de code d octet fournit une solution alternative au problème de sous-programme de la section A.3.3 : l analyse polyvariante permet à des instructions à l'intérieur des corps de sous-programme d'être analysées plusieurs fois.. - Dans le cas de la vérification de code d octet, les contours sont des piles d'appel de sous- programme : les listes d'adresses de retour pour la séquence des instructions jsr qui mènent à l'état correspondant. - Donc, seulement un état est associé à chaque instruction et l'analyse se dégénère dans l'analyse monovariant de flux de données de la section A.3.1.2. - Il est que ce n'est pas pratique de reproduire des corps de sous-programmes avant la vérification monovariante, parce qu'elle demande la connaissance antérieure de la structure de sous-programme (pour déterminer quelles instructions appartiennent à quel corps de sous-programme), et comme montré, la structure de sous-programme est difficile à déterminer exactement. - Un autre avantage de la vérification polyvariante est qu'elle manipule le code qui est accessible à partir des corps de sous-programme et de programme principal, tel que les traiteurs d'exception mentionnés dans la section A.3.3.2 : plutôt que de décider si de tels traiteurs d'exception font partie d'un sous-programme ou pas, l'analyse polyvariant les analyse simplement plusieurs fois, une fois dans le contour vide et une fois ou plusieurs fois dans des contours de sous-programme.. - Un inconvénient de la vérification polyvariante est qu'elle est plus complexe que l'approche de Sun au niveau de calculs. - En particulier, si des sous-programmes sont nichées à la profondeur N, et chaque sous-programme est appelé k fois, les instructions de la sous- programme la plus intérieure sont analysées k N fois au lieu d'une fois dans l'algorithme de Sun. - Ils emploient alors un vérificateur de modèle disponible immédiatement pour déterminer la validité de la formule. - Tandis que cette application emploie seulement une petite partie de la puissance et de la généralité de la logique temporelle et du vérificateur de modèle, l'approche semble intéressante pour établir des propriétés plus fines du code d octet qui dépassent les propriétés de base de sûreté de la vérification de code d octet.. - Cette relation est de la forme (p,S,R) (p',S',R. - L'algorithme de vérification BC (Brisset-Coglio) explore simplement tous les états accessibles par des applications répétées de la relation étendue de transitions commençant. - Cet algorithme se termine toujours parce que le nombre d'états distincts est fini (quoique grand), puisqu'il y a un nombre fini de types distincts utilisés dans le programme, et que la taille de la pile est bornée, et que le nombre de registres est fixe.. - Considérons maintenant le flux de contrôle montré dans la partie droite de la Figure 11. - Une façon est d'employer la mémoire persistante réenregistrable au lieu de la RAM pour maintenir les structures de données du vérificateur. - Une limitation pratique de cette approche est que les certificats sont relativement grands : environ 50% de la taille du code qu'ils annotent [A15]. - Le travail de Rose [A26] aborde la question de la taille de certificat en notant que l'information de type pour certaines branches de cible peut être omises par le certificat, lorsque cette information de type est correctement calculée par l'algorithme de vérification dans son balayage linéaire du code d octet. - La vérification légère de code d octet est utilisée dans le KVM, une des variantes embarquées de la JVM de Sun [A31]. - L'implémentation de KVM suit cette approche, et se fonde sur l'expansion de sous- programme avant la vérification, en tant qu'une partie de la phase de génération de certificat. - La formalisation de Klein et de Nipkow, cependant, est applicable non seulement à la vérification monovariante, mais à n'importe quel algorithme de vérification qui peut être exprimé en utilisant des équations de flux de données, y compris les algorithmes polyvariants de la section A.3.4.. - Les transformations hors-carte incluent des normalisations de pile autour de la réallocation de branches et de registres par la coloration du graphe, et sont décrites dans [A15].. - A l image de la taille d information supplémentaire facilitant la vérification sur- carte, l approche décrite dans la section A.4.2 donne un meilleur résultat.. - Vérification de code d'octet de la machine virtuelle Java : formalisation et implantation