• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 27
  • 18
  • 3
  • Tagged with
  • 51
  • 51
  • 30
  • 28
  • 26
  • 25
  • 24
  • 24
  • 14
  • 14
  • 12
  • 12
  • 11
  • 9
  • 8
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
11

Réduction du nombre de variables en analyse de relations linéaires

Merchat, David 18 May 2005 (has links) (PDF)
Cette thèse s'inscrit dans la vérification automatique de propriétés <br />numériques de programmes, principalement des logiciels embarqués. Lors de la <br />vérification on doit représenter de façon finie des ensembles éventuellement <br />infinis de valeurs, pour cela une solution possible est l'utilisation de <br />polyèdres convexes. Cette <br />représentation est précise mais coûteuse ce qui limite le nombre de variables <br />qu'il est possible de manipuler. Le but de cette thèse est d'augmenter le <br />nombre maximal de variables qu'il est possible de représenter. Deux approches <br />ont été envisagées puis testées. Dans un premier temps on a voulu tirer <br />profit de la présence d'équations affines pour éliminer une variable par <br />équation. Cette approche s'est révélée, expérimentalement, assez décevante. <br />Une autre approche, bien plus prometteuse, est l'utilisation du produit <br />cartésien. L'idée est alors de représenter indépendamment les variables dont <br />l'évolution n'est pas liée. Cette décomposition peut être améliorée grâce à <br />un changement de base. Un analyseur a été réalisé afin de <br />tester ces deux approches.
12

Méthodes algorithmiques de vérification des protocoles cryptographiques

Lazar (Bozga), Liana 09 December 2004 (has links) (PDF)
Les protocoles cryptographiques jouent un rôle majeur dans les applications ou l'intégrité des données, la confidentialité, l'authenticité et autres propriétés sont essentielles. Ils sont utilisés par exemple dans le commerce électronique, la téléphonie mobile, le vote électronique. Dans la première partie de la thèse nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est décidable est NP-complet. Notre procédure se base sur une logique de Hoare complète pour des protocoles cryptographiques bornés et un langage de propriétés très expressif. Dans la deuxième partie, en utilisant des techniques d'interprétation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour les protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ainsi que des messages de taille arbitraire. Nous proposons un algorithme qui calcule un invariant inductif en utilisant des patterns comme représentation symbolique. Cette méthode a été implanté dans l'outil Hermes et validée sur plusieurs études de cas.
13

Contributions à l'analyse statique de programmes manipulant des tableaux

Péron, Mathias 22 September 2010 (has links) (PDF)
Si l'analyse automatique des accès aux tableaux a été largement étudiée, on trouve très peu de résultats convaincants sur l'analyse du contenu des tableaux. Pour une telle analyse, les analyses numériques sont centrales. Notamment, si l'on découvre l'invariant i ≠ j, on évite d'affaiblir la connaissance sur a[j] lors d'une affectation à a[i]. Nous proposons une nouvelle analyse numérique faiblement relationnelle, combinant des contraintes de zones (x - y ≤ c ou ±x ≤ c) à des contraintes de non-égalités (x ≠ y ou x ≠ 0). Cette analyse a une complexité en O(n4), si les variables prennent leur valeurs dans un ensemble dense. Dans le cas arithmétique, décider de la satisfaisabilité d'une conjonction de telles contraintes est un problème NP-complet. Nous proposons une analyse en O(n4) également pour ce cas. Au cœur des analyses du contenu des tableaux on trouve aussi des analyses de partitionnement symbolique. Pour une boucle " for i = 1 to n ", où un tableau est accédé à la cellule i, il est nécessaire de considérer le contenu des tableaux sur les tranches [1, i - 1], [i, i] et [i + 1, n] pour être précis. Nous définissons une analyse de partitionnement sémantique, puis une analyse du contenu des tableaux basée sur ses résultats. Cette dernière associe à chaque tranche φ une propriété ψ dont les variables représentent le contenu des tableaux sur cette tranche. La propriété ψ est interprétée cellule-par-cellule, ainsi pour φ = [1, i - 1] et ψ = (a = b + 1) il est exprimé que ∀ k ∈ [1, i - 1], a[k] = b[k] + 1. Les résultats expérimentaux montrent que notre analyse automatique est efficace et précise, sur une classe de programmes simples : tableaux unidimensionnels, indexés par une variable au plus (x + c ou c), traversés par des boucles, imbriquées ou non, avec des compteurs suivant une progression arithmétique. Elle découvre par exemple que le résultat d'un tri par insertion est un tableau trié, ou que durant le parcours d'un tableau gardé par une "sentinelle", tous les accès à ce tableau sont corrects.
14

