Th. 3e cycle--Phys. théor.--Grenoble 1, 1979. N°: 46.

Th.--Sci.--Bordeaux 1, 1979. N°: 627.

Th.--Sci.--Bordeaux 1, 1979. N°: 564. / Extr. en partie de Nuclear physics, A 192, 1972, 372-390 ; A 271, 1976, 477-494 et de Physical review letters, 39, 1977, 15, 922-924.

Mon travail de thèse a porté sur le développement de méthodes avancées de RMN des solides. Nous avons notamment introduit de nouvelles méthodes de corrélation homonucléaire compatibles avec une rotation rapide de l’échantillon et des champs magnétiques élevés. Nous avons montré que la robustesse de la technique fp-RFDR peut être améliorée par l’utilisation d’un supercyclage (XY8)41. Cette méthode a été employée pour sonder les proximités 13C-13C and 31P-31P dans les solides. Nous avons aussi introduit expériences de corrélation 13C-13C du deuxième ordre avec assistance des protons, appelées SHA+, afin d’observer les proximités 13C-13C à longue distance dans les solides. Au cours de ma thèse, nous avons aussi amélioré les méthodes de corrélation hétéronucléaire pour l’observation indirecte des noyaux 14N via les protons. Nous avons montré que la résolution spectrale dans la dimension indirecte des spectres HMQC peut être accrue par l’utilisation de séquences de découplage homonucléaire pendant le temps t1. Nous avons aussi proposé l’utilisation d’impulsion sélective de la bande centrale pour l’excitation des noyaux 14N dans les expériences HMQC 1H{14N}. L’efficacité de ces impulsions sélectives de la bande centrale est comparable aux méthodes d’excitation large bande, compte tenu des champs radiofréquence produits par les sondes RMN pour l’étude des solides. La dernière partie de mon travail de thèse a porté sur l’amélioration des séquences d’écho quadripolaire pour l’acquisition des spectres 2H de solides. Les distorsions de ces spectres ont été réduites par l’introduction de nouvelles impulsions composites. / My PhD work has focused on the development of advanced solid-state NMR methods. We have notably developed homo-nuclear correlation methods compatible with high MAS frequencies and high magnetic fields. First, we have shown that the robustness of finite pulse RadioFrequency Driven Recoupling (fp-RFDR) technique can be improved by the use of nested (XY8)41 super-cycling. Such method has been employed to probe 13C-13C and 31P-31P proximities in solids. Second, we have also introduced a second-order proton-assisted 13C-13C correlation experiment, denoted “Second-order Hamiltonian among Analogous nuclei plus” (SHA+), to observe long-range 13C-13C proximities in solids at fast MAS and high magnetic field. During my PhD, we have also improved the heteronuclear correlation methods for the indirect observation of 14N nuclei via protons. We have shown that the spectral resolution along the indirect dimension of proton-detected Heteronuclear Multiple Quantum Correlation (HMQC) spectra can be enhanced by applying homonuclear dipolar decoupling schemes during the t1 period. We have also proposed the use of centerband-selective radio-frequency (rf) pulses for the excitation of 14N nuclei in 1H{14N} HMQC experiment. The efficiency of these centerband-selective pulse is comparable to that of broadband excitation given the rf field delivered by common solid-state NMR probes. The last part of my PhD focuses on the improvement of the quadrupolar echo sequence for the acquisition of the 2H spectra of solids. The distortions of such spectra were reduced by the introduction of novel composite pulses.

Thèse (M.Sc.)--Université Laval, 2004. / Bibliogr.: f. 75-88. Publié aussi en version électronique.

Th. 3e cycle--Instrumentation nucl.--Grenoble 1, 1979. N°: 106.

La progestérone est un stimulant respiratoire, mais l’implication des différents types de récepteurs de progesterone dans ces effets n’est pas connue. La progesterone possède 2 types de récepteurs: des récepteurs nucléaires (nPR) et des récepteurs membranaires (mPR). nPR est exprimé dans le noyau du tractus solitatrius (NTS), un des noyaux du tronc cérébral impliquées dans le contrôle respiratoire. En revanche on ne sait pas si les mPR sont exprimés dans ce noyaux. Nous avons effectués des marquages immunohistochimiques sur des coupes de tronc cérébral de souris adultes (mâles). Une coloration dense a été trouvé pour les récepteurs mPRα et mPRβ dans les NTS caudal et rostral, le noyau vague et le noyau hypoglosse. mPRα est exprimé dans les corps cellulaires, tandis que mPRβ se trouve dans les fibres neuronales. Des experiences de double marquage en immunofluorescence montrent une co-localisation de mPRα et mPRβ dans des neurones exprimant la tyrosine hydroxylase, enzyme de synthèse des catécholamines dans le NTS. De plus, la 3β-hydroxystéroïde déshydrogénase, impliquée dans la synthèse de progestérone, est également exprimé dans le NTS. Ces résultats suggèrent que mPRα et mPRβ peuvent jouer un rôle dans le contrôle respiratoire et que la synthèse de progestérone locale peut moduler la fonction respiratoire. / Progesterone is a potent respiratory stimulant, but the implication of progesterone receptor subtypes on this effect are not known. Progesterone has two main types of receptors, the "classical" nuclear receptor, and the recently identified membrane progesterone receptors. While it has been shown that the nuclear progesterone receptor is expressed in the nucleus tractus solitatrius, a brainstem nuclei involved in respiratory control, much less is known relatively to the expression of membrane progesterone receptors in this area. Accordingly, we used immunohistochemistry to determine the localization of membrane progesterone receptors (mPR) in respiratory-related areas in the brainstem of adult male mice. Serial slices were incubated with antibodies against alpha and beta mPR (mPRα and mPRβ). A prominent staining for mPRα, and mPRβ appeared in caudal and rostral parts of the nucleus tractus solitarius (NTS), X and XII nuclei, but while mPRα stained cell bodies, mPRβ stained fibers. With double fluorescence labeling and confocal microscopy we showed that mPRα is co-localized in catecholaminergic neurons (TH+) in NTS. mPRβ is expressed in TH+ fibers in these regions. Furthermore, 3β- hydroxysteroid dehydrogenase (3β-HSD), which is involved in progesterone synthesis, was also densily expressed in these regions. These results suggest that mPRα and mPRβ may play a role in respiratory control, and that local progesterone synthesis may modulate respiratory function.

Une majorité de neurones du noyau préoptique médian (MnPO) chez le rat sont sensibles aux variations de la concentration extracellulaire de sodium (Na⁺). L'objectif de cette étude était de déterminer le mécanisme cellulaire impliqué dans la détection du Na⁺ dans le MnPO. Pour étudier ce mécanisme, des enregistrements électrophysiologiques ont été réalisés sur des neurones dissociés et des neurones présents dans une tranche de l'hypothalamus. On a d'abord démontré la présence de "senseurs" de Na⁺ dans les neurones du MnPO. Ensuite, on a déterminé que la détection du Na⁺ extracellulaire était spécifiquement attribuée à un flux d'ions Na⁺ à travers un canal de fuite bloqué par le rubidium. Les propriétés de ce canal étaient similaires à celles d'un canal sodique. Même si cela reste à confirmer, la présence d'ARNm codant pour le canal Nax dans le MnPO fait de ce canal un candidat potentiel.

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.