Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

L’histoire de la République démocratique allemande (RDA) est un sujet d’enseignement en Allemagne de l’Est et de l’Ouest et, avec beaucoup moins d’heures de cours, aussi en France. L’enseignement d’histoire de la RDA à l’école est la première occasion d’une transmission du savoir sur cet État disparu. Cette transmission est encadrée par une volonté politique qui se reflète dans les programmes d’éducation. En comparant l’enseignement en Allemagne de l’Ouest, de l’Est et en France, les mécanismes de mémoire collective et d’appropriation deviennent visibles : Quel contenu entre dans l’enseignement et comment ? À quel moment surgissent des conflits d’interprétations ?Afin de mieux comprendre la circulation et la transmission du savoir, l’étude suit trois chemins différents. D’abord, l’enseignement de la RDA après 1990 est étudié dans les champs de l’éducation scolaire de deux pays ainsi que dans les activités pédagogiques des musées d’histoire. Ensuite, les manuels comme médias de transmission sont objets de l’analyse. Enfin, du côté de la réception, des leçons d’histoire de trois classes de lycée ont été observées et ensuite interprétées.Les interprétations les plus d’importants de la RDA sont celle d’ « État SED » (Klaus Schroeder), de « dictature de sollicitude » (Konrad H. Jarausch), de « dictature de participation » (Mary Fulbrook) et d’« obstination » (« Eigen-Sinn ») (Alf Lüdtke). De manière générale, les représentants d’une interprétation politologique et ceux de la sociohistoire se disputent la vue « juste » de la RDA. Chez les premiers, la dominance du parti communiste SED avec ses mécanismes de pouvoir caractérise la constitution de l’État et de la société. Les socio-historiens regardent la relation complexe du pouvoir comme une pratique sociale avec les stratégies des citoyens de s’arranger avec ce pouvoir dans la vie quotidienne.En résumé, l’enseignement de l’histoire de la RDA est influencé par cinq domaines, dont un ne se démarque pas entièrement de l’autre : par la politique du passé, par l’Histoire en tant que science sociale, par la présence publique, par le marché des éditions scolaires et par la mémoire familiale. Les médiateurs du savoir qui agissent entre la politique du passé, l’Histoire et la présence publique ont le plus d’influence sur l’enseignement. Ce sont des commissaires dans les musées, des membres de comités qui préparent les programmes, mais aussi des professeurs au lycée. La réception du savoir des élèves, par contre, dépend plus des domaines du marché – du manuel et son récit de la RDA –, ainsi que de la mémoire familiale et la présence de la RDA dans les médias. Le cours d’histoire est influencé par ces trois domaines. La présence publique du discours sur la RDA y devient souvent visible lorsque les élèves et le professeur présentent des anecdotes de films et de documentaires. Moins visibles sont la mémoire familiale et la logique du marché des éditions scolaires.Comparant la transmission et la réception, l’hypothèse préalable, selon laquelle les élèves savent très peu et relativisent le caractère de dictature de l’État faute de connaissances, se modifie. L’étude montre que beaucoup de jeunes possèdent un savoir informel sur le passé socialiste de l’Allemagne de l’Est. Ce savoir informel ne peut pas forcément être représenté dans un questionnaire. De plus, une relation causale entre le manque de savoir et la banalisation de la RDA n’existe pas. Plus précisément, l’interprétation d’une RDA minimisée, défendue par les élèves à Leipzig, est basée sur la culture matérielle de l’État disparu et n’exclut pas l’interprétation de la RDA comme « État SED ». Dans la classe est-allemande, la banalisation de la RDA par les élèves n’apparait pas comme étant le résultat de leur ignorance mais plutôt comme étant, d’une part, de l’attachement à l’héritage dévalorisé de la RDA, et, d’autre part, le reflet de la loyauté exprimé par leurs parents et grands-parents / The former German Democratic Republic (GDR) is a subject of history lessons in boarding schools both in Germany and in France. As the remembrance of the GDR is a highly debated topic, history lessons on the socialist state reflect conflicts of interpretation that circulate between the spheres of academic and public discourse and political education. The study looks on interpretations of the GDR developed in history lessons and the influence of the various plots of the state’s history in mass media, academic discourse and history politics on the lessons.The teaching of GDR history is influenced by five spheres: policy, academic history, public discourse, the textbook market and the family’s communicative memory. The actors who mediate between academia, public discourse and history/educational policy show the biggest influence on contents and forms of teaching: they are curators in museums, members of curricular committees or teachers at schools. How pupils appropriate GDR history is more influenced by family, the educational market with its textbooks and by public discourse, less by academia and policy.The study showed that the agency of teachers as filters of curricular knowledge has more impact than the political control of curricula and textbook suggests. Besides their duty as knowledge filters teacher have to moderate between different sources of knowledge which become visible during the lessons.In the field of transmission of knowledge at school, the same conflicts appear as in the field of education in memorials and museums. Whereas the memory of dictatorship has become dominant since 1990 and the tandem of repression and rebellion remain the most important aspects of GDR history in curricula and public discourse, the so-called ‘memory of arrangement’ survived as the East German counter-memory. It still appears in the case of a grammar school class in Leipzig in 2014, whose pupils where born in 1997 and 1998.It has become clear that pupils do not relativize the GDR as a dictatorship due to a lack of knowledge on the former state. In fact, most adolescents know more than a questionnaire could show. Their images, stories and interpretations that did not fit into the lessons were activated in the context of focus group discussions. More than that, there is no causality between little knowledge and putting things into perspective. In the Leipzig class, this was more a sign of loyalty towards family members and an emotional connection to the devaluated material and social heritage of GDR culture. In Frankfurt and Paris, where there was more distance, family memory was far less important and the judgement was more self-reflective. Where the teacher proposes mediating concepts of the GDR, as in Frankfurt, the pupils appear to learn the most. In Leipzig, a mediating concept as ‘participatory dictatorship’ or ‘welfare dictatorship’ (Konrad Jarausch) helped to come to terms with contradictory aspects. The content learned is just one element of the successful teaching on GDR history, the other being an irritation of stereotypes: the competence to question one’s own first judgement.The transmission of GDR history in school will, in the long term, remain important, especially if the GDR is integrated in wider contexts such as the twentieth-century history of ideas. As seen in the field research, the more mediating concepts between different sources and interpretations are discussed, the more educational success to be expected, both in learning about the GDR and learning about oneself