Préservation des preuves et transformation de programmes

Kunz, César 03 February 2009 (has links) (PDF)
Le paradigme du code mobile implique la distribution des applications par les producteurs de code à environnements hétérogènes dans lesquels elles sont exécutées. Une pratique étendue de ce paradigme est constituée par le développement d'applications telles que les applets ou les scripts Web, transferés à travers un réseau non sécurisé comme Internet à des systèmes distants, par exemple un ordinateur, un téléphone mobile ou un PDA (Assistant personnel). Naturellement, cet environnement peux ouvrir la porte au déploiement de programmes malveillants dans des plateformes distantes. Dans certains cas, la mauvaise conduite du code mobile ne constitue pas un risque grave, par exemple lorsque l'intégrité des données affectées par l'exécution n'est pas critique ou lorsque l'architecture d'exécution impose de fortes contraintes sur les capacités d'exécution du code non sécurisé. Il y a toujours, toutefois, des situations dans lesquelles il est indispensable de vérifier la correction fonctionnelle du code avant son exécution, par exemple lorsque la confidentialité de données critiques comme l'information des cartes de crédit pourrait être en danger, ou lorsque l'environnement d'exécution ne possède pas un mécanisme spécial pour surveiller la consommation excessive des ressources. George Necula a proposé une technique pour apporter de la confiance aux consommateurs sur la correction du code sans faire confiance aux producteurs. Cette technique, Proof Carrying Code (PCC), consiste à déploier le code avec une preuve formelle de sa correction. La correction est une propriété inhérente du code reçuu qui ne peut pas être directement déduite du producteur du code. Naturellement, cela donne un avantage à PCC quant-aux méthodes basées sur la confiance à l'autorité d'un tiers. En effet, une signature d'une autorité ne suffit pas à fournir une confiance absolue sur l'exécution du code reçu. Depuis les origines du PCC, le type de mécanisme utilisé pour générer des certificats repose sur des analyses statiques qui font partie du compilateur. Par conséquent, en restant automatique, il est intrinsèquement limité à des propriétés très simples. L'augmentation de l'ensemble des propriétés à considerer est difficile et, dans la plupart des cas, cela exige l'interaction humaine. Une possibilité consiste à vérifier directement le code exécutable. Toutefois, l'absence de structure rend la vérification du code de bas niveau moins naturelle, et donc plus laborieuse. Ceci, combiné avec le fait que la plupart des outils de vérification ciblent le code de haut niveau, rend plus appropriée l'idée de transferer la production de certificats au niveau du code source. Le principal inconvénient de produire des certificats pour assurer l'exactitude du code source est que les preuves ne comportent pas la correction du code compilé. Plusieurs techniques peuvent etre proposées pour transférer la preuve de correction d'un programme à sa version exécutable. Cela implique, par exemple, de déployer le programme source et ses certificats originaux (en plus du code exécutable) et de certifier la correction du processus de compilation. Toutefois, cette approche n'est pas satisfaisante, car en plus d'exiger la disponibilité du code source, la longueur du certificat garantissant la correction du compilation peut être prohibitive. Une alternative plus viable consiste à proposer un mécanisme permettant de générer des certificats de code compilé à partir des certificats du programme source. Les compilateurs sont des procédures complexes composées de plusieurs étapes, parmi lesquelles le programme original est progressivement transformé en représentations intermédiaires. Barthe et al. et Pavlova ont montré que les certificats originaux sont conservés, à quelques différences près non significatives, par la première phase de compilation: la compilation non optimale du code source vers une représentation non structurée de niveau intermédiaire. Toutefois, les optimisations des compilateurs sur les représentations intermédiaires représentent un défi, car a priori les certificats ne peuvent pas être réutilisés. Dans cette thèse, nous analysons comment les optimisations affectent la validité des certificats et nous proposons un mécanisme, Certificate Translation, qui rend possible la génération des certificats pour le code mobile exécutable à partir des certificats au niveau du code source. Cela implique transformer les certificats pour surmonter les effets des optimisations de programme.
15

Analyse des systèmes mobiles par interprétation abstraite.

