L'évolution et le succès qu'a connu Internet les dernières années a profondément marqué le domaine du génie logiciel et plus particulièrement des aspects tels que la conception, l'implémentation et l'exploitation de systèmes distribués. Cette ouverture qu'offre la toile aux systèmes brave les limites architecturales et géographiques pour permettre une interconnexion permanente des utilisateurs. Cependant, ce flux de communication et de code mobile comporte des risques de sécurité qui vont à l'encontre des politiques des entreprises concernées par ces échanges. Étant données la multitude et la diversité des intervenants, des mesures préventives s'imposent pour remédier à cette faille sécuritaire. Ce mémoire s'inscrit dans le cadre d'une contribution à cet effort, par la voie de la certification. En effet, le potentiel de l'approche proposée émerge de la synthèse des techniques fondamentales de ce domaine, qui sont le code incorporant une preuve (PCC), le langage assembleur typé (TAL) et le code incorporant un modèle (MCC). Toujours dans l'optique de renforcer la relation de confiance entre le producteur et le consommateur, et au-delà de la vérification du respect du code envers une politique de sécurité, notre projet qui s'intitule ±code incorporant un modèle certifié¿ (CMCC) couvre en plus des aspects pratiques jusque là souvent délaissés par les concepteurs.