Dans cette thèse nous proposons un nouveau concept de noyau adapté à la preuve que nous avons appelé « proto-noyau ». Il s’agit d’un noyau de système d’exploitation minimal où la minimisation de sa taille est principalement motivée par la réduction du coût de la preuve mais aussi de la surface d’attaque. Ceci nous amène à définir une nouvelle stratégie de « co-design » du noyau et de sa preuve. Elle est fondée principalement sur les feedbacks entre les différentes phases de développement du noyau, allant de la définition des besoins jusqu’à la vérification formelle de ses propriétés. Ainsi, dans ce contexte nous avons conçu et implémenté le proto-noyau Pip. L’ensemble de ses appels système a été choisi minutieusement pendant la phase de conception pour assurer à la fois la faisabilité de la preuve et l’utilisabilité du système. Le code de Pip est écrit en Gallina (le langage de spécification de l’assistant de preuve Coq) puis traduit automatiquement vers le langage C. La propriété principale étudiée dans ces travaux est une propriété de sécurité, exprimée en termes d’isolation mémoire. Cette propriété a été largement étudiée dans la littérature de par son importance. Ainsi, nos travaux consistent plus particulièrement à orienter le développement des concepts de base de ce noyau minimaliste par la vérification formelle de cette propriété. La stratégie de vérification a été expérimentée, dans un premier temps, sur un modèle générique de micro-noyau que nous avons également écrit en Gallina. Par ce modèle simplifié de micro-noyau nous avons pu valider notre approche de vérification avant de l’appliquer sur l’implémentation concrète du proto-noyau Pip. / In this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel.