Feret, Jérôme 25 February 2005 (has links) (PDF)
Un système mobile est un ensemble de composants qui peuvent interagir entre eux, tout en modifiant dynamiquement le système lui-même. Ces interactions contrôlent ainsi la création et la destruction des liaisons entre les composants, mais aussi la création dynamique de nouveaux composants au sein du système. La taille d'un tel système varie au cours du temps, elle n'est pas bornée en général. Un système mobile peut représenter des réseaux de télécommunication, des systèmes reconfigurables, des applications client-serveur sur la toile, des protocoles cryptographiques, ou des systèmes biologiques. Plusieurs modèles sont disponibles selon le domaine d'application et la granularité du niveau d'observation. Dans cette thèse, nous proposons un cadre de travail unifiant pour découvrir et prouver statiquement (avant leur exécution) et automatiquement les propriétés des systèmes mobiles. Nous proposons un méta-langage dans lequel nous encodons les modèles les plus couramment utilisés dans la littérature (le p-calcul, le calcul des ambients, le join-calcul, le spi-calcul, les BIO-ambients, etc). Pour chaque modèle encodé, le méta-langage calcule une sémantique enrichie dans laquelle à la fois les composants et les objets qu'ils manipulent (adresses mémoires, noms de canaux, clefs secrètes ou partagées, etc) sont identifiés par l'historique de leur création. Ainsi, nous n'utilisons pas de relation de congruence (ni de renommage), ce qui rend l'analyse plus facile. Le cadre général de l'Interprétation Abstraite nous permet ensuite de dériver des sémantiques abstraites, qui sont décidables, correctes, et approchées. Dans cette thèse, nous donnons trois analyses génériques que nous instancions selon le compromis désiré entre le temps de calcul et la précision de l'analyse. La première analyse se concentre sur les propriétés dynamiques du système. Elle infère des relations entre les historiques des objets qui sont manipulés par les composants du système. Cette analyse distingue les instances récursives d'un même objet, et ce, même lorsque le nombre de ces instances n'est pas borné. à titre d'exemple, cette analyse prouve dans le cas d'une application client-serveur à nombre illimité de clients, que les données de chaque client ne sont pas communiquées aux autres clients. La deuxième analyse se concentre sur des propriétés de concurrence. Cette analyse compte le nombre de composants du système. Elle permet de détecter que certains composants ne peuvent pas interagir, car ils ne coexistent jamais. Elle peut aussi garantir à un système qu'il n'épuisera pas les ressources physiques disponibles. Une troisième analyse mêle concurrence et dynamicité.
16

Analyses de Pointeurs et Logique de Séparation.

Sims, Elodie-Jane 01 December 2007 (has links) (PDF)
Le cadre de cette thèse est l'analyse statique modulaire par interprétation abstraite de logiciels en vue de leur vérification automatique. Nous nous intéressons en particulier aux programmes comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements et d'alias) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique. Isthiaq, Pym, O'Hearn et Reynolds ont développé récemment des logiques de fragmentation (separation logics) qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct. La sémantique des triplets de la logique ({P}C{P
17

Analyse statique par interprétation abstraite de systèmes hybrides.