Avec la croissance majeure de l’Internet des Objets et du Cloud Computing, la sécurité dans ces systèmes est devenue un problème majeur. Plusieurs attaques ont eu lieu dans les dernières années, mettant en avant la nécessité de garanties de sécurité fortes sur ces systèmes. La plupart du temps, une vulnérabilité dans le noyau ou un de ses modules est suffisante pour compromettre l’intégralité du système. Établir et prouver des propriétés de sécurité par le biais d’assistants de preuve semble être un grand pas en avant vers l’apport de garanties de sécurité. Cela repose sur l’utilisation de modèles mathématiques dans le but de raisonner sur leur comportement, et d’assurer que ce dernier reste correct. Cependant, en raison de la base de code importante des logiciels s’exécutant dans ces systèmes, plus particulièrement le noyau, cela n’est pas une tâche aisée. La compréhension du fonctionnement interne de ces noyaux, et l’écriture de la preuve associée à une quelconque propriété de sécurité, est de plus en plus difficile à mesure que le noyau grandit en taille. Dans cette thèse, je propose une nouvelle approche de conception de noyau, le proto-noyau. En réduisant les fonctionnalités offertes par le noyau jusqu’à leur plus minimal ensemble, ce modèle, en plus de réduire au maximum la surface d’attaque, réduit le coût de preuve au maximum. Il permet également à un vaste ensemble de systèmes d’être construits par-dessus, considérant que la minimalité des fonctionnalités comprises dans le noyau oblige les fonctionnalités restantes à être implémentées en espace utilisateur. Je propose également dans cette thèse une implémentation complète de ce noyau, sous la forme du proto-noyau Pip. En ne fournissant que les appels systèmes les plus minimaux et indispensables, l’adaptation du noyau à des usages concrets et la faisabilité de la preuve sont assurées. Afin de réduire le coût de transition modèlevers-binaire, la majorité du noyau est écrite directement en Gallina, le langage de l’assistant de preuve Coq, et est automatiquement convertie en code C compilable pendant la phase de compilation. Pip ne repose alors que sur une fine couche d’abstraction matérielle écrite dans des langages de bas niveau, qui ne fournit que les primitives que le modèle requiert, telles que la configuration du matériel. De plus, étant donné que l’Internet des Objets et le Cloud Computing nécessitent aujourd’hui ces architectures, je propose plusieurs extensions au modèle de Pip afin de supporter le matériel multi-cœur. Soutenus par des implémentations, ces modèles permettent d’apporter le proto-noyau Pip dans les architectures multi-coeur, apportant ainsi des garanties de sécurité fortes dans ces environnement. Enfin, je valide mon approche et son implémentation par le biais d’évaluations de performances et d’une preuve de concept de portage de noyau Linux, démontrant ainsi la flexibilité du proto-noyau Pip dans des environnements réels. / Due to the major growth of the Internet of Things and Cloud Computing worlds, security in those systems has become a major issue. Many exploits and attacks happened in the last few years, highlighting the need of strong security guarantees on those systems. Most of the times, a vulnerability in the kernel or one of its modules is enough to compromise the whole system. Etablishing and proving security properties through proof assistants seems to be a huge step towards bringing security guarantees. This relies on using mathematical models in order to reason on their behaviour, and prove the latter remains correct. Still, due to the huge and complex code base of the software running on those systems, especially the kernel, this is a tedious task. Understanding the internals of those kernels, and writing an associated proof on some security property, is more and more difficult as the kernel grows in size. In this thesis, I propose a new approach of kernel design, the proto-kernel. By reducing the features provided by the kernel to their most minimal subset, this model, in addition to lowering the attack surface, reduces the cost of the proof effort. It also allows a wide range of systems to be built on top of it, as the minimality of the features embedded into the kernel causes the remaining features to be built at the userland level. I also provide in this thesis a concrete implementation of this model, the Pip proto-kernel. By providing only the most minimal and mandatory system calls, both the usability of the kernel and the feasibility of the proof are ensured. In order to reduce the model-to-binary transition effort, most of the kernel is written directly in Gallina, the language of the Coq Proof Assistant, and is automatically converted to compilable C code during compilation phase. Pip only relies on a thin hardware abstraction layer written in low-level languages, which provides the operations the model requires, such as modifying the hardware configuration. Moreover, as Internet of Things and Cloud Computing use cases would require, I propose some extensions of Pip’s model, in order to support multicore hardware. Backed up by real implementations, those models bring the Pip proto-kernel to multicore architectures, bringing strong security guarantees in those modern environments. Finally, I validate my approach and its implementation through benchmarks and a Linux kernel port proof-of-concept, displaying the flexibility of the Pip proto-kernel in real world environments.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

No description available.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.