Bouissou, Olivier 23 September 2008 (has links) (PDF)
Si l'interet et l'efficacite des methodes d'analyse statique par interpretation abstraite pour la verification des programmes critiques embarques ne sont plus a demontrer, il est maintenant necessaire d'obtenir des methodes les plus precises possibles. Si l'utilisation de domaines abstraits relationnels de plus en plus elabores permet de diminuer la surapproximation dont souffre les domaines les plus simples, les analyses actuelles souffrent toujours d'une mauvais prise en compte des entrees du programme. Ces entrees sont fournies par un capteur qui mesure une grandeur physique, et sont generalement surapproximees par un intervalle. Une piste d'etude recente pour mieux gerer ces entrees continues consiste a etudier, outre le programme lui-meme, l'environnement physique dans lequel il est execute. On obtient ainsi un systeme plus complexe comprenant une dynamique discrete (le programme) et une dynamique continue (l'environnement). L'etude de tels systemes hybrides repose actuellement essentiellement sur des extensions des automates a etats finis et des algebres de processus introduisant une dynamique continue. L'analyse de ces systemes par des techniques de model-checking souffre encore d'une explosion combinatoire excluant leur utilisation pour les logiciels embarques critiques les plus gros. La premiere contribution de cette these est une extension des langages de programmation imperatifs permettant de d´ecrire a la fois le programme, l'environnement exterieur et les interactions entre le programme et l'environnement. L'environnement physique est d´ecrit par un ensemble d'equations differentielles representant chacune un mode continu, et les interactions entre le programme et l'exterieur sont modelises par deux mots cles representant les capteurs et actionneurs. Nous donnons a l'ensemble (programme plus environnement physique) une semantique denotationnelle qui reste tres proche de celle definie pour les langages imperatifs classiques. La difficulte majeure dans la construction de cette semantique a ete de definir une semantique pour la partie continue : les solutions des equations diff´erentielles sont exprimees comme le plus petit point fixe d'un operateur monotone dans un CPO, et nous montrons que les iterees de Kleene convergent vers ce point fixe. La seconde contribution est une methode d'analyse statique par interpretation abstraite de ces systemes hybrides. Cette methode fonctionne en deux temps. Tout d'abord, sous certaines restrictions portant sur le programme a analyser, on construit un recouvrement de l'espace des variables d'entree via une analyse par intervalle couplee a une analyse d'atteignabilite en avant. On obtient ainsi une abstraction de l'impact qu'a le programme sur l'evolution continue : l'espace d'entree du programme est d´coupe en zones dans lesquelles on est sur qu'un actionneur sera active. Dans un deuxieme temps, nous utilisons ce recouvrement et une methode d'integration garantie des equations differentielles pour obtenir une surapproximation de l'evolution continue. Un analyseur prototype implementant ces techniques a ete developpe et les tests sur les exemples classiques de systemes hybrides montrent de bons resultats. Enfin, la troisieme contribution de cette these est une nouvelle methode d'integration garantie nommee GRKLib. Contrairement aux methodes existantes, GRKLib se fonde sur un schema d'integration numerique non garantie (nous avons choisi un schema de Runge-Kutta d'ordre 4, mais n'importe quelle autre convient) et nous calculons, en utilisant l'arithmetique d'intervalles, l'erreur globale commise lors de l'integration numerique. Cette erreur s'exprime comme la somme de trois termes : l'erreur sur un pas, la propagation de l'erreur et l'erreur due aux nombres flottants. Chaque terme est calcule separement et des techniques avancees permettent de les reduire et de controler au mieux le pas d'integration pour limiter l'accroissement de l'erreur globale. Une librairie C++ implementant ces concepts a ete developpee, et les resultats presentes dans cette these sont prometteurs.
18

Vérification et Synthèse de Contrôleur pour des Propriétés de Confidentialité

Dubreil, Jérémy 25 November 2009 (has links) (PDF)
Les systèmes fonctionnant sur un réseau ouvert tels que les bases de données médicales ou les systèmes bancaires peuvent manipuler des informations dont la confidentialité doit être impérativement préservée. Dans ce contexte, la notion d'opacité formalise la capacité d'un système à garder secrètes certaines informations critiques. Dans cette thèse, nous nous intéressons à la fois à vérifier que la propriété d'opacité est satisfaite et à la synthèse de systèmes opaques. Vérifier l'opacité est un problème décidable pour des systèmes de transition finis. Pour les systèmes infinis, nous étudions l'application de techniques d'interprétation abstraite à la détection de vulnérabilité. Nous présentons aussi une méthode alternative qui s'appuie sur des abstractions régulières et sur des techniques de diagnostique pour détecter de telles vulnérabilité à l'exécution du système. Pour la synthèse de système opaque, nous appliquons dans un premier temps la théorie du contrôle à la Ramadge et Wonham pour calculer un contrôleur assurant l'opacité. Nous montrons que les techniques habituelles de synthèse de contrôleur ne peuvent être appliqué pour ce problème d'opacité et nous développons alors de nouveaux algorithmes pour calculer l'unique système opaque qui soit maximal au sens de l'inclusion des langages. Ces résultats sont à rapprocher des techniques de construction de système sécurisé par assemblage de composant. Finalement, nous présentons une autre approche pour la synthèse de système opaque qui consiste à synthétiser un filtre qui décide, dynamiquement, de masquer des événements observable afin d'éviter que de l'information secrète ne soit révélée. Ceci permet d'étudier dans un cadre formel la synthèse automatique de pare-feu assurant la confidentialité de certaines informations critiques.
19

La représentation SSA: sémantique, analyses et implémentation dans GCC

Pop, Sebastian 12 1900 (has links) (PDF)
Le langage d'assignation statique unique, SSA, est l'une des représentations intermédiaires les plus communément utilisées dans les compilateurs industriels. Cependant l'intérêt de la communauté d'analyse statique de programmes est minime, un fait dû aux faibles fondations formelles du langage SSA. Cette thèse présente une sémantique dénotationelle du langage SSA, permettant des définitions formelles des analyses statiques du langage SSA en se basant sur les méthodes classiques de l'interprétation abstraite. D'un point de vue pratique, cette thèse présente l'implémentation des analyseurs statiques définis formellement dans un compilateur industriel, la Collection de Compilateurs GNU, GCC.
20

The Fixpoint Checking Problem: An Abstraction Refinement Perspective

Ganty, Pierre P 28 September 2007 (has links)
<P align="justify">Model-checking is an automated technique which aims at verifying properties of computer systems. A model-checker is fed with a model of the system (which capture all its possible behaviors) and a property to verify on this model. Both are given by a convenient mathematical formalism like, for instance, a transition system for the model and a temporal logic formula for the property.</P> <P align="justify">For several reasons (the model-checking is undecidable for this class of model or the model-checking needs too much resources for this model) model-checking may not be applicable. For safety properties (which basically says "nothing bad happen"), a solution to this problem uses a simpler model for which model-checkers might terminate without too much resources. This simpler model, called the abstract model, over-approximates the behaviors of the concrete model. However the abstract model might be too imprecise. In fact, if the property is true on the abstract model, the same holds on the concrete. On the contrary, when the abstract model violates the property, either the violation is reproducible on the concrete model and so we found an error; or it is not reproducible and so the model-checker is said to be inconclusive. Inconclusiveness stems from the over-approximation of the concrete model by the abstract model. So a precise model yields the model-checker to conclude, but precision comes generally with an increased computational cost.</P> <P align="justify">Recently, a lot of work has been done to define abstraction refinement algorithms. Those algorithms compute automatically abstract models which are refined as long as the model-checker is inconclusive. In the thesis, we give a new abstraction refinement algorithm which applies for safety properties. We compare our algorithm with previous attempts to build abstract models automatically and show, using formal proofs that our approach has several advantages. We also give several extensions of our algorithm which allow to integrate existing techniques used in model-checking such as acceleration techniques.</P> <P align="justify">Following a rigorous methodology we then instantiate our algorithm for a variety of models ranging from finite state transition systems to infinite state transition systems. For each of those models we prove the instantiated algorithm terminates and provide encouraging preliminary experimental results.</P> <br> <br> <P align="justify">Le model-checking est une technique automatisée qui vise à vérifier des propriétés sur des systèmes informatiques. Les données passées au model-checker sont le modèle du système (qui en capture tous les comportements possibles) et la propriété à vérifier. Les deux sont donnés dans un formalisme mathématique adéquat tel qu'un système de transition pour le modèle et une formule de logique temporelle pour la propriété.</P> <P align="justify">Pour diverses raisons (le model-checking est indécidable pour cette classe de modèle ou le model-checking nécessite trop de ressources pour ce modèle) le model-checking peut être inapplicable. Pour des propriétés de sûreté (qui disent dans l'ensemble "il ne se produit rien d'incorrect"), une solution à ce problème recourt à un modèle simplifié pour lequel le model-checker peut terminer sans trop de ressources. Ce modèle simplifié, appelé modèle abstrait, surapproxime les comportements du modèle concret. Le modèle abstrait peut cependant être trop imprécis. En effet, si la propriété est vraie sur le modèle abstrait alors elle l'est aussi sur le modèle concret. En revanche, lorsque le modèle abstrait enfreint la propriété : soit l'infraction peut être reproduite sur le modèle concret et alors nous avons trouvé une erreur ; soit l'infraction ne peut être reproduite et dans ce cas le model-checker est dit non conclusif. Ceci provient de la surapproximation du modèle concret faite par le modèle abstrait. Un modèle précis aboutit donc à un model-checking conclusif mais son coût augmente avec sa précision.</P> <P align="justify">Récemment, différents algorithmes d'abstraction raffinement ont été proposés. Ces algorithmes calculent automatiquement des modèles abstraits qui sont progressivement raffinés jusqu'à ce que leur model-checking soit conclusif. Dans la thèse, nous définissons un nouvel algorithme d'abstraction raffinement pour les propriétés de sûreté. Nous comparons notre algorithme avec les algorithmes d'abstraction raffinement antérieurs. A l'aide de preuves formelles, nous montrons les avantages de notre approche. Par ailleurs, nous définissons des extensions de l'algorithme qui intègrent d'autres techniques utilisées en model-checking comme les techniques d'accélérations.</P> <P align="justify">Suivant une méthodologie rigoureuse, nous instancions ensuite notre algorithme pour une variété de modèles allant des systèmes de transitions finis aux systèmes de transitions infinis. Pour chacun des modèles nous établissons la terminaison de l'algorithme instancié et donnons des résultats expérimentaux préliminaires encourageants.</P>

Page generated in 0.1871 seconds